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