-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# 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.Char (Char)
+import Data.Bool (Bool(..))
import Data.Either (Either(..), either)
import Data.Eq (Eq(..))
-import Data.Function ((.))
-import qualified Prelude as Pre
+import Data.Function (($), (.))
+import Data.Kind (Constraint)
+import Data.Maybe (Maybe(..))
+import Data.Set (Set)
+import Data.Functor.Identity (Identity(..))
+import Data.Functor.Product (Product(..))
+import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
+import qualified Data.Foldable as Foldable
+import qualified Data.Functor as Functor
+import qualified Data.List as List
-import Symantic.Parser.Grammar.Combinators as Comb
-import Symantic.Parser.Staging (ValueCode(..), Value(..), Code(..), getValue, getCode)
-import Symantic.Univariant.Letable
-import Symantic.Univariant.Liftable
-import qualified Language.Haskell.TH.Syntax as TH
-import qualified Symantic.Parser.Staging as Hask
+import Symantic.Parser.Grammar.Combinators
+import Symantic.Parser.Grammar.Production
+import Symantic.Typed.Letable
+import Symantic.Typed.Trans
+import qualified Symantic.Typed.Data as Prod
+import qualified Symantic.Typed.Lang as Prod
--- * Type 'Grammar'
-data Grammar a where
- Pure :: Hask.Haskell a -> Grammar a
- Satisfy :: Hask.Haskell (Char -> Bool) -> Grammar Char
- Item :: Grammar Char
- Try :: Grammar a -> Grammar a
- Look :: Grammar a -> Grammar a
- NegLook :: Grammar a -> Grammar ()
- (:<*>) :: Grammar (a -> b) -> Grammar a -> Grammar b
- (:<|>) :: Grammar a -> Grammar a -> Grammar a
- Empty :: Grammar a
- Branch :: Grammar (Either a b) -> Grammar (a -> c) -> Grammar (b -> c) -> Grammar c
- Match :: Eq a => [Hask.Haskell (a -> Bool)] -> [Grammar b] -> Grammar a -> Grammar b -> Grammar b
- ChainPre :: Grammar (a -> a) -> Grammar a -> Grammar a
- ChainPost :: Grammar a -> Grammar (a -> a) -> Grammar a
- Def :: TH.Name -> Grammar a -> Grammar a
- Ref :: Bool -> TH.Name -> Grammar a
+{-
+import Data.Function (($), flip)
+import Debug.Trace (trace)
-pattern (:<$>) :: Hask.Haskell (a -> b) -> Grammar a -> Grammar b
-pattern (:$>) :: Grammar a -> Hask.Haskell b -> Grammar b
-pattern (:<$) :: Hask.Haskell a -> Grammar b -> Grammar a
-pattern (:*>) :: Grammar a -> Grammar b -> Grammar b
-pattern (:<*) :: Grammar a -> Grammar b -> Grammar a
-pattern x :<$> p = Pure x :<*> p
-pattern p :$> x = p :*> Pure x
-pattern x :<$ p = Pure x :<* p
-pattern x :<* p = Hask.Const :<$> x :<*> p
-pattern p :*> x = Hask.Id :<$ p :<*> x
+(&) = flip ($)
+infix 0 &
+-}
-infixl 3 :<|>
-infixl 4 :<*>, :<*, :*>
-infixl 4 :<$>, :<$, :$>
+-- * Type 'OptimizeGrammar'
+type OptimizeGrammar = SomeComb
-instance Applicable Grammar where
- pure = Pure
- (<*>) = (:<*>)
-instance Alternable Grammar where
- (<|>) = (:<|>)
- empty = Empty
- try = Try
-instance Selectable Grammar where
- branch = Branch
-instance Matchable Grammar where
- conditional = Match
-instance Foldable Grammar where
- chainPre = ChainPre
- chainPost = ChainPost
-instance Charable Grammar where
- satisfy = Satisfy
-instance Lookable Grammar where
- look = Look
- negLook = NegLook
-instance Letable TH.Name Grammar where
- def = Def
- ref = Ref
-instance MakeLetName TH.Name where
- makeLetName _ = TH.qNewName "let"
+optimizeGrammar ::
+ Trans (SomeComb repr) repr =>
+ SomeComb repr a -> repr a
+optimizeGrammar = trans
-instance
- ( Applicable repr
- , Alternable repr
- , Selectable repr
- , Foldable repr
- , Charable repr
- , Lookable repr
- , Matchable repr
- , Letable TH.Name repr
- ) =>
- Symantic Grammar repr where
- sym = \case
- Pure a -> pure a
- Satisfy p -> satisfy p
- Item -> item
- Try x -> try (sym x)
- Look x -> look (sym x)
- NegLook x -> negLook (sym x)
- x :<*> y -> sym x <*> sym y
- x :<|> y -> sym x <|> sym y
+-- * Data family 'Comb'
+-- | 'Comb'inators of the 'Grammar'.
+-- This is an extensible data-type.
+data family Comb
+ (comb :: ReprComb -> Constraint)
+ :: 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 '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 understandable 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
+
+-- CombAlternable
+data instance Comb CombAlternable repr a where
+ Alt :: Exception -> SomeComb repr a -> SomeComb repr a -> Comb CombAlternable repr a
+ Empty :: Comb CombAlternable repr a
+ Failure :: SomeFailure -> Comb CombAlternable repr a
+ Throw :: ExceptionLabel -> Comb CombAlternable repr a
+ Try :: SomeComb repr a -> Comb CombAlternable repr a
+instance CombAlternable repr => Trans (Comb CombAlternable repr) repr where
+ trans = \case
+ Alt exn x y -> alt exn (trans x) (trans y)
Empty -> empty
- Branch lr l r -> branch (sym lr) (sym l) (sym r)
- Match cs bs a b -> conditional cs (sym Pre.<$> bs) (sym a) (sym b)
- ChainPre x y -> chainPre (sym x) (sym y)
- ChainPost x y -> chainPost (sym x) (sym y)
- Def n x -> def n (sym x)
- Ref r n -> ref r n
-{-
-type instance Unlift Grammar = repr
+ Failure sf -> failure sf
+ Throw exn -> throw exn
+ Try x -> try (trans x)
instance
- ( Applicable repr
- , Alternable repr
- , Selectable repr
- , Foldable repr
- , Charable repr
- , Lookable repr
- , Matchable repr
- , Letable repr
- ) => Unliftable Grammar where
- unlift = \case
- Pure a -> pure a
- Satisfy p -> satisfy p
- Item -> item
- Try x -> try (unlift x)
- Look x -> look (unlift x)
- NegLook x -> negLook (unlift x)
- x :<*> y -> unlift x <*> unlift y
- x :<|> y -> unlift x <|> unlift y
- Empty -> empty
- Branch lr l r -> branch (unlift lr) (unlift l) (unlift r)
- Match cs bs a b -> conditional cs (unlift Pre.<$> bs) (unlift a) (unlift b)
- ChainPre x y -> chainPre (unlift x) (unlift y)
- ChainPost x y -> chainPost (unlift x) (unlift y)
- Ref{..} -> let_ let_rec let_name
+ ( CombAlternable repr
+ , CombApplicable repr
+ , CombLookable repr
+ , CombMatchable repr
+ , CombSelectable repr
+ ) => CombAlternable (SomeComb repr) where
+ empty = SomeComb Empty
+ failure sf = SomeComb (Failure sf)
-unComb ::
- ( Applicable repr
- , Alternable repr
- , Selectable repr
- , Foldable repr
- , Charable repr
- , Lookable repr
- , Matchable repr
- , Letable repr
- ) => Grammar repr a -> repr a
-unComb = unlift
--}
+ alt _exn p@(Comb Pure{}) _ = p
+ -- & trace "Left Catch Law"
+ alt _exn (Comb Empty) u = u
+ -- & trace "Left Neutral Law"
+ alt _exn u (Comb Empty) = u
+ -- & trace "Right Neutral Law"
+ alt exn (Comb (Alt exn' u v)) w | exn' == exn = u <|> (v <|> w)
+ -- See Lemma 1 (Associativity of choice for labeled PEGs)
+ -- in https://doi.org/10.1145/2851613.2851750
+ -- & trace "Associativity Law"
+ alt exn (Comb (Look p)) (Comb (Look q)) = look (alt exn (try p) q)
+ -- & trace "Distributivity Law"
+ alt exn x y = SomeComb (Alt exn x y)
--- * Type 'OptimizeGrammar'
-newtype OptimizeGrammar letName a = OptimizeGrammar { unOptimizeGrammar ::
- Grammar a }
+ throw exn = SomeComb (Throw exn)
-optimizeGrammar :: OptimizeGrammar TH.Name a -> Grammar a
-optimizeGrammar = unOptimizeGrammar
+ 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)
-type instance Unlift (OptimizeGrammar letName) = Grammar
-instance Unliftable (OptimizeGrammar letName) where
- unlift = unOptimizeGrammar
-instance Liftable (OptimizeGrammar letName) where
- lift = OptimizeGrammar . optimizeGrammarNode
+-- CombApplicable
+data instance Comb CombApplicable repr a where
+ Pure :: Production a -> Comb CombApplicable repr a
+ (:<*>:) :: SomeComb repr (a -> b) -> SomeComb repr a -> Comb CombApplicable repr b
+ (:<*:) :: SomeComb repr a -> SomeComb repr b -> Comb CombApplicable repr a
+ (:*>:) :: SomeComb repr a -> SomeComb repr b -> Comb CombApplicable repr b
+infixl 4 :<*>:, :<*:, :*>:
+pattern (:<$>:) :: Production (a -> b) -> SomeComb repr a -> Comb CombApplicable repr b
+pattern t :<$>: x <- Comb (Pure t) :<*>: x
+pattern (:$>:) :: SomeComb repr a -> Production b -> Comb CombApplicable repr b
+pattern x :$>: t <- x :*>: Comb (Pure t)
+instance CombApplicable repr => Trans (Comb CombApplicable repr) repr where
+ trans = \case
+ Pure x -> pure (optimizeProduction x)
+ f :<*>: x -> trans f <*> trans x
+ x :<*: y -> trans x <* trans y
+ x :*>: y -> trans x *> trans y
instance
- Letable letName Grammar =>
- Letable letName (OptimizeGrammar letName)
-instance Comb.Applicable (OptimizeGrammar letName)
-instance Comb.Alternable (OptimizeGrammar letName)
-instance Comb.Charable (OptimizeGrammar letName)
-instance Comb.Selectable (OptimizeGrammar letName)
-instance Comb.Matchable (OptimizeGrammar letName)
-instance Comb.Lookable (OptimizeGrammar letName)
-instance Comb.Foldable (OptimizeGrammar letName)
+ ( CombApplicable repr
+ , CombAlternable repr
+ , CombLookable repr
+ , CombMatchable repr
+ , CombSelectable repr
+ ) => CombApplicable (SomeComb repr) where
+ pure = SomeComb . Pure
+ f <$> Comb (Branch b l r) =
+ branch b
+ ((Prod..) Prod..@ f <$> l)
+ ((Prod..) Prod..@ 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
-optimizeGrammarNode :: Grammar a -> Grammar a
-optimizeGrammarNode = \case
- -- Recurse into shared and/or recursive 'let' definition
- Def n x -> Def n (optimizeGrammarNode x)
+ x <$ u = u $> x
+ -- & trace "Commutativity Law"
- -- Applicable Right Absorption Law
- Empty :<*> _ -> Empty
- Empty :*> _ -> Empty
- Empty :<* _ -> Empty
- -- Applicable Failure Weakening Law
- u :<*> Empty -> optimizeGrammarNode (u :*> Empty)
- u :<* Empty -> optimizeGrammarNode (u :*> Empty)
- -- Branch Absorption Law
- Branch Empty _ _ -> empty
- -- Branch Weakening Law
- Branch b Empty Empty -> optimizeGrammarNode (b :*> Empty)
+ 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 Prod..@ 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.
+ (Prod..) Prod..@ f Prod..@ g <$> p
+ -- & trace "Functor Composition Law"
+ -}
+ u <*> Comb (Pure x) = Prod.flip Prod..@ (Prod.$) Prod..@ x <$> u
+ -- & trace "Interchange Law"
+ u <*> Comb (v :<*>: w) = (((Prod..) <$> 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 Prod.unit) <* negLook q
+ -- & trace "Absorption Law"
+ x <*> y = SomeComb (x :<*>: y)
- -- Applicable Identity Law
- Hask.Id :<$> x -> x
- -- Flip const optimisation
- Hask.Flip Hask.:@ Hask.Const :<$> u -> optimizeGrammarNode (u :*> Pure Hask.Id)
- -- Homomorphism Law
- f :<$> Pure x -> Pure (f Hask.:@ x)
- -- Functor Composition Law
- -- (a shortcut that could also have been be caught
- -- by the Composition Law and Homomorphism law)
- f :<$> (g :<$> p) -> optimizeGrammarNode ((Hask.:.) Hask.:@ f Hask.:@ g :<$> p)
- -- Composition Law
- u :<*> (v :<*> w) -> optimizeGrammarNode (optimizeGrammarNode (optimizeGrammarNode ((Hask.:.) :<$> u) :<*> v) :<*> w)
- -- Definition of *>
- Hask.Flip Hask.:@ Hask.Const :<$> p :<*> q -> p :*> q
- -- Definition of <*
- Hask.Const :<$> p :<*> q -> p :<* q
- -- Reassociation Law 1
- (u :*> v) :<*> w -> optimizeGrammarNode (u :*> optimizeGrammarNode (v :<*> w))
- -- Pure merge optimisation
- Pure x :<*> Pure y -> Pure (x Hask.:@ y)
- -- Interchange Law
- u :<*> Pure x -> optimizeGrammarNode (Hask.Flip Hask.:@ (Hask.:$) Hask.:@ x :<$> u)
- -- Right Absorption Law
- (_ :<$> p) :*> q -> p :*> q
- -- Left Absorption Law
- p :<* (_ :<$> q) -> p :<* q
- -- Reassociation Law 2
- u :<*> (v :<* w) -> optimizeGrammarNode (optimizeGrammarNode (u :<*> v) :<* w)
- -- Reassociation Law 3
- u :<*> (v :$> x) -> optimizeGrammarNode (optimizeGrammarNode (u :<*> Pure x) :<* v)
+ 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)
- -- Left Catch Law
- p@Pure{} :<|> _ -> p
- -- Left Neutral Law
- Empty :<|> u -> u
- -- Right Neutral Law
- u :<|> Empty -> u
- -- Associativity Law
- (u :<|> v) :<|> w -> u :<|> optimizeGrammarNode (v :<|> w)
+ 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)
- -- Identity law
- Pure _ :*> u -> u
- -- Identity law
- (u :$> _) :*> v -> u :*> v
- -- Associativity Law
- u :*> (v :*> w) -> optimizeGrammarNode (optimizeGrammarNode (u :*> v) :*> w)
- -- Identity law
- u :<* Pure _ -> u
- -- Identity law
- u :<* (v :$> _) -> optimizeGrammarNode (u :<* v)
- -- Commutativity Law
- x :<$ u -> optimizeGrammarNode (u :$> x)
- -- Associativity Law
- (u :<* v) :<* w -> optimizeGrammarNode (u :<* optimizeGrammarNode (v :<* w))
+-- CombFoldable
+data instance Comb CombFoldable repr a where
+ ChainPreC :: SomeComb repr (a -> a) -> SomeComb repr a -> Comb CombFoldable repr a
+ ChainPostC :: SomeComb repr a -> SomeComb repr (a -> a) -> Comb CombFoldable repr a
+instance CombFoldable repr => Trans (Comb CombFoldable repr) repr where
+ trans = \case
+ ChainPreC x y -> chainPre (trans x) (trans y)
+ ChainPostC x y -> chainPost (trans x) (trans y)
+instance CombFoldable repr => CombFoldable (SomeComb repr) where
+ chainPre x = SomeComb . ChainPreC x
+ chainPost x = SomeComb . ChainPostC x
- -- Pure lookahead
- Look p@Pure{} -> p
- -- Dead lookahead
- Look p@Empty -> p
- -- Pure negative-lookahead
- NegLook Pure{} -> Empty
+-- 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
- -- Dead negative-lookahead
- NegLook Empty -> Pure Hask.unit
- -- Double Negation Law
- NegLook (NegLook p) -> optimizeGrammarNode (Look (Try p) :*> Pure Hask.unit)
- -- Zero Consumption Law
- NegLook (Try p) -> optimizeGrammarNode (NegLook p)
- -- Idempotence Law
- Look (Look p) -> Look p
- -- Right Identity Law
- NegLook (Look p) -> optimizeGrammarNode (NegLook p)
+-- 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
- -- Left Identity Law
- Look (NegLook p) -> NegLook p
- -- Transparency Law
- NegLook (Try p :<|> q) -> optimizeGrammarNode (optimizeGrammarNode (NegLook p) :*> optimizeGrammarNode (NegLook q))
- -- Distributivity Law
- Look p :<|> Look q -> optimizeGrammarNode (Look (optimizeGrammarNode (Try p :<|> q)))
- -- Interchange Law
- Look (p :$> x) -> optimizeGrammarNode (optimizeGrammarNode (Look p) :$> x)
- -- Interchange law
- Look (f :<$> p) -> optimizeGrammarNode (f :<$> optimizeGrammarNode (Look p))
- -- Absorption Law
- p :<*> NegLook q -> optimizeGrammarNode (optimizeGrammarNode (p :<*> Pure Hask.unit) :<* NegLook q)
- -- Idempotence Law
- NegLook (p :$> _) -> optimizeGrammarNode (NegLook p)
- -- Idempotence Law
- NegLook (_ :<$> p) -> optimizeGrammarNode (NegLook p)
- -- Interchange Law
- Try (p :$> x) -> optimizeGrammarNode (optimizeGrammarNode (Try p) :$> x)
- -- Interchange law
- Try (f :<$> p) -> optimizeGrammarNode (f :<$> optimizeGrammarNode (Try p))
+-- CombLookable
+data instance Comb CombLookable repr a where
+ Look :: SomeComb repr a -> Comb CombLookable repr a
+ NegLook :: SomeComb repr a -> Comb CombLookable repr ()
+ Eof :: Comb CombLookable repr ()
+instance CombLookable repr => Trans (Comb CombLookable repr) repr where
+ trans = \case
+ Look x -> look (trans x)
+ NegLook x -> negLook (trans x)
+ Eof -> eof
+instance
+ ( CombAlternable repr
+ , CombApplicable repr
+ , CombLookable repr
+ , CombSelectable repr
+ , CombMatchable repr
+ ) => CombLookable (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)
- -- pure Left/Right laws
- Branch (Pure (unlift -> lr)) l r ->
- case getValue lr of
- Left v -> optimizeGrammarNode (l :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
- where c = Code [|| case $$(getCode lr) of Left x -> x ||]
- Right v -> optimizeGrammarNode (r :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
- where c = Code [|| case $$(getCode lr) of Right x -> x ||]
- -- Generalised Identity law
- Branch b (Pure (unlift -> l)) (Pure (unlift -> r)) ->
- optimizeGrammarNode (Hask.Haskell (ValueCode v c) :<$> b)
+ negLook (Comb Pure{}) = empty
+ -- & trace "Pure Negative-Look"
+ negLook (Comb Empty) = pure Prod.unit
+ -- & trace "Dead Negative-Look"
+ negLook (Comb (NegLook x)) = look (try x *> pure Prod.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 (Alt _exn (Comb (Try p)) q)) = negLook p *> negLook q
+ -- FIXME: see if this really holds for all exceptions.
+ -- & trace "Transparency Law"
+ negLook (Comb (p :$>: _)) = negLook p
+ -- & trace "NegLook Idempotence Law"
+ negLook x = SomeComb (NegLook x)
+
+ eof = SomeComb Eof
+
+-- CombMatchable
+data instance Comb CombMatchable repr a where
+ Conditional :: Eq a =>
+ SomeComb repr a ->
+ [Production (a -> Bool)] ->
+ [SomeComb repr b] ->
+ SomeComb repr b ->
+ Comb CombMatchable repr b
+instance CombMatchable repr => Trans (Comb CombMatchable repr) repr where
+ trans = \case
+ Conditional a ps bs b ->
+ conditional (trans a)
+ (optimizeProduction Functor.<$> ps)
+ (trans Functor.<$> bs) (trans b)
+instance
+ ( CombApplicable repr
+ , CombAlternable repr
+ , CombLookable repr
+ , CombSelectable repr
+ , CombMatchable repr
+ ) => CombMatchable (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 a)) ps bs d =
+ Foldable.foldr (\(p, b) next ->
+ if runValue (p Prod..@ 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)
+
+-- CombSatisfiable
+data instance Comb (CombSatisfiable tok) repr a where
+ -- | To include the @('Set' 'SomeFailure')@ is a little kludge
+ -- it would be cleaner to be able to pattern-match
+ -- on @(alt exn (Comb 'Satisfy'{}) (Failure{}))@
+ -- when generating 'Program', but this is not easily possible then
+ -- because data types have already been converted back to class methods,
+ -- hence pattern-matching is no longer possible
+ -- (at least not without reintroducing data types).
+ SatisfyOrFail ::
+ CombSatisfiable tok repr =>
+ Set SomeFailure ->
+ Production (tok -> Bool) ->
+ Comb (CombSatisfiable tok) repr tok
+instance
+ CombSatisfiable tok repr =>
+ Trans (Comb (CombSatisfiable tok) repr) repr where
+ trans = \case
+ SatisfyOrFail fs p -> satisfyOrFail fs (optimizeProduction p)
+instance
+ (CombSatisfiable tok repr, Typeable tok) =>
+ CombSatisfiable tok (SomeComb repr) where
+ satisfyOrFail fs = SomeComb . SatisfyOrFail fs
+
+-- CombSelectable
+data instance Comb CombSelectable repr a where
+ Branch ::
+ SomeComb repr (Either a b) ->
+ SomeComb repr (a -> c) ->
+ SomeComb repr (b -> c) ->
+ Comb CombSelectable repr c
+instance CombSelectable repr => Trans (Comb CombSelectable repr) repr where
+ trans = \case
+ Branch lr l r -> branch (trans lr) (trans l) (trans r)
+instance
+ ( CombApplicable repr
+ , CombAlternable repr
+ , CombLookable repr
+ , CombSelectable repr
+ , CombMatchable repr
+ ) => CombSelectable (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 lr)) l r =
+ case runValue lr of
+ Left value -> l <*> pure (Pair v c)
+ where
+ v = Prod.SomeData $ Prod.Var $ Identity value
+ c = Prod.SomeData $ Prod.Var
+ [|| case $$(runCode lr) of Left x -> x ||]
+ Right value -> r <*> pure (Pair v c)
+ where
+ v = Prod.SomeData $ Prod.Var $ Identity value
+ c = Prod.SomeData $ Prod.Var
+ [|| case $$(runCode lr) of Right x -> x ||]
+ -- & trace "Branch Pure Either Law"
+ branch b (Comb (Pure l)) (Comb (Pure r)) =
+ Pair v c <$> b
+ -- & trace "Branch Generalised Identity Law"
where
- v = Value (either (getValue l) (getValue r))
- c = Code [|| either $$(getCode l) $$(getCode r) ||]
- -- Interchange law
- Branch (x :*> y) p q ->
- optimizeGrammarNode (x :*> optimizeGrammarNode (Branch y p q))
- -- Negated Branch law
- Branch b l Empty ->
- Branch (Pure (Hask.Haskell (ValueCode v c)) :<*> b) Empty l
+ v = Prod.SomeData $ Prod.Var $ Identity $ either (runValue l) (runValue r)
+ c = Prod.SomeData $ Prod.Var [|| either $$(runCode l) $$(runCode r) ||]
+ branch (Comb (x :*>: y)) p q = x *> branch y p q
+ -- & trace "Interchange Law"
+ branch b l (Comb Empty) =
+ branch (pure (Pair v c) <*> b) empty l
+ -- & trace "Negated Branch Law"
where
- v = Value (either Right Left)
- c = Code [||either Right Left||]
- -- Branch Fusion law
- Branch (Branch b Empty (Pure (unlift -> lr))) Empty br ->
- optimizeGrammarNode (Branch (optimizeGrammarNode (Pure (Hask.Haskell (ValueCode (Value v) c)) :<*> b)) Empty br)
+ v = Prod.SomeData $ Prod.Var $ Identity $ either Right Left
+ c = Prod.SomeData $ Prod.Var $ [||either Right Left||]
+ branch (Comb (Branch b (Comb Empty) (Comb (Pure lr)))) (Comb Empty) br =
+ branch (pure (Pair v c) <*> b) empty br
+ -- & trace "Branch Fusion Law"
where
- v Left{} = Left ()
- v (Right r) = case getValue lr r of
- Left _ -> Left ()
- Right rr -> Right rr
- c = Code [|| \case Left{} -> Left ()
- Right r -> case $$(getCode lr) r of
- Left _ -> Left ()
- Right rr -> Right rr ||]
- -- Distributivity Law
- f :<$> Branch b l r -> optimizeGrammarNode (Branch b (optimizeGrammarNode ((Hask..@) (Hask..) f :<$> l))
- (optimizeGrammarNode ((Hask..@) (Hask..) f :<$> r)))
-
- x -> x
+ v = Prod.SomeData $ Prod.Var $ Identity $ \case
+ Left{} -> Left ()
+ Right r ->
+ case runValue lr r of
+ Left{} -> Left ()
+ Right rr -> Right rr
+ c = Prod.SomeData $ Prod.Var
+ [|| \case Left{} -> Left ()
+ Right r -> case $$(runCode lr) r of
+ Left{} -> Left ()
+ Right rr -> Right rr ||]
+ branch b l r = SomeComb (Branch b l r)
sourcephile / git / haskell / symantic-parser.git / blobdiff