{-# LANGUAGE DerivingStrategies #-}
module Parsley.Internal.Frontend.CombinatorAnalyser (analyse, compliance, Compliance(..), emptyFlags, AnalysisFlags(..)) where

--import Control.Applicative                 (liftA2)
--import Control.Monad.Reader                (ReaderT, ask, runReaderT, local)
--import Control.Monad.State.Strict          (State, get, put, evalState)
import Data.Coerce                         (coerce)
import Data.Kind                           (Type)
--import Data.Map.Strict                     (Map)
--import Data.Set                            (Set)
import Parsley.Internal.Common.Indexed     (Fix(..){-, imap, cata-}, zygo, (:*:)(..), ifst)
import Parsley.Internal.Core.CombinatorAST (Combinator(..), MetaCombinator(..))
--import Parsley.Internal.Core.Identifiers   (IMVar, MVar(..))

--import qualified Data.Map.Strict as Map
--import qualified Data.Set        as Set

newtype AnalysisFlags = AnalysisFlags {
  AnalysisFlags -> Bool
letBound :: Bool
}
emptyFlags :: AnalysisFlags
emptyFlags :: AnalysisFlags
emptyFlags = Bool -> AnalysisFlags
AnalysisFlags Bool
False

analyse :: AnalysisFlags -> Fix Combinator a -> Fix Combinator a
analyse :: AnalysisFlags -> Fix Combinator a -> Fix Combinator a
analyse AnalysisFlags
flags = Bool -> Fix Combinator a -> Fix Combinator a
forall a. Bool -> Fix Combinator a -> Fix Combinator a
cutAnalysis (AnalysisFlags -> Bool
letBound AnalysisFlags
flags) {-. terminationAnalysis-}

data Compliance (k :: Type) = DomComp | NonComp | Comp | FullPure deriving stock (Int -> Compliance k -> ShowS
[Compliance k] -> ShowS
Compliance k -> String
(Int -> Compliance k -> ShowS)
-> (Compliance k -> String)
-> ([Compliance k] -> ShowS)
-> Show (Compliance k)
forall k. Int -> Compliance k -> ShowS
forall k. [Compliance k] -> ShowS
forall k. Compliance k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Compliance k] -> ShowS
$cshowList :: forall k. [Compliance k] -> ShowS
show :: Compliance k -> String
$cshow :: forall k. Compliance k -> String
showsPrec :: Int -> Compliance k -> ShowS
$cshowsPrec :: forall k. Int -> Compliance k -> ShowS
Show, Compliance k -> Compliance k -> Bool
(Compliance k -> Compliance k -> Bool)
-> (Compliance k -> Compliance k -> Bool) -> Eq (Compliance k)
forall k. Compliance k -> Compliance k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Compliance k -> Compliance k -> Bool
$c/= :: forall k. Compliance k -> Compliance k -> Bool
== :: Compliance k -> Compliance k -> Bool
$c== :: forall k. Compliance k -> Compliance k -> Bool
Eq)

seqCompliance :: Compliance a -> Compliance b -> Compliance c
seqCompliance :: Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance a
c Compliance b
FullPure = Compliance a -> Compliance c
coerce Compliance a
c
seqCompliance Compliance a
FullPure Compliance b
c = Compliance b -> Compliance c
coerce Compliance b
c
seqCompliance Compliance a
Comp Compliance b
_     = Compliance c
forall k. Compliance k
Comp
seqCompliance Compliance a
_ Compliance b
_        = Compliance c
forall k. Compliance k
NonComp

caseCompliance :: Compliance a -> Compliance b -> Compliance c
caseCompliance :: Compliance a -> Compliance b -> Compliance c
caseCompliance Compliance a
c Compliance b
FullPure              = Compliance a -> Compliance c
coerce Compliance a
c
caseCompliance Compliance a
FullPure Compliance b
c              = Compliance b -> Compliance c
coerce Compliance b
c
caseCompliance Compliance a
c1 Compliance b
c2 | Compliance a
c1 Compliance a -> Compliance a -> Bool
forall a. Eq a => a -> a -> Bool
== Compliance b -> Compliance a
coerce Compliance b
c2 = Compliance a -> Compliance c
coerce Compliance a
c1
caseCompliance Compliance a
_ Compliance b
_                     = Compliance c
forall k. Compliance k
NonComp

