{-# LANGUAGE PatternSynonyms #-} -- For aliased combinators {-# LANGUAGE TemplateHaskell #-} -- For optimizeCombNode {-# LANGUAGE ViewPatterns #-} -- For optimizeCombNode {-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name module Symantic.Parser.Grammar.Optimize where import Data.Bool (Bool(..)) import Data.Either (Either(..), either) import Data.Eq (Eq(..)) import Data.Foldable (all, foldr) import Data.Function ((.)) import Data.Kind (Type) import qualified Data.Functor as Functor import qualified Data.List as List import qualified Language.Haskell.TH.Syntax as TH import Symantic.Parser.Grammar.Combinators as Comb import Symantic.Parser.Staging (ValueCode(..), Value(..), getValue, code) import Symantic.Univariant.Letable import Symantic.Univariant.Trans import qualified Symantic.Parser.Staging as H -- import Debug.Trace (trace) -- * Type 'Comb' -- | Pattern-matchable 'Comb'inators of the grammar. -- @(repr)@ is not strictly necessary since it's only a phantom type -- (no constructor use it as a value), but having it: -- -- 1. emphasizes that those 'Comb'inators will be 'trans'formed again -- (eg. in 'DumpComb' or 'Instr'uctions). -- -- 2. Avoid overlapping instances between -- @('Trans' ('Comb' repr) repr)@ and -- @('Trans' ('Comb' repr) ('OptimizeComb' letName repr))@ data Comb (repr :: Type -> Type) a where Pure :: H.Haskell a -> Comb repr a Satisfy :: Satisfiable repr tok => [ErrorItem tok] -> H.Haskell (tok -> Bool) -> Comb repr tok Item :: Satisfiable repr tok => Comb repr tok Try :: Comb repr a -> Comb repr a Look :: Comb repr a -> Comb repr a NegLook :: Comb repr a -> Comb repr () Eof :: Comb repr () (:<*>) :: Comb repr (a -> b) -> Comb repr a -> Comb repr b (:<|>) :: Comb repr a -> Comb repr a -> Comb repr a Empty :: Comb repr a Branch :: Comb repr (Either a b) -> Comb repr (a -> c) -> Comb repr (b -> c) -> Comb repr c Match :: Eq a => [H.Haskell (a -> Bool)] -> [Comb repr b] -> Comb repr a -> Comb repr b -> Comb repr b ChainPre :: Comb repr (a -> a) -> Comb repr a -> Comb repr a ChainPost :: Comb repr a -> Comb repr (a -> a) -> Comb repr a Def :: TH.Name -> Comb repr a -> Comb repr a Ref :: Bool -> TH.Name -> Comb repr a pattern (:<$>) :: H.Haskell (a -> b) -> Comb repr a -> Comb repr b pattern (:$>) :: Comb repr a -> H.Haskell b -> Comb repr b pattern (:<$) :: H.Haskell a -> Comb repr b -> Comb repr a pattern (:*>) :: Comb repr a -> Comb repr b -> Comb repr b pattern (:<*) :: Comb repr a -> Comb repr b -> Comb repr a pattern x :<$> p = Pure x :<*> p pattern p :$> x = p :*> Pure x pattern x :<$ p = Pure x :<* p pattern x :<* p = H.Const :<$> x :<*> p pattern p :*> x = H.Id :<$ p :<*> x infixl 3 :<|> infixl 4 :<*>, :<*, :*> infixl 4 :<$>, :<$, :$> instance Applicable (Comb repr) where pure = Pure (<*>) = (:<*>) instance Alternable (Comb repr) where (<|>) = (:<|>) empty = Empty try = Try instance Selectable (Comb repr) where branch = Branch instance Matchable (Comb repr) where conditional = Match instance Foldable (Comb repr) where chainPre = ChainPre chainPost = ChainPost instance Satisfiable repr tok => Satisfiable (Comb repr) tok where satisfy = Satisfy instance Lookable (Comb repr) where look = Look negLook = NegLook eof = Eof instance Letable TH.Name (Comb repr) where def = Def ref = Ref instance MakeLetName TH.Name where makeLetName _ = TH.qNewName "name" -- Pattern-matchable 'Comb'inators keep enough structure -- to have some of the symantics producing them interpreted again -- (eg. after being modified by 'optimizeComb'). type instance Output (Comb repr) = repr instance ( Applicable repr , Alternable repr , Selectable repr , Foldable repr , Lookable repr , Matchable repr , Letable TH.Name repr ) => Trans (Comb repr) repr where trans = \case Pure a -> pure a Satisfy es p -> satisfy es p Item -> item Try x -> try (trans x) Look x -> look (trans x) NegLook x -> negLook (trans x) Eof -> eof x :<*> y -> trans x <*> trans y x :<|> y -> trans x <|> trans y Empty -> empty Branch lr l r -> branch (trans lr) (trans l) (trans r) Match ps bs a b -> conditional ps (trans Functor.<$> bs) (trans a) (trans b) ChainPre x y -> chainPre (trans x) (trans y) ChainPost x y -> chainPost (trans x) (trans y) Def n x -> def n (trans x) Ref r n -> ref r n -- * Type 'OptimizeComb' -- Bottom-up application of 'optimizeCombNode'. newtype OptimizeComb letName repr a = OptimizeComb { unOptimizeComb :: Comb repr a } optimizeComb :: Trans (OptimizeComb TH.Name repr) repr => OptimizeComb TH.Name repr a -> repr a optimizeComb = trans instance Trans (Comb repr) repr => Trans (OptimizeComb letName repr) repr where trans = trans . unOptimizeComb type instance Output (OptimizeComb _letName repr) = Comb repr instance Trans (OptimizeComb letName repr) (Comb repr) where trans = unOptimizeComb instance Trans (Comb repr) (OptimizeComb letName repr) where trans = OptimizeComb . optimizeCombNode instance Trans1 (Comb repr) (OptimizeComb letName repr) instance Trans2 (Comb repr) (OptimizeComb letName repr) instance Trans3 (Comb repr) (OptimizeComb letName repr) instance Letable letName (Comb repr) => Letable letName (OptimizeComb letName repr) where -- Disable useless calls to 'optimizeCombNode' -- because 'Def' or 'Ref' have no matching in it. def n = OptimizeComb . def n . unOptimizeComb ref r n = OptimizeComb (ref r n) instance Comb.Applicable (OptimizeComb letName repr) instance Comb.Alternable (OptimizeComb letName repr) instance Comb.Satisfiable repr tok => Comb.Satisfiable (OptimizeComb letName repr) tok instance Comb.Selectable (OptimizeComb letName repr) instance Comb.Matchable (OptimizeComb letName repr) instance Comb.Lookable (OptimizeComb letName repr) instance Comb.Foldable (OptimizeComb letName repr) optimizeCombNode :: Comb repr a -> Comb repr a optimizeCombNode = \case -- Functor Identity Law H.Id :<$> x -> -- trace "Functor Identity Law" $ x -- Functor Commutativity Law x :<$ u -> -- trace "Functor Commutativity Law" $ optimizeCombNode (u :$> x) -- Functor Flip Const Law H.Flip H.:@ H.Const :<$> u -> -- trace "Functor Flip Const Law" $ optimizeCombNode (u :*> Pure H.Id) -- Functor Homomorphism Law f :<$> Pure x -> -- trace "Functor Homomorphism Law" $ Pure (f H..@ x) -- App Right Absorption Law Empty :<*> _ -> -- trace "App Right Absorption Law" $ Empty _ :<*> Empty -> -- In Parsley: this is only a weakening to u :*> Empty -- but here :*> is an alias to :<*> -- hence it would loop on itself forever. -- trace "App Left Absorption Law" $ Empty -- App Composition Law u :<*> (v :<*> w) -> -- trace "App Composition Law" $ optimizeCombNode (optimizeCombNode (optimizeCombNode ((H.:.) :<$> u) :<*> v) :<*> w) -- App Interchange Law u :<*> Pure x -> -- trace "App Interchange Law" $ optimizeCombNode (H.Flip H..@ (H.:$) H..@ x :<$> u) -- App Left Absorption Law p :<* (_ :<$> q) -> -- trace "App Left Absorption Law" $ p :<* q -- App Right Absorption Law (_ :<$> p) :*> q -> -- trace "App Right Absorption Law" $ p :*> q -- App Pure Left Identity Law Pure _ :*> u -> -- trace "App Pure Left Identity Law" $ u -- App Functor Left Identity Law (u :$> _) :*> v -> -- trace "App Functor Left Identity Law" $ u :*> v -- App Pure Right Identity Law u :<* Pure _ -> -- trace "App Pure Right Identity Law" $ u -- App Functor Right Identity Law u :<* (v :$> _) -> -- trace "App Functor Right Identity Law" $ optimizeCombNode (u :<* v) -- App Left Associativity Law (u :<* v) :<* w -> -- trace "App Left Associativity Law" $ optimizeCombNode (u :<* optimizeCombNode (v :<* w)) -- Alt Left CatchFail Law p@Pure{} :<|> _ -> -- trace "Alt Left CatchFail Law" $ p -- Alt Left Neutral Law Empty :<|> u -> -- trace "Alt Left Neutral Law" $ u -- All Right Neutral Law u :<|> Empty -> -- trace "Alt Right Neutral Law" $ u -- Alt Associativity Law (u :<|> v) :<|> w -> -- trace "Alt Associativity Law" $ u :<|> optimizeCombNode (v :<|> w) -- Look Pure Law Look p@Pure{} -> -- trace "Look Pure Law" $ p -- Look Empty Law Look p@Empty -> -- trace "Look Empty Law" $ p -- NegLook Pure Law NegLook Pure{} -> -- trace "NegLook Pure Law" $ Empty -- NegLook Empty Law NegLook Empty -> -- trace "NegLook Dead Law" $ Pure H.unit -- NegLook Double Negation Law NegLook (NegLook p) -> -- trace "NegLook Double Negation Law" $ optimizeCombNode (Look (Try p) :*> Pure H.unit) -- NegLook Zero Consumption Law NegLook (Try p) -> -- trace "NegLook Zero Consumption Law" $ optimizeCombNode (NegLook p) -- Idempotence Law Look (Look p) -> -- trace "Look Idempotence Law" $ Look p -- Look Right Identity Law NegLook (Look p) -> -- trace "Look Right Identity Law" $ optimizeCombNode (NegLook p) -- Look Left Identity Law Look (NegLook p) -> -- trace "Look Left Identity Law" $ NegLook p -- NegLook Transparency Law NegLook (Try p :<|> q) -> -- trace "NegLook Transparency Law" $ optimizeCombNode (optimizeCombNode (NegLook p) :*> optimizeCombNode (NegLook q)) -- Look Distributivity Law Look p :<|> Look q -> -- trace "Look Distributivity Law" $ optimizeCombNode (Look (optimizeCombNode (Try p :<|> q))) -- Look Interchange Law Look (f :<$> p) -> -- trace "Look Interchange Law" $ optimizeCombNode (f :<$> optimizeCombNode (Look p)) -- NegLook Idempotence Right Law NegLook (_ :<$> p) -> -- trace "NegLook Idempotence Law" $ optimizeCombNode (NegLook p) -- Try Interchange Law Try (f :<$> p) -> -- trace "Try Interchange Law" $ optimizeCombNode (f :<$> optimizeCombNode (Try p)) -- Branch Absorption Law Branch Empty _ _ -> -- trace "Branch Absorption Law" $ empty -- Branch Weakening Law Branch b Empty Empty -> -- trace "Branch Weakening Law" $ optimizeCombNode (b :*> Empty) -- Branch Pure Left/Right Laws Branch (Pure (trans -> lr)) l r -> -- trace "Branch Pure Left/Right Law" $ case getValue lr of Left v -> optimizeCombNode (l :<*> Pure (H.Haskell (ValueCode (Value v) c))) where c = [|| case $$(code lr) of Left x -> x ||] Right v -> optimizeCombNode (r :<*> Pure (H.Haskell (ValueCode (Value v) c))) where c = [|| case $$(code lr) of Right x -> x ||] -- Branch Generalised Identity Law Branch b (Pure (trans -> l)) (Pure (trans -> r)) -> -- trace "Branch Generalised Identity Law" $ optimizeCombNode (H.Haskell (ValueCode v c) :<$> b) where v = Value (either (getValue l) (getValue r)) c = [|| either $$(code l) $$(code r) ||] -- Branch Interchange Law Branch (x :*> y) p q -> -- trace "Branch Interchange Law" $ optimizeCombNode (x :*> optimizeCombNode (Branch y p q)) -- Branch Empty Right Law Branch b l Empty -> -- trace " Branch Empty Right Law" $ Branch (Pure (H.Haskell (ValueCode v c)) :<*> b) Empty l where v = Value (either Right Left) c = [||either Right Left||] -- Branch Fusion Law Branch (Branch b Empty (Pure (trans -> lr))) Empty br -> -- trace "Branch Fusion Law" $ optimizeCombNode (Branch (optimizeCombNode (Pure (H.Haskell (ValueCode (Value v) c)) :<*> b)) Empty br) where v Left{} = Left () v (Right r) = case getValue lr r of Left _ -> Left () Right rr -> Right rr c = [|| \case Left{} -> Left () Right r -> case $$(code lr) r of Left _ -> Left () Right rr -> Right rr ||] -- Branch Distributivity Law f :<$> Branch b l r -> -- trace "Branch Distributivity Law" $ optimizeCombNode (Branch b (optimizeCombNode ((H..@) (H..) f :<$> l)) (optimizeCombNode ((H..@) (H..) f :<$> r))) -- Match Absorption Law Match _ _ Empty d -> -- trace "Match Absorption Law" $ d -- Match Weakening Law Match _ bs a Empty | all (\case {Empty -> True; _ -> False}) bs -> -- trace "Match Weakening Law" $ optimizeCombNode (a :*> Empty) -- Match Pure Law Match ps bs (Pure (trans -> a)) d -> -- trace "Match Pure Law" $ foldr (\(trans -> p, b) next -> if getValue p (getValue a) then b else next ) d (List.zip ps bs) -- Match Distributivity Law f :<$> Match ps bs a d -> -- trace "Match Distributivity Law" $ Match ps (optimizeCombNode . (f :<$>) Functor.<$> bs) a (optimizeCombNode (f :<$> d)) {- Possibly useless laws to be tested Empty :*> _ -> Empty Empty :<* _ -> Empty -- App Definition of *> Law H.Flip H..@ H.Const :<$> p :<*> q -> -- -- trace "EXTRALAW: App Definition of *> Law" $ p :*> q -- App Definition of <* Law H.Const :<$> p :<*> q -> -- -- trace "EXTRALAW: App Definition of <* Law" $ p :<* q -- Functor Composition Law -- (a shortcut that could also have been be caught -- by the Composition Law and Homomorphism Law) f :<$> (g :<$> p) -> -- -- trace "EXTRALAW: Functor Composition Law" $ optimizeCombNode ((H.:.) H..@ f H..@ g :<$> p) -- Applicable Failure Weakening Law u :<* Empty -> -- -- trace "EXTRALAW: App Failure Weakening Law" $ optimizeCombNode (u :*> Empty) Try (p :$> x) -> -- -- trace "EXTRALAW: Try Interchange Right Law" $ optimizeCombNode (optimizeCombNode (Try p) :$> x) -- App Reassociation Law 1 (u :*> v) :<*> w -> -- -- trace "EXTRALAW: App Reassociation Law 1" $ optimizeCombNode (u :*> optimizeCombNode (v :<*> w)) -- App Reassociation Law 2 u :<*> (v :<* w) -> -- -- trace "EXTRALAW: App Reassociation Law 2" $ optimizeCombNode (optimizeCombNode (u :<*> v) :<* w) -- App Right Associativity Law u :*> (v :*> w) -> -- -- trace "EXTRALAW: App Right Associativity Law" $ optimizeCombNode (optimizeCombNode (u :*> v) :*> w) -- App Reassociation Law 3 u :<*> (v :$> x) -> -- -- trace "EXTRALAW: App Reassociation Law 3" $ optimizeCombNode (optimizeCombNode (u :<*> Pure x) :<* v) Look (p :$> x) -> optimizeCombNode (optimizeCombNode (Look p) :$> x) NegLook (p :$> _) -> optimizeCombNode (NegLook p) -- NegLook Absorption Law p :<*> NegLook q -> -- trace "EXTRALAW: Neglook Absorption Law" $ optimizeCombNode (optimizeCombNode (p :<*> Pure H.unit) :<* NegLook q) -- Infinite loop, because :<* expands to :<*> -} x -> x