{-# 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)
| 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)
extractEEPList :: forall fs l. (ListF :-<: fs, Typeable l) => EnterExitPair fs [l] -> [EnterExitPair fs l]
(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)
(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
extractEEPMaybe :: (All (KExtractF' Maybe) fs, Monad m) => m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
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
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
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
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
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)