{-# INLINE compliance #-}
compliance :: Combinator Compliance a -> Compliance a
compliance :: Combinator Compliance a -> Compliance a
compliance (Pure Defunc a
_)                 = Compliance a
forall k. Compliance k
FullPure
compliance (Satisfy Defunc (Char -> Bool)
_)              = Compliance a
forall k. Compliance k
NonComp
compliance Combinator Compliance a
Empty                    = Compliance a
forall k. Compliance k
FullPure
compliance Let{}                    = Compliance a
forall k. Compliance k
DomComp
compliance (Try Compliance a
_)                  = Compliance a
forall k. Compliance k
DomComp
compliance (Compliance a
NonComp :<|>: Compliance a
FullPure) = Compliance a
forall k. Compliance k
Comp
compliance (Compliance a
_ :<|>: Compliance a
_)              = Compliance a
forall k. Compliance k
NonComp
compliance (Compliance (a -> a)
l :<*>: Compliance a
r)              = Compliance (a -> a) -> Compliance a -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance (a -> a)
l Compliance a
r
compliance (Compliance a
l :<*: Compliance b
r)               = Compliance a -> Compliance b -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance a
l Compliance b
r
compliance (Compliance a
l :*>: Compliance a
r)               = Compliance a -> Compliance a -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance a
l Compliance a
r
compliance (LookAhead Compliance a
c)            = Compliance a
c -- Lookahead will consume input on failure, so its compliance matches that which is beneath it
compliance (NotFollowedBy Compliance a
_)        = Compliance a
forall k. Compliance k
FullPure
compliance (Debug String
_ Compliance a
c)              = Compliance a
c
compliance (ChainPre Compliance (a -> a)
NonComp Compliance a
p)     = Compliance Any -> Compliance a -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance Any
forall k. Compliance k
Comp Compliance a
p
compliance (ChainPre Compliance (a -> a)
_ Compliance a
p)           = Compliance Any -> Compliance a -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance Any
forall k. Compliance k
NonComp Compliance a
p
compliance (ChainPost Compliance a
p Compliance (a -> a)
NonComp)    = Compliance a -> Compliance Any -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance a
p Compliance Any
forall k. Compliance k
Comp
compliance (ChainPost Compliance a
p Compliance (a -> a)
_)          = Compliance a -> Compliance Any -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance a
p Compliance Any
forall k. Compliance k
NonComp
compliance (Branch Compliance (Either a b)
b Compliance (a -> a)
p Compliance (b -> a)
q)           = Compliance (Either a b) -> Compliance Any -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance (Either a b)
b (Compliance (a -> a) -> Compliance (b -> a) -> Compliance Any
forall a b c. Compliance a -> Compliance b -> Compliance c
caseCompliance Compliance (a -> a)
p Compliance (b -> a)
q)
compliance (Match Compliance a
p [Defunc (a -> Bool)]
_ [Compliance a]
qs Compliance a
def)       = Compliance a -> Compliance a -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance a
p ((Compliance a -> Compliance a -> Compliance a)
-> [Compliance a] -> Compliance a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1 Compliance a -> Compliance a -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
caseCompliance (Compliance a
defCompliance a -> [Compliance a] -> [Compliance a]
forall a. a -> [a] -> [a]
:[Compliance a]
qs))
compliance (MakeRegister ΣVar a
_ Compliance a
l Compliance a
r)     = Compliance a -> Compliance a -> Compliance a
forall a b c. Compliance a -> Compliance b -> Compliance c
seqCompliance Compliance a
l Compliance a
r
compliance (GetRegister ΣVar a
_)          = Compliance a
forall k. Compliance k
FullPure
compliance (PutRegister ΣVar a
_ Compliance a
c)        = Compliance a -> Compliance a
coerce Compliance a
c
compliance (MetaCombinator MetaCombinator
_ Compliance a
c)     = Compliance a
c

newtype CutAnalysis a = CutAnalysis {CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut :: Bool -> (Fix Combinator a, Bool)}

biliftA2 :: (a -> b -> c) -> (x -> y -> z) -> (a, x) -> (b, y) -> (c, z)
biliftA2 :: (a -> b -> c) -> (x -> y -> z) -> (a, x) -> (b, y) -> (c, z)
biliftA2 a -> b -> c
f x -> y -> z
g (a
x1, x
y1) (b
x2, y
y2) = (a -> b -> c
f a
x1 b
x2, x -> y -> z
g x
y1 y
y2)

cutAnalysis :: Bool -> Fix Combinator a -> Fix Combinator a
cutAnalysis :: Bool -> Fix Combinator a -> Fix Combinator a
cutAnalysis Bool
letBound = (Fix Combinator a, Bool) -> Fix Combinator a
forall a b. (a, b) -> a
fst ((Fix Combinator a, Bool) -> Fix Combinator a)
-> (Fix Combinator a -> (Fix Combinator a, Bool))
-> Fix Combinator a
-> Fix Combinator a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Bool -> (Fix Combinator a, Bool))
-> Bool -> (Fix Combinator a, Bool)
forall a b. (a -> b) -> a -> b
$ Bool
letBound) ((Bool -> (Fix Combinator a, Bool)) -> (Fix Combinator a, Bool))
-> (Fix Combinator a -> Bool -> (Fix Combinator a, Bool))
-> Fix Combinator a
-> (Fix Combinator a, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut (CutAnalysis a -> Bool -> (Fix Combinator a, Bool))
-> (Fix Combinator a -> CutAnalysis a)
-> Fix Combinator a
-> Bool
-> (Fix Combinator a, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall j.
 Combinator (CutAnalysis :*: Compliance) j -> CutAnalysis j)
-> (forall j. Combinator Compliance j -> Compliance j)
-> Fix Combinator a
-> CutAnalysis a
forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. f (a :*: b) j -> a j)
-> (forall j. f b j -> b j) -> Fix f i -> a i
zygo ((Bool -> (Fix Combinator j, Bool)) -> CutAnalysis j
forall a. (Bool -> (Fix Combinator a, Bool)) -> CutAnalysis a
CutAnalysis ((Bool -> (Fix Combinator j, Bool)) -> CutAnalysis j)
-> (Combinator (CutAnalysis :*: Compliance) j
    -> Bool -> (Fix Combinator j, Bool))
-> Combinator (CutAnalysis :*: Compliance) j
-> CutAnalysis j
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Combinator (CutAnalysis :*: Compliance) j
-> Bool -> (Fix Combinator j, Bool)
forall a.
Combinator (CutAnalysis :*: Compliance) a
-> Bool -> (Fix Combinator a, Bool)
alg) forall j. Combinator Compliance j -> Compliance j
compliance
  where
    mkCut :: Bool -> Fix Combinator a -> Fix Combinator a
