{-# 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 qualified Language.Haskell.TH.Syntax as TH
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

{- Uncomment to trace optimizations
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 :: forall (repr :: ReprComb) a.
Trans (SomeComb repr) repr =>
SomeComb repr a -> repr a
optimizeGrammar = SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
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 $mComb :: forall {r} {comb :: ReprComb -> Constraint} {repr :: ReprComb} {a}.
Typeable comb =>
SomeComb repr a -> (Comb comb repr a -> r) -> (Void# -> r) -> r
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 :: forall a. SomeComb repr a -> repr a
trans (SomeComb Comb comb repr a
x) = Comb comb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans Comb comb repr a
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 :: forall (comb :: ReprComb -> Constraint) (repr :: ReprComb) a.
Typeable comb =>
SomeComb repr a -> Maybe (Comb comb repr a)
unSomeComb (SomeComb (Comb comb repr a
c::Comb c repr a)) =
  case forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: ReprComb -> Constraint). Typeable a => TypeRep a
typeRep @comb TypeRep comb -> TypeRep comb -> Maybe (comb :~~: comb)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: ReprComb -> Constraint). Typeable a => TypeRep a
typeRep @c of
    Just comb :~~: comb
HRefl -> Comb comb repr a -> Maybe (Comb comb repr a)
forall a. a -> Maybe a
Just Comb comb repr a
c
    Maybe (comb :~~: comb)
Nothing -> Maybe (Comb comb repr a)
forall a. Maybe a
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 $m:<$>: :: forall {r} {b} {repr :: ReprComb}.
Comb Applicable repr b
-> (forall {a}. TermGrammar (a -> b) -> SomeComb repr a -> r)
-> (Void# -> r)
-> r
:<$>: x <- Comb (Pure t) :<*>: x
pattern (:$>:) :: SomeComb repr a -> TermGrammar b -> Comb Applicable repr b
pattern x $m:$>: :: forall {r} {repr :: ReprComb} {b}.
Comb Applicable repr b
-> (forall {a}. SomeComb repr a -> TermGrammar b -> r)
-> (Void# -> r)
-> r
:$>: t <- x :*>: Comb (Pure t)
instance Applicable repr => Trans (Comb Applicable repr) repr where
  trans :: forall a. Comb Applicable repr a -> repr a
trans = \case
    Pure TermGrammar a
x -> TermGrammar a -> repr a
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure (TermGrammar a -> TermGrammar a
forall (repr :: ReprComb) a. Term repr a -> Term repr a
H.optimizeTerm TermGrammar a
x)
    SomeComb repr (a -> a)
f :<*>: SomeComb repr a
x -> SomeComb repr (a -> a) -> repr (a -> a)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr (a -> a)
f repr (a -> a) -> repr a -> repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
x
    SomeComb repr a
x :<*: SomeComb repr b
y -> SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
x repr a -> repr b -> repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr a
<* SomeComb repr b -> repr b
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr b
y
    SomeComb repr a
x :*>: SomeComb repr a
y -> SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
x repr a -> repr a -> repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
y
instance
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Matchable repr
  , Selectable repr
  ) => Applicable (SomeComb repr) where
  pure :: forall a. TermGrammar a -> SomeComb repr a
pure = Comb Applicable repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (Comb Applicable repr a -> SomeComb repr a)
-> (TermGrammar a -> Comb Applicable repr a)
-> TermGrammar a
-> SomeComb repr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermGrammar a -> Comb Applicable repr a
forall a (repr :: ReprComb).
TermGrammar a -> Comb Applicable repr a
Pure
  TermGrammar (a -> b)
f <$> :: forall a b.
TermGrammar (a -> b) -> SomeComb repr a -> SomeComb repr b
<$> Comb (Branch SomeComb repr (Either a b)
b SomeComb repr (a -> a)
l SomeComb repr (b -> a)
r) =
    SomeComb repr (Either a b)
-> SomeComb repr (a -> b)
-> SomeComb repr (b -> b)
-> SomeComb repr b
forall (repr :: ReprComb) a b c.
Selectable repr =>
repr (Either a b) -> repr (a -> c) -> repr (b -> c) -> repr c
branch SomeComb repr (Either a b)
b
      (Term ValueCode ((a -> b) -> (a -> a) -> a -> b)
forall (repr :: ReprComb) b c a.
Termable repr =>
repr ((b -> c) -> (a -> b) -> a -> c)
(H..) Term ValueCode ((a -> b) -> (a -> a) -> a -> b)
-> TermGrammar (a -> b) -> Term ValueCode ((a -> a) -> a -> b)
forall (repr :: ReprComb) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
H..@ TermGrammar (a -> b)
f Term ValueCode ((a -> a) -> a -> b)
-> SomeComb repr (a -> a) -> SomeComb repr (a -> b)
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr (a -> a)
l)
      (Term ValueCode ((a -> b) -> (b -> a) -> b -> b)
forall (repr :: ReprComb) b c a.
Termable repr =>
repr ((b -> c) -> (a -> b) -> a -> c)
(H..) Term ValueCode ((a -> b) -> (b -> a) -> b -> b)
-> TermGrammar (a -> b) -> Term ValueCode ((b -> a) -> b -> b)
forall (repr :: ReprComb) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
H..@ TermGrammar (a -> b)
f Term ValueCode ((b -> a) -> b -> b)
-> SomeComb repr (b -> a) -> SomeComb repr (b -> b)
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr (b -> a)
r)
    -- & trace "Branch Distributivity Law"
  TermGrammar (a -> b)
f <$> Comb (Conditional SomeComb repr a
a [TermGrammar (a -> Bool)]
ps [SomeComb repr a]
bs SomeComb repr a
d) =
    SomeComb repr a
-> [TermGrammar (a -> Bool)]
-> [SomeComb repr b]
-> SomeComb repr b
-> SomeComb repr b
forall (repr :: ReprComb) a b.
(Matchable repr, Eq a) =>
repr a -> [TermGrammar (a -> Bool)] -> [repr b] -> repr b -> repr b
conditional SomeComb repr a
a [TermGrammar (a -> Bool)]
ps
      ((TermGrammar (a -> b)
f TermGrammar (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$>) (SomeComb repr a -> SomeComb repr b)
-> [SomeComb repr a] -> [SomeComb repr b]
forall (f :: ReprComb) a b. Functor f => (a -> b) -> f a -> f b
Functor.<$> [SomeComb repr a]
bs)
      (TermGrammar (a -> b)
f TermGrammar (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr a
d)
    -- & trace "Conditional Distributivity Law"
  -- Being careful here to use (<*>),
  -- instead of SomeComb (f <$> unOptComb x),
  -- in order to apply the optimizations of (<*>).
  TermGrammar (a -> b)
f <$> SomeComb repr a
x = TermGrammar (a -> b) -> SomeComb repr (a -> b)
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure TermGrammar (a -> b)
f SomeComb repr (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> SomeComb repr a
x

  TermGrammar a
x <$ :: forall a b. TermGrammar a -> SomeComb repr b -> SomeComb repr a
<$ SomeComb repr b
u = SomeComb repr b
u SomeComb repr b -> TermGrammar a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> TermGrammar b -> repr b
$> TermGrammar a
x
    -- & trace "Commutativity Law"

  Comb Comb Alternable repr (a -> b)
R:CombAlternablerepra repr (a -> b)
Empty <*> :: forall a b.
SomeComb repr (a -> b) -> SomeComb repr a -> SomeComb repr b
<*> SomeComb repr a
_ = SomeComb repr b
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    -- & trace "App Right Absorption Law"
  SomeComb repr (a -> b)
u <*> Comb Comb Alternable repr a
R:CombAlternablerepra repr a
Empty = SomeComb repr (a -> b)
u SomeComb repr (a -> b) -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr b
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    -- & trace "App Failure Weakening Law"
  Comb (Pure TermGrammar (a -> b)
f) <*> Comb (Pure TermGrammar a
x) = TermGrammar b -> SomeComb repr b
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure (TermGrammar (a -> b)
f TermGrammar (a -> b) -> TermGrammar a -> TermGrammar b
forall (repr :: ReprComb) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
H..@ TermGrammar a
x)
    -- & trace "Homomorphism Law"
  Comb (Pure TermGrammar (a -> b)
f) <*> Comb (TermGrammar (a -> a)
g :<$>: SomeComb repr a
p) =
    -- This is basically a shortcut,
    -- it can be caught by the Composition Law
    -- and Homomorphism Law.
    Term ValueCode ((a -> b) -> (a -> a) -> a -> b)
forall (repr :: ReprComb) b c a.
Termable repr =>
repr ((b -> c) -> (a -> b) -> a -> c)
(H..) Term ValueCode ((a -> b) -> (a -> a) -> a -> b)
-> TermGrammar (a -> b) -> Term ValueCode ((a -> a) -> a -> b)
forall (repr :: ReprComb) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
H..@ TermGrammar (a -> b)
f Term ValueCode ((a -> a) -> a -> b)
-> TermGrammar (a -> a) -> Term ValueCode (a -> b)
forall (repr :: ReprComb) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
H..@ TermGrammar (a -> a)
g Term ValueCode (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr a
p
    -- & trace "Functor Composition Law"
  SomeComb repr (a -> b)
u <*> Comb (SomeComb repr (a -> a)
v :<*>: SomeComb repr a
w) = ((Term ValueCode ((a -> b) -> (a -> a) -> a -> b)
forall (repr :: ReprComb) b c a.
Termable repr =>
repr ((b -> c) -> (a -> b) -> a -> c)
(H..) Term ValueCode ((a -> b) -> (a -> a) -> a -> b)
-> SomeComb repr (a -> b) -> SomeComb repr ((a -> a) -> a -> b)
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr (a -> b)
u) SomeComb repr ((a -> a) -> a -> b)
-> SomeComb repr (a -> a) -> SomeComb repr (a -> b)
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> SomeComb repr (a -> a)
v) SomeComb repr (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> SomeComb repr a
w
    -- & trace "Composition Law"
  SomeComb repr (a -> b)
u <*> Comb (Pure TermGrammar a
x) = Term ValueCode (((a -> b) -> a -> b) -> a -> (a -> b) -> b)
forall (repr :: ReprComb) a b c.
Termable repr =>
repr ((a -> b -> c) -> b -> a -> c)
H.flip Term ValueCode (((a -> b) -> a -> b) -> a -> (a -> b) -> b)
-> Term ValueCode ((a -> b) -> a -> b)
-> Term ValueCode (a -> (a -> b) -> b)
forall (repr :: ReprComb) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
H..@ Term ValueCode ((a -> b) -> a -> b)
forall (repr :: ReprComb) a b.
Termable repr =>
repr ((a -> b) -> a -> b)
(H.$) Term ValueCode (a -> (a -> b) -> b)
-> TermGrammar a -> Term ValueCode ((a -> b) -> b)
forall (repr :: ReprComb) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
H..@ TermGrammar a
x Term ValueCode ((a -> b) -> b)
-> SomeComb repr (a -> b) -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr (a -> b)
u
    -- & trace "Interchange Law"
  Comb (SomeComb repr a
u :*>: SomeComb repr (a -> b)
v) <*> SomeComb repr a
w = SomeComb repr a
u SomeComb repr a -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> (SomeComb repr (a -> b)
v SomeComb repr (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> SomeComb repr a
w)
    -- & trace "Reassociation Law 1"
  SomeComb repr (a -> b)
u <*> Comb (SomeComb repr a
v :<*: SomeComb repr b
w) = (SomeComb repr (a -> b)
u SomeComb repr (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> SomeComb repr a
v) SomeComb repr b -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr a
<* SomeComb repr b
w
    -- & trace "Reassociation Law 2"
  SomeComb repr (a -> b)
u <*> Comb (SomeComb repr a
v :$>: TermGrammar a
x) = (SomeComb repr (a -> b)
u SomeComb repr (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> TermGrammar a -> SomeComb repr a
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure TermGrammar a
x) SomeComb repr b -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr a
<* SomeComb repr a
v
    -- & trace "Reassociation Law 3"
  SomeComb repr (a -> b)
p <*> Comb (NegLook SomeComb repr a
q) =
    (SomeComb repr (a -> b)
p SomeComb repr (a -> b) -> SomeComb repr a -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> TermGrammar () -> SomeComb repr ()
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure TermGrammar ()
forall (repr :: ReprComb). Termable repr => repr ()
H.unit) SomeComb repr b -> SomeComb repr () -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr a
<* SomeComb repr a -> SomeComb repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr ()
negLook (SomeComb repr a
q)
    -- & trace "Absorption Law"
  SomeComb repr (a -> b)
x <*> SomeComb repr a
y = Comb Applicable repr b -> SomeComb repr b
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr (a -> b)
x SomeComb repr (a -> b) -> SomeComb repr a -> Comb Applicable repr b
forall (repr :: ReprComb) a b.
SomeComb repr (a -> b) -> SomeComb repr a -> Comb Applicable repr b
:<*>: SomeComb repr a
y)

  Comb Comb Alternable repr a
R:CombAlternablerepra repr a
Empty *> :: forall a b. SomeComb repr a -> SomeComb repr b -> SomeComb repr b
*> SomeComb repr b
_ = SomeComb repr b
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    -- & trace "App Right Absorption Law"
  Comb (TermGrammar (a -> a)
_ :<$>: SomeComb repr a
p) *> SomeComb repr b
q = SomeComb repr a
p SomeComb repr a -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr b
q
    -- & trace "Right Absorption Law"
  Comb Pure{} *> SomeComb repr b
u = SomeComb repr b
u
    -- & trace "Identity Law"
  Comb (SomeComb repr a
u :$>: TermGrammar a
_) *> SomeComb repr b
v = SomeComb repr a
u SomeComb repr a -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr b
v
    -- & trace "Identity Law"
  SomeComb repr a
u *> Comb (SomeComb repr a
v :*>: SomeComb repr b
w) = (SomeComb repr a
u SomeComb repr a -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr a
v) SomeComb repr a -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr b
w
    -- & trace "Associativity Law"
  SomeComb repr a
x *> SomeComb repr b
y = Comb Applicable repr b -> SomeComb repr b
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr a
x SomeComb repr a -> SomeComb repr b -> Comb Applicable repr b
forall (repr :: ReprComb) a b.
SomeComb repr a -> SomeComb repr b -> Comb Applicable repr b
:*>: SomeComb repr b
y)

  Comb Comb Alternable repr a
R:CombAlternablerepra repr a
Empty <* :: forall a b. SomeComb repr a -> SomeComb repr b -> SomeComb repr a
<* SomeComb repr b
_ = SomeComb repr a
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    -- & trace "App Right Absorption Law"
  SomeComb repr a
u <* Comb Comb Alternable repr b
R:CombAlternablerepra repr b
Empty = SomeComb repr a
u SomeComb repr a -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr a
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    -- & trace "App Failure Weakening Law"
  SomeComb repr a
p <* Comb (TermGrammar (a -> b)
_ :<$>: SomeComb repr a
q) = SomeComb repr a
p SomeComb repr a -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr a
<* SomeComb repr a
q
    -- & trace "Left Absorption Law"
  SomeComb repr a
u <* Comb Pure{} = SomeComb repr a
u
    -- & trace "Identity Law"
  SomeComb repr a
u <* Comb (SomeComb repr a
v :$>: TermGrammar b
_) = SomeComb repr a
u SomeComb repr a -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr a
<* SomeComb repr a
v
    -- & trace "Identity Law"
  Comb (SomeComb repr a
u :<*: SomeComb repr b
v) <* SomeComb repr b
w = SomeComb repr a
u SomeComb repr a -> SomeComb repr b -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr a
<* (SomeComb repr b
v SomeComb repr b -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr a
<* SomeComb repr b
w)
    -- & trace "Associativity Law"
  SomeComb repr a
x <* SomeComb repr b
y = Comb Applicable repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr a
x SomeComb repr a -> SomeComb repr b -> Comb Applicable repr a
forall (repr :: ReprComb) a a.
SomeComb repr a -> SomeComb repr a -> Comb Applicable repr a
:<*: SomeComb repr b
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 :: forall a. Comb Alternable repr a -> repr a
trans = \case
    Comb Alternable repr a
R:CombAlternablerepra repr a
Empty -> repr a
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    SomeComb repr a
f :<|>: SomeComb repr a
x -> SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
f repr a -> repr a -> repr a
forall (repr :: ReprComb) a.
Alternable repr =>
repr a -> repr a -> repr a
<|> SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
x
    Try SomeComb repr a
x -> repr a -> repr a
forall (repr :: ReprComb) a. Alternable repr => repr a -> repr a
try (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
x)
instance
  ( Alternable repr
  , Applicable repr
  , Lookable repr
  , Matchable repr
  , Selectable repr
  ) => Alternable (SomeComb repr) where
  empty :: forall a. SomeComb repr a
empty = Comb Alternable repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb Comb Alternable repr a
forall (repr :: ReprComb) a. Comb Alternable repr a
Empty

  p :: SomeComb repr a
p@(Comb Pure{}) <|> :: forall a. SomeComb repr a -> SomeComb repr a -> SomeComb repr a
<|> SomeComb repr a
_ = SomeComb repr a
p
    -- & trace "Left Catch Law"
  Comb Comb Alternable repr a
R:CombAlternablerepra repr a
Empty <|> SomeComb repr a
u = SomeComb repr a
u
    -- & trace "Left Neutral Law"
  SomeComb repr a
u <|> Comb Comb Alternable repr a
R:CombAlternablerepra repr a
Empty = SomeComb repr a
u
    -- & trace "Right Neutral Law"
  Comb (SomeComb repr a
u :<|>: SomeComb repr a
v) <|> SomeComb repr a
w = SomeComb repr a
u SomeComb repr a -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a.
Alternable repr =>
repr a -> repr a -> repr a
<|> (SomeComb repr a
v SomeComb repr a -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a.
Alternable repr =>
repr a -> repr a -> repr a
<|> SomeComb repr a
w)
    -- & trace "Associativity Law"
  Comb (Look SomeComb repr a
p) <|> Comb (Look SomeComb repr a
q) = SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr a
look (SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a. Alternable repr => repr a -> repr a
try SomeComb repr a
p SomeComb repr a -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a.
Alternable repr =>
repr a -> repr a -> repr a
<|> SomeComb repr a
q)
    -- & trace "Distributivity Law"
  SomeComb repr a
x <|> SomeComb repr a
y = Comb Alternable repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr a
x SomeComb repr a -> SomeComb repr a -> Comb Alternable repr a
forall (repr :: ReprComb) a.
SomeComb repr a -> SomeComb repr a -> Comb Alternable repr a
:<|>: SomeComb repr a
y)

  try :: forall a. SomeComb repr a -> SomeComb repr a
try (Comb (SomeComb repr a
p :$>: TermGrammar a
x)) = SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a. Alternable repr => repr a -> repr a
try SomeComb repr a
p SomeComb repr a -> TermGrammar a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> TermGrammar b -> repr b
$> TermGrammar a
x
    -- & trace "Try Interchange Law"
  try (Comb (TermGrammar (a -> a)
f :<$>: SomeComb repr a
p)) = TermGrammar (a -> a)
f TermGrammar (a -> a) -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a. Alternable repr => repr a -> repr a
try SomeComb repr a
p
    -- & trace "Try Interchange Law"
  try SomeComb repr a
x = Comb Alternable repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr a -> Comb Alternable repr a
forall (repr :: ReprComb) a.
SomeComb repr a -> Comb Alternable repr a
Try SomeComb repr a
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 :: forall a. Comb Selectable repr a -> repr a
trans = \case
    Branch SomeComb repr (Either a b)
lr SomeComb repr (a -> a)
l SomeComb repr (b -> a)
r -> repr (Either a b) -> repr (a -> a) -> repr (b -> a) -> repr a
forall (repr :: ReprComb) a b c.
Selectable repr =>
repr (Either a b) -> repr (a -> c) -> repr (b -> c) -> repr c
branch (SomeComb repr (Either a b) -> repr (Either a b)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr (Either a b)
lr) (SomeComb repr (a -> a) -> repr (a -> a)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr (a -> a)
l) (SomeComb repr (b -> a) -> repr (b -> a)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr (b -> a)
r)
instance
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Selectable (SomeComb repr) where
  branch :: forall a b c.
SomeComb repr (Either a b)
-> SomeComb repr (a -> c)
-> SomeComb repr (b -> c)
-> SomeComb repr c
branch (Comb Comb Alternable repr (Either a b)
R:CombAlternablerepra repr (Either a b)
Empty) SomeComb repr (a -> c)
_ SomeComb repr (b -> c)
_ = SomeComb repr c
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    -- & trace "Branch Absorption Law"
  branch SomeComb repr (Either a b)
b (Comb Comb Alternable repr (a -> c)
R:CombAlternablerepra repr (a -> c)
Empty) (Comb Comb Alternable repr (b -> c)
R:CombAlternablerepra repr (b -> c)
Empty) = SomeComb repr (Either a b)
b SomeComb repr (Either a b) -> SomeComb repr c -> SomeComb repr c
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr c
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    -- & trace "Branch Weakening Law"
  branch (Comb (Pure (TermGrammar (Either a b) -> ValueCode (Either a b)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans -> ValueCode (Either a b)
lr))) SomeComb repr (a -> c)
l SomeComb repr (b -> c)
r =
    case ValueCode (Either a b) -> Either a b
forall a. ValueCode a -> a
H.value ValueCode (Either a b)
lr of
      Left a
value -> SomeComb repr (a -> c)
l SomeComb repr (a -> c) -> SomeComb repr a -> SomeComb repr c
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> TermGrammar a -> SomeComb repr a
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure (ValueCode a -> TermGrammar a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans ValueCode :: forall a. a -> CodeQ a -> ValueCode a
H.ValueCode{a
Code Q a
code :: Code Q a
code :: Code Q a
value :: a
value :: a
..})
        where code :: Code Q a
code = [|| case $$(H.code lr) of Left x -> x ||]
      Right b
value -> SomeComb repr (b -> c)
r SomeComb repr (b -> c) -> SomeComb repr b -> SomeComb repr c
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> TermGrammar b -> SomeComb repr b
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure (ValueCode b -> TermGrammar b
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans ValueCode :: forall a. a -> CodeQ a -> ValueCode a
H.ValueCode{b
Code Q b
code :: Code Q b
value :: b
code :: Code Q b
value :: b
..})
        where code :: Code Q b
code = [|| case $$(H.code lr) of Right x -> x ||]
    -- & trace "Branch Pure Left/Right Law" $
  branch SomeComb repr (Either a b)
b (Comb (Pure (TermGrammar (a -> c) -> ValueCode (a -> c)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans -> ValueCode (a -> c)
l))) (Comb (Pure (TermGrammar (b -> c) -> ValueCode (b -> c)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans -> ValueCode (b -> c)
r))) =
    ValueCode (Either a b -> c) -> Term ValueCode (Either a b -> c)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans ValueCode :: forall a. a -> CodeQ a -> ValueCode a
H.ValueCode{Code Q (Either a b -> c)
Either a b -> c
code :: Code Q (Either a b -> c)
value :: Either a b -> c
code :: Code Q (Either a b -> c)
value :: Either a b -> c
..} Term ValueCode (Either a b -> c)
-> SomeComb repr (Either a b) -> SomeComb repr c
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr (Either a b)
b
    -- & trace "Branch Generalised Identity Law"
    where
    value :: Either a b -> c
value = (a -> c) -> (b -> c) -> Either a b -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ValueCode (a -> c) -> a -> c
forall a. ValueCode a -> a
H.value ValueCode (a -> c)
l) (ValueCode (b -> c) -> b -> c
forall a. ValueCode a -> a
H.value ValueCode (b -> c)
r)
    code :: Code Q (Either a b -> c)
code = [|| either $$(H.code l) $$(H.code r) ||]
  branch (Comb (SomeComb repr a
x :*>: SomeComb repr (Either a b)
y)) SomeComb repr (a -> c)
p SomeComb repr (b -> c)
q = SomeComb repr a
x SomeComb repr a -> SomeComb repr c -> SomeComb repr c
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr (Either a b)
-> SomeComb repr (a -> c)
-> SomeComb repr (b -> c)
-> SomeComb repr c
forall (repr :: ReprComb) a b c.
Selectable repr =>
repr (Either a b) -> repr (a -> c) -> repr (b -> c) -> repr c
branch SomeComb repr (Either a b)
y SomeComb repr (a -> c)
p SomeComb repr (b -> c)
q
    -- & trace "Interchange Law"
  branch SomeComb repr (Either a b)
b SomeComb repr (a -> c)
l (Comb Comb Alternable repr (b -> c)
R:CombAlternablerepra repr (b -> c)
Empty) =
    SomeComb repr (Either b a)
-> SomeComb repr (b -> c)
-> SomeComb repr (a -> c)
-> SomeComb repr c
forall (repr :: ReprComb) a b c.
Selectable repr =>
repr (Either a b) -> repr (a -> c) -> repr (b -> c) -> repr c
branch (TermGrammar (Either a b -> Either b a)
-> SomeComb repr (Either a b -> Either b a)
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure (ValueCode (Either a b -> Either b a)
-> TermGrammar (Either a b -> Either b a)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans (ValueCode :: forall a. a -> CodeQ a -> ValueCode a
H.ValueCode{Code Q (Either a b -> Either b a)
Either a b -> Either b a
forall {a} {a}. Code Q (Either a a -> Either a a)
forall {a} {a}. Either a a -> Either a a
code :: forall {a} {a}. Code Q (Either a a -> Either a a)
value :: forall {a} {a}. Either a a -> Either a a
code :: Code Q (Either a b -> Either b a)
value :: Either a b -> Either b a
..})) SomeComb repr (Either a b -> Either b a)
-> SomeComb repr (Either a b) -> SomeComb repr (Either b a)
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> SomeComb repr (Either a b)
b) SomeComb repr (b -> c)
forall (repr :: ReprComb) a. Alternable repr => repr a
empty SomeComb repr (a -> c)
l
    -- & trace "Negated Branch Law"
    where
    value :: Either a a -> Either a a
value = (a -> Either a a) -> (a -> Either a a) -> Either a a -> Either a a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Either a a
forall a b. b -> Either a b
Right a -> Either a a
forall a b. a -> Either a b
Left
    code :: Code Q (Either a a -> Either a a)
code = [||either Right Left||]
  branch (Comb (Branch SomeComb repr (Either a b)
b (Comb Comb Alternable repr (a -> Either a b)
R:CombAlternablerepra repr (a -> Either a b)
Empty) (Comb (Pure (TermGrammar (b -> Either a b) -> ValueCode (b -> Either a b)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans -> ValueCode (b -> Either a b)
lr))))) (Comb Comb Alternable repr (a -> c)
R:CombAlternablerepra repr (a -> c)
Empty) SomeComb repr (b -> c)
br =
    SomeComb repr (Either () b)
-> SomeComb repr (() -> c)
-> SomeComb repr (b -> c)
-> SomeComb repr c
forall (repr :: ReprComb) a b c.
Selectable repr =>
repr (Either a b) -> repr (a -> c) -> repr (b -> c) -> repr c
branch (TermGrammar (Either a b -> Either () b)
-> SomeComb repr (Either a b -> Either () b)
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure (ValueCode (Either a b -> Either () b)
-> TermGrammar (Either a b -> Either () b)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans ValueCode :: forall a. a -> CodeQ a -> ValueCode a
H.ValueCode{Code Q (Either a b -> Either () b)
Either a b -> Either () b
code :: Code Q (Either a b -> Either () b)
value :: Either a b -> Either () b
code :: Code Q (Either a b -> Either () b)
value :: Either a b -> Either () b
..}) SomeComb repr (Either a b -> Either () b)
-> SomeComb repr (Either a b) -> SomeComb repr (Either () b)
forall (repr :: ReprComb) a b.
Applicable repr =>
repr (a -> b) -> repr a -> repr b
<*> SomeComb repr (Either a b)
b) SomeComb repr (() -> c)
forall (repr :: ReprComb) a. Alternable repr => repr a
empty SomeComb repr (b -> c)
br
    -- & trace "Branch Fusion Law"
    where
    value :: Either a b -> Either () b
value Left{} = () -> Either () b
forall a b. a -> Either a b
Left ()
    value (Right b
r) = case ValueCode (b -> Either a b) -> b -> Either a b
forall a. ValueCode a -> a
H.value ValueCode (b -> Either a b)
lr b
r of
                        Left a
_ -> () -> Either () b
forall a b. a -> Either a b
Left ()
                        Right b
rr -> b -> Either () b
forall a b. b -> Either a b
Right b
rr
    code :: Code Q (Either a b -> Either () b)
code = [|| \case Left{} -> Left ()
                     Right r -> case $$(H.code lr) r of
                                  Left _ -> Left ()
                                  Right rr -> Right rr ||]
  branch SomeComb repr (Either a b)
b SomeComb repr (a -> c)
l SomeComb repr (b -> c)
r = Comb Selectable repr c -> SomeComb repr c
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr (Either a b)
-> SomeComb repr (a -> c)
-> SomeComb repr (b -> c)
-> Comb Selectable repr c
forall (repr :: ReprComb) a b c.
SomeComb repr (Either a b)
-> SomeComb repr (a -> c)
-> SomeComb repr (b -> c)
-> Comb Selectable repr c
Branch SomeComb repr (Either a b)
b SomeComb repr (a -> c)
l SomeComb repr (b -> c)
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 :: forall a. Comb Matchable repr a -> repr a
trans = \case
    Conditional SomeComb repr a
a [TermGrammar (a -> Bool)]
ps [SomeComb repr a]
bs SomeComb repr a
b -> repr a -> [TermGrammar (a -> Bool)] -> [repr a] -> repr a -> repr a
forall (repr :: ReprComb) a b.
(Matchable repr, Eq a) =>
repr a -> [TermGrammar (a -> Bool)] -> [repr b] -> repr b -> repr b
conditional (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
a) [TermGrammar (a -> Bool)]
ps (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans (SomeComb repr a -> repr a) -> [SomeComb repr a] -> [repr a]
forall (f :: ReprComb) a b. Functor f => (a -> b) -> f a -> f b
Functor.<$> [SomeComb repr a]
bs) (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
b)
instance
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Matchable (SomeComb repr) where
  conditional :: forall a b.
Eq a =>
SomeComb repr a
-> [TermGrammar (a -> Bool)]
-> [SomeComb repr b]
-> SomeComb repr b
-> SomeComb repr b
conditional (Comb Comb Alternable repr a
R:CombAlternablerepra repr a
Empty) [TermGrammar (a -> Bool)]
_ [SomeComb repr b]
_ SomeComb repr b
d = SomeComb repr b
d
    -- & trace "Conditional Absorption Law"
  conditional SomeComb repr a
p [TermGrammar (a -> Bool)]
_ [SomeComb repr b]
qs (Comb Comb Alternable repr b
R:CombAlternablerepra repr b
Empty)
    | (SomeComb repr b -> Bool) -> [SomeComb repr b] -> Bool
forall (t :: ReprComb) a. Foldable t => (a -> Bool) -> t a -> Bool
Foldable.all (\case { Comb Comb Alternable repr b
R:CombAlternablerepra repr b
Empty -> Bool
True; SomeComb repr b
_ -> Bool
False }) [SomeComb repr b]
qs = SomeComb repr a
p SomeComb repr a -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr b
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
      -- & trace "Conditional Weakening Law"
  conditional SomeComb repr a
a [TermGrammar (a -> Bool)]
_ps [SomeComb repr b]
bs (Comb Comb Alternable repr b
R:CombAlternablerepra repr b
Empty)
    | (SomeComb repr b -> Bool) -> [SomeComb repr b] -> Bool
forall (t :: ReprComb) a. Foldable t => (a -> Bool) -> t a -> Bool
Foldable.all (\case { Comb Comb Alternable repr b
R:CombAlternablerepra repr b
Empty -> Bool
True; SomeComb repr b
_ -> Bool
False }) [SomeComb repr b]
bs = SomeComb repr a
a SomeComb repr a -> SomeComb repr b -> SomeComb repr b
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr b
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
      -- & trace "Conditional Weakening Law"
  conditional (Comb (Pure (TermGrammar a -> ValueCode a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans -> ValueCode a
a))) [TermGrammar (a -> Bool)]
ps [SomeComb repr b]
bs SomeComb repr b
d =
    ((TermGrammar (a -> Bool), SomeComb repr b)
 -> SomeComb repr b -> SomeComb repr b)
-> SomeComb repr b
-> [(TermGrammar (a -> Bool), SomeComb repr b)]
-> SomeComb repr b
forall (t :: ReprComb) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Foldable.foldr (\(TermGrammar (a -> Bool) -> ValueCode (a -> Bool)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans -> ValueCode (a -> Bool)
p, SomeComb repr b
b) SomeComb repr b
next ->
      if ValueCode (a -> Bool) -> a -> Bool
forall a. ValueCode a -> a
H.value ValueCode (a -> Bool)
p (ValueCode a -> a
forall a. ValueCode a -> a
H.value ValueCode a
a) then SomeComb repr b
b else SomeComb repr b
next
    ) SomeComb repr b
d ([TermGrammar (a -> Bool)]
-> [SomeComb repr b]
-> [(TermGrammar (a -> Bool), SomeComb repr b)]
forall a b. [a] -> [b] -> [(a, b)]
List.zip [TermGrammar (a -> Bool)]
ps [SomeComb repr b]
bs)
    -- & trace "Conditional Pure Law"
  conditional SomeComb repr a
a [TermGrammar (a -> Bool)]
ps [SomeComb repr b]
bs SomeComb repr b
d = Comb Matchable repr b -> SomeComb repr b
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr a
-> [TermGrammar (a -> Bool)]
-> [SomeComb repr b]
-> SomeComb repr b
-> Comb Matchable repr b
forall a (repr :: ReprComb) b.
Eq a =>
SomeComb repr a
-> [TermGrammar (a -> Bool)]
-> [SomeComb repr b]
-> SomeComb repr b
-> Comb Matchable repr b
Conditional SomeComb repr a
a [TermGrammar (a -> Bool)]
ps [SomeComb repr b]
bs SomeComb repr b
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 :: forall a. Comb Foldable repr a -> repr a
trans = \case
    ChainPreC SomeComb repr (a -> a)
x SomeComb repr a
y -> repr (a -> a) -> repr a -> repr a
forall (repr :: ReprComb) a.
Foldable repr =>
repr (a -> a) -> repr a -> repr a
chainPre (SomeComb repr (a -> a) -> repr (a -> a)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr (a -> a)
x) (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
y)
    ChainPostC SomeComb repr a
x SomeComb repr (a -> a)
y -> repr a -> repr (a -> a) -> repr a
forall (repr :: ReprComb) a.
Foldable repr =>
repr a -> repr (a -> a) -> repr a
chainPost (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
x) (SomeComb repr (a -> a) -> repr (a -> a)
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr (a -> a)
y)
instance Foldable repr => Foldable (SomeComb repr) where
  chainPre :: forall a.
SomeComb repr (a -> a) -> SomeComb repr a -> SomeComb repr a
chainPre SomeComb repr (a -> a)
x = Comb Foldable repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (Comb Foldable repr a -> SomeComb repr a)
-> (SomeComb repr a -> Comb Foldable repr a)
-> SomeComb repr a
-> SomeComb repr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeComb repr (a -> a) -> SomeComb repr a -> Comb Foldable repr a
forall (repr :: ReprComb) a.
SomeComb repr (a -> a) -> SomeComb repr a -> Comb Foldable repr a
ChainPreC SomeComb repr (a -> a)
x
  chainPost :: forall a.
SomeComb repr a -> SomeComb repr (a -> a) -> SomeComb repr a
chainPost SomeComb repr a
x = Comb Foldable repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (Comb Foldable repr a -> SomeComb repr a)
-> (SomeComb repr (a -> a) -> Comb Foldable repr a)
-> SomeComb repr (a -> a)
-> SomeComb repr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeComb repr a -> SomeComb repr (a -> a) -> Comb Foldable repr a
forall (repr :: ReprComb) a.
SomeComb repr a -> SomeComb repr (a -> a) -> Comb Foldable repr a
ChainPostC SomeComb repr a
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 :: forall a. Comb Lookable repr a -> repr a
trans = \case
    Look SomeComb repr a
x -> repr a -> repr a
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr a
look (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
x)
    NegLook SomeComb repr a
x -> repr a -> repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr ()
negLook (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
x)
    Comb Lookable repr a
R:CombLookablerepra repr a
Eof -> repr a
forall (repr :: ReprComb). Lookable repr => repr ()
eof
instance
  ( Alternable repr
  , Applicable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Lookable (SomeComb repr) where
  look :: forall a. SomeComb repr a -> SomeComb repr a
look p :: SomeComb repr a
p@(Comb Pure{}) = SomeComb repr a
p
    -- & trace "Pure Look Law"
  look p :: SomeComb repr a
p@(Comb Comb Alternable repr a
R:CombAlternablerepra repr a
Empty) = SomeComb repr a
p
    -- & trace "Dead Look Law"
  look (Comb (Look SomeComb repr a
x)) = SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr a
look SomeComb repr a
x
    -- & trace "Idempotence Law"
  look (Comb (NegLook SomeComb repr a
x)) = SomeComb repr a -> SomeComb repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr ()
negLook SomeComb repr a
x
    -- & trace "Left Identity Law"
  look (Comb (SomeComb repr a
p :$>: TermGrammar a
x)) = SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr a
look SomeComb repr a
p SomeComb repr a -> TermGrammar a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> TermGrammar b -> repr b
$> TermGrammar a
x
    -- & trace "Interchange Law"
  look (Comb (TermGrammar (a -> a)
f :<$>: SomeComb repr a
p)) = TermGrammar (a -> a)
f TermGrammar (a -> a) -> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a b.
Applicable repr =>
TermGrammar (a -> b) -> repr a -> repr b
<$> SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr a
look SomeComb repr a
p
    -- & trace "Interchange Law"
  look SomeComb repr a
x = Comb Lookable repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr a -> Comb Lookable repr a
forall (repr :: ReprComb) a.
SomeComb repr a -> Comb Lookable repr a
Look SomeComb repr a
x)

  negLook :: forall a. SomeComb repr a -> SomeComb repr ()
negLook (Comb Pure{}) = SomeComb repr ()
forall (repr :: ReprComb) a. Alternable repr => repr a
empty
    -- & trace "Pure Negative-Look"
  negLook (Comb Comb Alternable repr a
R:CombAlternablerepra repr a
Empty) = TermGrammar () -> SomeComb repr ()
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure TermGrammar ()
forall (repr :: ReprComb). Termable repr => repr ()
H.unit
    -- & trace "Dead Negative-Look"
  negLook (Comb (NegLook SomeComb repr a
x)) = SomeComb repr () -> SomeComb repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr a
look (SomeComb repr a -> SomeComb repr a
forall (repr :: ReprComb) a. Alternable repr => repr a -> repr a
try SomeComb repr a
x SomeComb repr a -> SomeComb repr () -> SomeComb repr ()
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> TermGrammar () -> SomeComb repr ()
forall (repr :: ReprComb) a.
Applicable repr =>
TermGrammar a -> repr a
pure TermGrammar ()
forall (repr :: ReprComb). Termable repr => repr ()
H.unit)
    -- & trace "Double Negation Law"
  negLook (Comb (Try SomeComb repr a
x)) = SomeComb repr a -> SomeComb repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr ()
negLook SomeComb repr a
x
    -- & trace "Zero Consumption Law"
  negLook (Comb (Look SomeComb repr a
x)) = SomeComb repr a -> SomeComb repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr ()
negLook SomeComb repr a
x
    -- & trace "Right Identity Law"
  negLook (Comb (Comb (Try SomeComb repr a
p) :<|>: SomeComb repr a
q)) = SomeComb repr a -> SomeComb repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr ()
negLook SomeComb repr a
p SomeComb repr () -> SomeComb repr () -> SomeComb repr ()
forall (repr :: ReprComb) a b.
Applicable repr =>
repr a -> repr b -> repr b
*> SomeComb repr a -> SomeComb repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr ()
negLook SomeComb repr a
q
    -- & trace "Transparency Law"
  negLook (Comb (SomeComb repr a
p :$>: TermGrammar a
_)) = SomeComb repr a -> SomeComb repr ()
forall (repr :: ReprComb) a. Lookable repr => repr a -> repr ()
negLook SomeComb repr a
p
    -- & trace "NegLook Idempotence Law"
  negLook SomeComb repr a
x = Comb Lookable repr () -> SomeComb repr ()
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (SomeComb repr a -> Comb Lookable repr ()
forall (repr :: ReprComb) a.
SomeComb repr a -> Comb Lookable repr ()
NegLook SomeComb repr a
x)

  eof :: SomeComb repr ()
eof = Comb Lookable repr () -> SomeComb repr ()
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb Comb Lookable repr ()
forall (repr :: ReprComb). Comb Lookable repr ()
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 :: forall a. Comb (Satisfiable tok) repr a -> repr a
trans = \case
    Satisfy [ErrorItem tok]
es TermGrammar (tok -> Bool)
p -> [ErrorItem tok] -> TermGrammar (tok -> Bool) -> repr tok
forall tok (repr :: ReprComb).
Satisfiable tok repr =>
[ErrorItem tok] -> TermGrammar (tok -> Bool) -> repr tok
satisfy [ErrorItem tok]
es TermGrammar (tok -> Bool)
p
    Comb (Satisfiable tok) repr a
R:CombSatisfiablerepra tok repr a
Item -> repr a
forall tok (repr :: ReprComb). Satisfiable tok repr => repr tok
item
instance
  (Satisfiable tok repr, Typeable tok) =>
  Satisfiable tok (SomeComb repr) where
  satisfy :: [ErrorItem tok] -> TermGrammar (tok -> Bool) -> SomeComb repr tok
satisfy [ErrorItem tok]
es = Comb (Satisfiable tok) repr tok -> SomeComb repr tok
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (Comb (Satisfiable tok) repr tok -> SomeComb repr tok)
-> (TermGrammar (tok -> Bool) -> Comb (Satisfiable tok) repr tok)
-> TermGrammar (tok -> Bool)
-> SomeComb repr tok
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ErrorItem tok]
-> TermGrammar (tok -> Bool) -> Comb (Satisfiable tok) repr tok
forall tok (repr :: ReprComb).
Satisfiable tok repr =>
[ErrorItem tok]
-> TermGrammar (tok -> Bool) -> Comb (Satisfiable tok) repr tok
Satisfy [ErrorItem tok]
es
  item :: SomeComb repr tok
item = Comb (Satisfiable tok) repr tok -> SomeComb repr tok
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb Comb (Satisfiable tok) repr tok
forall tok (repr :: ReprComb).
Satisfiable tok repr =>
Comb (Satisfiable tok) repr tok
Item

-- Letable
data instance Comb (Letable letName) repr a where
  Def :: 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 :: forall a. Comb (Letable letName) repr a -> repr a
trans = \case
    Def letName
n SomeComb repr a
v -> letName -> repr a -> repr a
forall letName (repr :: ReprComb) a.
Letable letName repr =>
letName -> repr a -> repr a
def letName
n (SomeComb repr a -> repr a
forall (from :: ReprComb) (to :: ReprComb) a.
Trans from to =>
from a -> to a
trans SomeComb repr a
v)
    Ref Bool
isRec letName
n -> Bool -> letName -> repr a
forall letName (repr :: ReprComb) a.
Letable letName repr =>
Bool -> letName -> repr a
ref Bool
isRec letName
n
instance
  (Letable letName repr, Typeable letName) =>
  Letable letName (SomeComb repr) where
  def :: forall a. letName -> SomeComb repr a -> SomeComb repr a
def letName
n = Comb (Letable letName) repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (Comb (Letable letName) repr a -> SomeComb repr a)
-> (SomeComb repr a -> Comb (Letable letName) repr a)
-> SomeComb repr a
-> SomeComb repr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. letName -> SomeComb repr a -> Comb (Letable letName) repr a
forall letName (repr :: ReprComb) a.
letName -> SomeComb repr a -> Comb (Letable letName) repr a
Def letName
n
  ref :: forall a. Bool -> letName -> SomeComb repr a
ref Bool
isRec = Comb (Letable letName) repr a -> SomeComb repr a
forall (repr :: ReprComb) a (comb :: ReprComb -> Constraint).
(Trans (Comb comb repr) repr, Typeable comb) =>
Comb comb repr a -> SomeComb repr a
SomeComb (Comb (Letable letName) repr a -> SomeComb repr a)
-> (letName -> Comb (Letable letName) repr a)
-> letName
-> SomeComb repr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> letName -> Comb (Letable letName) repr a
forall letName (repr :: ReprComb) a.
Bool -> letName -> Comb (Letable letName) repr a
Ref Bool
isRec
instance MakeLetName TH.Name where
  makeLetName :: SharingName -> IO Name
makeLetName SharingName
_ = String -> IO Name
forall (m :: ReprComb). Quasi m => String -> m Name
TH.qNewName String
"name"