{-# LANGUAGE PatternSynonyms #-} -- For Comb {-# LANGUAGE TemplateHaskell #-} -- For branch {-# LANGUAGE ViewPatterns #-} -- For unSomeComb {-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name -- | Bottom-up optimization of 'Comb'inators, -- reexamining downward as needed after each optimization. module Symantic.Parser.Grammar.Optimize where import Data.Bool (Bool(..)) import Data.Either (Either(..), either) import Data.Eq (Eq(..)) import Data.Function ((.)) import Data.Maybe (Maybe(..)) import qualified Data.Functor as Functor import qualified Data.Foldable as Foldable import qualified Data.List as List import Data.Kind (Constraint, Type) import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..)) import Symantic.Parser.Grammar.Combinators as Comb import Symantic.Parser.Haskell () import Symantic.Univariant.Letable import Symantic.Univariant.Trans import qualified Symantic.Parser.Haskell as H {- import Data.Function (($), flip) import Debug.Trace (trace) (&) = flip ($) infix 0 & -} -- * Type 'OptimizeGrammar' type OptimizeGrammar = SomeComb optimizeGrammar :: Trans (SomeComb repr) repr => SomeComb repr a -> repr a optimizeGrammar = trans -- * Data family 'Comb' -- | 'Comb'inators of the 'Grammar'. -- This is an extensible data-type. data family Comb (comb :: ReprComb -> Constraint) (repr :: ReprComb) :: ReprComb -- | Convenient utility to pattern-match a 'SomeComb'. pattern Comb :: Typeable comb => Comb comb repr a -> SomeComb repr a pattern Comb x <- (unSomeComb -> Just x) -- ** Type 'ReprComb' type ReprComb = Type -> Type -- ** Type 'SomeComb' -- | Some 'Comb'inator existentialized over the actual combinator symantic class. -- Useful to handle a list of 'Comb'inators -- without requiring impredicative quantification. -- Must be used by pattern-matching -- on the 'SomeComb' data-constructor, -- to bring the constraints in scope. -- -- The optimizations are directly applied within it, -- to avoid introducing an extra newtype, -- this also give a more comprehensible code. data SomeComb repr a = forall comb. (Trans (Comb comb repr) repr, Typeable comb) => SomeComb (Comb comb repr a) instance Trans (SomeComb repr) repr where trans (SomeComb x) = trans x -- | @(unSomeComb c :: 'Maybe' ('Comb' comb repr a))@ -- extract the data-constructor from the given 'SomeComb' -- iif. it belongs to the @('Comb' comb repr a)@ data-instance. unSomeComb :: forall comb repr a. Typeable comb => SomeComb repr a -> Maybe (Comb comb repr a) unSomeComb (SomeComb (c::Comb c repr a)) = case typeRep @comb `eqTypeRep` typeRep @c of Just HRefl -> Just c Nothing -> Nothing -- Applicable data instance Comb Applicable repr a where Pure :: TermGrammar a -> Comb Applicable repr a (:<*>:) :: SomeComb repr (a -> b) -> SomeComb repr a -> Comb Applicable repr b (:<*:) :: SomeComb repr a -> SomeComb repr b -> Comb Applicable repr a (:*>:) :: SomeComb repr a -> SomeComb repr b -> Comb Applicable repr b infixl 4 :<*>:, :<*:, :*>: pattern (:<$>:) :: TermGrammar (a -> b) -> SomeComb repr a -> Comb Applicable repr b pattern t :<$>: x <- Comb (Pure t) :<*>: x pattern (:$>:) :: SomeComb repr a -> TermGrammar b -> Comb Applicable repr b pattern x :$>: t <- x :*>: Comb (Pure t) instance Applicable repr => Trans (Comb Applicable repr) repr where trans = \case Pure x -> pure (H.optimizeTerm x) f :<*>: x -> trans f <*> trans x x :<*: y -> trans x <* trans y x :*>: y -> trans x *> trans y instance ( Applicable repr , Alternable repr , Lookable repr , Matchable repr , Selectable repr ) => Applicable (SomeComb repr) where pure = SomeComb . Pure f <$> Comb (Branch b l r) = branch b ((H..) H..@ f <$> l) ((H..) H..@ f <$> r) -- & trace "Branch Distributivity Law" f <$> Comb (Conditional a ps bs d) = conditional a ps ((f <$>) Functor.<$> bs) (f <$> d) -- & trace "Conditional Distributivity Law" -- Being careful here to use (<*>), -- instead of SomeComb (f <$> unOptComb x), -- in order to apply the optimizations of (<*>). f <$> x = pure f <*> x x <$ u = u $> x -- & trace "Commutativity Law" Comb Empty <*> _ = empty -- & trace "App Right Absorption Law" u <*> Comb Empty = u *> empty -- & trace "App Failure Weakening Law" Comb (Pure f) <*> Comb (Pure x) = pure (f H..@ x) -- & trace "Homomorphism Law" {- Comb (Pure f) <*> Comb (g :<$>: p) = -- This is basically a shortcut, -- it can be caught by one Composition Law -- and two Homomorphism Law. (H..) H..@ f H..@ g <$> p -- & trace "Functor Composition Law" -} u <*> Comb (Pure x) = H.flip H..@ (H.$) H..@ x <$> u -- & trace "Interchange Law" u <*> Comb (v :<*>: w) = (((H..) <$> u) <*> v) <*> w -- & trace "Composition Law" Comb (u :*>: v) <*> w = u *> (v <*> w) -- & trace "Reassociation Law 1" u <*> Comb (v :<*: w) = (u <*> v) <* w -- & trace "Reassociation Law 2" u <*> Comb (v :$>: x) = (u <*> pure x) <* v -- & trace "Reassociation Law 3" p <*> Comb (NegLook q) = (p <*> pure H.unit) <* negLook q -- & trace "Absorption Law" x <*> y = SomeComb (x :<*>: y) Comb Empty *> _ = empty -- & trace "App Right Absorption Law" Comb (_ :<$>: p) *> q = p *> q -- & trace "Right Absorption Law" Comb Pure{} *> u = u -- & trace "Identity Law" Comb (u :$>: _) *> v = u *> v -- & trace "Identity Law" u *> Comb (v :*>: w) = (u *> v) *> w -- & trace "Associativity Law" x *> y = SomeComb (x :*>: y) Comb Empty <* _ = empty -- & trace "App Right Absorption Law" u <* Comb Empty = u *> empty -- & trace "App Failure Weakening Law" p <* Comb (_ :<$>: q) = p <* q -- & trace "Left Absorption Law" u <* Comb Pure{} = u -- & trace "Identity Law" u <* Comb (v :$>: _) = u <* v -- & trace "Identity Law" Comb (u :<*: v) <* w = u <* (v <* w) -- & trace "Associativity Law" x <* y = SomeComb (x :<*: y) -- Alternable data instance Comb Alternable repr a where Empty :: Comb Alternable repr a (:<|>:) :: SomeComb repr a -> SomeComb repr a -> Comb Alternable repr a Try :: SomeComb repr a -> Comb Alternable repr a infixl 3 :<|>: instance Alternable repr => Trans (Comb Alternable repr) repr where trans = \case Empty -> empty f :<|>: x -> trans f <|> trans x Try x -> try (trans x) instance ( Alternable repr , Applicable repr , Lookable repr , Matchable repr , Selectable repr ) => Alternable (SomeComb repr) where empty = SomeComb Empty p@(Comb Pure{}) <|> _ = p -- & trace "Left Catch Law" Comb Empty <|> u = u -- & trace "Left Neutral Law" u <|> Comb Empty = u -- & trace "Right Neutral Law" Comb (u :<|>: v) <|> w = u <|> (v <|> w) -- & trace "Associativity Law" Comb (Look p) <|> Comb (Look q) = look (try p <|> q) -- & trace "Distributivity Law" x <|> y = SomeComb (x :<|>: y) try (Comb (p :$>: x)) = try p $> x -- & trace "Try Interchange Law" try (Comb (f :<$>: p)) = f <$> try p -- & trace "Try Interchange Law" try x = SomeComb (Try x) -- Selectable data instance Comb Selectable repr a where Branch :: SomeComb repr (Either a b) -> SomeComb repr (a -> c) -> SomeComb repr (b -> c) -> Comb Selectable repr c instance Selectable repr => Trans (Comb Selectable repr) repr where trans = \case Branch lr l r -> branch (trans lr) (trans l) (trans r) instance ( Applicable repr , Alternable repr , Lookable repr , Selectable repr , Matchable repr ) => Selectable (SomeComb repr) where branch (Comb Empty) _ _ = empty -- & trace "Branch Absorption Law" branch b (Comb Empty) (Comb Empty) = b *> empty -- & trace "Branch Weakening Law" branch (Comb (Pure (trans -> lr))) l r = case H.value lr of Left value -> l <*> pure (trans H.ValueCode{..}) where code = [|| case $$(H.code lr) of Left x -> x ||] Right value -> r <*> pure (trans H.ValueCode{..}) where code = [|| case $$(H.code lr) of Right x -> x ||] -- & trace "Branch Pure Left/Right Law" branch b (Comb (Pure (trans -> l))) (Comb (Pure (trans -> r))) = trans H.ValueCode{..} <$> b -- & trace "Branch Generalised Identity Law" where value = either (H.value l) (H.value r) code = [|| either $$(H.code l) $$(H.code r) ||] branch (Comb (x :*>: y)) p q = x *> branch y p q -- & trace "Interchange Law" branch b l (Comb Empty) = branch (pure (trans (H.ValueCode{..})) <*> b) empty l -- & trace "Negated Branch Law" where value = either Right Left code = [||either Right Left||] branch (Comb (Branch b (Comb Empty) (Comb (Pure (trans -> lr))))) (Comb Empty) br = branch (pure (trans H.ValueCode{..}) <*> b) empty br -- & trace "Branch Fusion Law" where value Left{} = Left () value (Right r) = case H.value lr r of Left _ -> Left () Right rr -> Right rr code = [|| \case Left{} -> Left () Right r -> case $$(H.code lr) r of Left _ -> Left () Right rr -> Right rr ||] branch b l r = SomeComb (Branch b l r) -- Matchable data instance Comb Matchable repr a where Conditional :: Eq a => SomeComb repr a -> [TermGrammar (a -> Bool)] -> [SomeComb repr b] -> SomeComb repr b -> Comb Matchable repr b instance Matchable repr => Trans (Comb Matchable repr) repr where trans = \case Conditional a ps bs b -> conditional (trans a) (H.optimizeTerm Functor.<$> ps) (trans Functor.<$> bs) (trans b) instance ( Applicable repr , Alternable repr , Lookable repr , Selectable repr , Matchable repr ) => Matchable (SomeComb repr) where conditional (Comb Empty) _ _ d = d -- & trace "Conditional Absorption Law" conditional p _ qs (Comb Empty) | Foldable.all (\case { Comb Empty -> True; _ -> False }) qs = p *> empty -- & trace "Conditional Weakening Law" conditional a _ps bs (Comb Empty) | Foldable.all (\case { Comb Empty -> True; _ -> False }) bs = a *> empty -- & trace "Conditional Weakening Law" conditional (Comb (Pure (trans -> a))) ps bs d = Foldable.foldr (\(trans -> p, b) next -> if H.value p (H.value a) then b else next ) d (List.zip ps bs) -- & trace "Conditional Pure Law" conditional a ps bs d = SomeComb (Conditional a ps bs d) -- Foldable data instance Comb Foldable repr a where ChainPreC :: SomeComb repr (a -> a) -> SomeComb repr a -> Comb Foldable repr a ChainPostC :: SomeComb repr a -> SomeComb repr (a -> a) -> Comb Foldable repr a instance Foldable repr => Trans (Comb Foldable repr) repr where trans = \case ChainPreC x y -> chainPre (trans x) (trans y) ChainPostC x y -> chainPost (trans x) (trans y) instance Foldable repr => Foldable (SomeComb repr) where chainPre x = SomeComb . ChainPreC x chainPost x = SomeComb . ChainPostC x -- Lookable data instance Comb Lookable repr a where Look :: SomeComb repr a -> Comb Lookable repr a NegLook :: SomeComb repr a -> Comb Lookable repr () Eof :: Comb Lookable repr () instance Lookable repr => Trans (Comb Lookable repr) repr where trans = \case Look x -> look (trans x) NegLook x -> negLook (trans x) Eof -> eof instance ( Alternable repr , Applicable repr , Lookable repr , Selectable repr , Matchable repr ) => Lookable (SomeComb repr) where look p@(Comb Pure{}) = p -- & trace "Pure Look Law" look p@(Comb Empty) = p -- & trace "Dead Look Law" look (Comb (Look x)) = look x -- & trace "Idempotence Law" look (Comb (NegLook x)) = negLook x -- & trace "Left Identity Law" look (Comb (p :$>: x)) = look p $> x -- & trace "Interchange Law" look (Comb (f :<$>: p)) = f <$> look p -- & trace "Interchange Law" look x = SomeComb (Look x) negLook (Comb Pure{}) = empty -- & trace "Pure Negative-Look" negLook (Comb Empty) = pure H.unit -- & trace "Dead Negative-Look" negLook (Comb (NegLook x)) = look (try x *> pure H.unit) -- & trace "Double Negation Law" negLook (Comb (Try x)) = negLook x -- & trace "Zero Consumption Law" negLook (Comb (Look x)) = negLook x -- & trace "Right Identity Law" negLook (Comb (Comb (Try p) :<|>: q)) = negLook p *> negLook q -- & trace "Transparency Law" negLook (Comb (p :$>: _)) = negLook p -- & trace "NegLook Idempotence Law" negLook x = SomeComb (NegLook x) eof = SomeComb Eof -- Satisfiable data instance Comb (Satisfiable tok) repr a where Satisfy :: Satisfiable tok repr => [ErrorItem tok] -> TermGrammar (tok -> Bool) -> Comb (Satisfiable tok) repr tok Item :: Satisfiable tok repr => Comb (Satisfiable tok) repr tok instance Satisfiable tok repr => Trans (Comb (Satisfiable tok) repr) repr where trans = \case Satisfy es p -> satisfy es (H.optimizeTerm p) Item -> item instance (Satisfiable tok repr, Typeable tok) => Satisfiable tok (SomeComb repr) where satisfy es = SomeComb . Satisfy es item = SomeComb Item -- Letable data instance Comb (Letable letName) repr a where Shareable :: letName -> SomeComb repr a -> Comb (Letable letName) repr a Ref :: Bool -> letName -> Comb (Letable letName) repr a instance Letable letName repr => Trans (Comb (Letable letName) repr) repr where trans = \case Shareable n x -> shareable n (trans x) Ref isRec n -> ref isRec n instance (Letable letName repr, Typeable letName) => Letable letName (SomeComb repr) where shareable n = SomeComb . Shareable n ref isRec = SomeComb . Ref isRec -- Letsable data instance Comb (Letsable letName) repr a where Lets :: LetBindings letName (SomeComb repr) -> SomeComb repr a -> Comb (Letsable letName) repr a instance Letsable letName repr => Trans (Comb (Letsable letName) repr) repr where trans = \case Lets defs x -> lets ((\(SomeLet sub) -> SomeLet (trans sub)) Functor.<$> defs) (trans x) instance (Letsable letName repr, Typeable letName) => Letsable letName (SomeComb repr) where lets defs = SomeComb . Lets defs