mkCut Bool
True = Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Combinator (Fix Combinator) a -> Fix Combinator a)
-> (Fix Combinator a -> Combinator (Fix Combinator) a)
-> Fix Combinator a
-> Fix Combinator a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaCombinator -> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a.
MetaCombinator -> k a -> Combinator k a
MetaCombinator MetaCombinator
Cut
    mkCut Bool
False = Fix Combinator a -> Fix Combinator a
forall a. a -> a
id

    requiresCut :: Fix Combinator a -> Fix Combinator a
requiresCut = Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Combinator (Fix Combinator) a -> Fix Combinator a)
-> (Fix Combinator a -> Combinator (Fix Combinator) a)
-> Fix Combinator a
-> Fix Combinator a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaCombinator -> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a.
MetaCombinator -> k a -> Combinator k a
MetaCombinator MetaCombinator
RequiresCut

    seqAlg :: (Fix Combinator a -> Fix Combinator b -> Combinator (Fix Combinator) c) -> Bool -> CutAnalysis a -> CutAnalysis b -> (Fix Combinator c, Bool)
    seqAlg :: (Fix Combinator a
 -> Fix Combinator b -> Combinator (Fix Combinator) c)
-> Bool
-> CutAnalysis a
-> CutAnalysis b
-> (Fix Combinator c, Bool)
seqAlg Fix Combinator a
-> Fix Combinator b -> Combinator (Fix Combinator) c
con Bool
cut CutAnalysis a
l CutAnalysis b
r =
      let (Fix Combinator a
l', Bool
handled) = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut CutAnalysis a
l Bool
cut
          (Fix Combinator b
r', Bool
handled') = CutAnalysis b -> Bool -> (Fix Combinator b, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut CutAnalysis b
r (Bool
cut Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
handled)
      in (Combinator (Fix Combinator) c -> Fix Combinator c
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
-> Fix Combinator b -> Combinator (Fix Combinator) c
con Fix Combinator a
l' Fix Combinator b
r'), Bool
handled Bool -> Bool -> Bool
|| Bool
handled')

    rewrap :: (Fix Combinator a -> Combinator (Fix Combinator) b) -> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
    rewrap :: (Fix Combinator a -> Combinator (Fix Combinator) b)
-> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
rewrap Fix Combinator a -> Combinator (Fix Combinator) b
con Bool
cut CutAnalysis a
p = let (Fix Combinator a
p', Bool
handled) = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut CutAnalysis a
p Bool
cut in (Combinator (Fix Combinator) b -> Fix Combinator b
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a -> Combinator (Fix Combinator) b
con Fix Combinator a
p'), Bool
handled)

    alg :: Combinator (CutAnalysis :*: Compliance) a -> Bool -> (Fix Combinator a, Bool)
    alg :: Combinator (CutAnalysis :*: Compliance) a
-> Bool -> (Fix Combinator a, Bool)
alg (Pure Defunc a
x) Bool
_ = (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Defunc a -> Combinator (Fix Combinator) a
forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure Defunc a
x), Bool
False)
    alg (Satisfy Defunc (Char -> Bool)
f) Bool
cut = (Bool -> Fix Combinator Char -> Fix Combinator Char
forall a. Bool -> Fix Combinator a -> Fix Combinator a
mkCut Bool
cut (Combinator (Fix Combinator) Char -> Fix Combinator Char
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Defunc (Char -> Bool) -> Combinator (Fix Combinator) Char
forall (k :: Type -> Type).
Defunc (Char -> Bool) -> Combinator k Char
Satisfy Defunc (Char -> Bool)
f)), Bool
True)
    alg Combinator (CutAnalysis :*: Compliance) a
