src/Symantic/Parser/Grammar/Optimizations.hs

   1 {-# LANGUAGE PatternSynonyms #-}
   2 {-# LANGUAGE TemplateHaskell #-}
   3 {-# LANGUAGE ViewPatterns #-}
   4 module Symantic.Parser.Grammar.Optimizations where
   5
   6 import Data.Bool (Bool)
   7 import Data.Char (Char)
   8 import Data.Either (Either(..), either)
   9 import Prelude (undefined)
  10 import qualified Data.Function as Function
  11 import Data.Eq (Eq(..))
  12 import Data.Typeable
  13 import Data.Maybe (Maybe(..))
  14
  15 import Symantic.Base.Univariant
  16 import Symantic.Parser.Grammar.Combinators
  17 import Symantic.Parser.Staging hiding (Runtimeable(..), OptRuntime(..))
  18 import qualified Symantic.Parser.Staging as S
  19 import qualified Language.Haskell.TH.Syntax as TH
  20
  21 -- * Type 'OptGram'
  22 data OptGram repr a where
  23   Pure    :: Pure repr a -> OptGram repr a
  24   Satisfy :: Pure repr (Char -> Bool) -> OptGram repr Char
  25   Try     :: OptGram repr a -> OptGram repr a
  26   Look    :: OptGram repr a -> OptGram repr a
  27   NegLook :: OptGram repr a -> OptGram repr ()
  28   (:<*>)  :: OptGram repr (a -> b) -> OptGram repr a -> OptGram repr b
  29   (:<*)   :: OptGram repr a -> OptGram repr b -> OptGram repr a
  30   (:*>)   :: OptGram repr a -> OptGram repr b -> OptGram repr b
  31   (:<|>)  :: OptGram repr a -> OptGram repr a -> OptGram repr a
  32   Empty   :: OptGram repr a
  33   Branch  :: OptGram repr (Either a b) -> OptGram repr (a -> c) -> OptGram repr (b -> c) -> OptGram repr c
  34
  35 pattern (:<$>) :: Pure repr (a -> b) -> OptGram repr a -> OptGram repr b
  36 pattern (:$>) :: OptGram repr a -> Pure repr b -> OptGram repr b
  37 pattern (:<$) :: Pure repr a -> OptGram repr b -> OptGram repr a
  38 pattern x :<$> p = Pure x :<*> p
  39 pattern p  :$> x = p :*> Pure x
  40 pattern x :<$  p = Pure x :<* p
  41
  42 infixl 3 :<|>
  43 infixl 4 :<*>, :<*, :*>
  44 infixl 4 :<$>, :<$, :$>
  45
  46 instance Applicable (OptGram repr) where
  47   type Pure (OptGram repr) = Pure repr
  48   pure = Pure
  49   (<$>) f = (Pure f :<*>)
  50   (<*>) = (:<*>)
  51   (<*) = (:<*)
  52   (*>) = (:*>)
  53 instance Alternable (OptGram repr) where
  54   (<|>) = (:<|>)
  55   empty = Empty
  56   try = Try
  57 instance Selectable (OptGram repr) where
  58   branch = Branch
  59 instance Charable (OptGram repr) where
  60   satisfy = Satisfy
  61 instance Lookable (OptGram repr) where
  62   look = Look
  63   negLook = NegLook
  64 type instance Unlift (OptGram repr) = repr
  65 instance
  66  ( Applicable repr
  67  , Alternable repr
  68  , Selectable repr
  69  , Charable repr
  70  , Lookable repr
  71  ) => Unliftable (OptGram repr) where
  72   unlift = \case
  73     Pure a    -> pure a
  74     Satisfy p -> satisfy p
  75     Try x     -> try (unlift x)
  76     Look x    -> look (unlift x)
  77     NegLook x -> negLook (unlift x)
  78     x :<*> y  -> unlift x <*> unlift y
  79     x :<*  y  -> unlift x <*  unlift y
  80     x  :*> y  -> unlift x  *> unlift y
  81     x :<|> y  -> unlift x <|> unlift y
  82     Empty     -> empty
  83     Branch lr l r -> branch (unlift lr) (unlift l) (unlift r)
  84
  85 optGram ::
  86  Pure repr ~ S.OptRuntime Runtime =>
  87  OptGram repr a -> OptGram repr a
  88 optGram = \case
  89   -- Applicable Right Absorption Law
  90   Empty :<*> _ -> Empty
  91   Empty  :*> _ -> Empty
  92   Empty :<*  _ -> Empty
  93   -- Applicable Failure Weakening Law
  94   u :<*> Empty -> optGram (u :*> Empty)
  95   u :<*  Empty -> optGram (u :*> Empty)
  96   -- Branch Absorption Law
  97   Branch Empty _ _ -> empty
  98   -- Branch Weakening Law
  99   Branch b Empty Empty -> optGram (b :*> Empty)
 100
 101   -- Applicable Identity Law
 102   S.Id :<$> x -> x
 103   -- Flip const optimisation
 104   S.Flip S.:@ S.Const :<$> u -> optGram (u :*> Pure S.Id)
 105   -- Homomorphism Law
 106   f :<$> Pure x -> Pure (f S.:@ x)
 107   -- Functor Composition Law
 108   -- (a shortcut that could also have been be caught
 109   -- by the Composition Law and Homomorphism law)
 110   f :<$> (g :<$> p) -> optGram ((S.:.) S.:@ f S.:@ g :<$> p)
 111   -- Composition Law
 112   u :<*> (v :<*> w) -> optGram (optGram (optGram ((S.:.) :<$> u) :<*> v) :<*> w)
 113   -- Definition of *>
 114   S.Flip S.:@ S.Const :<$> p :<*> q -> p :*> q
 115   -- Definition of <*
 116   S.Const :<$> p :<*> q -> p :<* q
 117   -- Reassociation Law 1
 118   (u :*> v) :<*> w -> optGram (u :*> (optGram (v :<*> w)))
 119   -- Interchange Law
 120   u :<*> Pure x -> optGram (S.Flip S.:@ (S.:$) S.:@ x :<$> u)
 121   -- Right Absorption Law
 122   (_ :<$> p) :*> q -> p :*> q
 123   -- Left Absorption Law
 124   p :<* (_ :<$> q) -> p :<* q
 125   -- Reassociation Law 2
 126   u :<*> (v :<* w) -> optGram (optGram (u :<*> v) :<* w)
 127   -- Reassociation Law 3
 128   u :<*> (v :$> x) -> optGram (optGram (u :<*> Pure x) :<* v)
 129
 130   -- Left Catch Law
 131   p@Pure{} :<|> _ -> p
 132   -- Left Neutral Law
 133   Empty :<|> u -> u
 134   -- Right Neutral Law
 135   u :<|> Empty -> u
 136   -- Associativity Law
 137   (u :<|> v) :<|> w -> u :<|> optGram (v :<|> w)
 138
 139   -- Identity law
 140   Pure _ :*> u -> u
 141   -- Identity law
 142   (u :$> _) :*> v -> u :*> v
 143   -- Associativity Law
 144   u :*> (v :*> w) -> optGram (optGram (u :*> v) :*> w)
 145   -- Identity law
 146   u :<* Pure _ -> u
 147   -- Identity law
 148   u :<* (v :$> _) -> optGram (u :<* v)
 149   -- Commutativity Law
 150   x :<$ u -> optGram (u :$> x)
 151   -- Associativity Law
 152   (u :<* v) :<* w -> optGram (u :<* optGram (v :<* w))
 153
 154   -- Pure lookahead
 155   Look p@Pure{} -> p
 156   -- Dead lookahead
 157   Look p@Empty -> p
 158   -- Pure negative-lookahead
 159   NegLook Pure{} -> Empty
 160
 161   -- Dead negative-lookahead
 162   NegLook Empty -> Pure S.unit
 163   -- Double Negation Law
 164   NegLook (NegLook p) -> optGram (Look (Try p) :*> Pure S.unit)
 165   -- Zero Consumption Law
 166   NegLook (Try p) -> optGram (NegLook p)
 167   -- Idempotence Law
 168   Look (Look p) -> Look p
 169   -- Right Identity Law
 170   NegLook (Look p) -> optGram (NegLook p)
 171
 172   -- Left Identity Law
 173   Look (NegLook p) -> NegLook p
 174   -- Transparency Law
 175   NegLook (Try p :<|> q) -> optGram (optGram (NegLook p) :*> optGram (NegLook q))
 176   -- Distributivity Law
 177   Look p :<|> Look q -> optGram (Look (optGram (Try p :<|> q)))
 178   -- Interchange Law
 179   Look (p :$> x) -> optGram (optGram (Look p) :$> x)
 180   -- Interchange law
 181   Look (f :<$> p) -> optGram (f :<$> optGram (Look p))
 182   -- Absorption Law
 183   p :<*> NegLook q -> optGram (optGram (p :<*> Pure S.unit) :<* NegLook q)
 184   -- Idempotence Law
 185   NegLook (p :$> _) -> optGram (NegLook p)
 186   -- Idempotence Law
 187   NegLook (_ :<$> p) -> optGram (NegLook p)
 188   -- Interchange Law
 189   Try (p :$> x) -> optGram (optGram (Try p) :$> x)
 190   -- Interchange law
 191   Try (f :<$> p) -> optGram (f :<$> optGram (Try p))
 192
 193   -- pure Left/Right laws
 194   Branch (Pure (unlift -> lr)) l r ->
 195     case getEval lr of
 196      Left e -> optGram (l :<*> Pure (S.OptRuntime (Runtime (Eval e) c)))
 197       where c = Code [|| case $$(getCode lr) of Left x -> x ||]
 198      Right e -> optGram (r :<*> Pure (S.OptRuntime (Runtime (Eval e) c)))
 199       where c = Code [|| case $$(getCode lr) of Right x -> x ||]
 200   -- Generalised Identity law
 201   Branch b (Pure (unlift -> l)) (Pure (unlift -> r)) ->
 202     optGram (S.OptRuntime (Runtime e c) :<$> b)
 203     where
 204     e = Eval (either (getEval l) (getEval r))
 205     c = Code [|| either $$(getCode l) $$(getCode r) ||]
 206   -- Interchange law
 207   Branch (x :*> y) p q ->
 208     optGram (x :*> optGram (Branch y p q))
 209   -- Negated Branch law
 210   Branch b l Empty ->
 211     Branch (Pure (S.OptRuntime (Runtime e c)) :<*> b) Empty l
 212     where
 213     e = Eval (either Right Left)
 214     c = Code [||either Right Left||]
 215   -- Branch Fusion law
 216   Branch (Branch b Empty (Pure (unlift -> lr))) Empty br ->
 217     optGram (Branch (optGram (Pure (S.OptRuntime (Runtime (Eval e) c)) :<*> b)) Empty br)
 218     where
 219     e Left{} = Left ()
 220     e (Right r) = case getEval lr r of
 221                    Left _ -> Left ()
 222                    Right rr -> Right rr
 223     c = Code [|| \case Left{} -> Left ()
 224                        Right r -> case $$(getCode lr) r of
 225                                    Left _ -> Left ()
 226                                    Right rr -> Right rr ||]
 227   -- Distributivity Law
 228   f :<$> Branch b l r -> optGram (Branch b (optGram ((S..@) (S..) f :<$> l))
 229                                            (optGram ((S..@) (S..) f :<$> r)))
 230
 231   x -> x