{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE UndecidableInstances #-}

module Cubix.Language.Parametric.Semantics.Cfg.CfgConstruction (
    collapseFProd
  , collapseFProd'
  , fprodFst'
  , EnterExitPair(..)
  , extractEEPList
  , extractEEPPair
  , extractEEPMaybe
  , identEnterExit
  , combineEnterExit
  , collapseEnterExit

  , ComputationSorts
  , SuspendedComputationSorts
  , ContainerFunctors

  , labeledIsComputationSort
  , labeledIsSuspendedComputationSort
  , labeledIsContainer

  , PreRAlg
  , ConstructCfg(..)
  , HState(..)
  , runSubCfgs
  , CfgComponent
  , constructCfgGeneric
  , constructCfgDefault

  , CfgState
  , CfgInitState(..)
  , CfgBuilder
  , makeCfg
 ) where


import Control.Monad.State ( MonadState, State, execState )
import Data.Proxy ( Proxy(..) )
import Data.Typeable ( Typeable )

import Control.Lens ( (^.), (%=)  )

import Data.Comp.Multi ( Node, Signature, Cxt(..), (:->), K(..), inj, proj, project, para, stripA, inj, Sum, HFunctor(..), HFoldable(..), HTraversable(..), (:*:)(..), (:&:)(..), ffst, fsnd, ShowHF(..), inj', caseCxt', All, HFix, AnnTerm, Term, (:-<:) )
import Data.Comp.Multi.Strategy.Classification ( DynCase, isSort, hasAnySort )

import Cubix.Language.Info
import Cubix.Language.Parametric.Semantics.Cfg.Graph
import Cubix.Language.Parametric.Syntax.Functor

--------------------------------------------------------------------------------------


------------------------------------------------------------------
--------------------------- Sort checking ------------------------
------------------------------------------------------------------

---------
---- Computation Sorts
---------

type family ComputationSorts (fs :: Signature) :: [*]

type IsComputationSort fs = All (DynCase (Term fs)) (ComputationSorts fs)

isComputationSort :: forall fs l. (IsComputationSort fs) => Term fs l -> Bool
isComputationSort :: forall (fs :: Signature) l.
IsComputationSort fs =>
Term fs l -> Bool
isComputationSort = forall (ls :: [*]) (e :: * -> *) i.
All (DynCase e) ls =>
e i -> Bool
hasAnySort @(ComputationSorts fs)

labeledIsComputationSort :: forall fs l. (IsComputationSort fs, All HFunctor fs) => TermLab fs l -> Bool
labeledIsComputationSort :: forall (fs :: Signature) l.
(IsComputationSort fs, All HFunctor fs) =>
TermLab fs l -> Bool
labeledIsComputationSort = Term fs l -> Bool
forall (fs :: Signature) l.
IsComputationSort fs =>
Term fs l -> Bool
isComputationSort (Term fs l -> Bool)
-> (TermLab fs l -> Term fs l) -> TermLab fs l -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermLab fs l -> Term fs l
CxtFun (Sum fs :&: Label) (Sum fs)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA

---------
---- Suspended Computation Sorts
---------

type family SuspendedComputationSorts (fs :: Signature) :: [*]

type IsSuspendedComputationSort fs = All (DynCase (Term fs)) (SuspendedComputationSorts fs)

isSuspendedComputationSort :: forall fs l. (IsSuspendedComputationSort fs) => Term fs l -> Bool
isSuspendedComputationSort :: forall (fs :: Signature) l.
IsSuspendedComputationSort fs =>
Term fs l -> Bool
isSuspendedComputationSort = forall (ls :: [*]) (e :: * -> *) i.
All (DynCase e) ls =>
e i -> Bool
hasAnySort @(SuspendedComputationSorts fs)

labeledIsSuspendedComputationSort :: (IsSuspendedComputationSort fs, All HFunctor fs) => AnnTerm a fs l -> Bool
labeledIsSuspendedComputationSort :: forall (fs :: Signature) a l.
(IsSuspendedComputationSort fs, All HFunctor fs) =>
AnnTerm a fs l -> Bool
labeledIsSuspendedComputationSort = Term fs l -> Bool
forall (fs :: Signature) l.
IsSuspendedComputationSort fs =>
Term fs l -> Bool
isSuspendedComputationSort (Term fs l -> Bool)
-> (AnnTerm a fs l -> Term fs l) -> AnnTerm a fs l -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnTerm a fs l -> Term fs l
CxtFun (Sum fs :&: a) (Sum fs)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA

---------
---- Container Functors
---------

type family ContainerFunctors (fs :: Signature) :: [Node]

class IsContainer' fs (l :: Signature)where
  isContainer' :: Proxy l -> Term fs i -> Bool

class IsContainer fs where
  isContainer :: Term fs i -> Bool

instance (IsContainer' fs (ContainerFunctors fs)) => IsContainer fs where
  isContainer :: forall i. Term fs i -> Bool
isContainer = Proxy (ContainerFunctors fs) -> Term fs i -> Bool
forall (fs :: Signature) (l :: Signature) i.
IsContainer' fs l =>
Proxy l -> Term fs i -> Bool
forall i. Proxy (ContainerFunctors fs) -> Term fs i -> Bool
isContainer' (forall (t :: Signature). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(ContainerFunctors fs))

instance IsContainer' fs '[] where
  isContainer' :: forall i. Proxy '[] -> Term fs i -> Bool
isContainer' Proxy '[]
_ = Bool -> Term fs i -> Bool
forall a b. a -> b -> a
const Bool
False

instance (IsContainer' fs ls, l :-<: fs) => IsContainer' fs (l ': ls) where
  isContainer' :: forall i. Proxy (l : ls) -> Term fs i -> Bool
isContainer' Proxy (l : ls)
_ Term fs i
t = case Term fs i -> Maybe (l (Term fs) i)
forall lab. Term fs lab -> Maybe (l (Term fs) lab)
go Term fs i
t of
                       Just l (Term fs) i
_  -> Bool
True
                       Maybe (l (Term fs) i)
Nothing -> Proxy ls -> Term fs i -> Bool
forall (fs :: Signature) (l :: Signature) i.
IsContainer' fs l =>
Proxy l -> Term fs i -> Bool
forall i. Proxy ls -> Term fs i -> Bool
isContainer' (forall (t :: Signature). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ls) Term fs i
t

    where go :: forall lab. Term fs lab -> Maybe (l (Term fs) lab)
          go :: forall lab. Term fs lab -> Maybe (l (Term fs) lab)
go = Cxt NoHole (Sum fs) (K ()) lab -> Maybe (l (Term fs) lab)
forall lab. Term fs lab -> Maybe (l (Term fs) lab)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project

labeledIsContainer :: (IsContainer fs, All HFunctor fs) => AnnTerm a fs l -> Bool
labeledIsContainer :: forall (fs :: Signature) a l.
(IsContainer fs, All HFunctor fs) =>
AnnTerm a fs l -> Bool
labeledIsContainer = Term fs l -> Bool
forall (fs :: Signature) i. IsContainer fs => Term fs i -> Bool
forall i. Term fs i -> Bool
isContainer (Term fs l -> Bool)
-> (AnnTerm a fs l -> Term fs l) -> AnnTerm a fs l -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnTerm a fs l -> Term fs l
CxtFun (Sum fs :&: a) (Sum fs)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA

------------------------------------------------------------------
--------------------------- Uncategorized ------------------------
------------------------------------------------------------------


data EnterExitPair fs l = EnterExitPair { forall (fs :: Signature) l. EnterExitPair fs l -> CfgNode fs
enter :: CfgNode fs
                                        , forall (fs :: Signature) l. EnterExitPair fs l -> CfgNode fs
exit  :: CfgNode fs
                                        }
                       | SubPairs (Sum fs (EnterExitPair fs) l) -- naming is hard
                       | EmptyEnterExit

instance (All ShowHF fs, All HFunctor fs) => Show (EnterExitPair fs l) where
  show :: EnterExitPair fs l -> String
show (EnterExitPair CfgNode fs
ent CfgNode fs
ex) = String
"(EnterExitPair " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CfgNode fs -> String
forall a. Show a => a -> String
show CfgNode fs
ent String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CfgNode fs -> String
forall a. Show a => a -> String
show CfgNode fs
ex String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (SubPairs Sum fs (EnterExitPair fs) l
t) = String
"(SubPairs " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sum fs (K String) l -> String
Sum fs (K String) :=> String
forall (f :: (* -> *) -> * -> *).
ShowHF f =>
f (K String) :=> String
showHF' ((EnterExitPair fs :-> K String)
-> Sum fs (EnterExitPair fs) :-> Sum fs (K String)
forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> Sum fs f :-> Sum fs g
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (String -> K String i
forall a i. a -> K a i
K (String -> K String i)
-> (EnterExitPair fs i -> String)
-> EnterExitPair fs i
-> K String i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EnterExitPair fs i -> String
forall a. Show a => a -> String
show) Sum fs (EnterExitPair fs) l
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show EnterExitPair fs l
EmptyEnterExit = String
"EmptyEnterExit"

mapEnterExitPair :: (All HFunctor fs) => (forall e i. Sum fs e i -> Sum gs e i) -> (EnterExitPair fs l -> EnterExitPair gs l)
mapEnterExitPair :: forall (fs :: Signature) (gs :: Signature) l.
All HFunctor fs =>
(forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> EnterExitPair fs l -> EnterExitPair gs l
mapEnterExitPair forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f EnterExitPair fs l
EmptyEnterExit = EnterExitPair gs l
forall (fs :: Signature) l. EnterExitPair fs l
EmptyEnterExit
mapEnterExitPair forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f (EnterExitPair CfgNode fs
n CfgNode fs
x) = CfgNode gs -> CfgNode gs -> EnterExitPair gs l
forall (fs :: Signature) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair ((forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> CfgNode fs -> CfgNode gs
forall (fs :: Signature) (gs :: Signature).
All HFunctor fs =>
(forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> CfgNode fs -> CfgNode gs
mapCfgNode Sum fs e i -> Sum gs e i
forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f CfgNode fs
n) ((forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> CfgNode fs -> CfgNode gs
forall (fs :: Signature) (gs :: Signature).
All HFunctor fs =>
(forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> CfgNode fs -> CfgNode gs
mapCfgNode Sum fs e i -> Sum gs e i
forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f CfgNode fs
x)
mapEnterExitPair forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f (SubPairs Sum fs (EnterExitPair fs) l
t) = Sum gs (EnterExitPair gs) l -> EnterExitPair gs l
forall (fs :: Signature) l.
Sum fs (EnterExitPair fs) l -> EnterExitPair fs l
SubPairs (Sum gs (EnterExitPair gs) l -> EnterExitPair gs l)
-> Sum gs (EnterExitPair gs) l -> EnterExitPair gs l
forall a b. (a -> b) -> a -> b
$ Sum fs (EnterExitPair gs) l -> Sum gs (EnterExitPair gs) l
forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f (Sum fs (EnterExitPair gs) l -> Sum gs (EnterExitPair gs) l)
-> Sum fs (EnterExitPair gs) l -> Sum gs (EnterExitPair gs) l
forall a b. (a -> b) -> a -> b
$ (EnterExitPair fs :-> EnterExitPair gs)
-> Sum fs (EnterExitPair fs) :-> Sum fs (EnterExitPair gs)
forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> Sum fs f :-> Sum fs g
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap ((forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> EnterExitPair fs i -> EnterExitPair gs i
forall (fs :: Signature) (gs :: Signature) l.
All HFunctor fs =>
(forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> EnterExitPair fs l -> EnterExitPair gs l
mapEnterExitPair Sum fs e i -> Sum gs e i
forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f) Sum fs (EnterExitPair fs) l
t

iSubPairs ::  (f' :-<: fs) => f' (EnterExitPair fs) l -> EnterExitPair fs l
iSubPairs :: forall (f' :: (* -> *) -> * -> *) (fs :: Signature) l.
(f' :-<: fs) =>
f' (EnterExitPair fs) l -> EnterExitPair fs l
iSubPairs f' (EnterExitPair fs) l
x = Sum fs (EnterExitPair fs) l -> EnterExitPair fs l
forall (fs :: Signature) l.
Sum fs (EnterExitPair fs) l -> EnterExitPair fs l
SubPairs (f' (EnterExitPair fs) l -> Sum fs (EnterExitPair fs) l
forall (a :: * -> *). f' a :-> Sum fs a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
f a :-> g a
inj f' (EnterExitPair fs) l
x)

-- Had such confusing type errors with this
extractEEPList :: forall fs l. (ListF :-<: fs, Typeable l) => EnterExitPair fs [l] -> [EnterExitPair fs l]
extractEEPList :: forall (fs :: Signature) l.
(ListF :-<: fs, Typeable l) =>
EnterExitPair fs [l] -> [EnterExitPair fs l]
extractEEPList (SubPairs Sum fs (EnterExitPair fs) [l]
ps) =
  case Sum fs (EnterExitPair fs) [l]
-> Maybe (ListF (EnterExitPair fs) [l])
forall (e :: * -> *). Sum fs e [l] -> Maybe (ListF e [l])
go Sum fs (EnterExitPair fs) [l]
ps of
    Just (ConsF EnterExitPair fs l1
x EnterExitPair fs [l1]
xs) -> EnterExitPair fs l
EnterExitPair fs l1
x EnterExitPair fs l -> [EnterExitPair fs l] -> [EnterExitPair fs l]
forall a. a -> [a] -> [a]
: EnterExitPair fs [l] -> [EnterExitPair fs l]
forall (fs :: Signature) l.
(ListF :-<: fs, Typeable l) =>
EnterExitPair fs [l] -> [EnterExitPair fs l]
extractEEPList EnterExitPair fs [l]
EnterExitPair fs [l1]
xs
    Just ListF (EnterExitPair fs) [l]
NilF         -> []

  where go :: Sum fs e [l] -> Maybe (ListF e [l])
        go :: forall (e :: * -> *). Sum fs e [l] -> Maybe (ListF e [l])
go = Sum fs e [l] -> Maybe (ListF e [l])
forall (a :: * -> *). NatM Maybe (Sum fs a) (ListF a)
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj

extractEEPPair :: forall fs a b. (PairF :-<: fs) => EnterExitPair fs (a,b) -> (EnterExitPair fs a, EnterExitPair fs b)
extractEEPPair :: forall (fs :: Signature) a b.
(PairF :-<: fs) =>
EnterExitPair fs (a, b) -> (EnterExitPair fs a, EnterExitPair fs b)
extractEEPPair (SubPairs Sum fs (EnterExitPair fs) (a, b)
ps) =
  case Sum fs (EnterExitPair fs) (a, b)
-> Maybe (PairF (EnterExitPair fs) (a, b))
forall (e :: * -> *). Sum fs e (a, b) -> Maybe (PairF e (a, b))
go Sum fs (EnterExitPair fs) (a, b)
ps of
    Just (PairF EnterExitPair fs i
x EnterExitPair fs j
y) -> (EnterExitPair fs a
EnterExitPair fs i
x, EnterExitPair fs b
EnterExitPair fs j
y)

  where go :: Sum fs e (a, b) -> Maybe (PairF e (a, b))
        go :: forall (e :: * -> *). Sum fs e (a, b) -> Maybe (PairF e (a, b))
go = Sum fs e (a, b) -> Maybe (PairF e (a, b))
forall (a :: * -> *). NatM Maybe (Sum fs a) (PairF a)
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj

-- Yes, it's ugly that this has a different signature from the above. No, I don't have
-- time to care ATM
extractEEPMaybe :: (All (KExtractF' Maybe) fs, Monad m) => m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe :: forall (fs :: Signature) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe m (EnterExitPair fs (Maybe l))
m = do
  EnterExitPair fs (Maybe l)
p' <- m (EnterExitPair fs (Maybe l))
m
  let SubPairs Sum fs (EnterExitPair fs) (Maybe l)
p = EnterExitPair fs (Maybe l)
p'
  Maybe (EnterExitPair fs l) -> m (Maybe (EnterExitPair fs l))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
return (Maybe (EnterExitPair fs l) -> m (Maybe (EnterExitPair fs l)))
-> Maybe (EnterExitPair fs l) -> m (Maybe (EnterExitPair fs l))
forall a b. (a -> b) -> a -> b
$ Sum fs (EnterExitPair fs) (Maybe l) -> Maybe (EnterExitPair fs l)
forall (e :: * -> *) l. Sum fs e (Maybe l) -> Maybe (e l)
forall (f :: * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) l.
KExtractF' f g =>
g e (f l) -> f (e l)
kextractF' Sum fs (EnterExitPair fs) (Maybe l)
p


identEnterExit :: CfgNode fs -> EnterExitPair fs l
identEnterExit :: forall (fs :: Signature) l. CfgNode fs -> EnterExitPair fs l
identEnterExit CfgNode fs
n = CfgNode fs -> CfgNode fs -> EnterExitPair fs l
forall (fs :: Signature) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode fs
n CfgNode fs
n

collapseEnterExit ::
  ( HasCurCfg s fs
  , All HTraversable fs
  , All HFoldable fs
  , All HFunctor fs
  , MonadState s m
  ) => EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit :: forall s (fs :: Signature) (m :: * -> *) i j.
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit p :: EnterExitPair fs i
p@(EnterExitPair CfgNode fs
n CfgNode fs
x) = EnterExitPair fs j -> m (EnterExitPair fs j)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (EnterExitPair fs j -> m (EnterExitPair fs j))
-> EnterExitPair fs j -> m (EnterExitPair fs j)
forall a b. (a -> b) -> a -> b
$ CfgNode fs -> CfgNode fs -> EnterExitPair fs j
forall (fs :: Signature) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode fs
n CfgNode fs
x
collapseEnterExit EnterExitPair fs i
EmptyEnterExit = EnterExitPair fs j -> m (EnterExitPair fs j)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair fs j
forall (fs :: Signature) l. EnterExitPair fs l
EmptyEnterExit
collapseEnterExit (SubPairs Sum fs (EnterExitPair fs) i
subCfgs) =
    (EnterExitPair fs
 :=> (m (EnterExitPair fs j) -> m (EnterExitPair fs j)))
-> m (EnterExitPair fs j)
-> Sum fs (EnterExitPair fs) :=> m (EnterExitPair fs j)
forall (a :: * -> *) b. (a :=> (b -> b)) -> b -> Sum fs a :=> b
forall (h :: (* -> *) -> * -> *) (a :: * -> *) b.
HFoldable h =>
(a :=> (b -> b)) -> b -> h a :=> b
hfoldr (\EnterExitPair fs i
k m (EnterExitPair fs j)
t -> m (EnterExitPair fs j)
t m (EnterExitPair fs j)
-> (EnterExitPair fs j -> m (EnterExitPair fs j))
-> m (EnterExitPair fs j)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs j)
forall s (fs :: Signature) (m :: * -> *) i j k.
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit EnterExitPair fs i
k) (EnterExitPair fs j -> m (EnterExitPair fs j)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair fs j
forall (fs :: Signature) l. EnterExitPair fs l
EmptyEnterExit) Sum fs (EnterExitPair fs) i
subCfgs

combineEnterExit ::
  ( HasCurCfg s fs
  , All HTraversable fs
  , All HFoldable fs
  , All HFunctor fs  
  , MonadState s m
  ) => EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit :: forall s (fs :: Signature) (m :: * -> *) i j k.
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit EnterExitPair fs i
p1 EnterExitPair fs j
p2 = do
  EnterExitPair fs k
p1' <- EnterExitPair fs i -> m (EnterExitPair fs k)
forall s (fs :: Signature) (m :: * -> *) i j.
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit EnterExitPair fs i
p1
  EnterExitPair fs k
p2' <- EnterExitPair fs j -> m (EnterExitPair fs k)
forall s (fs :: Signature) (m :: * -> *) i j.
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit EnterExitPair fs j
p2
  case EnterExitPair fs k
p1' of
    EnterExitPair fs k
EmptyEnterExit                    -> EnterExitPair fs k -> m (EnterExitPair fs k)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair fs k
p2'
    EnterExitPair {enter :: forall (fs :: Signature) l. EnterExitPair fs l -> CfgNode fs
enter=CfgNode fs
n1, exit :: forall (fs :: Signature) l. EnterExitPair fs l -> CfgNode fs
exit=CfgNode fs
x1} -> case EnterExitPair fs k
p2' of
      EnterExitPair fs k
EmptyEnterExit                    -> EnterExitPair fs k -> m (EnterExitPair fs k)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair fs k
p1'
      EnterExitPair {enter :: forall (fs :: Signature) l. EnterExitPair fs l -> CfgNode fs
enter=CfgNode fs
n2, exit :: forall (fs :: Signature) l. EnterExitPair fs l -> CfgNode fs
exit=CfgNode fs
x2} -> do
          (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall c (fs :: Signature). HasCurCfg c fs => Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode fs
x1 CfgNode fs
n2
          return $ CfgNode fs -> CfgNode fs -> EnterExitPair fs k
forall (fs :: Signature) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode fs
n1 CfgNode fs
x2

collapseFProdG :: (HFunctor f, f :-<: gs) => f (Term gs :*: t) :-> Term gs :*: f t
collapseFProdG :: forall (f :: (* -> *) -> * -> *) (gs :: Signature) (t :: * -> *).
(HFunctor f, f :-<: gs) =>
f (Term gs :*: t) :-> (Term gs :*: f t)
collapseFProdG f (Term gs :*: t) i
t = (Sum gs (Term gs) i -> Cxt NoHole (Sum gs) (K ()) i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (Sum gs (Term gs) i -> Cxt NoHole (Sum gs) (K ()) i)
-> Sum gs (Term gs) i -> Cxt NoHole (Sum gs) (K ()) i
forall a b. (a -> b) -> a -> b
$ f (Term gs) i -> Sum gs (Term gs) i
forall (a :: * -> *). f a :-> Sum gs a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
f a :-> g a
inj (f (Term gs) i -> Sum gs (Term gs) i)
-> f (Term gs) i -> Sum gs (Term gs) i
forall a b. (a -> b) -> a -> b
$ ((Term gs :*: t) :-> Term gs) -> f (Term gs :*: t) :-> f (Term gs)
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> f f :-> f g
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (:*:) (Term gs) t i -> Cxt NoHole (Sum gs) (K ()) i
(Term gs :*: t) :-> Term gs
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst f (Term gs :*: t) i
t) Cxt NoHole (Sum gs) (K ()) i -> f t i -> (:*:) (Term gs) (f t) i
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: (((Term gs :*: t) :-> t) -> f (Term gs :*: t) :-> f t
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> f f :-> f g
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (:*:) (Term gs) t i -> t i
(Term gs :*: t) :-> t
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> g a
fsnd f (Term gs :*: t) i
t)

collapseFProd :: (HFunctor f, f :-<: gs) => f (Term gs :*: t) :-> Term gs :*: f t
collapseFProd :: forall (f :: (* -> *) -> * -> *) (gs :: Signature) (t :: * -> *).
(HFunctor f, f :-<: gs) =>
f (Term gs :*: t) :-> (Term gs :*: f t)
collapseFProd = f (Term gs :*: t) i -> (:*:) (Term gs) (f t) i
f (Term gs :*: t) :-> (Term gs :*: f t)
forall (f :: (* -> *) -> * -> *) (gs :: Signature) (t :: * -> *).
(HFunctor f, f :-<: gs) =>
f (Term gs :*: t) :-> (Term gs :*: f t)
collapseFProdG

collapseFProd' :: (HFunctor f, f :-<: gs) => (f :&: a) (AnnTerm a gs :*: t) :-> AnnTerm a gs :*: f t
collapseFProd' :: forall (f :: (* -> *) -> * -> *) (gs :: Signature) a (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' t :: (:&:) f a (AnnTerm a gs :*: t) i
t@(f (AnnTerm a gs :*: t) i
x :&: a
_) = ((:&:) (Sum gs) a (AnnTerm a gs) i
-> Cxt NoHole (Sum gs :&: a) (K ()) i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term ((:&:) (Sum gs) a (AnnTerm a gs) i
 -> Cxt NoHole (Sum gs :&: a) (K ()) i)
-> (:&:) (Sum gs) a (AnnTerm a gs) i
-> Cxt NoHole (Sum gs :&: a) (K ()) i
forall a b. (a -> b) -> a -> b
$ (:&:) f a (AnnTerm a gs) i -> (:&:) (Sum gs) a (AnnTerm a gs) i
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p
       (e :: * -> *) l.
(f :<: g) =>
(:&:) f p e l -> (:&:) g p e l
inj' ((:&:) f a (AnnTerm a gs) i -> (:&:) (Sum gs) a (AnnTerm a gs) i)
-> (:&:) f a (AnnTerm a gs) i -> (:&:) (Sum gs) a (AnnTerm a gs) i
forall a b. (a -> b) -> a -> b
$ ((AnnTerm a gs :*: t) :-> AnnTerm a gs)
-> (:&:) f a (AnnTerm a gs :*: t) :-> (:&:) f a (AnnTerm a gs)
forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> (:&:) f a f :-> (:&:) f a g
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (:*:) (AnnTerm a gs) t i -> Cxt NoHole (Sum gs :&: a) (K ()) i
(AnnTerm a gs :*: t) :-> AnnTerm a gs
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst (:&:) f a (AnnTerm a gs :*: t) i
t) Cxt NoHole (Sum gs :&: a) (K ()) i
-> f t i -> (:*:) (AnnTerm a gs) (f t) i
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: (((AnnTerm a gs :*: t) :-> t) -> f (AnnTerm a gs :*: t) :-> f t
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> f f :-> f g
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (:*:) (AnnTerm a gs) t i -> t i
(AnnTerm a gs :*: t) :-> t
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> g a
fsnd f (AnnTerm a gs :*: t) i
x)

fprodFst' :: (HFunctor f, f :-<: gs) => (f :&: a) (AnnTerm a gs :*: t) :-> AnnTerm a gs
fprodFst' :: forall (f :: (* -> *) -> * -> *) (gs :: Signature) a (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> AnnTerm a gs
fprodFst' ((:&:) f a (AnnTerm a gs :*: t) i -> (:*:) (AnnTerm a gs) (f t) i
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
forall (f :: (* -> *) -> * -> *) (gs :: Signature) a (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> AnnTerm a gs i
t :*: f t i
_) = AnnTerm a gs i
t

-- | PreRAlg's are things that can be modularly composed
-- to form R-algebras. R-algebras are in turn the building
-- block used to define paramorphisms, a recursion scheme
-- where each step can depend on both an entire term and the
-- previous results. Because the map of variables in scope
-- within a term depends both on the entire term and the
-- variables in scope in each subterm, this is a correct
-- recursion scheme to use.
--
-- @
-- PreRAlg f f a == RAlg f a
-- @
--
-- In @PreRAlg f g a@, @f@ is the signature functor of
-- the outer layer, while @g@ is the recursive signature
-- functor, and @a@ is the carrier of the R-algebra.
type PreRAlg f g a = f (HFix g :*: a) :-> a

data HState s f l = HState { forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState :: State s (f l) }

class ConstructCfg gs s f where
  constructCfg :: PreRAlg (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))

type CfgComponent gs s = (HasLabelGen s, HasCurCfg s gs, All HTraversable gs, All HFoldable gs, All HFunctor gs)
type SortChecks gs = (IsComputationSort gs, IsSuspendedComputationSort gs, IsContainer gs)

runSubCfgs ::
  ( f :-<: gs
  , HTraversable f
  , CfgComponent gs s
  ) => f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs j)
runSubCfgs :: forall (f :: (* -> *) -> * -> *) (gs :: Signature) s i j.
(f :-<: gs, HTraversable f, CfgComponent gs s) =>
f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs j)
runSubCfgs f (HState s (EnterExitPair gs)) i
subCfgs = do
  f (EnterExitPair gs) i
x <- NatM
  (StateT s Identity)
  (HState s (EnterExitPair gs))
  (EnterExitPair gs)
-> NatM
     (StateT s Identity)
     (f (HState s (EnterExitPair gs)))
     (f (EnterExitPair gs))
forall (m :: * -> *) (a :: * -> *) (b :: * -> *).
Monad m =>
NatM m a b -> NatM m (f a) (f b)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM HState s (EnterExitPair gs) i -> State s (EnterExitPair gs i)
NatM
  (StateT s Identity)
  (HState s (EnterExitPair gs))
  (EnterExitPair gs)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState f (HState s (EnterExitPair gs)) i
subCfgs
  EnterExitPair gs i -> State s (EnterExitPair gs j)
forall s (fs :: Signature) (m :: * -> *) i j.
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit (EnterExitPair gs i -> State s (EnterExitPair gs j))
-> EnterExitPair gs i -> State s (EnterExitPair gs j)
forall a b. (a -> b) -> a -> b
$ Sum gs (EnterExitPair gs) i -> EnterExitPair gs i
forall (fs :: Signature) l.
Sum fs (EnterExitPair fs) l -> EnterExitPair fs l
SubPairs (f (EnterExitPair gs) i -> Sum gs (EnterExitPair gs) i
forall (a :: * -> *). f a :-> Sum gs a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
f a :-> g a
inj f (EnterExitPair gs) i
x)

constructCfgGeneric ::
  forall f gs s.
  ( f :-<: gs
  , HTraversable f
  , CfgComponent gs s
  ) => PreRAlg (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
constructCfgGeneric :: forall (f :: (* -> *) -> * -> *) (gs :: Signature) s.
(f :-<: gs, HTraversable f, CfgComponent gs s) =>
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
constructCfgGeneric ((:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs)) i
-> (:*:)
     (HFix (Sum gs :&: Label)) (f (HState s (EnterExitPair gs))) i
(:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs))
:-> (HFix (Sum gs :&: Label) :*: f (HState s (EnterExitPair gs)))
forall (f :: (* -> *) -> * -> *) (gs :: Signature) a (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (AnnTerm Label gs i
t :*: f (HState s (EnterExitPair gs)) i
subCfgs)) = State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i)
-> State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i
forall a b. (a -> b) -> a -> b
$ do
  CfgNode gs
enterNode <- AnnTerm Label gs i -> CfgNodeType -> StateT s Identity (CfgNode gs)
forall s (fs :: Signature) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode AnnTerm Label gs i
t CfgNodeType
EnterNode
  CfgNode gs
exitNode  <- AnnTerm Label gs i -> CfgNodeType -> StateT s Identity (CfgNode gs)
forall s (fs :: Signature) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode AnnTerm Label gs i
t CfgNodeType
ExitNode

  EnterExitPair gs Any
body <- f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs Any)
forall (f :: (* -> *) -> * -> *) (gs :: Signature) s i j.
(f :-<: gs, HTraversable f, CfgComponent gs s) =>
f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs j)
runSubCfgs f (HState s (EnterExitPair gs)) i
subCfgs

  EnterExitPair gs Any
tmpNode <- EnterExitPair gs Any
-> EnterExitPair gs Any -> State s (EnterExitPair gs Any)
forall s (fs :: Signature) (m :: * -> *) i j k.
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit (CfgNode gs -> EnterExitPair gs Any
forall (fs :: Signature) l. CfgNode fs -> EnterExitPair fs l
identEnterExit CfgNode gs
enterNode) EnterExitPair gs Any
body
  EnterExitPair gs Any
-> EnterExitPair gs Any -> State s (EnterExitPair gs i)
forall s (fs :: Signature) (m :: * -> *) i j k.
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit EnterExitPair gs Any
tmpNode (CfgNode gs -> EnterExitPair gs Any
forall (fs :: Signature) l. CfgNode fs -> EnterExitPair fs l
identEnterExit CfgNode gs
exitNode)

constructCfgDefault ::
  forall f gs s.
  ( f :-<: gs
  , HTraversable f
  , CfgComponent gs s
  , SortChecks gs
  ) => PreRAlg (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
constructCfgDefault :: forall (f :: (* -> *) -> * -> *) (gs :: Signature) s.
(f :-<: gs, HTraversable f, CfgComponent gs s, SortChecks gs) =>
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
constructCfgDefault p :: (:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs)) i
p@((:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs)) i
-> (:*:)
     (HFix (Sum gs :&: Label)) (f (HState s (EnterExitPair gs))) i
(:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs))
:-> (HFix (Sum gs :&: Label) :*: f (HState s (EnterExitPair gs)))
forall (f :: (* -> *) -> * -> *) (gs :: Signature) a (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (AnnTerm Label gs i
t :*: f (HState s (EnterExitPair gs)) i
subCfgs)) =
  if AnnTerm Label gs i -> Bool
forall (fs :: Signature) l.
(IsComputationSort fs, All HFunctor fs) =>
TermLab fs l -> Bool
labeledIsComputationSort AnnTerm Label gs i
t then
    (:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs)) i
-> HState s (EnterExitPair gs) i
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
forall (f :: (* -> *) -> * -> *) (gs :: Signature) s.
(f :-<: gs, HTraversable f, CfgComponent gs s) =>
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
constructCfgGeneric (:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs)) i
p
  else if AnnTerm Label gs i -> Bool
forall (fs :: Signature) a l.
(IsSuspendedComputationSort fs, All HFunctor fs) =>
AnnTerm a fs l -> Bool
labeledIsSuspendedComputationSort AnnTerm Label gs i
t then
    State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i)
-> State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i
forall a b. (a -> b) -> a -> b
$ do
      -- Connect children to each other, but don't connect them to surrounding context
      f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs Any)
forall (f :: (* -> *) -> * -> *) (gs :: Signature) s i j.
(f :-<: gs, HTraversable f, CfgComponent gs s) =>
f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs j)
runSubCfgs f (HState s (EnterExitPair gs)) i
subCfgs
      return EnterExitPair gs i
forall (fs :: Signature) l. EnterExitPair fs l
EmptyEnterExit
  else if AnnTerm Label gs i -> Bool
forall (fs :: Signature) a l.
(IsContainer fs, All HFunctor fs) =>
AnnTerm a fs l -> Bool
labeledIsContainer AnnTerm Label gs i
t then
    State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i)
-> State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i
forall a b. (a -> b) -> a -> b
$ f (EnterExitPair gs) i -> EnterExitPair gs i
forall (f' :: (* -> *) -> * -> *) (fs :: Signature) l.
(f' :-<: fs) =>
f' (EnterExitPair fs) l -> EnterExitPair fs l
iSubPairs (f (EnterExitPair gs) i -> EnterExitPair gs i)
-> StateT s Identity (f (EnterExitPair gs) i)
-> State s (EnterExitPair gs i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatM
  (StateT s Identity)
  (HState s (EnterExitPair gs))
  (EnterExitPair gs)
-> NatM
     (StateT s Identity)
     (f (HState s (EnterExitPair gs)))
     (f (EnterExitPair gs))
forall (m :: * -> *) (a :: * -> *) (b :: * -> *).
Monad m =>
NatM m a b -> NatM m (f a) (f b)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM HState s (EnterExitPair gs) i -> State s (EnterExitPair gs i)
NatM
  (StateT s Identity)
  (HState s (EnterExitPair gs))
  (EnterExitPair gs)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState f (HState s (EnterExitPair gs)) i
subCfgs -- by default, don't make node for containers
  else
    State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i)
-> State s (EnterExitPair gs i) -> HState s (EnterExitPair gs) i
forall a b. (a -> b) -> a -> b
$ f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs i)
forall (f :: (* -> *) -> * -> *) (gs :: Signature) s i j.
(f :-<: gs, HTraversable f, CfgComponent gs s) =>
f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs j)
runSubCfgs f (HState s (EnterExitPair gs)) i
subCfgs

instance {-# OVERLAPPABLE #-}
  ( f :-<: gs
  , HTraversable f
  , CfgComponent gs s
  , SortChecks gs
  ) => ConstructCfg gs s f where
  constructCfg :: PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
constructCfg = (:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs)) i
-> HState s (EnterExitPair gs) i
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
forall (f :: (* -> *) -> * -> *) (gs :: Signature) s.
(f :-<: gs, HTraversable f, CfgComponent gs s, SortChecks gs) =>
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
constructCfgDefault

instance {-# OVERLAPPING #-} (All (ConstructCfg g s) fs) => ConstructCfg g s (Sum fs) where
  constructCfg :: PreRAlg
  (Sum fs :&: Label) (Sum g :&: Label) (HState s (EnterExitPair g))
constructCfg = forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: Signature) a (e :: * -> *) l t.
All cxt fs =>
(forall (f :: (* -> *) -> * -> *). cxt f => (:&:) f a e l -> t)
-> (:&:) (Sum fs) a e l -> t
caseCxt' @(ConstructCfg g s) (:&:)
  f Label (HFix (Sum g :&: Label) :*: HState s (EnterExitPair g)) i
-> HState s (EnterExitPair g) i
forall (gs :: Signature) s (f :: (* -> *) -> * -> *).
ConstructCfg gs s f =>
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
PreRAlg
  (f :&: Label) (Sum g :&: Label) (HState s (EnterExitPair g))
forall (f :: (* -> *) -> * -> *).
ConstructCfg g s f =>
(:&:)
  f Label (HFix (Sum g :&: Label) :*: HState s (EnterExitPair g)) i
-> HState s (EnterExitPair g) i
constructCfg


------------------------------------------------------------------------------------------------------------------------

type family CfgState (fs :: Signature) :: *

class CfgInitState fs where
   cfgInitState :: Proxy fs -> CfgState fs

class    (CfgComponent fs (CfgState fs), ConstructCfg fs (CfgState fs) (Sum fs), CfgInitState fs) => CfgBuilder fs
instance (CfgComponent fs (CfgState fs), ConstructCfg fs (CfgState fs) (Sum fs), CfgInitState fs) => CfgBuilder fs

-- | Constructs a CFG for the given labelled term
makeCfg :: forall fs l. (CfgBuilder fs) => TermLab fs l -> Cfg fs
makeCfg :: forall (fs :: Signature) l. CfgBuilder fs => TermLab fs l -> Cfg fs
makeCfg TermLab fs l
t = (State (CfgState fs) (EnterExitPair fs l)
-> CfgState fs -> CfgState fs
forall s a. State s a -> s -> s
execState (HState (CfgState fs) (EnterExitPair fs) l
-> State (CfgState fs) (EnterExitPair fs l)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState (HState (CfgState fs) (EnterExitPair fs) l
 -> State (CfgState fs) (EnterExitPair fs l))
-> HState (CfgState fs) (EnterExitPair fs) l
-> State (CfgState fs) (EnterExitPair fs l)
forall a b. (a -> b) -> a -> b
$ RAlg (Sum fs :&: Label) (HState (CfgState fs) (EnterExitPair fs))
-> HFix (Sum fs :&: Label)
   :-> HState (CfgState fs) (EnterExitPair fs)
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
RAlg f a -> HFix f :-> a
para (:&:)
  (Sum fs)
  Label
  (HFix (Sum fs :&: Label)
   :*: HState (CfgState fs) (EnterExitPair fs))
  i
-> HState (CfgState fs) (EnterExitPair fs) i
forall (gs :: Signature) s (f :: (* -> *) -> * -> *).
ConstructCfg gs s f =>
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
RAlg (Sum fs :&: Label) (HState (CfgState fs) (EnterExitPair fs))
constructCfg TermLab fs l
t) CfgState fs
initState) CfgState fs -> Getting (Cfg fs) (CfgState fs) (Cfg fs) -> Cfg fs
forall s a. s -> Getting a s a -> a
^. Getting (Cfg fs) (CfgState fs) (Cfg fs)
forall c (fs :: Signature). HasCurCfg c fs => Lens' c (Cfg fs)
Lens' (CfgState fs) (Cfg fs)
cur_cfg
  where
    initState :: CfgState fs
initState = Proxy fs -> CfgState fs
forall (fs :: Signature).
CfgInitState fs =>
Proxy fs -> CfgState fs
cfgInitState (forall (t :: Signature). Proxy t
forall {k} (t :: k). Proxy t
Proxy @fs)