Empty Bool
_ = (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. Combinator k a
Empty, Bool
False)
    alg (Let Bool
r MVar a
μ (:*:) CutAnalysis Compliance a
p) Bool
cut = (Bool -> Fix Combinator a -> Fix Combinator a
forall a. Bool -> Fix Combinator a -> Fix Combinator a
mkCut (Bool -> Bool
not Bool
cut) (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Bool -> MVar a -> Fix Combinator a -> Combinator (Fix Combinator) a
forall a (k :: Type -> Type).
Bool -> MVar a -> k a -> Combinator k a
Let Bool
r MVar a
μ ((Fix Combinator a, Bool) -> Fix Combinator a
forall a b. (a, b) -> a
fst (CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p) Bool
True)))), Bool
False) -- If there is no cut, we generate a piggy for the continuation
    alg (Try (:*:) CutAnalysis Compliance a
p) Bool
_ = Bool
False Bool -> (Fix Combinator a, Bool) -> (Fix Combinator a, Bool)
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ (Fix Combinator a -> Combinator (Fix Combinator) a)
-> Bool -> CutAnalysis a -> (Fix Combinator a, Bool)
forall a b.
(Fix Combinator a -> Combinator (Fix Combinator) b)
-> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
rewrap Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. k a -> Combinator k a
Try Bool
False ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p)
    alg ((CutAnalysis a
p :*: Compliance a
NonComp) :<|>: (CutAnalysis a
q :*: Compliance a
FullPure)) Bool
_ = (Fix Combinator a -> Fix Combinator a
forall a. Fix Combinator a -> Fix Combinator a
requiresCut (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In ((Fix Combinator a, Bool) -> Fix Combinator a
forall a b. (a, b) -> a
fst (CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut CutAnalysis a
p Bool
True) Fix Combinator a
-> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. k a -> k a -> Combinator k a
:<|>: (Fix Combinator a, Bool) -> Fix Combinator a
forall a b. (a, b) -> a
fst (CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut CutAnalysis a
q Bool
False))), Bool
True)
    alg ((:*:) CutAnalysis Compliance a
p :<|>: (:*:) CutAnalysis Compliance a
q) Bool
cut =
      let (Fix Combinator a
q', Bool
handled) = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
q) Bool
cut
      in (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In ((Fix Combinator a, Bool) -> Fix Combinator a
forall a b. (a, b) -> a
fst (CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p) Bool
False) Fix Combinator a
-> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. k a -> k a -> Combinator k a
:<|>: Fix Combinator a
q'), Bool
handled)
    alg ((:*:) CutAnalysis Compliance (a -> a)
l :<*>: (:*:) CutAnalysis Compliance a
r) Bool
cut = (Fix Combinator (a -> a)
 -> Fix Combinator a -> Combinator (Fix Combinator) a)
-> Bool
-> CutAnalysis (a -> a)
-> CutAnalysis a
-> (Fix Combinator a, Bool)
forall a b c.
(Fix Combinator a
 -> Fix Combinator b -> Combinator (Fix Combinator) c)
