src/Symantic/Parser/Grammar/Optimize.hs

   1 {-# LANGUAGE PatternSynonyms #-}
   2 {-# LANGUAGE TemplateHaskell #-}
   3 {-# LANGUAGE ViewPatterns #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6 module Symantic.Parser.Grammar.Optimize where
   7
   8 import Data.Bool (Bool)
   9 import Data.Char (Char)
  10 import Data.Either (Either(..), either)
  11 import Data.Eq (Eq(..))
  12 import Data.Function ((.))
  13 import qualified Prelude as Pre
  14
  15 import Symantic.Parser.Grammar.Combinators as Comb
  16 import Symantic.Parser.Staging (ValueCode(..), Value(..),  Code(..), getValue, getCode)
  17 import Symantic.Univariant.Letable
  18 import Symantic.Univariant.Liftable
  19 import qualified Language.Haskell.TH.Syntax as TH
  20 import qualified Symantic.Parser.Staging as Hask
  21
  22 -- * Type 'Grammar'
  23 data Grammar a where
  24   Pure :: Hask.Haskell a -> Grammar a
  25   Satisfy :: Hask.Haskell (Char -> Bool) -> Grammar Char
  26   Item :: Grammar Char
  27   Try :: Grammar a -> Grammar a
  28   Look :: Grammar a -> Grammar a
  29   NegLook :: Grammar a -> Grammar ()
  30   (:<*>) :: Grammar (a -> b) -> Grammar a -> Grammar b
  31   (:<|>) :: Grammar a -> Grammar a -> Grammar a
  32   Empty :: Grammar a
  33   Branch :: Grammar (Either a b) -> Grammar (a -> c) -> Grammar (b -> c) -> Grammar c
  34   Match :: Eq a => [Hask.Haskell (a -> Bool)] -> [Grammar b] -> Grammar a -> Grammar b -> Grammar b
  35   ChainPre :: Grammar (a -> a) -> Grammar a -> Grammar a
  36   ChainPost :: Grammar a -> Grammar (a -> a) -> Grammar a
  37   Def :: TH.Name -> Grammar a -> Grammar a
  38   Ref :: Bool -> TH.Name -> Grammar a
  39
  40 pattern (:<$>) :: Hask.Haskell (a -> b) -> Grammar a -> Grammar b
  41 pattern (:$>) :: Grammar a -> Hask.Haskell b -> Grammar b
  42 pattern (:<$) :: Hask.Haskell a -> Grammar b -> Grammar a
  43 pattern (:*>) :: Grammar a -> Grammar b -> Grammar b
  44 pattern (:<*) :: Grammar a -> Grammar b -> Grammar a
  45 pattern x :<$> p = Pure x :<*> p
  46 pattern p :$> x = p :*> Pure x
  47 pattern x :<$ p = Pure x :<* p
  48 pattern x :<* p = Hask.Const :<$> x :<*> p
  49 pattern p :*> x = Hask.Id :<$ p :<*> x
  50
  51 infixl 3 :<|>
  52 infixl 4 :<*>, :<*, :*>
  53 infixl 4 :<$>, :<$, :$>
  54
  55 instance Applicable Grammar where
  56   pure = Pure
  57   (<*>) = (:<*>)
  58 instance Alternable Grammar where
  59   (<|>) = (:<|>)
  60   empty = Empty
  61   try = Try
  62 instance Selectable Grammar where
  63   branch = Branch
  64 instance Matchable Grammar where
  65   conditional = Match
  66 instance Foldable Grammar where
  67   chainPre = ChainPre
  68   chainPost = ChainPost
  69 instance Charable Grammar where
  70   satisfy = Satisfy
  71 instance Lookable Grammar where
  72   look = Look
  73   negLook = NegLook
  74 instance Letable TH.Name Grammar where
  75   def = Def
  76   ref = Ref
  77 instance MakeLetName TH.Name where
  78   makeLetName _ = TH.qNewName "let"
  79
  80 instance
  81   ( Applicable repr
  82   , Alternable repr
  83   , Selectable repr
  84   , Foldable repr
  85   , Charable repr
  86   , Lookable repr
  87   , Matchable repr
  88   , Letable TH.Name repr
  89   ) =>
  90   Symantic Grammar repr where
  91   sym = \case
  92     Pure a -> pure a
  93     Satisfy p -> satisfy p
  94     Item -> item
  95     Try x -> try (sym x)
  96     Look x -> look (sym x)
  97     NegLook x -> negLook (sym x)
  98     x :<*> y -> sym x <*> sym y
  99     x :<|> y -> sym x <|> sym y
 100     Empty -> empty
 101     Branch lr l r -> branch (sym lr) (sym l) (sym r)
 102     Match cs bs a b -> conditional cs (sym Pre.<$> bs) (sym a) (sym b)
 103     ChainPre x y -> chainPre (sym x) (sym y)
 104     ChainPost x y -> chainPost (sym x) (sym y)
 105     Def n x -> def n (sym x)
 106     Ref r n -> ref r n
 107 {-
 108 type instance Unlift Grammar = repr
 109 instance
 110   ( Applicable repr
 111   , Alternable repr
 112   , Selectable repr
 113   , Foldable repr
 114   , Charable repr
 115   , Lookable repr
 116   , Matchable repr
 117   , Letable repr
 118   ) => Unliftable Grammar where
 119   unlift = \case
 120     Pure a -> pure a
 121     Satisfy p -> satisfy p
 122     Item -> item
 123     Try x -> try (unlift x)
 124     Look x -> look (unlift x)
 125     NegLook x -> negLook (unlift x)
 126     x :<*> y -> unlift x <*> unlift y
 127     x :<|> y -> unlift x <|> unlift y
 128     Empty -> empty
 129     Branch lr l r -> branch (unlift lr) (unlift l) (unlift r)
 130     Match cs bs a b -> conditional cs (unlift Pre.<$> bs) (unlift a) (unlift b)
 131     ChainPre x y -> chainPre (unlift x) (unlift y)
 132     ChainPost x y -> chainPost (unlift x) (unlift y)
 133     Ref{..} -> let_ let_rec let_name
 134
 135 unComb ::
 136   ( Applicable repr
 137   , Alternable repr
 138   , Selectable repr
 139   , Foldable repr
 140   , Charable repr
 141   , Lookable repr
 142   , Matchable repr
 143   , Letable repr
 144   ) => Grammar repr a -> repr a
 145 unComb = unlift
 146 -}
 147
 148 -- * Type 'OptimizeGrammar'
 149 newtype OptimizeGrammar letName a = OptimizeGrammar { unOptimizeGrammar ::
 150   Grammar a }
 151
 152 optimizeGrammar :: OptimizeGrammar TH.Name a -> Grammar a
 153 optimizeGrammar = unOptimizeGrammar
 154
 155 type instance Unlift (OptimizeGrammar letName) = Grammar
 156 instance Unliftable (OptimizeGrammar letName) where
 157   unlift = unOptimizeGrammar
 158 instance Liftable (OptimizeGrammar letName) where
 159   lift = OptimizeGrammar . optimizeGrammarNode
 160 instance
 161   Letable letName Grammar =>
 162   Letable letName (OptimizeGrammar letName)
 163 instance Comb.Applicable (OptimizeGrammar letName)
 164 instance Comb.Alternable (OptimizeGrammar letName)
 165 instance Comb.Charable (OptimizeGrammar letName)
 166 instance Comb.Selectable (OptimizeGrammar letName)
 167 instance Comb.Matchable (OptimizeGrammar letName)
 168 instance Comb.Lookable (OptimizeGrammar letName)
 169 instance Comb.Foldable (OptimizeGrammar letName)
 170
 171 optimizeGrammarNode :: Grammar a -> Grammar a
 172 optimizeGrammarNode = \case
 173   -- Recurse into shared and/or recursive 'let' definition
 174   Def n x -> Def n (optimizeGrammarNode x)
 175
 176   -- Applicable Right Absorption Law
 177   Empty :<*> _ -> Empty
 178   Empty  :*> _ -> Empty
 179   Empty :<*  _ -> Empty
 180   -- Applicable Failure Weakening Law
 181   u :<*> Empty -> optimizeGrammarNode (u :*> Empty)
 182   u :<*  Empty -> optimizeGrammarNode (u :*> Empty)
 183   -- Branch Absorption Law
 184   Branch Empty _ _ -> empty
 185   -- Branch Weakening Law
 186   Branch b Empty Empty -> optimizeGrammarNode (b :*> Empty)
 187
 188   -- Applicable Identity Law
 189   Hask.Id :<$> x -> x
 190   -- Flip const optimisation
 191   Hask.Flip Hask.:@ Hask.Const :<$> u -> optimizeGrammarNode (u :*> Pure Hask.Id)
 192   -- Homomorphism Law
 193   f :<$> Pure x -> Pure (f Hask.:@ x)
 194   -- Functor Composition Law
 195   -- (a shortcut that could also have been be caught
 196   -- by the Composition Law and Homomorphism law)
 197   f :<$> (g :<$> p) -> optimizeGrammarNode ((Hask.:.) Hask.:@ f Hask.:@ g :<$> p)
 198   -- Composition Law
 199   u :<*> (v :<*> w) -> optimizeGrammarNode (optimizeGrammarNode (optimizeGrammarNode ((Hask.:.) :<$> u) :<*> v) :<*> w)
 200   -- Definition of *>
 201   Hask.Flip Hask.:@ Hask.Const :<$> p :<*> q -> p :*> q
 202   -- Definition of <*
 203   Hask.Const :<$> p :<*> q -> p :<* q
 204   -- Reassociation Law 1
 205   (u :*> v) :<*> w -> optimizeGrammarNode (u :*> optimizeGrammarNode (v :<*> w))
 206   -- Pure merge optimisation
 207   Pure x :<*> Pure y -> Pure (x Hask.:@ y)
 208   -- Interchange Law
 209   u :<*> Pure x -> optimizeGrammarNode (Hask.Flip Hask.:@ (Hask.:$) Hask.:@ x :<$> u)
 210   -- Right Absorption Law
 211   (_ :<$> p) :*> q -> p :*> q
 212   -- Left Absorption Law
 213   p :<* (_ :<$> q) -> p :<* q
 214   -- Reassociation Law 2
 215   u :<*> (v :<* w) -> optimizeGrammarNode (optimizeGrammarNode (u :<*> v) :<* w)
 216   -- Reassociation Law 3
 217   u :<*> (v :$> x) -> optimizeGrammarNode (optimizeGrammarNode (u :<*> Pure x) :<* v)
 218
 219   -- Left Catch Law
 220   p@Pure{} :<|> _ -> p
 221   -- Left Neutral Law
 222   Empty :<|> u -> u
 223   -- Right Neutral Law
 224   u :<|> Empty -> u
 225   -- Associativity Law
 226   (u :<|> v) :<|> w -> u :<|> optimizeGrammarNode (v :<|> w)
 227
 228   -- Identity law
 229   Pure _ :*> u -> u
 230   -- Identity law
 231   (u :$> _) :*> v -> u :*> v
 232   -- Associativity Law
 233   u :*> (v :*> w) -> optimizeGrammarNode (optimizeGrammarNode (u :*> v) :*> w)
 234   -- Identity law
 235   u :<* Pure _ -> u
 236   -- Identity law
 237   u :<* (v :$> _) -> optimizeGrammarNode (u :<* v)
 238   -- Commutativity Law
 239   x :<$ u -> optimizeGrammarNode (u :$> x)
 240   -- Associativity Law
 241   (u :<* v) :<* w -> optimizeGrammarNode (u :<* optimizeGrammarNode (v :<* w))
 242
 243   -- Pure lookahead
 244   Look p@Pure{} -> p
 245   -- Dead lookahead
 246   Look p@Empty -> p
 247   -- Pure negative-lookahead
 248   NegLook Pure{} -> Empty
 249
 250   -- Dead negative-lookahead
 251   NegLook Empty -> Pure Hask.unit
 252   -- Double Negation Law
 253   NegLook (NegLook p) -> optimizeGrammarNode (Look (Try p) :*> Pure Hask.unit)
 254   -- Zero Consumption Law
 255   NegLook (Try p) -> optimizeGrammarNode (NegLook p)
 256   -- Idempotence Law
 257   Look (Look p) -> Look p
 258   -- Right Identity Law
 259   NegLook (Look p) -> optimizeGrammarNode (NegLook p)
 260
 261   -- Left Identity Law
 262   Look (NegLook p) -> NegLook p
 263   -- Transparency Law
 264   NegLook (Try p :<|> q) -> optimizeGrammarNode (optimizeGrammarNode (NegLook p) :*> optimizeGrammarNode (NegLook q))
 265   -- Distributivity Law
 266   Look p :<|> Look q -> optimizeGrammarNode (Look (optimizeGrammarNode (Try p :<|> q)))
 267   -- Interchange Law
 268   Look (p :$> x) -> optimizeGrammarNode (optimizeGrammarNode (Look p) :$> x)
 269   -- Interchange law
 270   Look (f :<$> p) -> optimizeGrammarNode (f :<$> optimizeGrammarNode (Look p))
 271   -- Absorption Law
 272   p :<*> NegLook q -> optimizeGrammarNode (optimizeGrammarNode (p :<*> Pure Hask.unit) :<* NegLook q)
 273   -- Idempotence Law
 274   NegLook (p :$> _) -> optimizeGrammarNode (NegLook p)
 275   -- Idempotence Law
 276   NegLook (_ :<$> p) -> optimizeGrammarNode (NegLook p)
 277   -- Interchange Law
 278   Try (p :$> x) -> optimizeGrammarNode (optimizeGrammarNode (Try p) :$> x)
 279   -- Interchange law
 280   Try (f :<$> p) -> optimizeGrammarNode (f :<$> optimizeGrammarNode (Try p))
 281
 282   -- pure Left/Right laws
 283   Branch (Pure (unlift -> lr)) l r ->
 284     case getValue lr of
 285      Left v -> optimizeGrammarNode (l :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
 286       where c = Code [|| case $$(getCode lr) of Left x -> x ||]
 287      Right v -> optimizeGrammarNode (r :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
 288       where c = Code [|| case $$(getCode lr) of Right x -> x ||]
 289   -- Generalised Identity law
 290   Branch b (Pure (unlift -> l)) (Pure (unlift -> r)) ->
 291     optimizeGrammarNode (Hask.Haskell (ValueCode v c) :<$> b)
 292     where
 293     v = Value (either (getValue l) (getValue r))
 294     c = Code [|| either $$(getCode l) $$(getCode r) ||]
 295   -- Interchange law
 296   Branch (x :*> y) p q ->
 297     optimizeGrammarNode (x :*> optimizeGrammarNode (Branch y p q))
 298   -- Negated Branch law
 299   Branch b l Empty ->
 300     Branch (Pure (Hask.Haskell (ValueCode v c)) :<*> b) Empty l
 301     where
 302     v = Value (either Right Left)
 303     c = Code [||either Right Left||]
 304   -- Branch Fusion law
 305   Branch (Branch b Empty (Pure (unlift -> lr))) Empty br ->
 306     optimizeGrammarNode (Branch (optimizeGrammarNode (Pure (Hask.Haskell (ValueCode (Value v) c)) :<*> b)) Empty br)
 307     where
 308     v Left{} = Left ()
 309     v (Right r) = case getValue lr r of
 310                    Left _ -> Left ()
 311                    Right rr -> Right rr
 312     c = Code [|| \case Left{} -> Left ()
 313                        Right r -> case $$(getCode lr) r of
 314                                    Left _ -> Left ()
 315                                    Right rr -> Right rr ||]
 316   -- Distributivity Law
 317   f :<$> Branch b l r -> optimizeGrammarNode (Branch b (optimizeGrammarNode ((Hask..@) (Hask..) f :<$> l))
 318                                            (optimizeGrammarNode ((Hask..@) (Hask..) f :<$> r)))
 319
 320   x -> x