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