{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Cubix.Language.C.Parametric.Common.Cfg () where

#ifndef ONLY_ONE_LANGUAGE
import Control.Monad ( liftM, liftM2, forM_ )
import Control.Monad.State ( State, MonadState )

import Control.Lens ( makeLenses, (%=), (.=), use, uses )

import Data.List as List ( (\\) )
import Data.Map as Map ( Map, partitionWithKey, delete )
import Data.Set as Set ( Set, member, empty, fromList )

import Data.Comp.Multi ( stripA, remA, (:*:)(..), ffst, fsnd, project, proj, E(..), (:&:)(..), subterms, (:-<:), Cxt (..) )

import Cubix.Language.Info

import Cubix.Language.C.Parametric.Common.Types as C
import Cubix.Language.C.Parametric.Full.Types as F
import Cubix.Language.Parametric.InjF
import Cubix.Language.Parametric.Semantics.Cfg
import Cubix.Language.Parametric.Syntax as P

data CCfgState = CCfgState {
                   CCfgState -> Cfg MCSig
_ccs_cfg       :: Cfg MCSig
                 , CCfgState -> LabelGen
_ccs_labeler   :: LabelGen
                 , CCfgState -> LoopStack
_ccs_stack     :: LoopStack
                 , CCfgState -> LabelMap
_ccs_goto_labs :: LabelMap
                 , CCfgState -> LocalLabels
_ccs_local_goto_labs :: LocalLabels
                 }

type LocalLabels = Set String

makeLenses ''CCfgState

-----------------------------------------------------------------------------------
---------------           Labelling mechanism              ------------------------
-----------------------------------------------------------------------------------

-- With a GNU C extension it is possible to have nested function definitions.
-- From GCC docs:
-- GCC allows you to declare local labels in any nested block scope.
-- A local label is just like an ordinary label, but you can only reference it
-- (with a goto statement, or by taking its address) within the block in which it is declared.
-- Local label declarations also make the labels they declare visible to nested functions.

type LabelMap0 = Map.Map String (Label, [Label])

cLabeledBlockLabMap ::
  ( Monad m
  , MonadState CCfgState m
  ) => [String] -> m a -> m a
cLabeledBlockLabMap :: [String] -> m a -> m a
cLabeledBlockLabMap lls :: [String]
lls act :: m a
act = do
  let curLocalLabs :: LocalLabels
curLocalLabs = [String] -> LocalLabels
forall a. Ord a => [a] -> Set a
Set.fromList [String]
lls
  LocalLabels -> m a -> m a
forall (m :: * -> *) a.
(Monad m, MonadState CCfgState m) =>
LocalLabels -> m a -> m a
withExtendedLocalLabels LocalLabels
curLocalLabs (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
    -- NOTE: resets outer labels which shadows local labels in this block
    --       and after the work is done, restores it.
    (locLabMap :: LabelMap0
locLabMap, labMap :: LabelMap0
labMap) <- LensLike' (Const (LabelMap0, LabelMap0)) CCfgState LabelMap0
-> (LabelMap0 -> (LabelMap0, LabelMap0))
-> m (LabelMap0, LabelMap0)
forall s (m :: * -> *) r a.
MonadState s m =>
LensLike' (Const r) s a -> (a -> r) -> m r
uses LensLike' (Const (LabelMap0, LabelMap0)) CCfgState LabelMap0
forall c. HasLabelMap c => Lens' c LabelMap0
label_map (LocalLabels -> LabelMap0 -> (LabelMap0, LabelMap0)
resetLabMap LocalLabels
curLocalLabs)
    (LabelMap0 -> Identity LabelMap0)
-> CCfgState -> Identity CCfgState
forall c. HasLabelMap c => Lens' c LabelMap0
label_map ((LabelMap0 -> Identity LabelMap0)
 -> CCfgState -> Identity CCfgState)
-> LabelMap0 -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= LabelMap0
labMap
    a
res <- m a
act
    (LabelMap0 -> Identity LabelMap0)
-> CCfgState -> Identity CCfgState
forall c. HasLabelMap c => Lens' c LabelMap0
label_map ((LabelMap0 -> Identity LabelMap0)
 -> CCfgState -> Identity CCfgState)
-> (LabelMap0 -> LabelMap0) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= LocalLabels -> LabelMap0 -> LabelMap0 -> LabelMap0
restoreLocalLabMap LocalLabels
curLocalLabs LabelMap0
locLabMap
    a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res

withExtendedLocalLabels :: (Monad m, MonadState CCfgState m) => LocalLabels -> m a -> m a
withExtendedLocalLabels :: LocalLabels -> m a -> m a
withExtendedLocalLabels lls :: LocalLabels
lls act :: m a
act = do
  LocalLabels
prevLocalLabs <- Getting LocalLabels CCfgState LocalLabels -> m LocalLabels
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting LocalLabels CCfgState LocalLabels
Lens' CCfgState LocalLabels
ccs_local_goto_labs
  (LocalLabels -> Identity LocalLabels)
-> CCfgState -> Identity CCfgState
Lens' CCfgState LocalLabels
ccs_local_goto_labs ((LocalLabels -> Identity LocalLabels)
 -> CCfgState -> Identity CCfgState)
-> LocalLabels -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= LocalLabels
prevLocalLabs LocalLabels -> LocalLabels -> LocalLabels
forall a. Semigroup a => a -> a -> a
<> LocalLabels
lls
  a
res <- m a
act
  (LocalLabels -> Identity LocalLabels)
-> CCfgState -> Identity CCfgState
Lens' CCfgState LocalLabels
ccs_local_goto_labs ((LocalLabels -> Identity LocalLabels)
 -> CCfgState -> Identity CCfgState)
-> LocalLabels -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= LocalLabels
prevLocalLabs
  a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res

-- NOTE: A Local label map is a label map which has
--       local labels as it's keys.

-- | Reset label map, returning (shadowed) local label map and rest.
resetLabMap :: LocalLabels -> LabelMap0 -> (LabelMap0, LabelMap0)
resetLabMap :: LocalLabels -> LabelMap0 -> (LabelMap0, LabelMap0)
resetLabMap = LocalLabels -> LabelMap0 -> (LabelMap0, LabelMap0)
splitLabMap

-- | Restores the (shadowed) local label map as it was previously.
restoreLocalLabMap :: LocalLabels -> LabelMap0 -> LabelMap0 -> LabelMap0
restoreLocalLabMap :: LocalLabels -> LabelMap0 -> LabelMap0 -> LabelMap0
restoreLocalLabMap lls :: LocalLabels
lls rlm :: LabelMap0
rlm lm :: LabelMap0
lm = LocalLabels -> LabelMap0 -> LabelMap0
deleteLocalLabMap LocalLabels
lls LabelMap0
lm LabelMap0 -> LabelMap0 -> LabelMap0
forall a. Semigroup a => a -> a -> a
<> LabelMap0
rlm

splitLabMap :: LocalLabels -> LabelMap0 -> (LabelMap0, LabelMap0)
splitLabMap :: LocalLabels -> LabelMap0 -> (LabelMap0, LabelMap0)
splitLabMap lls :: LocalLabels
lls lm :: LabelMap0
lm = (String -> (Label, [Label]) -> Bool)
-> LabelMap0 -> (LabelMap0, LabelMap0)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey String -> (Label, [Label]) -> Bool
go LabelMap0
lm
  where go :: String -> (Label, [Label]) -> Bool
go k :: String
k _ = String
k String -> LocalLabels -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` LocalLabels
lls

getLocalLabMap :: LocalLabels -> LabelMap0 -> LabelMap0
getLocalLabMap :: LocalLabels -> LabelMap0 -> LabelMap0
getLocalLabMap lls :: LocalLabels
lls lm :: LabelMap0
lm = (LabelMap0, LabelMap0) -> LabelMap0
forall a b. (a, b) -> a
fst (LocalLabels -> LabelMap0 -> (LabelMap0, LabelMap0)
splitLabMap LocalLabels
lls LabelMap0
lm)

deleteLocalLabMap :: LocalLabels -> LabelMap0 -> LabelMap0
deleteLocalLabMap :: LocalLabels -> LabelMap0 -> LabelMap0
deleteLocalLabMap lls :: LocalLabels
lls lm :: LabelMap0
lm = (LabelMap0, LabelMap0) -> LabelMap0
forall a b. (a, b) -> b
snd (LocalLabels -> LabelMap0 -> (LabelMap0, LabelMap0)
splitLabMap LocalLabels
lls LabelMap0
lm)

functionDefLabelMap ::
  ( Monad m
  , MonadState CCfgState m
  ) => m a -> m a
functionDefLabelMap :: m a -> m a
functionDefLabelMap act :: m a
act = do
  LabelMap0
oldLabMap <- Getting LabelMap0 CCfgState LabelMap0 -> m LabelMap0
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting LabelMap0 CCfgState LabelMap0
forall c. HasLabelMap c => Lens' c LabelMap0
label_map
  LocalLabels
localLabs <- Getting LocalLabels CCfgState LocalLabels -> m LocalLabels
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting LocalLabels CCfgState LocalLabels
Lens' CCfgState LocalLabels
ccs_local_goto_labs
  -- NOTE: Let the (outer) local labels alone
  --       be seen inside the function.
  (LabelMap0 -> Identity LabelMap0)
-> CCfgState -> Identity CCfgState
forall c. HasLabelMap c => Lens' c LabelMap0
label_map ((LabelMap0 -> Identity LabelMap0)
 -> CCfgState -> Identity CCfgState)
-> (LabelMap0 -> LabelMap0) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= LocalLabels -> LabelMap0 -> LabelMap0
getLocalLabMap LocalLabels
localLabs
  a
res <- m a
act
  -- NOTE: Propogate the local labels outwards
  --       while the restoring old map.
  (LabelMap0 -> Identity LabelMap0)
-> CCfgState -> Identity CCfgState
forall c. HasLabelMap c => Lens' c LabelMap0
label_map ((LabelMap0 -> Identity LabelMap0)
 -> CCfgState -> Identity CCfgState)
-> (LabelMap0 -> LabelMap0) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= LabelMap0 -> LabelMap0 -> LabelMap0
forall a. Monoid a => a -> a -> a
mappend LabelMap0
oldLabMap (LabelMap0 -> LabelMap0)
-> (LabelMap0 -> LabelMap0) -> LabelMap0 -> LabelMap0
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalLabels -> LabelMap0 -> LabelMap0
getLocalLabMap LocalLabels
localLabs
  a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
res

emptyLocalLabels :: LocalLabels
emptyLocalLabels :: LocalLabels
emptyLocalLabels = LocalLabels
forall a. Set a
Set.empty

-----------------------------------------------------------------------------------
---------------           CfgConstruction Instances        ------------------------
-----------------------------------------------------------------------------------


instance HasCurCfg CCfgState MCSig where cur_cfg :: (Cfg MCSig -> f (Cfg MCSig)) -> CCfgState -> f CCfgState
cur_cfg = (Cfg MCSig -> f (Cfg MCSig)) -> CCfgState -> f CCfgState
Lens' CCfgState (Cfg MCSig)
ccs_cfg
instance HasLabelGen CCfgState where labelGen :: (LabelGen -> f LabelGen) -> CCfgState -> f CCfgState
labelGen = (LabelGen -> f LabelGen) -> CCfgState -> f CCfgState
Lens' CCfgState LabelGen
ccs_labeler
instance HasLoopStack CCfgState where loopStack :: (LoopStack -> f LoopStack) -> CCfgState -> f CCfgState
loopStack = (LoopStack -> f LoopStack) -> CCfgState -> f CCfgState
Lens' CCfgState LoopStack
ccs_stack
instance HasLabelMap CCfgState where labelMap :: (LabelMap -> f LabelMap) -> CCfgState -> f CCfgState
labelMap = (LabelMap -> f LabelMap) -> CCfgState -> f CCfgState
Lens' CCfgState LabelMap
ccs_goto_labs


type instance ComputationSorts MCSig = '[CStatementL, CExpressionL, CCompoundBlockItemL, [BlockItemL]]
type instance SuspendedComputationSorts MCSig = '[FunctionDefL]
type instance ContainerFunctors MCSig = '[PairF, TripleF, ListF, MaybeF, EitherF]
type instance CfgState MCSig = CCfgState

nameString :: MCTermLab F.IdentL -> String
nameString :: MCTermLab IdentL -> String
nameString (MCTermLab IdentL -> Cxt NoHole (Sum MCSig) (K ()) IdentL
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA -> Cxt NoHole (Sum MCSig) (K ()) IdentL
-> Maybe (CxtS NoHole MCSig (K ()) IdentL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
projF -> Just (Ident' n :: String
n)) = String
n

singleton :: a -> [a]
singleton :: a -> [a]
singleton = a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return

extractForInit :: (HasCurCfg s MCSig) => HState s (EnterExitPair MCSig) (Either (Maybe CExpressionL) CDeclarationL) -> State s (Maybe (EnterExitPair MCSig ()))
extractForInit :: HState
  s (EnterExitPair MCSig) (Either (Maybe CExpressionL) CDeclarationL)
-> State s (Maybe (EnterExitPair MCSig ()))
extractForInit m :: HState
  s (EnterExitPair MCSig) (Either (Maybe CExpressionL) CDeclarationL)
m = do
  EnterExitPair MCSig (Either (Maybe CExpressionL) CDeclarationL)
p1' <- HState
  s (EnterExitPair MCSig) (Either (Maybe CExpressionL) CDeclarationL)
-> State
     s (EnterExitPair MCSig (Either (Maybe CExpressionL) CDeclarationL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState
  s (EnterExitPair MCSig) (Either (Maybe CExpressionL) CDeclarationL)
m
  let SubPairs p1 :: Sum
  MCSig
  (EnterExitPair MCSig)
  (Either (Maybe CExpressionL) CDeclarationL)
p1 = EnterExitPair MCSig (Either (Maybe CExpressionL) CDeclarationL)
p1'
  case Sum
  MCSig
  (EnterExitPair MCSig)
  (Either (Maybe CExpressionL) CDeclarationL)
-> Either
     (EnterExitPair MCSig (Maybe CExpressionL))
     (EnterExitPair MCSig CDeclarationL)
forall (f :: * -> * -> *) (g :: (* -> *) -> * -> *) (e :: * -> *) l
       l'.
KExtractF2' f g =>
g e (f l l') -> f (e l) (e l')
kextractF2' Sum
  MCSig
  (EnterExitPair MCSig)
  (Either (Maybe CExpressionL) CDeclarationL)
p1 of
    Left x :: EnterExitPair MCSig (Maybe CExpressionL)
x  -> (EnterExitPair MCSig CExpressionL
 -> StateT s Identity (EnterExitPair MCSig ()))
-> Maybe (EnterExitPair MCSig CExpressionL)
-> State s (Maybe (EnterExitPair MCSig ()))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM EnterExitPair MCSig CExpressionL
-> StateT s Identity (EnterExitPair MCSig ())
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 (Maybe (EnterExitPair MCSig CExpressionL)
 -> State s (Maybe (EnterExitPair MCSig ())))
-> StateT s Identity (Maybe (EnterExitPair MCSig CExpressionL))
-> State s (Maybe (EnterExitPair MCSig ()))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (StateT s Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT s Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT s Identity (EnterExitPair MCSig (Maybe CExpressionL))
 -> StateT s Identity (Maybe (EnterExitPair MCSig CExpressionL)))
-> StateT s Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT s Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall a b. (a -> b) -> a -> b
$ EnterExitPair MCSig (Maybe CExpressionL)
-> StateT s Identity (EnterExitPair MCSig (Maybe CExpressionL))
forall (m :: * -> *) a. Monad m => a -> m a
return EnterExitPair MCSig (Maybe CExpressionL)
x)
    Right x :: EnterExitPair MCSig CDeclarationL
x -> EnterExitPair MCSig () -> Maybe (EnterExitPair MCSig ())
forall a. a -> Maybe a
Just (EnterExitPair MCSig () -> Maybe (EnterExitPair MCSig ()))
-> StateT s Identity (EnterExitPair MCSig ())
-> State s (Maybe (EnterExitPair MCSig ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EnterExitPair MCSig CDeclarationL
-> StateT s Identity (EnterExitPair MCSig ())
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 MCSig CDeclarationL
x


-- TODO: test this for Duff's device (once we have switches working)
instance ConstructCfg MCSig CCfgState CStatement where
  constructCfg :: (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> HState CCfgState (EnterExitPair MCSig) i
constructCfg t :: (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t@((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> CStatement
     (HFix (Sum MCSig :&: Label)
      :*: HState CCfgState (EnterExitPair MCSig))
     i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> CLabel (nam :: MCTermLab IdentL
nam :*: _) (_ :*: mStatEE :: HState CCfgState (EnterExitPair MCSig) CStatementL
mStatEE) _ _) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ do
    -- It's easiest to model it as if the label and the ensuing statement are separate
   EnterExitPair MCSig Any
labEE <- TermLab MCSig i
-> String -> StateT CCfgState Identity (EnterExitPair MCSig Any)
forall (gs :: [(* -> *) -> * -> *]) s (m :: * -> *) l i.
(MonadState s m, HasLabelMap s, CfgComponent gs s) =>
TermLab gs l -> String -> m (EnterExitPair gs i)
constructCfgLabel ((:*:)
  (HFix (Sum MCSig :&: Label))
  (CStatement (HState CCfgState (EnterExitPair MCSig)))
  i
-> TermLab MCSig i
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst ((:*:)
   (HFix (Sum MCSig :&: Label))
   (CStatement (HState CCfgState (EnterExitPair MCSig)))
   i
 -> TermLab MCSig i)
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
-> TermLab MCSig i
forall a b. (a -> b) -> a -> b
$ (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t) (MCTermLab IdentL -> String
nameString MCTermLab IdentL
nam)
   EnterExitPair MCSig CStatementL
statEE <- HState CCfgState (EnterExitPair MCSig) CStatementL
-> State CCfgState (EnterExitPair MCSig CStatementL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CStatementL
mStatEE
   EnterExitPair MCSig Any
-> EnterExitPair MCSig CStatementL
-> State CCfgState (EnterExitPair MCSig 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 MCSig Any
labEE EnterExitPair MCSig CStatementL
statEE

  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CIf e :: HState CCfgState (EnterExitPair MCSig) CExpressionL
e thn :: HState CCfgState (EnterExitPair MCSig) CStatementL
thn optElse :: HState CCfgState (EnterExitPair MCSig) (Maybe CStatementL)
optElse _))) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i
-> StateT
     CCfgState
     Identity
     [(EnterExitPair MCSig CExpressionL,
       EnterExitPair MCSig CStatementL)]
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CStatementL))
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i j k.
(MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m [(EnterExitPair gs i, EnterExitPair gs j)]
-> m (Maybe (EnterExitPair gs k))
-> m (EnterExitPair gs l)
constructCfgIfElseIfElse TermLab MCSig i
t (((EnterExitPair MCSig CExpressionL,
  EnterExitPair MCSig CStatementL)
 -> [(EnterExitPair MCSig CExpressionL,
      EnterExitPair MCSig CStatementL)])
-> StateT
     CCfgState
     Identity
     (EnterExitPair MCSig CExpressionL, EnterExitPair MCSig CStatementL)
-> StateT
     CCfgState
     Identity
     [(EnterExitPair MCSig CExpressionL,
       EnterExitPair MCSig CStatementL)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (EnterExitPair MCSig CExpressionL, EnterExitPair MCSig CStatementL)
-> [(EnterExitPair MCSig CExpressionL,
     EnterExitPair MCSig CStatementL)]
forall a. a -> [a]
singleton (StateT
   CCfgState
   Identity
   (EnterExitPair MCSig CExpressionL, EnterExitPair MCSig CStatementL)
 -> StateT
      CCfgState
      Identity
      [(EnterExitPair MCSig CExpressionL,
        EnterExitPair MCSig CStatementL)])
-> StateT
     CCfgState
     Identity
     (EnterExitPair MCSig CExpressionL, EnterExitPair MCSig CStatementL)
-> StateT
     CCfgState
     Identity
     [(EnterExitPair MCSig CExpressionL,
       EnterExitPair MCSig CStatementL)]
forall a b. (a -> b) -> a -> b
$ (EnterExitPair MCSig CExpressionL
 -> EnterExitPair MCSig CStatementL
 -> (EnterExitPair MCSig CExpressionL,
     EnterExitPair MCSig CStatementL))
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> State CCfgState (EnterExitPair MCSig CStatementL)
-> StateT
     CCfgState
     Identity
     (EnterExitPair MCSig CExpressionL, EnterExitPair MCSig CStatementL)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
e) (HState CCfgState (EnterExitPair MCSig) CStatementL
-> State CCfgState (EnterExitPair MCSig CStatementL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CStatementL
thn)) (StateT CCfgState Identity (EnterExitPair MCSig (Maybe CStatementL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CStatementL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT
   CCfgState Identity (EnterExitPair MCSig (Maybe CStatementL))
 -> StateT
      CCfgState Identity (Maybe (EnterExitPair MCSig CStatementL)))
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CStatementL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CStatementL))
forall a b. (a -> b) -> a -> b
$ HState CCfgState (EnterExitPair MCSig) (Maybe CStatementL)
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CStatementL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) (Maybe CStatementL)
optElse)
  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CWhile e :: HState CCfgState (EnterExitPair MCSig) CExpressionL
e b :: HState CCfgState (EnterExitPair MCSig) CStatementL
b False _))) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> State CCfgState (EnterExitPair MCSig CStatementL)
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i j k.
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (EnterExitPair gs i)
-> m (EnterExitPair gs j)
-> m (EnterExitPair gs k)
constructCfgWhile   TermLab MCSig i
t (HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
e) (HState CCfgState (EnterExitPair MCSig) CStatementL
-> State CCfgState (EnterExitPair MCSig CStatementL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CStatementL
b)
  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CWhile e :: HState CCfgState (EnterExitPair MCSig) CExpressionL
e b :: HState CCfgState (EnterExitPair MCSig) CStatementL
b True _)))  = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> State CCfgState (EnterExitPair MCSig CStatementL)
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i j k.
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (EnterExitPair gs i)
-> m (EnterExitPair gs j)
-> m (EnterExitPair gs k)
constructCfgDoWhile TermLab MCSig i
t (HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
e) (HState CCfgState (EnterExitPair MCSig) CStatementL
-> State CCfgState (EnterExitPair MCSig CStatementL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CStatementL
b)

  constructCfg t :: (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t@((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> CStatement
     (HFix (Sum MCSig :&: Label)
      :*: HState CCfgState (EnterExitPair MCSig))
     i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> CGoto (nam :: MCTermLab IdentL
nam :*: _) _) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i
-> String -> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(MonadState s m, HasLabelMap s, CfgComponent gs s) =>
TermLab gs l -> String -> m (EnterExitPair gs i)
constructCfgGoto ((:*:)
  (HFix (Sum MCSig :&: Label))
  (CStatement (HState CCfgState (EnterExitPair MCSig)))
  i
-> TermLab MCSig i
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst ((:*:)
   (HFix (Sum MCSig :&: Label))
   (CStatement (HState CCfgState (EnterExitPair MCSig)))
   i
 -> TermLab MCSig i)
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
-> TermLab MCSig i
forall a b. (a -> b) -> a -> b
$ (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t) (MCTermLab IdentL -> String
nameString MCTermLab IdentL
nam)
  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CGotoPtr e :: HState CCfgState (EnterExitPair MCSig) CExpressionL
e _))) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (Maybe (EnterExitPair gs i)) -> m (EnterExitPair gs l)
constructCfgReturn TermLab MCSig i
t ((EnterExitPair MCSig CExpressionL
 -> Maybe (EnterExitPair MCSig CExpressionL))
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM EnterExitPair MCSig CExpressionL
-> Maybe (EnterExitPair MCSig CExpressionL)
forall a. a -> Maybe a
Just (StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
 -> StateT
      CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL)))
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall a b. (a -> b) -> a -> b
$ HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
e)
  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CCont _))) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i -> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> m (EnterExitPair gs i)
constructCfgContinue TermLab MCSig i
t
  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CBreak _))) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i -> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> m (EnterExitPair gs i)
constructCfgBreak TermLab MCSig i
t
  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CReturn e :: HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
e _))) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (Maybe (EnterExitPair gs i)) -> m (EnterExitPair gs l)
constructCfgReturn TermLab MCSig i
t (StateT
  CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT
   CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
 -> StateT
      CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL)))
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall a b. (a -> b) -> a -> b
$ HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
e)

  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CFor init :: HState
  CCfgState
  (EnterExitPair MCSig)
  (Either (Maybe CExpressionL) CDeclarationL)
init cond :: HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
cond step :: HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
step body :: HState CCfgState (EnterExitPair MCSig) CStatementL
body _))) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ TermLab MCSig i
-> StateT CCfgState Identity (Maybe (EnterExitPair MCSig ()))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
-> State CCfgState (EnterExitPair MCSig CStatementL)
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l h i j k.
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (Maybe (EnterExitPair gs h))
-> m (Maybe (EnterExitPair gs i))
-> m (Maybe (EnterExitPair gs j))
-> m (EnterExitPair gs k)
-> m (EnterExitPair gs l)
constructCfgFor TermLab MCSig i
t (HState
  CCfgState
  (EnterExitPair MCSig)
  (Either (Maybe CExpressionL) CDeclarationL)
-> StateT CCfgState Identity (Maybe (EnterExitPair MCSig ()))
forall s.
HasCurCfg s MCSig =>
HState
  s (EnterExitPair MCSig) (Either (Maybe CExpressionL) CDeclarationL)
-> State s (Maybe (EnterExitPair MCSig ()))
extractForInit HState
  CCfgState
  (EnterExitPair MCSig)
  (Either (Maybe CExpressionL) CDeclarationL)
init) (StateT
  CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT
   CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
 -> StateT
      CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL)))
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall a b. (a -> b) -> a -> b
$ HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
cond) (StateT
  CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT
   CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
 -> StateT
      CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL)))
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall a b. (a -> b) -> a -> b
$ HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
step) (HState CCfgState (EnterExitPair MCSig) CStatementL
-> State CCfgState (EnterExitPair MCSig CStatementL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CStatementL
body)

  constructCfg ((:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CStatement (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (t :: TermLab MCSig i
t :*: (CSwitch exp :: HState CCfgState (EnterExitPair MCSig) CExpressionL
exp body :: HState CCfgState (EnterExitPair MCSig) CStatementL
body _))) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ do
    CfgNode MCSig
enterNode <- TermLab MCSig i
-> CfgNodeType -> StateT CCfgState Identity (CfgNode MCSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab MCSig i
t CfgNodeType
EnterNode
    CfgNode MCSig
exitNode  <- TermLab MCSig i
-> CfgNodeType -> StateT CCfgState Identity (CfgNode MCSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab MCSig i
t CfgNodeType
ExitNode

    EnterExitPair MCSig CExpressionL
expEE <- HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
exp

    CfgNode MCSig -> StateT CCfgState Identity ()
forall s (m :: * -> *) (fs :: [(* -> *) -> * -> *]).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> m ()
pushBreakNode CfgNode MCSig
exitNode
    EnterExitPair MCSig CStatementL
bodyEE <- HState CCfgState (EnterExitPair MCSig) CStatementL
-> State CCfgState (EnterExitPair MCSig CStatementL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CStatementL
body
    StateT CCfgState Identity ()
forall s (m :: * -> *). (MonadState s m, HasLoopStack s) => m ()
popBreakNode

    (Cfg MCSig -> Identity (Cfg MCSig))
-> CCfgState -> Identity CCfgState
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig))
 -> CCfgState -> Identity CCfgState)
-> (Cfg MCSig -> Cfg MCSig) -> StateT CCfgState Identity ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode MCSig
enterNode (EnterExitPair MCSig CExpressionL -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MCSig CExpressionL
expEE)
    (Cfg MCSig -> Identity (Cfg MCSig))
-> CCfgState -> Identity CCfgState
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig))
 -> CCfgState -> Identity CCfgState)
-> (Cfg MCSig -> Cfg MCSig) -> StateT CCfgState Identity ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig CExpressionL -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig CExpressionL
expEE) (EnterExitPair MCSig CStatementL -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MCSig CStatementL
bodyEE)
    (Cfg MCSig -> Identity (Cfg MCSig))
-> CCfgState -> Identity CCfgState
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig))
 -> CCfgState -> Identity CCfgState)
-> (Cfg MCSig -> Cfg MCSig) -> StateT CCfgState Identity ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig CStatementL -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig CStatementL
bodyEE) CfgNode MCSig
exitNode

    [E (HFix (Sum MCSig :&: Label))]
-> (E (HFix (Sum MCSig :&: Label)) -> StateT CCfgState Identity ())
-> StateT CCfgState Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [E (HFix (Sum MCSig :&: Label))]
cases ((E (HFix (Sum MCSig :&: Label)) -> StateT CCfgState Identity ())
 -> StateT CCfgState Identity ())
-> (E (HFix (Sum MCSig :&: Label)) -> StateT CCfgState Identity ())
-> StateT CCfgState Identity ()
forall a b. (a -> b) -> a -> b
$ \(E case0 :: MCTermLab i
case0) -> do
      Cfg MCSig
ccfg <- Getting (Cfg MCSig) CCfgState (Cfg MCSig)
-> StateT CCfgState Identity (Cfg MCSig)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Cfg MCSig) CCfgState (Cfg MCSig)
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg
      let Just enCase :: CfgNode MCSig
enCase = Cfg MCSig -> CfgNodeType -> MCTermLab i -> Maybe (CfgNode MCSig)
forall (fs :: [(* -> *) -> * -> *]) l.
Cfg fs -> CfgNodeType -> TermLab fs l -> Maybe (CfgNode fs)
cfgNodeForTerm Cfg MCSig
ccfg CfgNodeType
EnterNode MCTermLab i
case0
      (Cfg MCSig -> Identity (Cfg MCSig))
-> CCfgState -> Identity CCfgState
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig))
 -> CCfgState -> Identity CCfgState)
-> (Cfg MCSig -> Cfg MCSig) -> StateT CCfgState Identity ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig CExpressionL -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig CExpressionL
expEE) CfgNode MCSig
enCase

    EnterExitPair MCSig i -> State CCfgState (EnterExitPair MCSig i)
forall (m :: * -> *) a. Monad m => a -> m a
return (EnterExitPair MCSig i -> State CCfgState (EnterExitPair MCSig i))
-> EnterExitPair MCSig i -> State CCfgState (EnterExitPair MCSig i)
forall a b. (a -> b) -> a -> b
$ CfgNode MCSig -> CfgNode MCSig -> EnterExitPair MCSig i
forall (fs :: [(* -> *) -> * -> *]) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode MCSig
enterNode CfgNode MCSig
exitNode

      where cases :: [E (HFix (Sum MCSig :&: Label))]
cases = case TermLab MCSig i
-> Maybe ((:&:) CStatement Label (HFix (Sum MCSig :&: Label)) i)
forall (f :: (* -> *) -> * -> *) l.
(f :-<: MCSig) =>
MCTermLab l -> Maybe ((:&:) f Label (HFix (Sum MCSig :&: Label)) l)
project0 TermLab MCSig i
t of
              Just ((:&:) CStatement Label (HFix (Sum MCSig :&: Label)) i
-> CStatement (HFix (Sum MCSig :&: Label)) i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> CSwitch _ b0 :: MCTermLab CStatementL
b0 _) -> MCTermLab CStatementL -> [E (HFix (Sum MCSig :&: Label))]
forall i.
HFix (Sum MCSig :&: Label) i -> [E (HFix (Sum MCSig :&: Label))]
extractCases MCTermLab CStatementL
b0

            extractCases :: HFix (Sum MCSig :&: Label) i -> [E (HFix (Sum MCSig :&: Label))]
extractCases t0 :: HFix (Sum MCSig :&: Label) i
t0 =
              let subs :: [E (HFix (Sum MCSig :&: Label))]
subs = HFix (Sum MCSig :&: Label) i -> [E (HFix (Sum MCSig :&: Label))]
forall (f :: (* -> *) -> * -> *).
HFoldable f =>
HFix f :=> [E (HFix f)]
subterms HFix (Sum MCSig :&: Label) i
t0
                  cases0 :: [E (HFix (Sum MCSig :&: Label))]
cases0 = (E (HFix (Sum MCSig :&: Label)) -> Bool)
-> [E (HFix (Sum MCSig :&: Label))]
-> [E (HFix (Sum MCSig :&: Label))]
forall a. (a -> Bool) -> [a] -> [a]
filter E (HFix (Sum MCSig :&: Label)) -> Bool
isCase [E (HFix (Sum MCSig :&: Label))]
subs
                  switches :: [E (HFix (Sum MCSig :&: Label))]
switches = (E (HFix (Sum MCSig :&: Label)) -> Bool)
-> [E (HFix (Sum MCSig :&: Label))]
-> [E (HFix (Sum MCSig :&: Label))]
forall a. (a -> Bool) -> [a] -> [a]
filter E (HFix (Sum MCSig :&: Label)) -> Bool
isSwitch [E (HFix (Sum MCSig :&: Label))]
subs
                  subcases :: [E (HFix (Sum MCSig :&: Label))]
subcases = (E (HFix (Sum MCSig :&: Label)) -> Bool)
-> [E (HFix (Sum MCSig :&: Label))]
-> [E (HFix (Sum MCSig :&: Label))]
forall a. (a -> Bool) -> [a] -> [a]
filter E (HFix (Sum MCSig :&: Label)) -> Bool
isCase ((E (HFix (Sum MCSig :&: Label))
 -> [E (HFix (Sum MCSig :&: Label))])
-> [E (HFix (Sum MCSig :&: Label))]
-> [E (HFix (Sum MCSig :&: Label))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(E e0 :: MCTermLab i
e0) -> MCTermLab i -> [E (HFix (Sum MCSig :&: Label))]
forall (f :: (* -> *) -> * -> *).
HFoldable f =>
HFix f :=> [E (HFix f)]
subterms MCTermLab i
e0) [E (HFix (Sum MCSig :&: Label))]
switches)
              in  [E (HFix (Sum MCSig :&: Label))]
cases0 [E (HFix (Sum MCSig :&: Label))]
-> [E (HFix (Sum MCSig :&: Label))]
-> [E (HFix (Sum MCSig :&: Label))]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [E (HFix (Sum MCSig :&: Label))]
subcases

            isCase :: E MCTermLab -> Bool
            isCase :: E (HFix (Sum MCSig :&: Label)) -> Bool
isCase (E (MCTermLab i
-> Maybe ((:&:) CStatement Label (HFix (Sum MCSig :&: Label)) i)
forall (f :: (* -> *) -> * -> *) l.
(f :-<: MCSig) =>
MCTermLab l -> Maybe ((:&:) f Label (HFix (Sum MCSig :&: Label)) l)
project0 -> Just ((:&:) CStatement Label (HFix (Sum MCSig :&: Label)) i
-> CStatement (HFix (Sum MCSig :&: Label)) i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> CCase {}))) = Bool
True
            isCase (E (MCTermLab i
-> Maybe ((:&:) CStatement Label (HFix (Sum MCSig :&: Label)) i)
forall (f :: (* -> *) -> * -> *) l.
(f :-<: MCSig) =>
MCTermLab l -> Maybe ((:&:) f Label (HFix (Sum MCSig :&: Label)) l)
project0 -> Just ((:&:) CStatement Label (HFix (Sum MCSig :&: Label)) i
-> CStatement (HFix (Sum MCSig :&: Label)) i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> CDefault {}))) = Bool
True
            isCase _ = Bool
False

            isSwitch :: E MCTermLab -> Bool
            isSwitch :: E (HFix (Sum MCSig :&: Label)) -> Bool
isSwitch (E (MCTermLab i
-> Maybe ((:&:) CStatement Label (HFix (Sum MCSig :&: Label)) i)
forall (f :: (* -> *) -> * -> *) l.
(f :-<: MCSig) =>
MCTermLab l -> Maybe ((:&:) f Label (HFix (Sum MCSig :&: Label)) l)
project0 -> Just ((:&:) CStatement Label (HFix (Sum MCSig :&: Label)) i
-> CStatement (HFix (Sum MCSig :&: Label)) i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> CSwitch {}))) = Bool
True
            isSwitch _ = Bool
False

            project0 :: (f :-<: MCSig) => MCTermLab l -> Maybe ((f :&: Label) MCTermLab l)
            project0 :: MCTermLab l -> Maybe ((:&:) f Label (HFix (Sum MCSig :&: Label)) l)
project0 (Term (s :: Sum MCSig (HFix (Sum MCSig :&: Label)) l
s :&: l :: Label
l)) = (f (HFix (Sum MCSig :&: Label)) l
 -> (:&:) f Label (HFix (Sum MCSig :&: Label)) l)
-> Maybe (f (HFix (Sum MCSig :&: Label)) l)
-> Maybe ((:&:) f Label (HFix (Sum MCSig :&: Label)) l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f (HFix (Sum MCSig :&: Label)) l
-> Label -> (:&:) f Label (HFix (Sum MCSig :&: Label)) l
forall k (f :: (* -> *) -> k -> *) a (g :: * -> *) (e :: k).
f g e -> a -> (:&:) f a g e
:&: Label
l) (Sum MCSig (HFix (Sum MCSig :&: Label)) l
-> Maybe (f (HFix (Sum MCSig :&: Label)) l)
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj Sum MCSig (HFix (Sum MCSig :&: Label)) l
s)

  constructCfg t :: (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t = (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> HState CCfgState (EnterExitPair MCSig) 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 (:&:)
  CStatement
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t

instance ConstructCfg MCSig CCfgState CExpression where
  constructCfg :: (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> HState CCfgState (EnterExitPair MCSig) i
constructCfg t' :: (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t'@((:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> CExpression
     (HFix (Sum MCSig :&: Label)
      :*: HState CCfgState (EnterExitPair MCSig))
     i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> (CBinary (op :: HFix (Sum MCSig :&: Label) CBinaryOpL
op :*: _) _ _ _)) = do
    let (t :: AnnTerm Label MCSig i
t :*: (CBinary _ el er _)) = (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CExpression (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t'
    case HFix (Sum MCSig :&: Label) CBinaryOpL
-> CBinaryOp MCTerm CBinaryOpL
extractOp HFix (Sum MCSig :&: Label) CBinaryOpL
op of
      CLndOp -> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MCSig i
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (fs :: [(* -> *) -> * -> *]) l ls rs es.
(MonadState s m, CfgComponent fs s) =>
TermLab fs l
-> m (EnterExitPair fs ls)
-> m (EnterExitPair fs rs)
-> m (EnterExitPair fs es)
constructCfgShortCircuitingBinOp AnnTerm Label MCSig i
t (HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
el) (HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
er)
      CLorOp  -> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MCSig i
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) (fs :: [(* -> *) -> * -> *]) l ls rs es.
(MonadState s m, CfgComponent fs s) =>
TermLab fs l
-> m (EnterExitPair fs ls)
-> m (EnterExitPair fs rs)
-> m (EnterExitPair fs es)
constructCfgShortCircuitingBinOp AnnTerm Label MCSig i
t (HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
el) (HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
er)
      _   -> (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> HState CCfgState (EnterExitPair MCSig) 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 (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t'

    where extractOp :: MCTermLab CBinaryOpL -> CBinaryOp MCTerm CBinaryOpL
          extractOp :: HFix (Sum MCSig :&: Label) CBinaryOpL
-> CBinaryOp MCTerm CBinaryOpL
extractOp (HFix (Sum MCSig :&: Label) CBinaryOpL
-> Cxt NoHole (Sum MCSig) (K ()) CBinaryOpL
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA -> Cxt NoHole (Sum MCSig) (K ()) CBinaryOpL
-> Maybe (CBinaryOp MCTerm CBinaryOpL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
       (a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just bp :: CBinaryOp MCTerm CBinaryOpL
bp) = CBinaryOp MCTerm CBinaryOpL
bp

  constructCfg t' :: (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t'@((:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> CExpression
     (HFix (Sum MCSig :&: Label)
      :*: HState CCfgState (EnterExitPair MCSig))
     i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> CCond {}) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ do
    let (t :: AnnTerm Label MCSig i
t :*: (CCond test succ fail _)) = (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CExpression (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t'
    AnnTerm Label MCSig i
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
-> State CCfgState (EnterExitPair MCSig i)
-> State CCfgState (EnterExitPair MCSig i)
forall s (m :: * -> *) l ls rs es.
(MonadState s m, CfgComponent MCSig s) =>
TermLab MCSig l
-> m (EnterExitPair MCSig ls)
-> m (Maybe (EnterExitPair MCSig rs))
-> m (EnterExitPair MCSig es)
-> m (EnterExitPair MCSig es)
constructCfgCCondOp AnnTerm Label MCSig i
t (HState CCfgState (EnterExitPair MCSig) CExpressionL
-> StateT CCfgState Identity (EnterExitPair MCSig CExpressionL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) CExpressionL
test) (StateT
  CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
-> StateT
     CCfgState Identity (Maybe (EnterExitPair MCSig CExpressionL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
-> StateT
     CCfgState Identity (EnterExitPair MCSig (Maybe CExpressionL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) (Maybe CExpressionL)
succ)) (HState CCfgState (EnterExitPair MCSig) i
-> State CCfgState (EnterExitPair MCSig i)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState CCfgState (EnterExitPair MCSig) i
fail)

  constructCfg t :: (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t = (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> HState CCfgState (EnterExitPair MCSig) 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 (:&:)
  CExpression
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t

-- NOTE: because of gcc extension which allows things like x ? : y
constructCfgCCondOp ::
  ( MonadState s m
  , CfgComponent MCSig s
  ) => TermLab MCSig l -> m (EnterExitPair MCSig ls) -> m (Maybe (EnterExitPair MCSig rs)) -> m (EnterExitPair MCSig es) -> m (EnterExitPair MCSig es)
constructCfgCCondOp :: TermLab MCSig l
-> m (EnterExitPair MCSig ls)
-> m (Maybe (EnterExitPair MCSig rs))
-> m (EnterExitPair MCSig es)
-> m (EnterExitPair MCSig es)
constructCfgCCondOp t :: TermLab MCSig l
t mtest :: m (EnterExitPair MCSig ls)
mtest msucc :: m (Maybe (EnterExitPair MCSig rs))
msucc mfail :: m (EnterExitPair MCSig es)
mfail = do
  CfgNode MCSig
enterNode <- TermLab MCSig l -> CfgNodeType -> m (CfgNode MCSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab MCSig l
t CfgNodeType
EnterNode
  CfgNode MCSig
exitNode  <- TermLab MCSig l -> CfgNodeType -> m (CfgNode MCSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab MCSig l
t CfgNodeType
ExitNode

  EnterExitPair MCSig ls
test <- m (EnterExitPair MCSig ls)
mtest
  EnterExitPair MCSig es
fail <- m (EnterExitPair MCSig es)
mfail
  Maybe (EnterExitPair MCSig rs)
succ <- m (Maybe (EnterExitPair MCSig rs))
msucc

  case Maybe (EnterExitPair MCSig rs)
succ of
    Just succ0 :: EnterExitPair MCSig rs
succ0 -> do
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode MCSig
enterNode (EnterExitPair MCSig ls -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MCSig ls
test)
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig ls -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig ls
test) (EnterExitPair MCSig rs -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MCSig rs
succ0)
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig ls -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig ls
test) (EnterExitPair MCSig es -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MCSig es
fail)
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig rs -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig rs
succ0) CfgNode MCSig
exitNode
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig es -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig es
fail) CfgNode MCSig
exitNode
    Nothing -> do
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode MCSig
enterNode (EnterExitPair MCSig ls -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MCSig ls
test)
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig ls -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig ls
test) (EnterExitPair MCSig es -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MCSig es
fail)
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig ls -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig ls
test) CfgNode MCSig
exitNode
      (Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MCSig -> Identity (Cfg MCSig)) -> s -> Identity s)
-> (Cfg MCSig -> Cfg MCSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MCSig -> CfgNode MCSig -> Cfg MCSig -> Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MCSig es -> CfgNode MCSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MCSig es
fail) CfgNode MCSig
exitNode

  EnterExitPair MCSig es -> m (EnterExitPair MCSig es)
forall (m :: * -> *) a. Monad m => a -> m a
return (CfgNode MCSig -> CfgNode MCSig -> EnterExitPair MCSig es
forall (fs :: [(* -> *) -> * -> *]) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode MCSig
enterNode CfgNode MCSig
exitNode)

-- CLabelBlock's getting nodes is messing everything up
instance ConstructCfg MCSig CCfgState CLabeledBlock where
  constructCfg :: (:&:)
  CLabeledBlock
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> HState CCfgState (EnterExitPair MCSig) i
constructCfg t :: (:&:)
  CLabeledBlock
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t@((:&:)
  CLabeledBlock
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> CLabeledBlock
     (HFix (Sum MCSig :&: Label)
      :*: HState CCfgState (EnterExitPair MCSig))
     i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> (CLabeledBlock (idents :: HFix (Sum MCSig :&: Label) [IdentL]
idents :*: _) _)) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ do
    [String]
-> State CCfgState (EnterExitPair MCSig i)
-> State CCfgState (EnterExitPair MCSig i)
forall (m :: * -> *) a.
(Monad m, MonadState CCfgState m) =>
[String] -> m a -> m a
cLabeledBlockLabMap [String]
labels (State CCfgState (EnterExitPair MCSig i)
 -> State CCfgState (EnterExitPair MCSig i))
-> State CCfgState (EnterExitPair MCSig i)
-> State CCfgState (EnterExitPair MCSig i)
forall a b. (a -> b) -> a -> b
$
      CLabeledBlock (HState CCfgState (EnterExitPair MCSig)) i
-> State CCfgState (EnterExitPair MCSig 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 ((:*:)
  (HFix (Sum MCSig :&: Label))
  (CLabeledBlock (HState CCfgState (EnterExitPair MCSig)))
  i
-> CLabeledBlock (HState CCfgState (EnterExitPair MCSig)) i
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> g a
fsnd ((:*:)
   (HFix (Sum MCSig :&: Label))
   (CLabeledBlock (HState CCfgState (EnterExitPair MCSig)))
   i
 -> CLabeledBlock (HState CCfgState (EnterExitPair MCSig)) i)
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CLabeledBlock (HState CCfgState (EnterExitPair MCSig)))
     i
-> CLabeledBlock (HState CCfgState (EnterExitPair MCSig)) i
forall a b. (a -> b) -> a -> b
$ (:&:)
  CLabeledBlock
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (CLabeledBlock (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
  CLabeledBlock
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
t)

      where labels :: [String]
labels = (Cxt NoHole (Sum MCSig :&: Label) (K ()) IdentL -> String)
-> [Cxt NoHole (Sum MCSig :&: Label) (K ()) IdentL] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Cxt NoHole (Sum MCSig :&: Label) (K ()) IdentL -> String
forall (g :: (* -> *) -> * -> *) (fs :: [(* -> *) -> * -> *]) l' h
       (a :: * -> *).
(RemA g (Sum fs), HFunctor g, InjF fs IdentL l',
 KnownNat (Position Ident fs)) =>
Cxt h g a l' -> String
getIdent (HFix (Sum MCSig :&: Label) [IdentL]
-> [Cxt NoHole (Sum MCSig :&: Label) (K ()) IdentL]
forall (f :: * -> *) (e :: * -> *) l.
ExtractF f e =>
e (f l) -> f (e l)
extractF HFix (Sum MCSig :&: Label) [IdentL]
idents)
            getIdent :: Cxt h g a l' -> String
getIdent (Cxt h g a l' -> Cxt h (Sum fs) a l'
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA -> Cxt h (Sum fs) a l' -> Maybe (CxtS h fs a IdentL)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l' -> Maybe (CxtS h fs a l)
projF -> Just (Ident' s :: String
s)) = String
s

instance ConstructCfg MCSig CCfgState P.FunctionDef where
  constructCfg :: (:&:)
  FunctionDef
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> HState CCfgState (EnterExitPair MCSig) i
constructCfg ((:&:)
  FunctionDef
  Label
  (HFix (Sum MCSig :&: Label)
   :*: HState CCfgState (EnterExitPair MCSig))
  i
-> (:*:)
     (HFix (Sum MCSig :&: Label))
     (FunctionDef (HState CCfgState (EnterExitPair MCSig)))
     i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
       (t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (_ :*: subCfgs :: FunctionDef (HState CCfgState (EnterExitPair MCSig)) i
subCfgs)) = State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State CCfgState (EnterExitPair MCSig i)
 -> HState CCfgState (EnterExitPair MCSig) i)
-> State CCfgState (EnterExitPair MCSig i)
-> HState CCfgState (EnterExitPair MCSig) i
forall a b. (a -> b) -> a -> b
$ do
    State CCfgState (EnterExitPair MCSig i)
-> State CCfgState (EnterExitPair MCSig i)
forall (m :: * -> *) a.
(Monad m, MonadState CCfgState m) =>
m a -> m a
functionDefLabelMap (State CCfgState (EnterExitPair MCSig i)
 -> State CCfgState (EnterExitPair MCSig i))
-> State CCfgState (EnterExitPair MCSig i)
-> State CCfgState (EnterExitPair MCSig i)
forall a b. (a -> b) -> a -> b
$ do
      FunctionDef (HState CCfgState (EnterExitPair MCSig)) i
-> StateT CCfgState Identity (EnterExitPair MCSig 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 FunctionDef (HState CCfgState (EnterExitPair MCSig)) i
subCfgs
      EnterExitPair MCSig i -> State CCfgState (EnterExitPair MCSig i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure EnterExitPair MCSig i
forall (fs :: [(* -> *) -> * -> *]) l. EnterExitPair fs l
EmptyEnterExit

instance CfgInitState MCSig where
  cfgInitState :: Proxy MCSig -> CfgState MCSig
cfgInitState _ = Cfg MCSig
-> LabelGen -> LoopStack -> LabelMap -> LocalLabels -> CCfgState
CCfgState Cfg MCSig
forall (fs :: [(* -> *) -> * -> *]). Cfg fs
emptyCfg (() -> LabelGen
unsafeMkCSLabelGen ()) LoopStack
emptyLoopStack LabelMap
emptyLabelMap LocalLabels
emptyLocalLabels
#endif