{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

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 ( 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 )

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

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

type family ComputationSorts (fs :: [(* -> *) -> * -> *]) :: [*]

class IsComputationSort' fs (l :: [*]) where
  isComputationSort' :: Proxy l -> Term fs i -> Bool

class IsComputationSort fs where
  isComputationSort :: Term fs i -> Bool

instance (IsComputationSort' fs (ComputationSorts fs)) => IsComputationSort fs where
  isComputationSort :: Term fs i -> Bool
isComputationSort = Proxy (ComputationSorts fs) -> Term fs i -> Bool
forall (fs :: [(* -> *) -> * -> *]) (l :: [*]) i.
IsComputationSort' fs l =>
Proxy l -> Term fs i -> Bool
isComputationSort' (Proxy (ComputationSorts fs)
forall k (t :: k). Proxy t
Proxy :: Proxy (ComputationSorts fs))

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

instance (IsComputationSort' fs ls, DynCase (Term fs) l) => IsComputationSort' fs (l ': ls) where
  isComputationSort' :: Proxy (l : ls) -> Term fs i -> Bool
isComputationSort' _ t :: Term fs i
t = (Proxy l -> Term fs i -> Bool
forall (e :: * -> *) l.
DynCase e l =>
Proxy l -> forall i. e i -> Bool
isSort (Proxy l
forall k (t :: k). Proxy t
Proxy :: Proxy l) Term fs i
t) Bool -> Bool -> Bool
|| (Proxy ls -> Term fs i -> Bool
forall (fs :: [(* -> *) -> * -> *]) (l :: [*]) i.
IsComputationSort' fs l =>
Proxy l -> Term fs i -> Bool
isComputationSort' (Proxy ls
forall k (t :: k). Proxy t
Proxy :: Proxy ls) Term fs i
t)

labeledIsComputationSort :: forall fs l. (IsComputationSort fs, All HFunctor fs) => TermLab fs l -> Bool
labeledIsComputationSort :: TermLab fs l -> Bool
labeledIsComputationSort = Term fs l -> Bool
forall (fs :: [(* -> *) -> * -> *]) i.
IsComputationSort fs =>
Term fs i -> 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
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA

type family SuspendedComputationSorts (fs :: [(* -> *) -> * -> *]) :: [*]

class IsSuspendedComputationSort' fs (l :: [*]) where
  isSuspendedComputationSort' :: Proxy l -> Term fs i -> Bool

class IsSuspendedComputationSort fs where
  isSuspendedComputationSort :: Term fs i -> Bool

instance (IsSuspendedComputationSort' fs (SuspendedComputationSorts fs)) => IsSuspendedComputationSort fs where
  isSuspendedComputationSort :: Term fs i -> Bool
isSuspendedComputationSort = Proxy (SuspendedComputationSorts fs) -> Term fs i -> Bool
forall (fs :: [(* -> *) -> * -> *]) (l :: [*]) i.
IsSuspendedComputationSort' fs l =>
Proxy l -> Term fs i -> Bool
isSuspendedComputationSort' (Proxy (SuspendedComputationSorts fs)
forall k (t :: k). Proxy t
Proxy :: Proxy (SuspendedComputationSorts fs))

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

instance (IsSuspendedComputationSort' fs ls, DynCase (Term fs) l) => IsSuspendedComputationSort' fs (l ': ls) where
  isSuspendedComputationSort' :: Proxy (l : ls) -> Term fs i -> Bool
isSuspendedComputationSort' _ t :: Term fs i
t = (Proxy l -> Term fs i -> Bool
forall (e :: * -> *) l.
DynCase e l =>
Proxy l -> forall i. e i -> Bool
isSort (Proxy l
forall k (t :: k). Proxy t
Proxy :: Proxy l) Term fs i
t) Bool -> Bool -> Bool
|| (Proxy ls -> Term fs i -> Bool
forall (fs :: [(* -> *) -> * -> *]) (l :: [*]) i.
IsSuspendedComputationSort' fs l =>
Proxy l -> Term fs i -> Bool
isSuspendedComputationSort' (Proxy ls
forall k (t :: k). Proxy t
Proxy :: Proxy ls) Term fs i
t)

labeledIsSuspendedComputationSort :: (IsSuspendedComputationSort fs, All HFunctor fs) => AnnTerm a fs l -> Bool
labeledIsSuspendedComputationSort :: AnnTerm a fs l -> Bool
labeledIsSuspendedComputationSort = Term fs l -> Bool
forall (fs :: [(* -> *) -> * -> *]) i.
IsSuspendedComputationSort fs =>
Term fs i -> 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
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA

type family ContainerFunctors (fs :: [(* -> *) -> * -> *]) :: [(* -> *) -> * -> *]

class IsContainer' fs (l :: [(* -> *) -> * -> *])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 :: Term fs i -> Bool
isContainer = Proxy (ContainerFunctors fs) -> Term fs i -> Bool
forall (fs :: [(* -> *) -> * -> *]) (l :: [(* -> *) -> * -> *]) i.
IsContainer' fs l =>
Proxy l -> Term fs i -> Bool
isContainer' (Proxy (ContainerFunctors fs)
forall k (t :: k). Proxy t
Proxy :: Proxy (ContainerFunctors fs))

instance IsContainer' fs '[] where
  isContainer' :: Proxy '[] -> Term fs i -> Bool
isContainer' _ = 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' :: Proxy (l : ls) -> Term fs i -> Bool
isContainer' _ t :: 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 _  -> Bool
True
                       Nothing -> Proxy ls -> Term fs i -> Bool
forall (fs :: [(* -> *) -> * -> *]) (l :: [(* -> *) -> * -> *]) i.
IsContainer' fs l =>
Proxy l -> Term fs i -> Bool
isContainer' (Proxy ls
forall k (t :: k). Proxy t
Proxy :: Proxy ls) Term fs i
t

    where go :: forall lab. Term fs lab -> Maybe (l (Term fs) lab)
          go :: Term fs lab -> Maybe (l (Term fs) lab)
go = 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 :: AnnTerm a fs l -> Bool
labeledIsContainer = Term fs l -> Bool
forall (fs :: [(* -> *) -> * -> *]) i.
IsContainer fs =>
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
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA


data EnterExitPair fs l = EnterExitPair { EnterExitPair fs l -> CfgNode fs
enter :: CfgNode fs
                                        , 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 ent :: CfgNode fs
ent ex :: CfgNode fs
ex) = "(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 -> 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]
++ ")"
  show (SubPairs t :: Sum fs (EnterExitPair fs) l
t) = "(SubPairs " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sum fs (K String) l -> String
forall (f :: (* -> *) -> * -> *).
ShowHF f =>
f (K String) :=> String
showHF' ((EnterExitPair fs :-> K String)
-> Sum fs (EnterExitPair fs) l -> Sum fs (K String) l
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]
++ ")"
  show EmptyEnterExit = "EmptyEnterExit"

