src/Symantic/Parser/Grammar/Optimizations.hs

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