test: update
[haskell/symantic-parser.git] / src / Symantic / Parser / Grammar / Optimize.hs
index fd7b44f2b140a99065c2238385e086f8a517c9cd..e4e33f82c78eae7c5898336b3b7e50562adc69d4 100644 (file)
-{-# 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)