mapEnterExitPair :: (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)
-> EnterExitPair fs l -> EnterExitPair gs l
mapEnterExitPair f :: forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f EmptyEnterExit = EnterExitPair gs l
forall (fs :: [(* -> *) -> * -> *]) l. EnterExitPair fs l
EmptyEnterExit
mapEnterExitPair f :: forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f (EnterExitPair n :: CfgNode fs
n x :: CfgNode fs
x) = CfgNode gs -> CfgNode gs -> EnterExitPair gs l
forall (fs :: [(* -> *) -> * -> *]) 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 :: [(* -> *) -> * -> *]) (gs :: [(* -> *) -> * -> *]).
All HFunctor fs =>
(forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> CfgNode fs -> CfgNode gs
mapCfgNode 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 :: [(* -> *) -> * -> *]) (gs :: [(* -> *) -> * -> *]).
All HFunctor fs =>
(forall (e :: * -> *) i. Sum fs e i -> Sum gs e i)
-> CfgNode fs -> CfgNode gs
mapCfgNode forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f CfgNode fs
x)
mapEnterExitPair f :: forall (e :: * -> *) i. Sum fs e i -> Sum gs e i
f (SubPairs t :: Sum fs (EnterExitPair fs) l
t) = Sum gs (EnterExitPair gs) l -> EnterExitPair gs l
forall (fs :: [(* -> *) -> * -> *]) 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) l -> Sum fs (EnterExitPair gs) l
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 :: [(* -> *) -> * -> *]) (gs :: [(* -> *) -> * -> *]) 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) Sum fs (EnterExitPair fs) l
t

