-{-# LANGUAGE PatternSynonyms #-} -- For aliased combinators
-{-# LANGUAGE TemplateHaskell #-} -- For optimizeCombNode
-{-# LANGUAGE ViewPatterns #-} -- For optimizeCombNode
+{-# 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.Either (Either(..), either)
import Data.Eq (Eq(..))
-import Data.Foldable (all, foldr)
import Data.Function ((.))
-import Data.Kind (Type)
+import Data.Kind (Constraint)
+import Data.Maybe (Maybe(..))
+import Data.Set (Set)
+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 qualified Language.Haskell.TH.Syntax as TH
-import Symantic.Parser.Grammar.Combinators as Comb
-import Symantic.Parser.Staging (ValueCode(..), Value(..), getValue, code)
+import Symantic.Parser.Grammar.Combinators hiding (code)
+import Symantic.Parser.Haskell ()
import Symantic.Univariant.Letable
import Symantic.Univariant.Trans
-import qualified Symantic.Parser.Staging as H
+import qualified Symantic.Parser.Haskell as H
--- import Debug.Trace (trace)
+{-
+import Data.Function (($), flip)
+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 :: H.Haskell (Char -> Bool) -> Comb repr Char
- Item :: Comb repr Char
- Try :: Comb repr a -> Comb repr a
- Look :: Comb repr a -> Comb repr a
- NegLook :: Comb repr a -> 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
+(&) = flip ($)
+infix 0 &
+-}
-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
+-- * Type 'OptimizeGrammar'
+type OptimizeGrammar = SomeComb
-infixl 3 :<|>
-infixl 4 :<*>, :<*, :*>
-infixl 4 :<$>, :<$, :$>
+optimizeGrammar ::
+ Trans (SomeComb repr) repr =>
+ SomeComb repr a -> repr a
+optimizeGrammar = trans
-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 Charable (Comb repr) where
- satisfy = Satisfy
-instance Lookable (Comb repr) where
- look = Look
- negLook = NegLook
-instance Letable TH.Name (Comb repr) where
- def = Def
- ref = Ref
-instance MakeLetName TH.Name where
- makeLetName _ = TH.qNewName "name"
+-- * Data family 'Comb'
+-- | 'Comb'inators of the 'Grammar'.
+-- This is an extensible data-type.
+data family Comb
+ (comb :: ReprComb -> Constraint)
+ (repr :: ReprComb)
+ :: ReprComb
--- 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
- , Charable repr
- , Lookable repr
- , Matchable repr
- , Letable TH.Name repr
- ) => Trans (Comb repr) repr where
+-- | 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
- Pure a -> pure a
- Satisfy p -> satisfy p
- Item -> item
- Try x -> try (trans x)
- Look x -> look (trans x)
- NegLook x -> negLook (trans x)
- x :<*> y -> trans x <*> trans y
- x :<|> y -> trans x <|> trans y
+ Alt exn x y -> alt exn (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
+ Failure sf -> failure sf
+ Throw exn -> throw exn
+ Try x -> try (trans x)
+instance
+ ( CombAlternable repr
+ , CombApplicable repr
+ , CombLookable repr
+ , CombMatchable repr
+ , CombSelectable repr
+ ) => CombAlternable (SomeComb repr) where
+ empty = SomeComb Empty
+ failure sf = SomeComb (Failure sf)
--- * Type 'OptimizeComb'
--- Bottom-up application of 'optimizeCombNode'.
-newtype OptimizeComb letName repr a = OptimizeComb { unOptimizeComb :: Comb repr a }
+ 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)
-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
+ throw exn = SomeComb (Throw exn)
-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)
+ 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)
+-- CombApplicable
+data instance Comb CombApplicable repr a where
+ Pure :: TermGrammar 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 (:<$>:) :: TermGrammar (a -> b) -> SomeComb repr a -> Comb CombApplicable repr b
+pattern t :<$>: x <- Comb (Pure t) :<*>: x
+pattern (:$>:) :: SomeComb repr a -> TermGrammar 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 (H.optimizeTerm x)
+ f :<*>: x -> trans f <*> trans x
+ x :<*: y -> trans x <* trans y
+ x :*>: y -> trans x *> trans y
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.Charable (OptimizeComb letName repr)
-instance Comb.Selectable (OptimizeComb letName repr)
-instance Comb.Matchable (OptimizeComb letName repr)
-instance Comb.Lookable (OptimizeComb letName repr)
-instance Comb.Foldable (OptimizeComb letName repr)
+ ( 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
+ ((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
-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)
+ x <$ u = u $> x
+ -- & trace "Commutativity Law"
- -- 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))
+ 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)
- -- Alt Left Catch Law
- p@Pure{} :<|> _ ->
- -- trace "Alt Left Catch 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)
+ 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)
- -- 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 Absorption Law
- p :<*> NegLook q ->
- -- trace "Neglook Absorption Law" $
- optimizeCombNode (optimizeCombNode (p :<*> Pure H.unit) :<* NegLook q)
- -- 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))
+ 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)
- -- 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)))
+-- 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
- -- 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))
+-- 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
- {- 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
+-- 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
- -- 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)
+-- 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)
- Look (p :$> x) ->
- optimizeCombNode (optimizeCombNode (Look p) :$> x)
- NegLook (p :$> _) -> optimizeCombNode (NegLook p)
+ 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 (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
- x -> x
+-- CombMatchable
+data instance Comb CombMatchable repr a where
+ Conditional :: Eq a =>
+ SomeComb repr a ->
+ [TermGrammar (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)
+ (H.optimizeTerm 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 (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)
+
+-- 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 ->
+ TermGrammar (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 (H.optimizeTerm 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 (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)