-> Bool
-> CutAnalysis a
-> CutAnalysis b
-> (Fix Combinator c, Bool)
seqAlg Fix Combinator (a -> a)
-> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a b. k (a -> b) -> k a -> Combinator k b
(:<*>:) Bool
cut ((:*:) CutAnalysis Compliance (a -> a) -> CutAnalysis (a -> a)
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance (a -> a)
l) ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
r)
    alg ((:*:) CutAnalysis Compliance a
l :<*: (:*:) CutAnalysis Compliance b
r) Bool
cut = (Fix Combinator a
 -> Fix Combinator b -> Combinator (Fix Combinator) a)
-> Bool
-> CutAnalysis a
-> CutAnalysis b
-> (Fix Combinator a, Bool)
forall a b c.
(Fix Combinator a
 -> Fix Combinator b -> Combinator (Fix Combinator) c)
-> Bool
-> CutAnalysis a
-> CutAnalysis b
-> (Fix Combinator c, Bool)
seqAlg Fix Combinator a
-> Fix Combinator b -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
(:<*:) Bool
cut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
l) ((:*:) CutAnalysis Compliance b -> CutAnalysis b
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance b
r)
    alg ((:*:) CutAnalysis Compliance a
l :*>: (:*:) CutAnalysis Compliance a
r) Bool
cut = (Fix Combinator a
 -> Fix Combinator a -> Combinator (Fix Combinator) a)
-> Bool
-> CutAnalysis a
-> CutAnalysis a
-> (Fix Combinator a, Bool)
forall a b c.
(Fix Combinator a
 -> Fix Combinator b -> Combinator (Fix Combinator) c)