iSubPairs ::  (f' :-<: fs) => f' (EnterExitPair fs) l -> EnterExitPair fs l
iSubPairs :: f' (EnterExitPair fs) l -> EnterExitPair fs l
iSubPairs x :: f' (EnterExitPair fs) l
x = Sum fs (EnterExitPair fs) l -> EnterExitPair fs l
forall (fs :: [(* -> *) -> * -> *]) l.
Sum fs (EnterExitPair fs) l -> EnterExitPair fs l
SubPairs (f' (EnterExitPair fs) l -> Sum fs (EnterExitPair fs) l
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 :: EnterExitPair fs [l] -> [EnterExitPair fs l]
extractEEPList (SubPairs ps :: 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 x :: EnterExitPair fs l
x xs :: EnterExitPair fs [l]
xs) -> EnterExitPair fs l
x EnterExitPair fs l -> [EnterExitPair fs l] -> [EnterExitPair fs l]
forall a. a -> [a] -> [a]
: EnterExitPair fs [l] -> [EnterExitPair fs l]
forall (fs :: [(* -> *) -> * -> *]) l.
(ListF :-<: fs, Typeable l) =>
EnterExitPair fs [l] -> [EnterExitPair fs l]
extractEEPList EnterExitPair fs [l]
xs
    Just NilF         -> []

  where go :: Sum fs e [l] -> Maybe (ListF e [l])
        go :: Sum fs e [l] -> Maybe (ListF e [l])
go = Sum fs e [l] -> Maybe (ListF e [l])
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 :: EnterExitPair fs (a, b) -> (EnterExitPair fs a, EnterExitPair fs b)
extractEEPPair (SubPairs ps :: 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 x :: EnterExitPair fs i
x y :: 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 :: Sum fs e (a, b) -> Maybe (PairF e (a, b))
go = Sum fs e (a, b) -> Maybe (PairF e (a, b))
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 :: m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe m :: m (EnterExitPair fs (Maybe l))
m = do
  EnterExitPair fs (Maybe l)
p' <- m (EnterExitPair fs (Maybe l))
m
  let SubPairs p :: Sum fs (EnterExitPair fs) (Maybe l)
p = EnterExitPair fs (Maybe l)
p'
  Maybe (EnterExitPair fs l) -> m (Maybe (EnterExitPair fs l))
forall (m :: * -> *) a. Monad m => a -> m 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 (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 :: CfgNode fs -> EnterExitPair fs l
identEnterExit n :: CfgNode fs
n = CfgNode fs -> CfgNode fs -> EnterExitPair fs l
forall (fs :: [(* -> *) -> * -> *]) 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 :: EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit p :: EnterExitPair fs i
p@(EnterExitPair n :: CfgNode fs
n x :: CfgNode fs
x) = EnterExitPair fs j -> m (EnterExitPair fs j)
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 :: [(* -> *) -> * -> *]) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode fs
n CfgNode fs
x
collapseEnterExit EmptyEnterExit = EnterExitPair fs j -> m (EnterExitPair fs j)
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair fs j
forall (fs :: [(* -> *) -> * -> *]) l. EnterExitPair fs l
EmptyEnterExit
collapseEnterExit (SubPairs subCfgs :: Sum fs (EnterExitPair fs) i
subCfgs) =
    (EnterExitPair fs
 :=> (m (EnterExitPair fs j) -> m (EnterExitPair fs j)))
-> m (EnterExitPair fs j)
-> Sum fs (EnterExitPair fs) i
-> m (EnterExitPair fs j)
forall (h :: (* -> *) -> * -> *) (a :: * -> *) b.
HFoldable h =>
(a :=> (b -> b)) -> b -> h a :=> b
hfoldr (\k :: EnterExitPair fs i
k t :: 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 (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 :: [(* -> *) -> * -> *]) (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 (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair fs j
forall (fs :: [(* -> *) -> * -> *]) 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 :: EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit p1 :: EnterExitPair fs i
p1 p2 :: EnterExitPair fs j
p2 = do
  EnterExitPair fs k
p1' <- EnterExitPair fs i -> m (EnterExitPair fs k)
forall s (fs :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) (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
    EmptyEnterExit                    -> EnterExitPair fs k -> m (EnterExitPair fs k)
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair fs k
p2'
    EnterExitPair {enter :: forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter=CfgNode fs
n1, exit :: forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit=CfgNode fs
x1} -> case EnterExitPair fs k
p2' of
      EmptyEnterExit                    -> EnterExitPair fs k -> m (EnterExitPair fs k)
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair fs k
p1'
      EnterExitPair {enter :: forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter=CfgNode fs
n2, exit :: forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit=CfgNode fs
x2} -> do
          (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (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 :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode fs
x1 CfgNode fs
n2
          EnterExitPair fs k -> m (EnterExitPair fs k)
forall (m :: * -> *) a. Monad m => a -> m a
return (EnterExitPair fs k -> m (EnterExitPair fs k))
-> EnterExitPair fs k -> m (EnterExitPair fs k)
forall a b. (a -> b) -> a -> b
$ CfgNode fs -> CfgNode fs -> EnterExitPair fs k
forall (fs :: [(* -> *) -> * -> *]) 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 :: f (Term gs :*: t) :-> (Term gs :*: f t)
collapseFProdG t :: 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 (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) i -> f (Term gs) i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (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) i -> f t i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (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 :: f (Term gs :*: t) :-> (Term gs :*: f t)
collapseFProd = f (Term gs :*: t) i -> (:*:) (Term gs) (f t) i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *])
       (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' :: (:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' t :: (:&:) f a (AnnTerm a gs :*: t) i
t@(x :: f (AnnTerm a gs :*: t) i
x :&: _) = ((:&:) (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) i -> (:&:) f a (AnnTerm a gs) i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (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) i -> f t i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (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' :: (:&:) f a (AnnTerm a gs :*: t) :-> AnnTerm a gs
fprodFst' ((:&:) f a (AnnTerm a gs :*: t) i -> (:*:) (AnnTerm a gs) (f t) i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> t :: AnnTerm a gs i
t :*: _) = 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 { 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 :: f (HState s (EnterExitPair gs)) i -> State s (EnterExitPair gs j)
runSubCfgs subCfgs :: f (HState s (EnterExitPair gs)) i
subCfgs = do
  f (EnterExitPair gs) i
x <- NatM
  (StateT s Identity)
  (HState s (EnterExitPair gs))
  (EnterExitPair gs)
-> f (HState s (EnterExitPair gs)) i
-> StateT s Identity (f (EnterExitPair gs) i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM 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 :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) l.
Sum fs (EnterExitPair fs) l -> EnterExitPair fs l
SubPairs (f (EnterExitPair gs) i -> Sum gs (EnterExitPair gs) i
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 :: 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
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: AnnTerm Label gs i
t :*: subCfgs :: 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 :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) 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 :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) 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 :: [(* -> *) -> * -> *]) (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 :: [(* -> *) -> * -> *]) 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 :: 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
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: AnnTerm Label gs i
t :*: subCfgs :: f (HState s (EnterExitPair gs)) i
subCfgs)) =
  if AnnTerm Label gs i -> Bool
forall (fs :: [(* -> *) -> * -> *]) 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
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) 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 :: [(* -> *) -> * -> *]) 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 :: [(* -> *) -> * -> *]) 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 i -> State s (EnterExitPair gs i)
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair gs i
forall (fs :: [(* -> *) -> * -> *]) l. EnterExitPair fs l
EmptyEnterExit
  else if AnnTerm Label gs i -> Bool
forall (fs :: [(* -> *) -> * -> *]) 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 :: [(* -> *) -> * -> *]) 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)
-> f (HState s (EnterExitPair gs)) i
-> StateT s Identity (f (EnterExitPair gs) i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM 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 :: [(* -> *) -> * -> *]) 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 :: (:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs)) i
-> HState s (EnterExitPair gs) i
constructCfg = (:&:)
  f Label (HFix (Sum gs :&: Label) :*: HState s (EnterExitPair gs)) i
-> HState s (EnterExitPair gs) i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) 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 :: (:&:)
  (Sum fs)
  Label
  (HFix (Sum g :&: Label) :*: HState s (EnterExitPair g))
  i
