{-# 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.Java.Parametric.Common.Cfg () where
#ifndef ONLY_ONE_LANGUAGE
import Control.Monad ( liftM, liftM2, forM_ )
import Control.Monad.State ( MonadState )
import Control.Lens ( makeLenses, (%=) )
import Data.Comp.Multi ( stripA, remA, (:*:)(..), ffst, proj, project', project )
import Data.Foldable
import Cubix.Language.Info
import Cubix.Language.Java.Parametric.Common.Types as C
import Cubix.Language.Java.Parametric.Full.Types as F
import Cubix.Language.Parametric.Semantics.Cfg
import Cubix.Language.Parametric.Syntax
data JavaCfgState = JavaCfgState {
JavaCfgState -> Cfg MJavaSig
_jcs_cfg :: Cfg MJavaSig
, JavaCfgState -> LabelGen
_jcs_labeler :: LabelGen
, JavaCfgState -> LoopStack
_jcs_stack :: LoopStack
, JavaCfgState -> ScopedLabelMap
_jcs_scoped_labs :: ScopedLabelMap
}
makeLenses ''JavaCfgState
instance HasCurCfg JavaCfgState MJavaSig where cur_cfg :: (Cfg MJavaSig -> f (Cfg MJavaSig))
-> JavaCfgState -> f JavaCfgState
cur_cfg = (Cfg MJavaSig -> f (Cfg MJavaSig))
-> JavaCfgState -> f JavaCfgState
Lens' JavaCfgState (Cfg MJavaSig)
jcs_cfg
instance HasLabelGen JavaCfgState where labelGen :: (LabelGen -> f LabelGen) -> JavaCfgState -> f JavaCfgState
labelGen = (LabelGen -> f LabelGen) -> JavaCfgState -> f JavaCfgState
Lens' JavaCfgState LabelGen
jcs_labeler
instance HasLoopStack JavaCfgState where loopStack :: (LoopStack -> f LoopStack) -> JavaCfgState -> f JavaCfgState
loopStack = (LoopStack -> f LoopStack) -> JavaCfgState -> f JavaCfgState
Lens' JavaCfgState LoopStack
jcs_stack
instance HasScopedLabelMap JavaCfgState where scopedLabelMap :: (ScopedLabelMap -> f ScopedLabelMap)
-> JavaCfgState -> f JavaCfgState
scopedLabelMap = (ScopedLabelMap -> f ScopedLabelMap)
-> JavaCfgState -> f JavaCfgState
Lens' JavaCfgState ScopedLabelMap
jcs_scoped_labs
type instance ComputationSorts MJavaSig = '[StmtL, ExpL, BlockStmtL, [BlockItemL]]
type instance SuspendedComputationSorts MJavaSig = '[MethodBodyL, ConstructorBodyL, LambdaExpressionL, CatchL, FunctionDefL]
type instance ContainerFunctors MJavaSig = '[PairF, ListF, MaybeF, SwitchBlock]
type instance CfgState MJavaSig = JavaCfgState
data Kleene = KTrue | KFalse | KMaybe
singleton :: a -> [a]
singleton :: a -> [a]
singleton = a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return
evaluateExp :: MJavaTermLab ExpL -> Kleene
evaluateExp :: MJavaTermLab ExpL -> Kleene
evaluateExp (MJavaTermLab ExpL
-> Maybe (Exp (Cxt NoHole (Sum MJavaSig :&: Label) (K ())) ExpL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
(s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' -> Just t :: Exp (Cxt NoHole (Sum MJavaSig :&: Label) (K ())) ExpL
t@(Lit lit :: Cxt NoHole (Sum MJavaSig :&: Label) (K ()) LiteralL
lit)) =
case Cxt NoHole (Sum MJavaSig :&: Label) (K ()) LiteralL
-> Maybe
(Literal (Cxt NoHole (Sum MJavaSig :&: Label) (K ())) LiteralL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
(s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt NoHole (Sum MJavaSig :&: Label) (K ()) LiteralL
lit of
Just (Boolean True) -> Kleene
KTrue
Just (Boolean False) -> Kleene
KFalse
_ -> Kleene
KMaybe
evaluateExp _ = Kleene
KMaybe
evaluateWhileExp :: MJavaTermLab l -> Kleene
evaluateWhileExp :: MJavaTermLab l -> Kleene
evaluateWhileExp (MJavaTermLab l
-> Maybe (Stmt (Cxt NoHole (Sum MJavaSig :&: Label) (K ())) l)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
(s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' -> Just t :: Stmt (Cxt NoHole (Sum MJavaSig :&: Label) (K ())) l
t@(While exp :: MJavaTermLab ExpL
exp body :: Cxt NoHole (Sum MJavaSig :&: Label) (K ()) StmtL
body)) = MJavaTermLab ExpL -> Kleene
evaluateExp MJavaTermLab ExpL
exp
constructCfgWhileJava :: (HasLoopStack s, MonadState s m, CfgComponent MJavaSig s) => MJavaTermLab l -> m (EnterExitPair MJavaSig i) -> m (EnterExitPair MJavaSig j) -> m (EnterExitPair MJavaSig k)
constructCfgWhileJava :: MJavaTermLab l
-> m (EnterExitPair MJavaSig i)
-> m (EnterExitPair MJavaSig j)
-> m (EnterExitPair MJavaSig k)
constructCfgWhileJava t :: MJavaTermLab l
t mExp :: m (EnterExitPair MJavaSig i)
mExp mBody :: m (EnterExitPair MJavaSig j)
mBody = do
CfgNode MJavaSig
enterNode <- MJavaTermLab l -> CfgNodeType -> m (CfgNode MJavaSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode MJavaTermLab l
t CfgNodeType
EnterNode
CfgNode MJavaSig
loopEntryNode <- MJavaTermLab l -> CfgNodeType -> m (CfgNode MJavaSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode MJavaTermLab l
t CfgNodeType
LoopEntryNode
CfgNode MJavaSig
exitNode <- MJavaTermLab l -> CfgNodeType -> m (CfgNode MJavaSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode MJavaTermLab l
t CfgNodeType
ExitNode
EnterExitPair MJavaSig Any
exp <- m (EnterExitPair MJavaSig i)
mExp m (EnterExitPair MJavaSig i)
-> (EnterExitPair MJavaSig i -> m (EnterExitPair MJavaSig Any))
-> m (EnterExitPair MJavaSig Any)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= EnterExitPair MJavaSig i -> m (EnterExitPair MJavaSig Any)
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
CfgNode MJavaSig -> CfgNode MJavaSig -> m ()
forall s (m :: * -> *) (fs :: [(* -> *) -> * -> *]).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> CfgNode fs -> m ()
pushLoopNode CfgNode MJavaSig
loopEntryNode CfgNode MJavaSig
exitNode
EnterExitPair MJavaSig j
body <- m (EnterExitPair MJavaSig j)
mBody
m ()
forall s (m :: * -> *). (MonadState s m, HasLoopStack s) => m ()
popLoopNode
case MJavaTermLab l -> Kleene
forall l. MJavaTermLab l -> Kleene
evaluateWhileExp MJavaTermLab l
t of
KTrue -> (Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s)
-> (Cfg MJavaSig -> Cfg MJavaSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MJavaSig Any -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MJavaSig Any
exp) (EnterExitPair MJavaSig j -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MJavaSig j
body)
KFalse -> (Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s)
-> (Cfg MJavaSig -> Cfg MJavaSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MJavaSig Any -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MJavaSig Any
exp) CfgNode MJavaSig
exitNode
KMaybe -> do
(Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s)
-> (Cfg MJavaSig -> Cfg MJavaSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MJavaSig Any -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MJavaSig Any
exp) (EnterExitPair MJavaSig j -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MJavaSig j
body)
(Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s)
-> (Cfg MJavaSig -> Cfg MJavaSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MJavaSig Any -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MJavaSig Any
exp) CfgNode MJavaSig
exitNode
(Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s)
-> (Cfg MJavaSig -> Cfg MJavaSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode MJavaSig
enterNode CfgNode MJavaSig
loopEntryNode
(Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s)
-> (Cfg MJavaSig -> Cfg MJavaSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode MJavaSig
loopEntryNode (EnterExitPair MJavaSig Any -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MJavaSig Any
exp)
(Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig)) -> s -> Identity s)
-> (Cfg MJavaSig -> Cfg MJavaSig) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MJavaSig j -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MJavaSig j
body) CfgNode MJavaSig
loopEntryNode
EnterExitPair MJavaSig k -> m (EnterExitPair MJavaSig k)
forall (m :: * -> *) a. Monad m => a -> m a
return (EnterExitPair MJavaSig k -> m (EnterExitPair MJavaSig k))
-> EnterExitPair MJavaSig k -> m (EnterExitPair MJavaSig k)
forall a b. (a -> b) -> a -> b
$ CfgNode MJavaSig -> CfgNode MJavaSig -> EnterExitPair MJavaSig k
forall (fs :: [(* -> *) -> * -> *]) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode MJavaSig
enterNode CfgNode MJavaSig
exitNode
extractAndRunSwitchBlocks :: (MonadState s m, CfgComponent MJavaSig s) => m (EnterExitPair MJavaSig [SwitchBlockL]) -> m [EnterExitPair MJavaSig [BlockStmtL]]
extractAndRunSwitchBlocks :: m (EnterExitPair MJavaSig [SwitchBlockL])
-> m [EnterExitPair MJavaSig [BlockStmtL]]
extractAndRunSwitchBlocks switchBlocks :: m (EnterExitPair MJavaSig [SwitchBlockL])
switchBlocks = (EnterExitPair MJavaSig [BlockStmtL]
-> m (EnterExitPair MJavaSig [BlockStmtL]))
-> [EnterExitPair MJavaSig [BlockStmtL]]
-> m [EnterExitPair MJavaSig [BlockStmtL]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM EnterExitPair MJavaSig [BlockStmtL]
-> m (EnterExitPair MJavaSig [BlockStmtL])
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 MJavaSig [BlockStmtL]]
-> m [EnterExitPair MJavaSig [BlockStmtL]])
-> m [EnterExitPair MJavaSig [BlockStmtL]]
-> m [EnterExitPair MJavaSig [BlockStmtL]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((EnterExitPair MJavaSig SwitchBlockL
-> EnterExitPair MJavaSig [BlockStmtL])
-> [EnterExitPair MJavaSig SwitchBlockL]
-> [EnterExitPair MJavaSig [BlockStmtL]]
forall a b. (a -> b) -> [a] -> [b]
map EnterExitPair MJavaSig SwitchBlockL
-> EnterExitPair MJavaSig [BlockStmtL]
extractBlock ([EnterExitPair MJavaSig SwitchBlockL]
-> [EnterExitPair MJavaSig [BlockStmtL]])
-> (EnterExitPair MJavaSig [SwitchBlockL]
-> [EnterExitPair MJavaSig SwitchBlockL])
-> EnterExitPair MJavaSig [SwitchBlockL]
-> [EnterExitPair MJavaSig [BlockStmtL]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EnterExitPair MJavaSig [SwitchBlockL]
-> [EnterExitPair MJavaSig SwitchBlockL]
forall (fs :: [(* -> *) -> * -> *]) l.
(ListF :-<: fs, Typeable l) =>
EnterExitPair fs [l] -> [EnterExitPair fs l]
extractEEPList (EnterExitPair MJavaSig [SwitchBlockL]
-> [EnterExitPair MJavaSig [BlockStmtL]])
-> m (EnterExitPair MJavaSig [SwitchBlockL])
-> m [EnterExitPair MJavaSig [BlockStmtL]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (EnterExitPair MJavaSig [SwitchBlockL])
switchBlocks)
where
extractBlock :: EnterExitPair MJavaSig SwitchBlockL -> EnterExitPair MJavaSig [BlockStmtL]
extractBlock :: EnterExitPair MJavaSig SwitchBlockL
-> EnterExitPair MJavaSig [BlockStmtL]
extractBlock (SubPairs (Sum MJavaSig (EnterExitPair MJavaSig) SwitchBlockL
-> Maybe (SwitchBlock (EnterExitPair MJavaSig) SwitchBlockL)
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj -> Just (SwitchBlock _ body :: EnterExitPair MJavaSig [BlockStmtL]
body))) = EnterExitPair MJavaSig [BlockStmtL]
body
nameString' :: MJavaTermLab F.IdentL -> String
nameString' :: MJavaTermLab IdentL -> String
nameString' = MJavaTerm IdentL -> String
nameString (MJavaTerm IdentL -> String)
-> (MJavaTermLab IdentL -> MJavaTerm IdentL)
-> MJavaTermLab IdentL
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MJavaTermLab IdentL -> MJavaTerm IdentL
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA
nameString :: MJavaTerm F.IdentL -> String
nameString :: MJavaTerm IdentL -> String
nameString (MJavaTerm IdentL
-> Maybe (IdentIsIdent (Cxt NoHole (Sum MJavaSig) (K ())) IdentL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just (IdentIsIdent (Ident' s :: String
s))) = String
s
instance ConstructCfg MJavaSig JavaCfgState Stmt where
constructCfg :: (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> HState JavaCfgState (EnterExitPair MJavaSig) i
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
(t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' -> (_ :*: subCfgs :: Stmt (HState JavaCfgState (EnterExitPair MJavaSig)) i
subCfgs@(StmtBlock _))) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ Stmt (HState JavaCfgState (EnterExitPair MJavaSig)) i
-> State JavaCfgState (EnterExitPair MJavaSig 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 Stmt (HState JavaCfgState (EnterExitPair MJavaSig)) i
subCfgs
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: (IfThen cond :: HState JavaCfgState (EnterExitPair MJavaSig) ExpL
cond thn :: HState JavaCfgState (EnterExitPair MJavaSig) StmtL
thn))) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT
JavaCfgState
Identity
[(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)]
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig Any))
-> State JavaCfgState (EnterExitPair MJavaSig 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 AnnTerm Label MJavaSig i
t (((EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> [(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)])
-> StateT
JavaCfgState
Identity
(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState
Identity
[(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> [(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)]
forall a. a -> [a]
singleton (StateT
JavaCfgState
Identity
(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState
Identity
[(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)])
-> StateT
JavaCfgState
Identity
(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState
Identity
[(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)]
forall a b. (a -> b) -> a -> b
$ (EnterExitPair MJavaSig ExpL
-> EnterExitPair MJavaSig StmtL
-> (EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL))
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState
Identity
(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
cond) (HState JavaCfgState (EnterExitPair MJavaSig) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) StmtL
thn)) (Maybe (EnterExitPair MJavaSig Any)
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig Any))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (EnterExitPair MJavaSig Any)
forall a. Maybe a
Nothing)
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: (IfThenElse cond :: HState JavaCfgState (EnterExitPair MJavaSig) ExpL
cond thn :: HState JavaCfgState (EnterExitPair MJavaSig) StmtL
thn els :: HState JavaCfgState (EnterExitPair MJavaSig) StmtL
els))) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT
JavaCfgState
Identity
[(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)]
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig StmtL))
-> State JavaCfgState (EnterExitPair MJavaSig 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 AnnTerm Label MJavaSig i
t (((EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> [(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)])
-> StateT
JavaCfgState
Identity
(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState
Identity
[(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> [(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)]
forall a. a -> [a]
singleton (StateT
JavaCfgState
Identity
(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState
Identity
[(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)])
-> StateT
JavaCfgState
Identity
(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState
Identity
[(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)]
forall a b. (a -> b) -> a -> b
$ (EnterExitPair MJavaSig ExpL
-> EnterExitPair MJavaSig StmtL
-> (EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL))
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState
Identity
(EnterExitPair MJavaSig ExpL, EnterExitPair MJavaSig StmtL)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
cond) (HState JavaCfgState (EnterExitPair MJavaSig) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) StmtL
thn)) ((EnterExitPair MJavaSig StmtL
-> Maybe (EnterExitPair MJavaSig StmtL))
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig StmtL))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM EnterExitPair MJavaSig StmtL
-> Maybe (EnterExitPair MJavaSig StmtL)
forall a. a -> Maybe a
Just (StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig StmtL)))
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig StmtL))
forall a b. (a -> b) -> a -> b
$ HState JavaCfgState (EnterExitPair MJavaSig) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) StmtL
els)
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: (While e :: HState JavaCfgState (EnterExitPair MJavaSig) ExpL
e s :: HState JavaCfgState (EnterExitPair MJavaSig) StmtL
s))) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> State JavaCfgState (EnterExitPair MJavaSig i)
forall s (m :: * -> *) l i j k.
(HasLoopStack s, MonadState s m, CfgComponent MJavaSig s) =>
MJavaTermLab l
-> m (EnterExitPair MJavaSig i)
-> m (EnterExitPair MJavaSig j)
-> m (EnterExitPair MJavaSig k)
constructCfgWhileJava AnnTerm Label MJavaSig i
t (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
e) (HState JavaCfgState (EnterExitPair MJavaSig) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) StmtL
s)
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: (BasicFor init :: HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ForInitL)
init cond :: HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ExpL)
cond step :: HState JavaCfgState (EnterExitPair MJavaSig) (Maybe [ExpL])
step body :: HState JavaCfgState (EnterExitPair MJavaSig) StmtL
body))) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ForInitL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig [ExpL]))
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> State JavaCfgState (EnterExitPair MJavaSig 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 AnnTerm Label MJavaSig i
t (StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ForInitL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ForInitL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ForInitL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ForInitL)))
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ForInitL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ForInitL))
forall a b. (a -> b) -> a -> b
$ HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ForInitL)
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ForInitL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ForInitL)
init) (StateT JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ExpL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ExpL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL)))
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ExpL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
forall a b. (a -> b) -> a -> b
$ HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ExpL)
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ExpL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ExpL)
cond) (StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe [ExpL]))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig [ExpL]))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe [ExpL]))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig [ExpL])))
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe [ExpL]))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig [ExpL]))
forall a b. (a -> b) -> a -> b
$ HState JavaCfgState (EnterExitPair MJavaSig) (Maybe [ExpL])
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe [ExpL]))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) (Maybe [ExpL])
step) (HState JavaCfgState (EnterExitPair MJavaSig) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) StmtL
body)
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: (EnhancedFor _ _ _ e :: HState JavaCfgState (EnterExitPair MJavaSig) ExpL
e s :: HState JavaCfgState (EnterExitPair MJavaSig) StmtL
s))) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> State JavaCfgState (EnterExitPair MJavaSig 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 AnnTerm Label MJavaSig i
t (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
e) (HState JavaCfgState (EnterExitPair MJavaSig) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) StmtL
s)
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: (Switch exp :: HState JavaCfgState (EnterExitPair MJavaSig) ExpL
exp switchBlocks :: HState JavaCfgState (EnterExitPair MJavaSig) [SwitchBlockL]
switchBlocks))) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ do
CfgNode MJavaSig
enterNode <- AnnTerm Label MJavaSig i
-> CfgNodeType -> StateT JavaCfgState Identity (CfgNode MJavaSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode AnnTerm Label MJavaSig i
t CfgNodeType
EnterNode
CfgNode MJavaSig
exitNode <- AnnTerm Label MJavaSig i
-> CfgNodeType -> StateT JavaCfgState Identity (CfgNode MJavaSig)
forall s (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode AnnTerm Label MJavaSig i
t CfgNodeType
ExitNode
EnterExitPair MJavaSig ExpL
expEE <- HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
exp
CfgNode MJavaSig -> StateT JavaCfgState Identity ()
forall s (m :: * -> *) (fs :: [(* -> *) -> * -> *]).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> m ()
pushBreakNode CfgNode MJavaSig
exitNode
[EnterExitPair MJavaSig [BlockStmtL]]
blocks <- StateT
JavaCfgState Identity (EnterExitPair MJavaSig [SwitchBlockL])
-> StateT
JavaCfgState Identity [EnterExitPair MJavaSig [BlockStmtL]]
forall s (m :: * -> *).
(MonadState s m, CfgComponent MJavaSig s) =>
m (EnterExitPair MJavaSig [SwitchBlockL])
-> m [EnterExitPair MJavaSig [BlockStmtL]]
extractAndRunSwitchBlocks (StateT
JavaCfgState Identity (EnterExitPair MJavaSig [SwitchBlockL])
-> StateT
JavaCfgState Identity [EnterExitPair MJavaSig [BlockStmtL]])
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig [SwitchBlockL])
-> StateT
JavaCfgState Identity [EnterExitPair MJavaSig [BlockStmtL]]
forall a b. (a -> b) -> a -> b
$ HState JavaCfgState (EnterExitPair MJavaSig) [SwitchBlockL]
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig [SwitchBlockL])
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) [SwitchBlockL]
switchBlocks
StateT JavaCfgState Identity ()
forall s (m :: * -> *). (MonadState s m, HasLoopStack s) => m ()
popBreakNode
(Cfg MJavaSig -> Identity (Cfg MJavaSig))
-> JavaCfgState -> Identity JavaCfgState
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig))
-> JavaCfgState -> Identity JavaCfgState)
-> (Cfg MJavaSig -> Cfg MJavaSig)
-> StateT JavaCfgState Identity ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode MJavaSig
enterNode (EnterExitPair MJavaSig ExpL -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair MJavaSig ExpL
expEE)
[EnterExitPair MJavaSig [BlockStmtL]]
-> (EnterExitPair MJavaSig [BlockStmtL]
-> StateT JavaCfgState Identity ())
-> StateT JavaCfgState Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [EnterExitPair MJavaSig [BlockStmtL]]
blocks ((EnterExitPair MJavaSig [BlockStmtL]
-> StateT JavaCfgState Identity ())
-> StateT JavaCfgState Identity ())
-> (EnterExitPair MJavaSig [BlockStmtL]
-> StateT JavaCfgState Identity ())
-> StateT JavaCfgState Identity ()
forall a b. (a -> b) -> a -> b
$ \b :: EnterExitPair MJavaSig [BlockStmtL]
b -> case EnterExitPair MJavaSig [BlockStmtL]
b of
EmptyEnterExit -> (Cfg MJavaSig -> Identity (Cfg MJavaSig))
-> JavaCfgState -> Identity JavaCfgState
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig))
-> JavaCfgState -> Identity JavaCfgState)
-> (Cfg MJavaSig -> Cfg MJavaSig)
-> StateT JavaCfgState Identity ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MJavaSig ExpL -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MJavaSig ExpL
expEE) CfgNode MJavaSig
exitNode
EnterExitPair bEnt :: CfgNode MJavaSig
bEnt bEx :: CfgNode MJavaSig
bEx -> do
(Cfg MJavaSig -> Identity (Cfg MJavaSig))
-> JavaCfgState -> Identity JavaCfgState
forall c (fs :: [(* -> *) -> * -> *]).
HasCurCfg c fs =>
Lens' c (Cfg fs)
cur_cfg ((Cfg MJavaSig -> Identity (Cfg MJavaSig))
-> JavaCfgState -> Identity JavaCfgState)
-> (Cfg MJavaSig -> Cfg MJavaSig)
-> StateT JavaCfgState Identity ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode MJavaSig
-> CfgNode MJavaSig -> Cfg MJavaSig -> Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair MJavaSig ExpL -> CfgNode MJavaSig
forall (fs :: [(* -> *) -> * -> *]) l.
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair MJavaSig ExpL
expEE) CfgNode MJavaSig
bEnt
EnterExitPair MJavaSig Any
blockEE <- (EnterExitPair MJavaSig Any
-> EnterExitPair MJavaSig [BlockStmtL]
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig Any))
-> EnterExitPair MJavaSig Any
-> [EnterExitPair MJavaSig [BlockStmtL]]
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig Any)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM EnterExitPair MJavaSig Any
-> EnterExitPair MJavaSig [BlockStmtL]
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig 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 EnterExitPair MJavaSig Any
forall (fs :: [(* -> *) -> * -> *]) l. EnterExitPair fs l
EmptyEnterExit [EnterExitPair MJavaSig [BlockStmtL]]
blocks
EnterExitPair MJavaSig Any
_ <- EnterExitPair MJavaSig Any
-> EnterExitPair MJavaSig Any
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig 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 EnterExitPair MJavaSig Any
blockEE (CfgNode MJavaSig -> EnterExitPair MJavaSig Any
forall (fs :: [(* -> *) -> * -> *]) l.
CfgNode fs -> EnterExitPair fs l
identEnterExit CfgNode MJavaSig
exitNode)
EnterExitPair MJavaSig i
-> State JavaCfgState (EnterExitPair MJavaSig i)
forall (m :: * -> *) a. Monad m => a -> m a
return (EnterExitPair MJavaSig i
-> State JavaCfgState (EnterExitPair MJavaSig i))
-> EnterExitPair MJavaSig i
-> State JavaCfgState (EnterExitPair MJavaSig i)
forall a b. (a -> b) -> a -> b
$ CfgNode MJavaSig -> CfgNode MJavaSig -> EnterExitPair MJavaSig i
forall (fs :: [(* -> *) -> * -> *]) l.
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode MJavaSig
enterNode CfgNode MJavaSig
exitNode
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: (Do s :: HState JavaCfgState (EnterExitPair MJavaSig) StmtL
s e :: HState JavaCfgState (EnterExitPair MJavaSig) ExpL
e))) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> State JavaCfgState (EnterExitPair MJavaSig 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 AnnTerm Label MJavaSig i
t (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
e) (HState JavaCfgState (EnterExitPair MJavaSig) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) StmtL
s)
constructCfg t :: (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t@((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> Stmt
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> Break ((HFix (Sum MJavaSig :&: Label) (Maybe IdentL)
-> Cxt NoHole (Sum MJavaSig) (K ()) (Maybe IdentL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA -> Cxt NoHole (Sum MJavaSig) (K ()) (Maybe IdentL)
Nothing') :*: _)) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> State JavaCfgState (EnterExitPair MJavaSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> m (EnterExitPair gs i)
constructCfgBreak ((:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
-> AnnTerm Label MJavaSig i
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst ((:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
-> AnnTerm Label MJavaSig i)
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
-> AnnTerm Label MJavaSig i
forall a b. (a -> b) -> a -> b
$ (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
(t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t)
constructCfg t :: (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t@((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> Stmt
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> Continue ((HFix (Sum MJavaSig :&: Label) (Maybe IdentL)
-> Cxt NoHole (Sum MJavaSig) (K ()) (Maybe IdentL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA -> Cxt NoHole (Sum MJavaSig) (K ()) (Maybe IdentL)
Nothing') :*: _)) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> State JavaCfgState (EnterExitPair MJavaSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> m (EnterExitPair gs i)
constructCfgContinue ((:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
-> AnnTerm Label MJavaSig i
forall k (f :: k -> *) (g :: k -> *) (a :: k). (:*:) f g a -> f a
ffst ((:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
-> AnnTerm Label MJavaSig i)
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
-> AnnTerm Label MJavaSig i
forall a b. (a -> b) -> a -> b
$ (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
(t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t)
constructCfg t :: (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t@((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> Stmt
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> Break ((HFix (Sum MJavaSig :&: Label) (Maybe IdentL)
-> Cxt NoHole (Sum MJavaSig) (K ()) (Maybe IdentL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA -> Just' targ :: MJavaTerm IdentL
targ) :*: _)) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> String -> State JavaCfgState (EnterExitPair MJavaSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(HasScopedLabelMap s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> String -> m (EnterExitPair gs i)
constructCfgScopedLabeledBreak ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> AnnTerm Label MJavaSig i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
(t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> AnnTerm a gs
fprodFst' (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t) (MJavaTerm IdentL -> String
nameString MJavaTerm IdentL
targ)
constructCfg t :: (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t@((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> Stmt
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> Continue ((HFix (Sum MJavaSig :&: Label) (Maybe IdentL)
-> Cxt NoHole (Sum MJavaSig) (K ()) (Maybe IdentL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA -> Just' targ :: MJavaTerm IdentL
targ) :*: _)) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> String -> State JavaCfgState (EnterExitPair MJavaSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l i.
(HasScopedLabelMap s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> String -> m (EnterExitPair gs i)
constructCfgScopedLabeledContinue ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> AnnTerm Label MJavaSig i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
(t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> AnnTerm a gs
fprodFst' (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t) (MJavaTerm IdentL -> String
nameString MJavaTerm IdentL
targ)
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: Return e :: HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ExpL)
e)) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
-> State JavaCfgState (EnterExitPair MJavaSig 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 AnnTerm Label MJavaSig i
t (StateT JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ExpL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
forall (fs :: [(* -> *) -> * -> *]) (m :: * -> *) l.
(All (KExtractF' Maybe) fs, Monad m) =>
m (EnterExitPair fs (Maybe l)) -> m (Maybe (EnterExitPair fs l))
extractEEPMaybe (StateT JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ExpL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL)))
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ExpL))
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
forall a b. (a -> b) -> a -> b
$ HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ExpL)
-> StateT
JavaCfgState Identity (EnterExitPair MJavaSig (Maybe ExpL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) (Maybe ExpL)
e)
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: Throw e :: HState JavaCfgState (EnterExitPair MJavaSig) ExpL
e)) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
-> State JavaCfgState (EnterExitPair MJavaSig 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 AnnTerm Label MJavaSig i
t ((EnterExitPair MJavaSig ExpL
-> Maybe (EnterExitPair MJavaSig ExpL))
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM EnterExitPair MJavaSig ExpL -> Maybe (EnterExitPair MJavaSig ExpL)
forall a. a -> Maybe a
Just (StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL)))
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT
JavaCfgState Identity (Maybe (EnterExitPair MJavaSig ExpL))
forall a b. (a -> b) -> a -> b
$ HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
e)
constructCfg ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Stmt (HState JavaCfgState (EnterExitPair MJavaSig)))
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 MJavaSig i
t :*: Try block :: HState JavaCfgState (EnterExitPair MJavaSig) BlockL
block catchs :: HState JavaCfgState (EnterExitPair MJavaSig) [CatchL]
catchs finally :: HState JavaCfgState (EnterExitPair MJavaSig) (Maybe BlockL)
finally)) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ do
HState JavaCfgState (EnterExitPair MJavaSig) BlockL
-> State JavaCfgState (EnterExitPair MJavaSig BlockL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) BlockL
block
HState JavaCfgState (EnterExitPair MJavaSig) [CatchL]
-> State JavaCfgState (EnterExitPair MJavaSig [CatchL])
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) [CatchL]
catchs
HState JavaCfgState (EnterExitPair MJavaSig) (Maybe BlockL)
-> State JavaCfgState (EnterExitPair MJavaSig (Maybe BlockL))
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) (Maybe BlockL)
finally
AnnTerm Label MJavaSig i
-> State JavaCfgState (EnterExitPair MJavaSig i)
forall s (m :: * -> *) (gs :: [(* -> *) -> * -> *]) l.
(MonadState s m, CfgComponent gs s) =>
TermLab gs l -> m (EnterExitPair gs l)
constructCfgEmpty AnnTerm Label MJavaSig i
t
constructCfg tp :: (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
tp@((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> Stmt
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> Labeled (name :: MJavaTermLab IdentL
name :*: _) (s :: Cxt NoHole (Sum MJavaSig :&: Label) (K ()) StmtL
s :*: mStmt :: HState JavaCfgState (EnterExitPair MJavaSig) StmtL
mStmt)) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> String
-> Cxt NoHole (Sum MJavaSig :&: Label) (K ()) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
-> State JavaCfgState (EnterExitPair MJavaSig i)
forall s (m :: * -> *) (fs :: [(* -> *) -> * -> *]) l s0 i.
(HasScopedLabelMap s, MonadState s m, CfgComponent fs s) =>
TermLab fs l
-> String
-> TermLab fs s0
-> m (EnterExitPair fs s0)
-> m (EnterExitPair fs i)
constructCfgScopedLabel ((:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> AnnTerm Label MJavaSig i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
(t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> AnnTerm a gs
fprodFst' (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
tp) (MJavaTermLab IdentL -> String
nameString' MJavaTermLab IdentL
name) Cxt NoHole (Sum MJavaSig :&: Label) (K ()) StmtL
s (HState JavaCfgState (EnterExitPair MJavaSig) StmtL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig StmtL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) StmtL
mStmt)
constructCfg t :: (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t = (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> HState JavaCfgState (EnterExitPair MJavaSig) 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 (:&:)
Stmt
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t
instance ConstructCfg MJavaSig JavaCfgState Exp where
constructCfg :: (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> HState JavaCfgState (EnterExitPair MJavaSig) i
constructCfg t' :: (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t'@((:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> Exp
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> (BinOp _ (op :: HFix (Sum MJavaSig :&: Label) OpL
op :*: _) _)) = do
let (t :: AnnTerm Label MJavaSig i
t :*: (BinOp el _ er)) = (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Exp (HState JavaCfgState (EnterExitPair MJavaSig)))
i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
(t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t'
case HFix (Sum MJavaSig :&: Label) OpL
-> Op (Cxt NoHole (Sum MJavaSig) (K ())) OpL
extractOp HFix (Sum MJavaSig :&: Label) OpL
op of
CAnd -> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> State JavaCfgState (EnterExitPair MJavaSig 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 MJavaSig i
t (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
el) (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
er)
COr -> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ AnnTerm Label MJavaSig i
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> State JavaCfgState (EnterExitPair MJavaSig 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 MJavaSig i
t (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
el) (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
er)
_ -> (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> HState JavaCfgState (EnterExitPair MJavaSig) 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 (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t'
where extractOp :: MJavaTermLab OpL -> Op MJavaTerm OpL
extractOp :: HFix (Sum MJavaSig :&: Label) OpL
-> Op (Cxt NoHole (Sum MJavaSig) (K ())) OpL
extractOp (HFix (Sum MJavaSig :&: Label) OpL
-> Cxt NoHole (Sum MJavaSig) (K ()) OpL
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA -> Cxt NoHole (Sum MJavaSig) (K ()) OpL
-> Maybe (Op (Cxt NoHole (Sum MJavaSig) (K ())) OpL)
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project -> Just bp :: Op (Cxt NoHole (Sum MJavaSig) (K ())) OpL
bp) = Op (Cxt NoHole (Sum MJavaSig) (K ())) OpL
bp
constructCfg t' :: (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t'@((:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> Exp
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA -> Cond {}) = State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall s (f :: * -> *) l. State s (f l) -> HState s f l
HState (State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> HState JavaCfgState (EnterExitPair MJavaSig) i
forall a b. (a -> b) -> a -> b
$ do
let (t :: AnnTerm Label MJavaSig i
t :*: (Cond test succ fail)) = (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> (:*:)
(Cxt NoHole (Sum MJavaSig :&: Label) (K ()))
(Exp (HState JavaCfgState (EnterExitPair MJavaSig)))
i
forall (f :: (* -> *) -> * -> *) (gs :: [(* -> *) -> * -> *]) a
(t :: * -> *).
(HFunctor f, f :-<: gs) =>
(:&:) f a (AnnTerm a gs :*: t) :-> (AnnTerm a gs :*: f t)
collapseFProd' (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t'
AnnTerm Label MJavaSig i
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
-> State JavaCfgState (EnterExitPair MJavaSig i)
-> State JavaCfgState (EnterExitPair MJavaSig 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)
-> m (EnterExitPair fs es)
constructCfgCondOp AnnTerm Label MJavaSig i
t (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
test) (HState JavaCfgState (EnterExitPair MJavaSig) ExpL
-> StateT JavaCfgState Identity (EnterExitPair MJavaSig ExpL)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) ExpL
succ) (HState JavaCfgState (EnterExitPair MJavaSig) i
-> State JavaCfgState (EnterExitPair MJavaSig i)
forall s (f :: * -> *) l. HState s f l -> State s (f l)
unHState HState JavaCfgState (EnterExitPair MJavaSig) i
fail)
constructCfg t :: (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t = (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
-> HState JavaCfgState (EnterExitPair MJavaSig) 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 (:&:)
Exp
Label
(Cxt NoHole (Sum MJavaSig :&: Label) (K ())
:*: HState JavaCfgState (EnterExitPair MJavaSig))
i
t
instance CfgInitState MJavaSig where
cfgInitState :: Proxy MJavaSig -> CfgState MJavaSig
cfgInitState _ = Cfg MJavaSig
-> LabelGen -> LoopStack -> ScopedLabelMap -> JavaCfgState
JavaCfgState Cfg MJavaSig
forall (fs :: [(* -> *) -> * -> *]). Cfg fs
emptyCfg (() -> LabelGen
unsafeMkCSLabelGen ()) LoopStack
emptyLoopStack ScopedLabelMap
emptyScopedLabelMap
#endif