-> Bool
-> CutAnalysis a
-> CutAnalysis b
-> (Fix Combinator c, Bool)
seqAlg Fix Combinator a
-> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a b. k a -> k b -> Combinator k b
(:*>:) Bool
cut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
l) ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
r)
    alg (LookAhead (:*:) CutAnalysis Compliance a
p) Bool
cut = (Fix Combinator a -> Combinator (Fix Combinator) a)
-> Bool -> CutAnalysis a -> (Fix Combinator a, Bool)
forall a b.
(Fix Combinator a -> Combinator (Fix Combinator) b)
-> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
rewrap Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. k a -> Combinator k a
LookAhead Bool
cut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p)
    alg (NotFollowedBy (:*:) CutAnalysis Compliance a
p) Bool
_ = Bool
False Bool -> (Fix Combinator (), Bool) -> (Fix Combinator (), Bool)
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ (Fix Combinator a -> Combinator (Fix Combinator) ())
-> Bool -> CutAnalysis a -> (Fix Combinator (), Bool)
forall a b.
(Fix Combinator a -> Combinator (Fix Combinator) b)
-> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
rewrap Fix Combinator a -> Combinator (Fix Combinator) ()
forall (k :: Type -> Type) a. k a -> Combinator k ()
NotFollowedBy Bool
False ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p)
    alg (Debug String
msg (:*:) CutAnalysis Compliance a
p) Bool
cut = (Fix Combinator a -> Combinator (Fix Combinator) a)
-> Bool -> CutAnalysis a -> (Fix Combinator a, Bool)
forall a b.
(Fix Combinator a -> Combinator (Fix Combinator) b)
-> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
rewrap (String -> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. String -> k a -> Combinator k a
Debug String
msg) Bool
cut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p)
    alg (ChainPre (CutAnalysis (a -> a)
op :*: Compliance (a -> a)
NonComp) (:*:) CutAnalysis Compliance a
p) Bool
_ =
      let (Fix Combinator (a -> a)
op', Bool
_) = CutAnalysis (a -> a) -> Bool -> (Fix Combinator (a -> a), Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut CutAnalysis (a -> a)
op Bool
True
          (Fix Combinator a
p', Bool
_) = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p) Bool
False
      in (Fix Combinator a -> Fix Combinator a
forall a. Fix Combinator a -> Fix Combinator a
requiresCut (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator (a -> a)
-> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. k (a -> a) -> k a -> Combinator k a
ChainPre Fix Combinator (a -> a)
op' Fix Combinator a
p')), Bool
True)
    alg (ChainPre (:*:) CutAnalysis Compliance (a -> a)
op (:*:) CutAnalysis Compliance a
p) Bool
cut =
      let (Fix Combinator (a -> a)
op', Bool
_) = CutAnalysis (a -> a) -> Bool -> (Fix Combinator (a -> a), Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance (a -> a) -> CutAnalysis (a -> a)
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance (a -> a)
op) Bool
False
          (Fix Combinator a
p', Bool
handled) = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p) Bool
cut
      in (Bool -> Fix Combinator a -> Fix Combinator a
forall a. Bool -> Fix Combinator a -> Fix Combinator a
mkCut (Bool -> Bool
not Bool
cut) (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator (a -> a)
-> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. k (a -> a) -> k a -> Combinator k a
ChainPre Fix Combinator (a -> a)
op' Fix Combinator a
p')), Bool
handled)
    alg (ChainPost (:*:) CutAnalysis Compliance a
p (CutAnalysis (a -> a)
op :*: Compliance (a -> a)
NonComp)) Bool
cut =
      let (Fix Combinator a
p', Bool
_) = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p) Bool
cut
          (Fix Combinator (a -> a)
op', Bool
_) = CutAnalysis (a -> a) -> Bool -> (Fix Combinator (a -> a), Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut CutAnalysis (a -> a)
op Bool
True
      in (Fix Combinator a -> Fix Combinator a
forall a. Fix Combinator a -> Fix Combinator a
requiresCut (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
-> Fix Combinator (a -> a) -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. k a -> k (a -> a) -> Combinator k a
ChainPost Fix Combinator a
p' Fix Combinator (a -> a)
op')), Bool
True)
    alg (ChainPost (:*:) CutAnalysis Compliance a
p (:*:) CutAnalysis Compliance (a -> a)
op) Bool
cut =
      let (Fix Combinator a
p', Bool
handled) = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p) Bool
cut
          (Fix Combinator (a -> a)
op', Bool
_) = CutAnalysis (a -> a) -> Bool -> (Fix Combinator (a -> a), Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance (a -> a) -> CutAnalysis (a -> a)
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance (a -> a)
op) Bool
False
      in (Bool -> Fix Combinator a -> Fix Combinator a
forall a. Bool -> Fix Combinator a -> Fix Combinator a
mkCut (Bool
cut Bool -> Bool -> Bool
&& Bool
handled) (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
-> Fix Combinator (a -> a) -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a. k a -> k (a -> a) -> Combinator k a
ChainPost Fix Combinator a
p' Fix Combinator (a -> a)
op')), Bool
handled)
    alg (Branch (:*:) CutAnalysis Compliance (Either a b)
b (:*:) CutAnalysis Compliance (a -> a)
p (:*:) CutAnalysis Compliance (b -> a)
q) Bool
cut =
      let (Fix Combinator (Either a b)
b', Bool
handled) = CutAnalysis (Either a b)
-> Bool -> (Fix Combinator (Either a b), Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance (Either a b)
-> CutAnalysis (Either a b)
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance (Either a b)
b) Bool
cut
          (Fix Combinator (a -> a)
p', Bool
handled') = CutAnalysis (a -> a) -> Bool -> (Fix Combinator (a -> a), Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance (a -> a) -> CutAnalysis (a -> a)
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance (a -> a)
p) (Bool
cut Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
handled)
          (Fix Combinator (b -> a)
q', Bool
handled'') = CutAnalysis (b -> a) -> Bool -> (Fix Combinator (b -> a), Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance (b -> a) -> CutAnalysis (b -> a)
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance (b -> a)
q) (Bool
cut Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
handled)
      in (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator (Either a b)
-> Fix Combinator (a -> a)
-> Fix Combinator (b -> a)
-> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a b c.
k (Either a b) -> k (a -> c) -> k (b -> c) -> Combinator k c
Branch Fix Combinator (Either a b)
b' Fix Combinator (a -> a)
p' Fix Combinator (b -> a)
q'), Bool
handled Bool -> Bool -> Bool
|| (Bool
handled' Bool -> Bool -> Bool
&& Bool
handled''))
    alg (Match (:*:) CutAnalysis Compliance a
p [Defunc (a -> Bool)]
f [(:*:) CutAnalysis Compliance a]
qs (:*:) CutAnalysis Compliance a
def) Bool
cut =
      let (Fix Combinator a
p', Bool
handled) = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p) Bool
cut
          (Fix Combinator a
def', Bool
handled') = CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
def) (Bool
cut Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
handled)
          ([Fix Combinator a]
qs', Bool
handled'') = ((:*:) CutAnalysis Compliance a
 -> ([Fix Combinator a], Bool) -> ([Fix Combinator a], Bool))
-> ([Fix Combinator a], Bool)
-> [(:*:) CutAnalysis Compliance a]
-> ([Fix Combinator a], Bool)
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(:*:) CutAnalysis Compliance a
q -> (Fix Combinator a -> [Fix Combinator a] -> [Fix Combinator a])
-> (Bool -> Bool -> Bool)
-> (Fix Combinator a, Bool)
-> ([Fix Combinator a], Bool)
-> ([Fix Combinator a], Bool)
forall a b c x y z.
(a -> b -> c) -> (x -> y -> z) -> (a, x) -> (b, y) -> (c, z)
biliftA2 (:) Bool -> Bool -> Bool
(&&) (CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
forall a. CutAnalysis a -> Bool -> (Fix Combinator a, Bool)
doCut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
q) (Bool
cut Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
handled))) ([], Bool
handled') [(:*:) CutAnalysis Compliance a]
qs
      in (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
-> [Defunc (a -> Bool)]
-> [Fix Combinator a]
-> Fix Combinator a
-> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a b.
k a -> [Defunc (a -> Bool)] -> [k b] -> k b -> Combinator k b
Match Fix Combinator a
p' [Defunc (a -> Bool)]
f [Fix Combinator a]
qs' Fix Combinator a
def'), Bool
handled Bool -> Bool -> Bool
|| Bool
handled'')
    alg (MakeRegister ΣVar a
σ (:*:) CutAnalysis Compliance a
l (:*:) CutAnalysis Compliance a
r) Bool
cut = (Fix Combinator a
 -> Fix Combinator a -> Combinator (Fix Combinator) a)
-> Bool
-> CutAnalysis a
-> CutAnalysis a
-> (Fix Combinator a, Bool)
forall a b c.
(Fix Combinator a
 -> Fix Combinator b -> Combinator (Fix Combinator) c)
-> Bool
-> CutAnalysis a
-> CutAnalysis b
-> (Fix Combinator c, Bool)
seqAlg (ΣVar a
-> Fix Combinator a
-> Fix Combinator a
-> Combinator (Fix Combinator) a
forall a (k :: Type -> Type) b.
ΣVar a -> k a -> k b -> Combinator k b
MakeRegister ΣVar a
σ) Bool
cut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
l) ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
r)
    alg (GetRegister ΣVar a
σ) Bool
_ = (Combinator (Fix Combinator) a -> Fix Combinator a
forall k (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (ΣVar a -> Combinator (Fix Combinator) a
forall a (k :: Type -> Type). ΣVar a -> Combinator k a
GetRegister ΣVar a
σ), Bool
False)
    alg (PutRegister ΣVar a
σ (:*:) CutAnalysis Compliance a
p) Bool
cut = (Fix Combinator a -> Combinator (Fix Combinator) ())
-> Bool -> CutAnalysis a -> (Fix Combinator (), Bool)
forall a b.
(Fix Combinator a -> Combinator (Fix Combinator) b)
-> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
rewrap (ΣVar a -> Fix Combinator a -> Combinator (Fix Combinator) ()
forall a (k :: Type -> Type). ΣVar a -> k a -> Combinator k ()
PutRegister ΣVar a
σ) Bool
cut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p)
    alg (MetaCombinator MetaCombinator
m (:*:) CutAnalysis Compliance a
p) Bool
cut = (Fix Combinator a -> Combinator (Fix Combinator) a)
-> Bool -> CutAnalysis a -> (Fix Combinator a, Bool)
forall a b.
(Fix Combinator a -> Combinator (Fix Combinator) b)
-> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
rewrap (MetaCombinator -> Fix Combinator a -> Combinator (Fix Combinator) a
forall (k :: Type -> Type) a.
MetaCombinator -> k a -> Combinator k a
MetaCombinator MetaCombinator
m) Bool
cut ((:*:) CutAnalysis Compliance a -> CutAnalysis a
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (:*:) CutAnalysis Compliance a
p)