-> HState s (EnterExitPair g) i
constructCfg = Proxy (ConstructCfg g s)
-> (forall (f :: (* -> *) -> * -> *).
    ConstructCfg g s f =>
    (:&:)
      f Label (HFix (Sum g :&: Label) :*: HState s (EnterExitPair g)) i
    -> HState s (EnterExitPair g) i)
-> (:&:)
     (Sum fs)
     Label
     (HFix (Sum g :&: Label) :*: HState s (EnterExitPair g))
     i
-> HState s (EnterExitPair g) i
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) a (e :: * -> *) l t.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => (:&:) f a e l -> t)
-> (:&:) (Sum fs) a e l
-> t
caseCxt' (Proxy (ConstructCfg g s)
forall k (t :: k). Proxy t
Proxy @(ConstructCfg g s)) forall (gs :: [(* -> *) -> * -> *]) s (f :: (* -> *) -> * -> *).
ConstructCfg gs s f =>
PreRAlg
  (f :&: Label) (Sum gs :&: Label) (HState s (EnterExitPair gs))
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 (f :: [(* -> *) -> * -> *]) :: *

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 :: TermLab fs l -> Cfg fs
makeCfg t :: 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))
-> TermLab fs l -> HState (CfgState fs) (EnterExitPair fs) l
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
RAlg f a -> HFix f :-> a
para forall (gs :: [(* -> *) -> * -> *]) 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 :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg
  where
    initState :: CfgState fs
initState = Proxy fs -> CfgState fs
forall (fs :: [(* -> *) -> * -> *]).
CfgInitState fs =>
Proxy fs -> CfgState fs
cfgInitState (Proxy fs
forall k (t :: k). Proxy t
Proxy :: Proxy fs)