{-# 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]]

-- Putting catch's here is a hack
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

-- Java code won't compile if the compiler detects unreachable code. For
-- example, while (true); stmt; will not compile because stmt is unreachable,
-- and so we should construct our CFG graph such that we won't generate
-- unreachable code. Here we perform a very basic check whether the loop
-- condition is always true, always false, or could be either. If always true or
-- always false, certain CFG edges are omitted.
--
-- See JLS 7 section 14.21, "Unreachable Statements."
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

    -- NOTE: fallthrough
    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)

  -- I think it will work to just pretend try-catch-finally blocks are separate computation units, and
  -- throw's go nowhere
  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