-- Termination Analysis (Generalised left-recursion checker)
{-data Consumption = Some | None | Never
data Prop = Prop {success :: Consumption, fails :: Consumption, indisputable :: Bool} | Unknown

looping (Prop Never Never _)          = True
looping _                             = False
strongLooping (Prop Never Never True) = True
strongLooping _                       = False
neverSucceeds (Prop Never _ _)        = True
neverSucceeds _                       = False
neverFails (Prop _ Never _)           = True
neverFails _                          = False

Never ||| _     = Never
_     ||| Never = Never
Some  ||| _     = Some
None  ||| p     = p

Some  &&& _    = Some
_     &&& Some = Some
None  &&& _    = None
Never &&& p    = p

Never ^^^ _     = Never
_     ^^^ Never = Never
None  ^^^ _     = None
Some  ^^^ p     = p

(==>) :: Prop -> Prop -> Prop
p ==> _ | neverSucceeds p            = p
_ ==> Prop Never Never True          = Prop Never Never True
Prop None _ _ ==> Prop Never Never _ = Prop Never Never False
Prop s1 f1 b1 ==> Prop s2 f2 b2      = Prop (s1 ||| s2) (f1 &&& (s1 ||| f2)) (b1 && b2)

branching :: Prop -> [Prop] -> Prop
branching b ps
  | neverSucceeds b = b
  | any strongLooping ps = Prop Never Never True
branching (Prop None f _) ps
  | any looping ps = Prop Never Never False
  | otherwise      = Prop (foldr1 (|||) (map success ps)) (f &&& (foldr1 (^^^) (map fails ps))) False
branching (Prop Some f _) ps = Prop (foldr (|||) Some (map success ps)) f False

--data InferredTerm = Loops | Safe | Undecidable
newtype Termination a = Termination {runTerm :: ReaderT (Set IMVar) (State (Map IMVar Prop)) Prop}
terminationAnalysis :: Fix Combinator a -> Fix Combinator a
terminationAnalysis p = if not (looping (evalState (runReaderT (runTerm (cata (Termination . alg) p)) Set.empty) Map.empty)) then p
                        else error "Parser will loop indefinitely: either it is left-recursive or iterates over pure computations"
  where
    alg :: Combinator Termination a -> ReaderT (Set IMVar) (State (Map IMVar Prop)) Prop
    alg (Satisfy _)                          = return $! Prop Some None True
    alg (Pure _)                             = return $! Prop None Never True
    alg Empty                                = return $! Prop Never None True
    alg (Try p)                              =
      do x <- runTerm p
         return $! if looping x then x
                   else Prop (success x) None (indisputable x)
    alg (LookAhead p)                        =
      do x <- runTerm p
         return $! if looping x then x
                   else Prop None (fails x) (indisputable x)
    alg (NotFollowedBy p)                    =
      do x <- runTerm p
         return $! if looping x then x
                   else Prop None None True
    alg (p :<*>: q)                          = liftA2 (==>) (runTerm p) (runTerm q)
    alg (p :*>: q)                           = liftA2 (==>) (runTerm p) (runTerm q)
    alg (p :<*: q)                           = liftA2 (==>) (runTerm p) (runTerm q)
    alg (p :<|>: q)                          =
      do x <- runTerm p; case x of
           -- If we fail without consuming input then q governs behaviour
           Prop _ None _       -> runTerm q
           -- If p never fails then q is irrelevant
           x | neverFails x    -> return $! x
           -- If p never succeeds then q governs
           x | neverSucceeds x -> runTerm q
           Prop s1 Some i1     -> do ~(Prop s2 f i2) <- runTerm q; return $! Prop (s1 &&& s2) (Some ||| f) (i1 && i2)
    alg (Branch b p q)                       = liftA2 branching (runTerm b) (sequence [runTerm p, runTerm q])
    alg (Match p _ qs def)                   = liftA2 branching (runTerm p) (traverse runTerm (def:qs))
    alg (ChainPre op p)                      =
      do x <- runTerm op; case x of
           -- Never failing implies you must either loop or not consume input
           Prop _ Never _ -> return $! Prop Never Never True
           -- Reaching p can take a route that consumes no input, if op failed
           _ -> do y <- runTerm p
                   return $! if looping y then y
                             else y -- TODO Verify!
    alg (ChainPost p op)                     =
      do y <- runTerm op; case y of
           Prop None _ _ -> return $! Prop Never Never True
           y -> do x <- runTerm p; case (x, y) of
                     (Prop Some f _, Prop _ Never _) -> return $! Prop Some f False
                     (x, y)                          -> return $! Prop (success x) (fails x &&& fails y) False -- TODO Verify
    alg (Let True (MVar v) p)                =
      do props <- get
         seen <- ask
         case Map.lookup v props of
           Just prop -> return $! prop
           Nothing | Set.member v seen -> return $! Prop Never Never False
           Nothing -> do prop <- local (Set.insert v) (runTerm p)
                         let prop' = if looping prop then Prop Never Never True else prop
                         put (Map.insert v prop' props)
                         return $! prop'
    alg (Debug _ p)                          = runTerm p
    --alg _                                    = return $! Unknown
-}