{-# LANGUAGE TemplateHaskell #-}

module Cubix.Language.Parametric.Semantics.Cfg.CommonNodes (
    constructCfgReturn
  , constructCfgEmpty
  , constructCfgIfElseIfElse

  , LoopStack
  , emptyLoopStack
  , HasLoopStack(..)
  , pushContinueNode
  , popContinueNode
  , pushBreakNode
  , popBreakNode
  , pushLoopNode
  , popLoopNode
  , constructCfgWhile
  , constructCfgDoWhile
  , constructCfgFor
  , constructCfgBreak
  , constructCfgContinue

  , LabelMap
  , emptyLabelMap
  , HasLabelMap(..)
  , constructCfgGoto
  , constructCfgLabel

  , ScopedLabelMap
  , emptyScopedLabelMap
  , HasScopedLabelMap(..)
  , withScopedLabel
  , edgeToScopedLabel
  , constructCfgScopedLabeledBreak
  , constructCfgScopedLabeledContinue
  , constructCfgScopedLabel

  , constructCfgShortCircuitingBinOp
  , constructCfgCondOp

) where

import Control.Monad ( liftM, when )
import Control.Monad.State ( MonadState )

import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Proxy ( Proxy(..) )
import Data.Traversable ( for )

import Control.Lens ( (^.), (%~), (%=), (.=), (.~), _2, at, use, makeClassy )

import Data.Comp.Multi ( HTraversable(..), All, HFunctor, HFoldable )

import Cubix.Language.Info
import Cubix.Language.Parametric.Semantics.Cfg.CfgConstruction
import Cubix.Language.Parametric.Semantics.Cfg.Graph
import Cubix.Language.Parametric.Semantics.SemanticProperties

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

eeNonEmpty :: EnterExitPair fs i -> Bool
eeNonEmpty :: forall (fs :: Signature) (i :: Sort). EnterExitPair fs i -> Bool
eeNonEmpty (EnterExitPair CfgNode fs
_ CfgNode fs
_) = Bool
True
eeNonEmpty EnterExitPair fs i
EmptyEnterExit      = Bool
False
eeNonEmpty EnterExitPair fs i
_                   = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"Passed non-collapsed EnterExitPair to eeNonEmpty"

collapseMaybeEnterExit :: Maybe (EnterExitPair fs i) -> EnterExitPair fs i
collapseMaybeEnterExit :: forall (fs :: Signature) (i :: Sort).
Maybe (EnterExitPair fs i) -> EnterExitPair fs i
collapseMaybeEnterExit (Just EnterExitPair fs i
eep) = EnterExitPair fs i
eep
collapseMaybeEnterExit Maybe (EnterExitPair fs i)
Nothing    = EnterExitPair fs i
forall (fs :: Signature) (l :: Sort). EnterExitPair fs l
EmptyEnterExit

mCombineEnterExit ::
  ( HasCurCfg s fs
  , MonadState s m
  , All HTraversable fs
  , All HFunctor fs
  , All HFoldable fs
  ) => m (EnterExitPair fs i) -> EnterExitPair fs j -> m (EnterExitPair fs k)
mCombineEnterExit :: forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, MonadState s m, All HTraversable fs,
 All HFunctor fs, All HFoldable fs) =>
m (EnterExitPair fs i)
-> EnterExitPair fs j -> m (EnterExitPair fs k)
mCombineEnterExit m (EnterExitPair fs i)
p1 EnterExitPair fs j
p2 = m (EnterExitPair fs i)
p1 m (EnterExitPair fs i)
-> (EnterExitPair fs i -> m (EnterExitPair fs k))
-> m (EnterExitPair fs k)
forall (a :: Sort) (b :: Sort). m a -> (a -> m b) -> m b
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
m a -> (a -> m b) -> m b
>>= (\EnterExitPair fs i
r -> EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit EnterExitPair fs i
r EnterExitPair fs j
p2)

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

-- Because we don't actually have function start and end nodes,
-- for now we can model "return" as just a black hole with no outgoing edges
-- This can also model the computed goto in GCC
constructCfgReturn ::
  ( MonadState s m
  , CfgComponent gs s
  ) => TermLab gs l -> m (Maybe (EnterExitPair gs i)) -> m (EnterExitPair gs l)
constructCfgReturn :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort).
(MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (Maybe (EnterExitPair gs i)) -> m (EnterExitPair gs l)
constructCfgReturn TermLab gs l
t m (Maybe (EnterExitPair gs i))
exp = do
  CfgNode gs
enterNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
exitNode  <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode
  EnterExitPair gs i
e <- (Maybe (EnterExitPair gs i) -> EnterExitPair gs i)
-> m (Maybe (EnterExitPair gs i)) -> m (EnterExitPair gs i)
forall (m :: Sort -> Sort) (a1 :: Sort) (r :: Sort).
Monad m =>
(a1 -> r) -> m a1 -> m r
liftM Maybe (EnterExitPair gs i) -> EnterExitPair gs i
forall (fs :: Signature) (i :: Sort).
Maybe (EnterExitPair fs i) -> EnterExitPair fs i
collapseMaybeEnterExit m (Maybe (EnterExitPair gs i))
exp
  EnterExitPair gs Any
-> EnterExitPair gs i -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit (CfgNode gs -> EnterExitPair gs Any
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> EnterExitPair fs l
identEnterExit CfgNode gs
enterNode) EnterExitPair gs i
e
  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs l
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode

constructCfgEmpty :: (MonadState s m, CfgComponent gs s) => TermLab gs l -> m (EnterExitPair gs l)
constructCfgEmpty :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort).
(MonadState s m, CfgComponent gs s) =>
TermLab gs l -> m (EnterExitPair gs l)
constructCfgEmpty TermLab gs l
t = do
  CfgNode gs
enterNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
exitNode  <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
enterNode CfgNode gs
exitNode
  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs l
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode


constructCfgIfElseIfElse ::
  ( 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 :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort) (j :: Sort) (k :: Sort).
(MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m [(EnterExitPair gs i, EnterExitPair gs j)]
-> m (Maybe (EnterExitPair gs k))
-> m (EnterExitPair gs l)
constructCfgIfElseIfElse TermLab gs l
t m [(EnterExitPair gs i, EnterExitPair gs j)]
clauses m (Maybe (EnterExitPair gs k))
optElse = do
  CfgNode gs
enterNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  [(EnterExitPair gs i, EnterExitPair gs j)]
evalledClauses <- m [(EnterExitPair gs i, EnterExitPair gs j)]
clauses

  [CfgNode gs]
midNodes <- [Int] -> (Int -> m (CfgNode gs)) -> m [CfgNode gs]
forall (t :: Sort -> Sort) (f :: Sort -> Sort) (a :: Sort)
       (b :: Sort).
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0..([(EnterExitPair gs i, EnterExitPair gs j)] -> Int
forall (a :: Sort). [a] -> Int
forall (t :: Sort -> Sort) (a :: Sort). Foldable t => t a -> Int
length [(EnterExitPair gs i, EnterExitPair gs j)]
evalledClauses Int -> Int -> Int
forall (a :: Sort). Num a => a -> a -> a
- Int
1)] ((Int -> m (CfgNode gs)) -> m [CfgNode gs])
-> (Int -> m (CfgNode gs)) -> m [CfgNode gs]
forall a b. (a -> b) -> a -> b
$ \Int
i ->
                        TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t (NodeEvaluationPoint -> CfgNodeType
evalPointToNodeType (Int -> NodeEvaluationPoint
BeforeIntermediateEvalPoint Int
i))

  CfgNode gs
exitNode  <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  [(EnterExitPair gs i, EnterExitPair gs j)]
-> ((EnterExitPair gs i, EnterExitPair gs j) -> m ()) -> m [()]
forall (t :: Sort -> Sort) (f :: Sort -> Sort) (a :: Sort)
       (b :: Sort).
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(EnterExitPair gs i, EnterExitPair gs j)]
evalledClauses (((EnterExitPair gs i, EnterExitPair gs j) -> m ()) -> m [()])
-> ((EnterExitPair gs i, EnterExitPair gs j) -> m ()) -> m [()]
forall a b. (a -> b) -> a -> b
$ \(EnterExitPair gs i
c, EnterExitPair gs j
b) -> do
    (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs i -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs i
c) (EnterExitPair gs j -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair gs j
b)
    (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs j -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs j
b) CfgNode gs
exitNode

  let condNodes :: [(CfgNode gs, EnterExitPair gs i)]
condNodes = [CfgNode gs]
-> [EnterExitPair gs i] -> [(CfgNode gs, EnterExitPair gs i)]
forall (a :: Sort) (b :: Sort). [a] -> [b] -> [(a, b)]
zip [CfgNode gs]
midNodes (((EnterExitPair gs i, EnterExitPair gs j) -> EnterExitPair gs i)
-> [(EnterExitPair gs i, EnterExitPair gs j)]
-> [EnterExitPair gs i]
forall (a :: Sort) (b :: Sort). (a -> b) -> [a] -> [b]
map (EnterExitPair gs i, EnterExitPair gs j) -> EnterExitPair gs i
forall (a :: Sort) (b :: Sort). (a, b) -> a
fst [(EnterExitPair gs i, EnterExitPair gs j)]
evalledClauses)
  let condPairs :: [((CfgNode gs, EnterExitPair gs i),
  (CfgNode gs, EnterExitPair gs i))]
condPairs = [(CfgNode gs, EnterExitPair gs i)]
-> [(CfgNode gs, EnterExitPair gs i)]
-> [((CfgNode gs, EnterExitPair gs i),
     (CfgNode gs, EnterExitPair gs i))]
forall (a :: Sort) (b :: Sort). [a] -> [b] -> [(a, b)]
zip [(CfgNode gs, EnterExitPair gs i)]
condNodes ([(CfgNode gs, EnterExitPair gs i)]
-> [(CfgNode gs, EnterExitPair gs i)]
forall (a :: Sort). HasCallStack => [a] -> [a]
tail [(CfgNode gs, EnterExitPair gs i)]
condNodes)

  [(CfgNode gs, EnterExitPair gs i)]
-> ((CfgNode gs, EnterExitPair gs i) -> m ()) -> m [()]
forall (t :: Sort -> Sort) (f :: Sort -> Sort) (a :: Sort)
       (b :: Sort).
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(CfgNode gs, EnterExitPair gs i)]
condNodes (((CfgNode gs, EnterExitPair gs i) -> m ()) -> m [()])
-> ((CfgNode gs, EnterExitPair gs i) -> m ()) -> m [()]
forall a b. (a -> b) -> a -> b
$ \(CfgNode gs
n, EnterExitPair gs i
x) -> (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
n (EnterExitPair gs i -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair gs i
x)

  [((CfgNode gs, EnterExitPair gs i),
  (CfgNode gs, EnterExitPair gs i))]
-> (((CfgNode gs, EnterExitPair gs i),
     (CfgNode gs, EnterExitPair gs i))
    -> m ())
-> m [()]
forall (t :: Sort -> Sort) (f :: Sort -> Sort) (a :: Sort)
       (b :: Sort).
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [((CfgNode gs, EnterExitPair gs i),
  (CfgNode gs, EnterExitPair gs i))]
condPairs ((((CfgNode gs, EnterExitPair gs i),
   (CfgNode gs, EnterExitPair gs i))
  -> m ())
 -> m [()])
-> (((CfgNode gs, EnterExitPair gs i),
     (CfgNode gs, EnterExitPair gs i))
    -> m ())
-> m [()]
forall a b. (a -> b) -> a -> b
$ \((CfgNode gs
xn, EnterExitPair gs i
x), (CfgNode gs
yn, EnterExitPair gs i
y)) -> do
    (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs i -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs i
x) CfgNode gs
yn

  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
enterNode ([CfgNode gs] -> CfgNode gs
forall (a :: Sort). HasCallStack => [a] -> a
head [CfgNode gs]
midNodes)

  Maybe (EnterExitPair gs k)
evalledOptElse <- m (Maybe (EnterExitPair gs k))
optElse
  let lastCondExit :: CfgNode gs
lastCondExit = EnterExitPair gs i -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit (EnterExitPair gs i -> CfgNode gs)
-> EnterExitPair gs i -> CfgNode gs
forall a b. (a -> b) -> a -> b
$ (EnterExitPair gs i, EnterExitPair gs j) -> EnterExitPair gs i
forall (a :: Sort) (b :: Sort). (a, b) -> a
fst ((EnterExitPair gs i, EnterExitPair gs j) -> EnterExitPair gs i)
-> (EnterExitPair gs i, EnterExitPair gs j) -> EnterExitPair gs i
forall a b. (a -> b) -> a -> b
$ [(EnterExitPair gs i, EnterExitPair gs j)]
-> (EnterExitPair gs i, EnterExitPair gs j)
forall (a :: Sort). HasCallStack => [a] -> a
last [(EnterExitPair gs i, EnterExitPair gs j)]
evalledClauses

  case Maybe (EnterExitPair gs k)
evalledOptElse of
    Maybe (EnterExitPair gs k)
Nothing             -> (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
lastCondExit CfgNode gs
exitNode
    Just EnterExitPair gs k
c              -> EnterExitPair gs k -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit EnterExitPair gs k
c m (EnterExitPair gs Any) -> (EnterExitPair gs Any -> m ()) -> m ()
forall (a :: Sort) (b :: Sort). m a -> (a -> m b) -> m b
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
m a -> (a -> m b) -> m b
>>= \EnterExitPair gs Any
c' -> case EnterExitPair gs Any
c' of
            EnterExitPair gs Any
EmptyEnterExit       -> (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
lastCondExit CfgNode gs
exitNode
            EnterExitPair CfgNode gs
ent CfgNode gs
ex -> do
               (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
lastCondExit CfgNode gs
ent
               (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
ex CfgNode gs
exitNode

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs l
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode


data LoopStack = LoopStack {
         LoopStack -> [Label]
_break_stack :: [Label]
       , LoopStack -> [Label]
_continue_stack :: [Label]
       }
  deriving ( LoopStack -> LoopStack -> Bool
(LoopStack -> LoopStack -> Bool)
-> (LoopStack -> LoopStack -> Bool) -> Eq LoopStack
forall (a :: Sort). (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LoopStack -> LoopStack -> Bool
== :: LoopStack -> LoopStack -> Bool
$c/= :: LoopStack -> LoopStack -> Bool
/= :: LoopStack -> LoopStack -> Bool
Eq, Eq LoopStack
Eq LoopStack =>
(LoopStack -> LoopStack -> Ordering)
-> (LoopStack -> LoopStack -> Bool)
-> (LoopStack -> LoopStack -> Bool)
-> (LoopStack -> LoopStack -> Bool)
-> (LoopStack -> LoopStack -> Bool)
-> (LoopStack -> LoopStack -> LoopStack)
-> (LoopStack -> LoopStack -> LoopStack)
-> Ord LoopStack
LoopStack -> LoopStack -> Bool
LoopStack -> LoopStack -> Ordering
LoopStack -> LoopStack -> LoopStack
forall (a :: Sort).
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LoopStack -> LoopStack -> Ordering
compare :: LoopStack -> LoopStack -> Ordering
$c< :: LoopStack -> LoopStack -> Bool
< :: LoopStack -> LoopStack -> Bool
$c<= :: LoopStack -> LoopStack -> Bool
<= :: LoopStack -> LoopStack -> Bool
$c> :: LoopStack -> LoopStack -> Bool
> :: LoopStack -> LoopStack -> Bool
$c>= :: LoopStack -> LoopStack -> Bool
>= :: LoopStack -> LoopStack -> Bool
$cmax :: LoopStack -> LoopStack -> LoopStack
max :: LoopStack -> LoopStack -> LoopStack
$cmin :: LoopStack -> LoopStack -> LoopStack
min :: LoopStack -> LoopStack -> LoopStack
Ord, Int -> LoopStack -> ShowS
[LoopStack] -> ShowS
LoopStack -> [Char]
(Int -> LoopStack -> ShowS)
-> (LoopStack -> [Char])
-> ([LoopStack] -> ShowS)
-> Show LoopStack
forall (a :: Sort).
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LoopStack -> ShowS
showsPrec :: Int -> LoopStack -> ShowS
$cshow :: LoopStack -> [Char]
show :: LoopStack -> [Char]
$cshowList :: [LoopStack] -> ShowS
showList :: [LoopStack] -> ShowS
Show )

emptyLoopStack :: LoopStack
emptyLoopStack :: LoopStack
emptyLoopStack = [Label] -> [Label] -> LoopStack
LoopStack [] []

makeClassy ''LoopStack

pushBreakNode :: (MonadState s m, HasLoopStack s) => CfgNode fs -> m ()
pushBreakNode :: forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> m ()
pushBreakNode CfgNode fs
n = ([Label] -> Identity [Label]) -> s -> Identity s
forall (c :: Sort). HasLoopStack c => Lens' c [Label]
Lens' s [Label]
break_stack (([Label] -> Identity [Label]) -> s -> Identity s)
-> ([Label] -> [Label]) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ((CfgNode fs
n CfgNode fs -> Getting Label (CfgNode fs) Label -> Label
forall (s :: Sort) (a :: Sort). s -> Getting a s a -> a
^. Getting Label (CfgNode fs) Label
forall (c :: Sort) (fs :: Signature).
HasCfgNode c fs =>
Lens' c Label
Lens' (CfgNode fs) Label
cfg_node_lab)Label -> [Label] -> [Label]
forall (a :: Sort). a -> [a] -> [a]
:)

popBreakNode :: (MonadState s m, HasLoopStack s) => m ()
popBreakNode :: forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLoopStack s) =>
m ()
popBreakNode = ([Label] -> Identity [Label]) -> s -> Identity s
forall (c :: Sort). HasLoopStack c => Lens' c [Label]
Lens' s [Label]
break_stack (([Label] -> Identity [Label]) -> s -> Identity s)
-> ([Label] -> [Label]) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= [Label] -> [Label]
forall (a :: Sort). HasCallStack => [a] -> [a]
tail

pushContinueNode :: (MonadState s m, HasLoopStack s) => CfgNode fs -> m ()
pushContinueNode :: forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> m ()
pushContinueNode CfgNode fs
n = ([Label] -> Identity [Label]) -> s -> Identity s
forall (c :: Sort). HasLoopStack c => Lens' c [Label]
Lens' s [Label]
continue_stack (([Label] -> Identity [Label]) -> s -> Identity s)
-> ([Label] -> [Label]) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ((CfgNode fs
n CfgNode fs -> Getting Label (CfgNode fs) Label -> Label
forall (s :: Sort) (a :: Sort). s -> Getting a s a -> a
^. Getting Label (CfgNode fs) Label
forall (c :: Sort) (fs :: Signature).
HasCfgNode c fs =>
Lens' c Label
Lens' (CfgNode fs) Label
cfg_node_lab)Label -> [Label] -> [Label]
forall (a :: Sort). a -> [a] -> [a]
:)

popContinueNode :: (MonadState s m, HasLoopStack s) => m ()
popContinueNode :: forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLoopStack s) =>
m ()
popContinueNode = ([Label] -> Identity [Label]) -> s -> Identity s
forall (c :: Sort). HasLoopStack c => Lens' c [Label]
Lens' s [Label]
continue_stack (([Label] -> Identity [Label]) -> s -> Identity s)
-> ([Label] -> [Label]) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= [Label] -> [Label]
forall (a :: Sort). HasCallStack => [a] -> [a]
tail

pushLoopNode :: (MonadState s m, HasLoopStack s) => CfgNode fs -> CfgNode fs -> m ()
pushLoopNode :: forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> CfgNode fs -> m ()
pushLoopNode CfgNode fs
n1 CfgNode fs
n2 = CfgNode fs -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> m ()
pushContinueNode CfgNode fs
n1 m () -> m () -> m ()
forall (a :: Sort) (b :: Sort). m a -> m b -> m b
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
m a -> m b -> m b
>> CfgNode fs -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> m ()
pushBreakNode CfgNode fs
n2

popLoopNode :: (MonadState s m, HasLoopStack s) => m ()
popLoopNode :: forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLoopStack s) =>
m ()
popLoopNode = m ()
forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLoopStack s) =>
m ()
popContinueNode m () -> m () -> m ()
forall (a :: Sort) (b :: Sort). m a -> m b -> m b
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
m a -> m b -> m b
>> m ()
forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLoopStack s) =>
m ()
popBreakNode

constructCfgWhile ::
  ( HasLoopStack s
  , MonadState s m
  , CfgComponent gs s
  ) => TermLab gs l -> m (EnterExitPair gs i) -> m (EnterExitPair gs j) -> m (EnterExitPair gs k)
constructCfgWhile :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort) (j :: Sort) (k :: Sort).
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (EnterExitPair gs i)
-> m (EnterExitPair gs j)
-> m (EnterExitPair gs k)
constructCfgWhile TermLab gs l
t m (EnterExitPair gs i)
mExp m (EnterExitPair gs j)
mBody = do
  CfgNode gs
enterNode     <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
loopEntryNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
LoopEntryNode
  CfgNode gs
exitNode      <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  EnterExitPair gs Any
exp <- m (EnterExitPair gs i)
mExp m (EnterExitPair gs i)
-> (EnterExitPair gs i -> m (EnterExitPair gs Any))
-> m (EnterExitPair gs Any)
forall (a :: Sort) (b :: Sort). m a -> (a -> m b) -> m b
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
m a -> (a -> m b) -> m b
>>= EnterExitPair gs i -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit
  CfgNode gs -> CfgNode gs -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> CfgNode fs -> m ()
pushLoopNode CfgNode gs
loopEntryNode CfgNode gs
exitNode
  EnterExitPair gs j
body <- m (EnterExitPair gs j)
mBody
  m ()
forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLoopStack s) =>
m ()
popLoopNode

  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
enterNode CfgNode gs
loopEntryNode
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
loopEntryNode (EnterExitPair gs Any -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair gs Any
exp)
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs Any -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs Any
exp) (EnterExitPair gs j -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair gs j
body)
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs Any -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs Any
exp) CfgNode gs
exitNode
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs j -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs j
body) CfgNode gs
loopEntryNode

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs k
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode

constructCfgDoWhile ::
  ( HasLoopStack s
  , MonadState s m
  , CfgComponent gs s
  ) => TermLab gs l -> m (EnterExitPair gs i) -> m (EnterExitPair gs j) -> m (EnterExitPair gs k)
constructCfgDoWhile :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort) (j :: Sort) (k :: Sort).
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (EnterExitPair gs i)
-> m (EnterExitPair gs j)
-> m (EnterExitPair gs k)
constructCfgDoWhile TermLab gs l
t m (EnterExitPair gs i)
mExp m (EnterExitPair gs j)
mBody = do
  CfgNode gs
enterNode     <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
loopEntryNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
LoopEntryNode
  CfgNode gs
exitNode      <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  EnterExitPair gs Any
exp <- m (EnterExitPair gs i)
mExp m (EnterExitPair gs i)
-> (EnterExitPair gs i -> m (EnterExitPair gs Any))
-> m (EnterExitPair gs Any)
forall (a :: Sort) (b :: Sort). m a -> (a -> m b) -> m b
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
m a -> (a -> m b) -> m b
>>= EnterExitPair gs i -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit
  CfgNode gs -> CfgNode gs -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> CfgNode fs -> m ()
pushLoopNode CfgNode gs
loopEntryNode CfgNode gs
exitNode
  EnterExitPair gs j
body <- m (EnterExitPair gs j)
mBody
  m ()
forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLoopStack s) =>
m ()
popLoopNode

  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
enterNode     (EnterExitPair gs j -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair gs j
body)
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs Any -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs Any
exp)    (EnterExitPair gs j -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair gs j
body)
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs Any -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs Any
exp)    CfgNode gs
exitNode
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs j -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs j
body)   CfgNode gs
loopEntryNode
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
loopEntryNode (EnterExitPair gs Any -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair gs Any
exp)

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs k
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode

constructCfgFor ::
  ( 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 :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (h :: Sort) (i :: Sort) (j :: Sort) (k :: Sort).
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l
-> m (Maybe (EnterExitPair gs h))
-> m (Maybe (EnterExitPair gs i))
-> m (Maybe (EnterExitPair gs j))
-> m (EnterExitPair gs k)
-> m (EnterExitPair gs l)
constructCfgFor TermLab gs l
t m (Maybe (EnterExitPair gs h))
mInit m (Maybe (EnterExitPair gs i))
mCond m (Maybe (EnterExitPair gs j))
mStep m (EnterExitPair gs k)
mBody = do
  CfgNode gs
enterNode     <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
loopEntryNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
LoopEntryNode
  CfgNode gs
exitNode      <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  EnterExitPair gs Any
init <- EnterExitPair gs h -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit (EnterExitPair gs h -> m (EnterExitPair gs Any))
-> m (EnterExitPair gs h) -> m (EnterExitPair gs Any)
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
(a -> m b) -> m a -> m b
=<< (Maybe (EnterExitPair gs h) -> EnterExitPair gs h)
-> m (Maybe (EnterExitPair gs h)) -> m (EnterExitPair gs h)
forall (m :: Sort -> Sort) (a1 :: Sort) (r :: Sort).
Monad m =>
(a1 -> r) -> m a1 -> m r
liftM Maybe (EnterExitPair gs h) -> EnterExitPair gs h
forall (fs :: Signature) (i :: Sort).
Maybe (EnterExitPair fs i) -> EnterExitPair fs i
collapseMaybeEnterExit m (Maybe (EnterExitPair gs h))
mInit
  EnterExitPair gs Any
cond <- EnterExitPair gs i -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit (EnterExitPair gs i -> m (EnterExitPair gs Any))
-> m (EnterExitPair gs i) -> m (EnterExitPair gs Any)
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
(a -> m b) -> m a -> m b
=<< (Maybe (EnterExitPair gs i) -> EnterExitPair gs i)
-> m (Maybe (EnterExitPair gs i)) -> m (EnterExitPair gs i)
forall (m :: Sort -> Sort) (a1 :: Sort) (r :: Sort).
Monad m =>
(a1 -> r) -> m a1 -> m r
liftM Maybe (EnterExitPair gs i) -> EnterExitPair gs i
forall (fs :: Signature) (i :: Sort).
Maybe (EnterExitPair fs i) -> EnterExitPair fs i
collapseMaybeEnterExit m (Maybe (EnterExitPair gs i))
mCond
  EnterExitPair gs Any
step <- EnterExitPair gs j -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> m (EnterExitPair fs j)
collapseEnterExit (EnterExitPair gs j -> m (EnterExitPair gs Any))
-> m (EnterExitPair gs j) -> m (EnterExitPair gs Any)
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
(a -> m b) -> m a -> m b
=<< (Maybe (EnterExitPair gs j) -> EnterExitPair gs j)
-> m (Maybe (EnterExitPair gs j)) -> m (EnterExitPair gs j)
forall (m :: Sort -> Sort) (a1 :: Sort) (r :: Sort).
Monad m =>
(a1 -> r) -> m a1 -> m r
liftM Maybe (EnterExitPair gs j) -> EnterExitPair gs j
forall (fs :: Signature) (i :: Sort).
Maybe (EnterExitPair fs i) -> EnterExitPair fs i
collapseMaybeEnterExit m (Maybe (EnterExitPair gs j))
mStep

  EnterExitPair gs Any
initCond <- EnterExitPair gs Any
-> EnterExitPair gs Any -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit EnterExitPair gs Any
init EnterExitPair gs Any
cond

  CfgNode gs -> CfgNode gs -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasLoopStack s) =>
CfgNode fs -> CfgNode fs -> m ()
pushLoopNode CfgNode gs
loopEntryNode CfgNode gs
exitNode
  EnterExitPair gs k
body <- m (EnterExitPair gs k)
mBody
  m ()
forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLoopStack s) =>
m ()
popLoopNode

  EnterExitPair gs Any
initCondBody <- EnterExitPair gs Any
-> EnterExitPair gs k -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
combineEnterExit EnterExitPair gs Any
initCond EnterExitPair gs k
body

  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
enterNode (EnterExitPair gs Any -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair gs Any
initCondBody)

  (((EnterExitPair gs k
body EnterExitPair gs k
-> EnterExitPair gs Any -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, All HTraversable fs, All HFoldable fs,
 All HFunctor fs, MonadState s m) =>
EnterExitPair fs i -> EnterExitPair fs j -> m (EnterExitPair fs k)
`combineEnterExit`  (CfgNode gs -> EnterExitPair gs Any
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> EnterExitPair fs l
identEnterExit CfgNode gs
loopEntryNode))
          m (EnterExitPair gs Any)
-> EnterExitPair gs Any -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, MonadState s m, All HTraversable fs,
 All HFunctor fs, All HFoldable fs) =>
m (EnterExitPair fs i)
-> EnterExitPair fs j -> m (EnterExitPair fs k)
`mCombineEnterExit` EnterExitPair gs Any
step)
          m (EnterExitPair gs Any)
-> EnterExitPair gs Any -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, MonadState s m, All HTraversable fs,
 All HFunctor fs, All HFoldable fs) =>
m (EnterExitPair fs i)
-> EnterExitPair fs j -> m (EnterExitPair fs k)
`mCombineEnterExit` EnterExitPair gs Any
cond)
          m (EnterExitPair gs Any)
-> EnterExitPair gs k -> m (EnterExitPair gs Any)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (i :: Sort) (j :: Sort) (k :: Sort).
(HasCurCfg s fs, MonadState s m, All HTraversable fs,
 All HFunctor fs, All HFoldable fs) =>
m (EnterExitPair fs i)
-> EnterExitPair fs j -> m (EnterExitPair fs k)
`mCombineEnterExit` EnterExitPair gs k
body

  Bool -> m () -> m ()
forall (f :: Sort -> Sort). Applicative f => Bool -> f () -> f ()
when (EnterExitPair gs Any -> Bool
forall (fs :: Signature) (i :: Sort). EnterExitPair fs i -> Bool
eeNonEmpty EnterExitPair gs Any
cond) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair gs Any -> CfgNode gs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair gs Any
cond) CfgNode gs
exitNode

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs l
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode



constructCfgBreak :: (HasLoopStack s, MonadState s m, CfgComponent gs s) => TermLab gs l -> m (EnterExitPair gs i)
constructCfgBreak :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort).
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> m (EnterExitPair gs i)
constructCfgBreak TermLab gs l
t = do
  CfgNode gs
enterNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
exitNode  <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  [Label]
l' <- Getting [Label] s [Label] -> m [Label]
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
MonadState s m =>
Getting a s a -> m a
use Getting [Label] s [Label]
forall (c :: Sort). HasLoopStack c => Lens' c [Label]
Lens' s [Label]
break_stack
  let (Label
l:[Label]
_) = [Label]
l'
  Maybe (CfgNode gs)
n' <- Label -> m (Maybe (CfgNode gs))
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort).
(HasCurCfg s fs, MonadState s m) =>
Label -> m (Maybe (CfgNode fs))
nodeForLab Label
l
  let Just CfgNode gs
n = Maybe (CfgNode gs)
n'
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
enterNode CfgNode gs
n -- go to end of loop
  -- do not connect enter to exit

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs i
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode

constructCfgContinue :: (HasLoopStack s, MonadState s m, CfgComponent gs s) => TermLab gs l -> m (EnterExitPair gs i)
constructCfgContinue :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort).
(HasLoopStack s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> m (EnterExitPair gs i)
constructCfgContinue TermLab gs l
t = do
  CfgNode gs
enterNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
exitNode  <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode
  [Label]
l' <- Getting [Label] s [Label] -> m [Label]
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
MonadState s m =>
Getting a s a -> m a
use Getting [Label] s [Label]
forall (c :: Sort). HasLoopStack c => Lens' c [Label]
Lens' s [Label]
continue_stack
  let (Label
l:[Label]
_) = [Label]
l'
  Maybe (CfgNode gs)
n' <- Label -> m (Maybe (CfgNode gs))
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort).
(HasCurCfg s fs, MonadState s m) =>
Label -> m (Maybe (CfgNode fs))
nodeForLab Label
l
  let Just CfgNode gs
n = Maybe (CfgNode gs)
n'
  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
enterNode CfgNode gs
n -- go to beginning of loop
  -- do not connect enter to exit

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs i
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode

-- For goto label nodes, we create a label for the node the first time it's referenced,
-- and accumulate a list of nodes that want to connect to it. When it's added for real, we clear this
--
-- "Label" can refer to both the annotation on nodes, and the program construct used as a goto target.
-- This is confusing.
data LabelMap = LabelMap {
                           LabelMap -> Map [Char] (Label, [Label])
_label_map :: Map String (Label, [Label])
                         }
  deriving ( LabelMap -> LabelMap -> Bool
(LabelMap -> LabelMap -> Bool)
-> (LabelMap -> LabelMap -> Bool) -> Eq LabelMap
forall (a :: Sort). (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LabelMap -> LabelMap -> Bool
== :: LabelMap -> LabelMap -> Bool
$c/= :: LabelMap -> LabelMap -> Bool
/= :: LabelMap -> LabelMap -> Bool
Eq, Eq LabelMap
Eq LabelMap =>
(LabelMap -> LabelMap -> Ordering)
-> (LabelMap -> LabelMap -> Bool)
-> (LabelMap -> LabelMap -> Bool)
-> (LabelMap -> LabelMap -> Bool)
-> (LabelMap -> LabelMap -> Bool)
-> (LabelMap -> LabelMap -> LabelMap)
-> (LabelMap -> LabelMap -> LabelMap)
-> Ord LabelMap
LabelMap -> LabelMap -> Bool
LabelMap -> LabelMap -> Ordering
LabelMap -> LabelMap -> LabelMap
forall (a :: Sort).
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LabelMap -> LabelMap -> Ordering
compare :: LabelMap -> LabelMap -> Ordering
$c< :: LabelMap -> LabelMap -> Bool
< :: LabelMap -> LabelMap -> Bool
$c<= :: LabelMap -> LabelMap -> Bool
<= :: LabelMap -> LabelMap -> Bool
$c> :: LabelMap -> LabelMap -> Bool
> :: LabelMap -> LabelMap -> Bool
$c>= :: LabelMap -> LabelMap -> Bool
>= :: LabelMap -> LabelMap -> Bool
$cmax :: LabelMap -> LabelMap -> LabelMap
max :: LabelMap -> LabelMap -> LabelMap
$cmin :: LabelMap -> LabelMap -> LabelMap
min :: LabelMap -> LabelMap -> LabelMap
Ord, Int -> LabelMap -> ShowS
[LabelMap] -> ShowS
LabelMap -> [Char]
(Int -> LabelMap -> ShowS)
-> (LabelMap -> [Char]) -> ([LabelMap] -> ShowS) -> Show LabelMap
forall (a :: Sort).
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LabelMap -> ShowS
showsPrec :: Int -> LabelMap -> ShowS
$cshow :: LabelMap -> [Char]
show :: LabelMap -> [Char]
$cshowList :: [LabelMap] -> ShowS
showList :: [LabelMap] -> ShowS
Show )

emptyLabelMap :: LabelMap
emptyLabelMap :: LabelMap
emptyLabelMap = Map [Char] (Label, [Label]) -> LabelMap
LabelMap Map [Char] (Label, [Label])
forall (k :: Sort) (a :: Sort). Map k a
Map.empty

makeClassy ''LabelMap

speculativeGetLabel :: (MonadState s m, HasLabelMap s, HasLabelGen s) => String -> m Label
speculativeGetLabel :: forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLabelMap s, HasLabelGen s) =>
[Char] -> m Label
speculativeGetLabel [Char]
s = do
  Map [Char] (Label, [Label])
lm <- Getting
  (Map [Char] (Label, [Label])) s (Map [Char] (Label, [Label]))
-> m (Map [Char] (Label, [Label]))
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
MonadState s m =>
Getting a s a -> m a
use Getting
  (Map [Char] (Label, [Label])) s (Map [Char] (Label, [Label]))
forall (c :: Sort).
HasLabelMap c =>
Lens' c (Map [Char] (Label, [Label]))
Lens' s (Map [Char] (Label, [Label]))
label_map
  case [Char] -> Map [Char] (Label, [Label]) -> Maybe (Label, [Label])
forall (k :: Sort) (a :: Sort). Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
s Map [Char] (Label, [Label])
lm of
    Just (Label
lab, [Label]
_) -> Label -> m Label
forall (a :: Sort). a -> m a
forall (m :: Sort -> Sort) (a :: Sort). Monad m => a -> m a
return Label
lab
    Maybe (Label, [Label])
Nothing -> do
      Label
lab <- m Label
forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLabelGen s) =>
m Label
nextLabel
      (Map [Char] (Label, [Label])
 -> Identity (Map [Char] (Label, [Label])))
-> s -> Identity s
forall (c :: Sort).
HasLabelMap c =>
Lens' c (Map [Char] (Label, [Label]))
Lens' s (Map [Char] (Label, [Label]))
label_map ((Map [Char] (Label, [Label])
  -> Identity (Map [Char] (Label, [Label])))
 -> s -> Identity s)
-> (Map [Char] (Label, [Label]) -> Map [Char] (Label, [Label]))
-> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= [Char]
-> (Label, [Label])
-> Map [Char] (Label, [Label])
-> Map [Char] (Label, [Label])
forall (k :: Sort) (a :: Sort).
Ord k =>
k -> a -> Map k a -> Map k a
Map.insert [Char]
s (Label
lab, [])
      return Label
lab

addGotoEdge :: (MonadState s m, HasLabelMap s, CfgComponent gs s) => CfgNode gs -> String -> m ()
addGotoEdge :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature).
(MonadState s m, HasLabelMap s, CfgComponent gs s) =>
CfgNode gs -> [Char] -> m ()
addGotoEdge CfgNode gs
n [Char]
targName = do
  Label
targL <- [Char] -> m Label
forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLabelMap s, HasLabelGen s) =>
[Char] -> m Label
speculativeGetLabel [Char]
targName
  Maybe (CfgNode gs)
targNode <- Label -> m (Maybe (CfgNode gs))
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort).
(HasCurCfg s fs, MonadState s m) =>
Label -> m (Maybe (CfgNode fs))
nodeForLab Label
targL
  case Maybe (CfgNode gs)
targNode of
    Just CfgNode gs
n' -> (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
n CfgNode gs
n'
    Maybe (CfgNode gs)
Nothing -> (Map [Char] (Label, [Label])
 -> Identity (Map [Char] (Label, [Label])))
-> s -> Identity s
forall (c :: Sort).
HasLabelMap c =>
Lens' c (Map [Char] (Label, [Label]))
Lens' s (Map [Char] (Label, [Label]))
label_map ((Map [Char] (Label, [Label])
  -> Identity (Map [Char] (Label, [Label])))
 -> s -> Identity s)
-> ((Maybe (Label, [Label]) -> Identity (Maybe (Label, [Label])))
    -> Map [Char] (Label, [Label])
    -> Identity (Map [Char] (Label, [Label])))
-> (Maybe (Label, [Label]) -> Identity (Maybe (Label, [Label])))
-> s
-> Identity s
forall (b :: Sort) (c :: Sort) (a :: Sort).
(b -> c) -> (a -> b) -> a -> c
. Index (Map [Char] (Label, [Label]))
-> Lens'
     (Map [Char] (Label, [Label]))
     (Maybe (IxValue (Map [Char] (Label, [Label]))))
forall (m :: Sort). At m => Index m -> Lens' m (Maybe (IxValue m))
at [Char]
Index (Map [Char] (Label, [Label]))
targName ((Maybe (Label, [Label]) -> Identity (Maybe (Label, [Label])))
 -> s -> Identity s)
-> (Maybe (Label, [Label]) -> Maybe (Label, [Label])) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ((Label, [Label]) -> (Label, [Label]))
-> Maybe (Label, [Label]) -> Maybe (Label, [Label])
forall (a :: Sort) (b :: Sort). (a -> b) -> Maybe a -> Maybe b
forall (f :: Sort -> Sort) (a :: Sort) (b :: Sort).
Functor f =>
(a -> b) -> f a -> f b
fmap (([Label] -> Identity [Label])
-> (Label, [Label]) -> Identity (Label, [Label])
forall (s :: Sort) (t :: Sort) (a :: Sort) (b :: Sort).
Field2 s t a b =>
Lens s t a b
Lens (Label, [Label]) (Label, [Label]) [Label] [Label]
_2 (([Label] -> Identity [Label])
 -> (Label, [Label]) -> Identity (Label, [Label]))
-> ([Label] -> [Label]) -> (Label, [Label]) -> (Label, [Label])
forall (s :: Sort) (t :: Sort) (a :: Sort) (b :: Sort).
ASetter s t a b -> (a -> b) -> s -> t
%~ ((CfgNode gs
n CfgNode gs -> Getting Label (CfgNode gs) Label -> Label
forall (s :: Sort) (a :: Sort). s -> Getting a s a -> a
^. Getting Label (CfgNode gs) Label
forall (c :: Sort) (fs :: Signature).
HasCfgNode c fs =>
Lens' c Label
Lens' (CfgNode gs) Label
cfg_node_lab)Label -> [Label] -> [Label]
forall (a :: Sort). a -> [a] -> [a]
:))

constructCfgGoto :: (MonadState s m, HasLabelMap s, CfgComponent gs s) => TermLab gs l -> String -> m (EnterExitPair gs i)
constructCfgGoto :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort).
(MonadState s m, HasLabelMap s, CfgComponent gs s) =>
TermLab gs l -> [Char] -> m (EnterExitPair gs i)
constructCfgGoto TermLab gs l
t [Char]
targ = do
  CfgNode gs
enterNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
exitNode  <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  CfgNode gs -> [Char] -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature).
(MonadState s m, HasLabelMap s, CfgComponent gs s) =>
CfgNode gs -> [Char] -> m ()
addGotoEdge CfgNode gs
enterNode [Char]
targ
  -- do not connect enter to exit

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs i
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode

constructCfgLabel :: forall gs s m l i. (MonadState s m, HasLabelMap s, CfgComponent gs s) => TermLab gs l -> String -> m (EnterExitPair gs i)
constructCfgLabel :: forall (gs :: Signature) (s :: Sort) (m :: Sort -> Sort)
       (l :: Sort) (i :: Sort).
(MonadState s m, HasLabelMap s, CfgComponent gs s) =>
TermLab gs l -> [Char] -> m (EnterExitPair gs i)
constructCfgLabel TermLab gs l
t [Char]
name = do
  Map [Char] (Label, [Label])
lm <- Getting
  (Map [Char] (Label, [Label])) s (Map [Char] (Label, [Label]))
-> m (Map [Char] (Label, [Label]))
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
MonadState s m =>
Getting a s a -> m a
use Getting
  (Map [Char] (Label, [Label])) s (Map [Char] (Label, [Label]))
forall (c :: Sort).
HasLabelMap c =>
Lens' c (Map [Char] (Label, [Label]))
Lens' s (Map [Char] (Label, [Label]))
label_map

  CfgNode gs
enterNode <- case [Char] -> Map [Char] (Label, [Label]) -> Maybe (Label, [Label])
forall (k :: Sort) (a :: Sort). Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
name Map [Char] (Label, [Label])
lm of
    Maybe (Label, [Label])
Nothing -> do
      Label
l <- m Label
forall (s :: Sort) (m :: Sort -> Sort).
(MonadState s m, HasLabelGen s) =>
m Label
nextLabel
      CfgNode gs
n <- TermLab gs l -> Label -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, MonadState s m) =>
TermLab fs l -> Label -> CfgNodeType -> m (CfgNode fs)
addCfgNodeWithLabel TermLab gs l
t Label
l CfgNodeType
EnterNode
      (Map [Char] (Label, [Label])
 -> Identity (Map [Char] (Label, [Label])))
-> s -> Identity s
forall (c :: Sort).
HasLabelMap c =>
Lens' c (Map [Char] (Label, [Label]))
Lens' s (Map [Char] (Label, [Label]))
label_map ((Map [Char] (Label, [Label])
  -> Identity (Map [Char] (Label, [Label])))
 -> s -> Identity s)
-> (Map [Char] (Label, [Label]) -> Map [Char] (Label, [Label]))
-> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= [Char]
-> (Label, [Label])
-> Map [Char] (Label, [Label])
-> Map [Char] (Label, [Label])
forall (k :: Sort) (a :: Sort).
Ord k =>
k -> a -> Map k a -> Map k a
Map.insert [Char]
name (Label
l, [])
      pure CfgNode gs
n

    Just (Label
l, [Label]
prevs) -> do
      CfgNode gs
n <- TermLab gs l -> Label -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, MonadState s m) =>
TermLab fs l -> Label -> CfgNodeType -> m (CfgNode fs)
addCfgNodeWithLabel TermLab gs l
t Label
l CfgNodeType
EnterNode
      [Label] -> (Label -> m ()) -> m [()]
forall (t :: Sort -> Sort) (f :: Sort -> Sort) (a :: Sort)
       (b :: Sort).
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Label]
prevs ((Label -> m ()) -> m [()]) -> (Label -> m ()) -> m [()]
forall a b. (a -> b) -> a -> b
$ \Label
p -> (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= forall (fs :: Signature). Label -> Label -> Cfg fs -> Cfg fs
addEdgeLab @gs Label
p Label
l
      (Map [Char] (Label, [Label])
 -> Identity (Map [Char] (Label, [Label])))
-> s -> Identity s
forall (c :: Sort).
HasLabelMap c =>
Lens' c (Map [Char] (Label, [Label]))
Lens' s (Map [Char] (Label, [Label]))
label_map ((Map [Char] (Label, [Label])
  -> Identity (Map [Char] (Label, [Label])))
 -> s -> Identity s)
-> ((Maybe (Label, [Label]) -> Identity (Maybe (Label, [Label])))
    -> Map [Char] (Label, [Label])
    -> Identity (Map [Char] (Label, [Label])))
-> (Maybe (Label, [Label]) -> Identity (Maybe (Label, [Label])))
-> s
-> Identity s
forall (b :: Sort) (c :: Sort) (a :: Sort).
(b -> c) -> (a -> b) -> a -> c
. Index (Map [Char] (Label, [Label]))
-> Lens'
     (Map [Char] (Label, [Label]))
     (Maybe (IxValue (Map [Char] (Label, [Label]))))
forall (m :: Sort). At m => Index m -> Lens' m (Maybe (IxValue m))
at [Char]
Index (Map [Char] (Label, [Label]))
name ((Maybe (Label, [Label]) -> Identity (Maybe (Label, [Label])))
 -> s -> Identity s)
-> (Maybe (Label, [Label]) -> Maybe (Label, [Label])) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ((Label, [Label]) -> (Label, [Label]))
-> Maybe (Label, [Label]) -> Maybe (Label, [Label])
forall (a :: Sort) (b :: Sort). (a -> b) -> Maybe a -> Maybe b
forall (f :: Sort -> Sort) (a :: Sort) (b :: Sort).
Functor f =>
(a -> b) -> f a -> f b
fmap (([Label] -> Identity [Label])
-> (Label, [Label]) -> Identity (Label, [Label])
forall (s :: Sort) (t :: Sort) (a :: Sort) (b :: Sort).
Field2 s t a b =>
Lens s t a b
Lens (Label, [Label]) (Label, [Label]) [Label] [Label]
_2 (([Label] -> Identity [Label])
 -> (Label, [Label]) -> Identity (Label, [Label]))
-> [Label] -> (Label, [Label]) -> (Label, [Label])
forall (s :: Sort) (t :: Sort) (a :: Sort) (b :: Sort).
ASetter s t a b -> b -> s -> t
.~ [])
      return CfgNode gs
n


  CfgNode gs
exitNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  (Cfg gs -> Identity (Cfg gs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg gs)
cur_cfg ((Cfg gs -> Identity (Cfg gs)) -> s -> Identity s)
-> (Cfg gs -> Cfg gs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode gs -> CfgNode gs -> Cfg gs -> Cfg gs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode gs
enterNode CfgNode gs
exitNode
  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs i
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode

-- |
-- Use this if labels are lexically scoped and may not be shadowed
-- In accordance with the representable/valid principle, we are not reusing LabelMap
-- for this purpose. LabelMap is for C's goto labels; ScopedLabelMap is for Java/JS labeled break/continue
data ScopedLabelMap = ScopedLabelMap {
                           ScopedLabelMap -> Map [Char] (Map CfgNodeType Label)
_scoped_label_map :: Map String (Map CfgNodeType Label)
                         }
  deriving ( ScopedLabelMap -> ScopedLabelMap -> Bool
(ScopedLabelMap -> ScopedLabelMap -> Bool)
-> (ScopedLabelMap -> ScopedLabelMap -> Bool) -> Eq ScopedLabelMap
forall (a :: Sort). (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ScopedLabelMap -> ScopedLabelMap -> Bool
== :: ScopedLabelMap -> ScopedLabelMap -> Bool
$c/= :: ScopedLabelMap -> ScopedLabelMap -> Bool
/= :: ScopedLabelMap -> ScopedLabelMap -> Bool
Eq, Eq ScopedLabelMap
Eq ScopedLabelMap =>
(ScopedLabelMap -> ScopedLabelMap -> Ordering)
-> (ScopedLabelMap -> ScopedLabelMap -> Bool)
-> (ScopedLabelMap -> ScopedLabelMap -> Bool)
-> (ScopedLabelMap -> ScopedLabelMap -> Bool)
-> (ScopedLabelMap -> ScopedLabelMap -> Bool)
-> (ScopedLabelMap -> ScopedLabelMap -> ScopedLabelMap)
-> (ScopedLabelMap -> ScopedLabelMap -> ScopedLabelMap)
-> Ord ScopedLabelMap
ScopedLabelMap -> ScopedLabelMap -> Bool
ScopedLabelMap -> ScopedLabelMap -> Ordering
ScopedLabelMap -> ScopedLabelMap -> ScopedLabelMap
forall (a :: Sort).
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ScopedLabelMap -> ScopedLabelMap -> Ordering
compare :: ScopedLabelMap -> ScopedLabelMap -> Ordering
$c< :: ScopedLabelMap -> ScopedLabelMap -> Bool
< :: ScopedLabelMap -> ScopedLabelMap -> Bool
$c<= :: ScopedLabelMap -> ScopedLabelMap -> Bool
<= :: ScopedLabelMap -> ScopedLabelMap -> Bool
$c> :: ScopedLabelMap -> ScopedLabelMap -> Bool
> :: ScopedLabelMap -> ScopedLabelMap -> Bool
$c>= :: ScopedLabelMap -> ScopedLabelMap -> Bool
>= :: ScopedLabelMap -> ScopedLabelMap -> Bool
$cmax :: ScopedLabelMap -> ScopedLabelMap -> ScopedLabelMap
max :: ScopedLabelMap -> ScopedLabelMap -> ScopedLabelMap
$cmin :: ScopedLabelMap -> ScopedLabelMap -> ScopedLabelMap
min :: ScopedLabelMap -> ScopedLabelMap -> ScopedLabelMap
Ord, Int -> ScopedLabelMap -> ShowS
[ScopedLabelMap] -> ShowS
ScopedLabelMap -> [Char]
(Int -> ScopedLabelMap -> ShowS)
-> (ScopedLabelMap -> [Char])
-> ([ScopedLabelMap] -> ShowS)
-> Show ScopedLabelMap
forall (a :: Sort).
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopedLabelMap -> ShowS
showsPrec :: Int -> ScopedLabelMap -> ShowS
$cshow :: ScopedLabelMap -> [Char]
show :: ScopedLabelMap -> [Char]
$cshowList :: [ScopedLabelMap] -> ShowS
showList :: [ScopedLabelMap] -> ShowS
Show )

emptyScopedLabelMap :: ScopedLabelMap
emptyScopedLabelMap :: ScopedLabelMap
emptyScopedLabelMap = Map [Char] (Map CfgNodeType Label) -> ScopedLabelMap
ScopedLabelMap Map [Char] (Map CfgNodeType Label)
forall (k :: Sort) (a :: Sort). Map k a
Map.empty

makeClassy ''ScopedLabelMap

withScopedLabel :: (MonadState s m, HasScopedLabelMap s) => String -> Map CfgNodeType Label -> m a -> m a
withScopedLabel :: forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
(MonadState s m, HasScopedLabelMap s) =>
[Char] -> Map CfgNodeType Label -> m a -> m a
withScopedLabel [Char]
s Map CfgNodeType Label
labMap m a
m = do
  Map [Char] (Map CfgNodeType Label)
oldLabMap <- Getting
  (Map [Char] (Map CfgNodeType Label))
  s
  (Map [Char] (Map CfgNodeType Label))
-> m (Map [Char] (Map CfgNodeType Label))
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
MonadState s m =>
Getting a s a -> m a
use Getting
  (Map [Char] (Map CfgNodeType Label))
  s
  (Map [Char] (Map CfgNodeType Label))
forall (c :: Sort).
HasScopedLabelMap c =>
Lens' c (Map [Char] (Map CfgNodeType Label))
Lens' s (Map [Char] (Map CfgNodeType Label))
scoped_label_map
  (Map [Char] (Map CfgNodeType Label)
 -> Identity (Map [Char] (Map CfgNodeType Label)))
-> s -> Identity s
forall (c :: Sort).
HasScopedLabelMap c =>
Lens' c (Map [Char] (Map CfgNodeType Label))
Lens' s (Map [Char] (Map CfgNodeType Label))
scoped_label_map ((Map [Char] (Map CfgNodeType Label)
  -> Identity (Map [Char] (Map CfgNodeType Label)))
 -> s -> Identity s)
-> (Map [Char] (Map CfgNodeType Label)
    -> Map [Char] (Map CfgNodeType Label))
-> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= [Char]
-> Map CfgNodeType Label
-> Map [Char] (Map CfgNodeType Label)
-> Map [Char] (Map CfgNodeType Label)
forall (k :: Sort) (a :: Sort).
Ord k =>
k -> a -> Map k a -> Map k a
Map.insert [Char]
s Map CfgNodeType Label
labMap
  a
res <- m a
m
  (Map [Char] (Map CfgNodeType Label)
 -> Identity (Map [Char] (Map CfgNodeType Label)))
-> s -> Identity s
forall (c :: Sort).
HasScopedLabelMap c =>
Lens' c (Map [Char] (Map CfgNodeType Label))
Lens' s (Map [Char] (Map CfgNodeType Label))
scoped_label_map ((Map [Char] (Map CfgNodeType Label)
  -> Identity (Map [Char] (Map CfgNodeType Label)))
 -> s -> Identity s)
-> Map [Char] (Map CfgNodeType Label) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Map [Char] (Map CfgNodeType Label)
oldLabMap
  return a
res


nodeForScopedLabel :: (MonadState s m, HasScopedLabelMap s, CfgComponent fs s) => String -> CfgNodeType -> m (Maybe (CfgNode fs))
nodeForScopedLabel :: forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasScopedLabelMap s, CfgComponent fs s) =>
[Char] -> CfgNodeType -> m (Maybe (CfgNode fs))
nodeForScopedLabel [Char]
nm CfgNodeType
tp = do
  Map [Char] (Map CfgNodeType Label)
slm <- Getting
  (Map [Char] (Map CfgNodeType Label))
  s
  (Map [Char] (Map CfgNodeType Label))
-> m (Map [Char] (Map CfgNodeType Label))
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
MonadState s m =>
Getting a s a -> m a
use Getting
  (Map [Char] (Map CfgNodeType Label))
  s
  (Map [Char] (Map CfgNodeType Label))
forall (c :: Sort).
HasScopedLabelMap c =>
Lens' c (Map [Char] (Map CfgNodeType Label))
Lens' s (Map [Char] (Map CfgNodeType Label))
scoped_label_map
  Cfg fs
gr <- Getting (Cfg fs) s (Cfg fs) -> m (Cfg fs)
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
MonadState s m =>
Getting a s a -> m a
use Getting (Cfg fs) s (Cfg fs)
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg
  return ([Char]
-> Map [Char] (Map CfgNodeType Label)
-> Maybe (Map CfgNodeType Label)
forall (k :: Sort) (a :: Sort). Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
nm Map [Char] (Map CfgNodeType Label)
slm Maybe (Map CfgNodeType Label)
-> (Map CfgNodeType Label -> Maybe Label) -> Maybe Label
forall (a :: Sort) (b :: Sort).
Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
m a -> (a -> m b) -> m b
>>= CfgNodeType -> Map CfgNodeType Label -> Maybe Label
forall (k :: Sort) (a :: Sort). Ord k => k -> Map k a -> Maybe a
Map.lookup CfgNodeType
tp Maybe Label -> (Label -> Maybe (CfgNode fs)) -> Maybe (CfgNode fs)
forall (a :: Sort) (b :: Sort).
Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
Monad m =>
m a -> (a -> m b) -> m b
>>= Cfg fs -> Label -> Maybe (CfgNode fs)
forall (fs :: Signature). Cfg fs -> Label -> Maybe (CfgNode fs)
safeLookupCfg Cfg fs
gr)

edgeToScopedLabel :: (MonadState s m, HasScopedLabelMap s, CfgComponent fs s) => CfgNode fs -> String -> CfgNodeType -> m ()
edgeToScopedLabel :: forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasScopedLabelMap s, CfgComponent fs s) =>
CfgNode fs -> [Char] -> CfgNodeType -> m ()
edgeToScopedLabel CfgNode fs
n [Char]
targName CfgNodeType
targTp = do
  Maybe (CfgNode fs)
targNode <- [Char] -> CfgNodeType -> m (Maybe (CfgNode fs))
forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasScopedLabelMap s, CfgComponent fs s) =>
[Char] -> CfgNodeType -> m (Maybe (CfgNode fs))
nodeForScopedLabel [Char]
targName CfgNodeType
targTp
  case Maybe (CfgNode fs)
targNode of
    Maybe (CfgNode fs)
Nothing -> [Char] -> m ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Label " [Char] -> ShowS
forall (a :: Sort). [a] -> [a] -> [a]
++ ShowS
forall (a :: Sort). Show a => a -> [Char]
show [Char]
targName [Char] -> ShowS
forall (a :: Sort). [a] -> [a] -> [a]
++ [Char]
" has no node of type " [Char] -> ShowS
forall (a :: Sort). [a] -> [a] -> [a]
++ CfgNodeType -> [Char]
forall (a :: Sort). Show a => a -> [Char]
show CfgNodeType
targTp
    Just CfgNode fs
n' -> (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode fs
n CfgNode fs
n'



constructCfgScopedLabeledBreak :: (HasScopedLabelMap s, MonadState s m, CfgComponent gs s) => TermLab gs l -> String -> m (EnterExitPair gs i)
constructCfgScopedLabeledBreak :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort).
(HasScopedLabelMap s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> [Char] -> m (EnterExitPair gs i)
constructCfgScopedLabeledBreak TermLab gs l
t [Char]
labStr = do
  CfgNode gs
enterNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
exitNode  <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  CfgNode gs -> [Char] -> CfgNodeType -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasScopedLabelMap s, CfgComponent fs s) =>
CfgNode fs -> [Char] -> CfgNodeType -> m ()
edgeToScopedLabel CfgNode gs
enterNode [Char]
labStr CfgNodeType
ExitNode
  -- do not connect enter to exit

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs i
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode


constructCfgScopedLabeledContinue :: (HasScopedLabelMap s, MonadState s m, CfgComponent gs s) => TermLab gs l -> String -> m (EnterExitPair gs i)
constructCfgScopedLabeledContinue :: forall (s :: Sort) (m :: Sort -> Sort) (gs :: Signature)
       (l :: Sort) (i :: Sort).
(HasScopedLabelMap s, MonadState s m, CfgComponent gs s) =>
TermLab gs l -> [Char] -> m (EnterExitPair gs i)
constructCfgScopedLabeledContinue TermLab gs l
t [Char]
labStr = do
  CfgNode gs
enterNode <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
EnterNode
  CfgNode gs
exitNode  <- TermLab gs l -> CfgNodeType -> m (CfgNode gs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab gs l
t CfgNodeType
ExitNode

  CfgNode gs -> [Char] -> CfgNodeType -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature).
(MonadState s m, HasScopedLabelMap s, CfgComponent fs s) =>
CfgNode fs -> [Char] -> CfgNodeType -> m ()
edgeToScopedLabel CfgNode gs
enterNode [Char]
labStr CfgNodeType
LoopEntryNode
  -- do not connect enter to exit

  return $ CfgNode gs -> CfgNode gs -> EnterExitPair gs i
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode gs
enterNode CfgNode gs
exitNode

constructCfgScopedLabel ::
  ( HasScopedLabelMap s
  , MonadState s m
  , CfgComponent fs s
  ) => TermLab fs l -> String -> TermLab fs s0 -> m (EnterExitPair fs s0) -> m (EnterExitPair fs i)
constructCfgScopedLabel :: forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature)
       (l :: Sort) (s0 :: Sort) (i :: Sort).
(HasScopedLabelMap s, MonadState s m, CfgComponent fs s) =>
TermLab fs l
-> [Char]
-> TermLab fs s0
-> m (EnterExitPair fs s0)
-> m (EnterExitPair fs i)
constructCfgScopedLabel TermLab fs l
t [Char]
labName TermLab fs s0
s m (EnterExitPair fs s0)
mStmt = do
  CfgNode fs
enterNode     <- TermLab fs l -> CfgNodeType -> m (CfgNode fs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab fs l
t CfgNodeType
EnterNode
  CfgNode fs
loopEntryNode <- TermLab fs l -> CfgNodeType -> m (CfgNode fs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab fs l
t CfgNodeType
LoopEntryNode
  CfgNode fs
exitNode      <- TermLab fs l -> CfgNodeType -> m (CfgNode fs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab fs l
t CfgNodeType
ExitNode

  -- Using a label as a continue target is not valid unless the labeled statement is a loop
  -- We assume that this code is valid JS / Java, and hence loopEntryNode is unused unless
  -- stmt is a loop
  let labMap :: Map CfgNodeType Label
labMap = [(CfgNodeType, Label)] -> Map CfgNodeType Label
forall (k :: Sort) (a :: Sort). Ord k => [(k, a)] -> Map k a
Map.fromList [ (CfgNodeType
LoopEntryNode, CfgNode fs
loopEntryNode CfgNode fs -> Getting Label (CfgNode fs) Label -> Label
forall (s :: Sort) (a :: Sort). s -> Getting a s a -> a
^. Getting Label (CfgNode fs) Label
forall (c :: Sort) (fs :: Signature).
HasCfgNode c fs =>
Lens' c Label
Lens' (CfgNode fs) Label
cfg_node_lab)
                            , (CfgNodeType
ExitNode, CfgNode fs
exitNode CfgNode fs -> Getting Label (CfgNode fs) Label -> Label
forall (s :: Sort) (a :: Sort). s -> Getting a s a -> a
^. Getting Label (CfgNode fs) Label
forall (c :: Sort) (fs :: Signature).
HasCfgNode c fs =>
Lens' c Label
Lens' (CfgNode fs) Label
cfg_node_lab)
                            ]

  EnterExitPair fs s0
stmt <- [Char]
-> Map CfgNodeType Label
-> m (EnterExitPair fs s0)
-> m (EnterExitPair fs s0)
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
(MonadState s m, HasScopedLabelMap s) =>
[Char] -> Map CfgNodeType Label -> m a -> m a
withScopedLabel [Char]
labName Map CfgNodeType Label
labMap m (EnterExitPair fs s0)
mStmt
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode fs
enterNode (EnterExitPair fs s0 -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair fs s0
stmt)
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair fs s0 -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair fs s0
stmt) CfgNode fs
exitNode

  -- loopEntryNode is just a temporary; contract it out
  Cfg fs
gr <- Getting (Cfg fs) s (Cfg fs) -> m (Cfg fs)
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort).
MonadState s m =>
Getting a s a -> m a
use Getting (Cfg fs) s (Cfg fs)
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg
  case Cfg fs -> CfgNodeType -> TermLab fs s0 -> Maybe (CfgNode fs)
forall (fs :: Signature) (l :: Sort).
Cfg fs -> CfgNodeType -> TermLab fs l -> Maybe (CfgNode fs)
cfgNodeForTerm Cfg fs
gr CfgNodeType
LoopEntryNode TermLab fs s0
s of
    Maybe (CfgNode fs)
Nothing -> () -> m ()
forall (a :: Sort). a -> m a
forall (m :: Sort -> Sort) (a :: Sort). Monad m => a -> m a
return ()
    Just CfgNode fs
n  -> (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode fs
loopEntryNode CfgNode fs
n

  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Label -> Cfg fs -> Cfg fs
forall (fs :: Signature). Label -> Cfg fs -> Cfg fs
contractNode (CfgNode fs
loopEntryNode CfgNode fs -> Getting Label (CfgNode fs) Label -> Label
forall (s :: Sort) (a :: Sort). s -> Getting a s a -> a
^. Getting Label (CfgNode fs) Label
forall (c :: Sort) (fs :: Signature).
HasCfgNode c fs =>
Lens' c Label
Lens' (CfgNode fs) Label
cfg_node_lab)

  return (CfgNode fs -> CfgNode fs -> EnterExitPair fs i
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode fs
enterNode CfgNode fs
exitNode)

constructCfgShortCircuitingBinOp ::
  ( MonadState s m
  , CfgComponent fs s
  ) => TermLab fs l -> m (EnterExitPair fs ls) -> m (EnterExitPair fs rs) -> m (EnterExitPair fs es)
constructCfgShortCircuitingBinOp :: forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature)
       (l :: Sort) (ls :: Sort) (rs :: Sort) (es :: Sort).
(MonadState s m, CfgComponent fs s) =>
TermLab fs l
-> m (EnterExitPair fs ls)
-> m (EnterExitPair fs rs)
-> m (EnterExitPair fs es)
constructCfgShortCircuitingBinOp TermLab fs l
t m (EnterExitPair fs ls)
mlArg m (EnterExitPair fs rs)
mrArg = do
  CfgNode fs
enterNode <- TermLab fs l -> CfgNodeType -> m (CfgNode fs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab fs l
t CfgNodeType
EnterNode
  CfgNode fs
exitNode  <- TermLab fs l -> CfgNodeType -> m (CfgNode fs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab fs l
t CfgNodeType
ExitNode
  EnterExitPair fs ls
lArg <- m (EnterExitPair fs ls)
mlArg
  EnterExitPair fs rs
rArg <- m (EnterExitPair fs rs)
mrArg
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode fs
enterNode (EnterExitPair fs ls -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair fs ls
lArg)
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair fs ls -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair fs ls
lArg) (EnterExitPair fs rs -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair fs rs
rArg)
  -- NOTE: short circuit edge.
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair fs ls -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair fs ls
lArg) CfgNode fs
exitNode
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair fs rs -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair fs rs
rArg) CfgNode fs
exitNode
  return (CfgNode fs -> CfgNode fs -> EnterExitPair fs es
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode fs
enterNode CfgNode fs
exitNode)

constructCfgCondOp ::
  ( 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 :: forall (s :: Sort) (m :: Sort -> Sort) (fs :: Signature)
       (l :: Sort) (ls :: Sort) (rs :: Sort) (es :: Sort).
(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 TermLab fs l
t m (EnterExitPair fs ls)
mtest m (EnterExitPair fs rs)
msucc m (EnterExitPair fs es)
mfail = do
  CfgNode fs
enterNode <- TermLab fs l -> CfgNodeType -> m (CfgNode fs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab fs l
t CfgNodeType
EnterNode
  CfgNode fs
exitNode  <- TermLab fs l -> CfgNodeType -> m (CfgNode fs)
forall (s :: Sort) (fs :: Signature) (m :: Sort -> Sort)
       (l :: Sort).
(HasCurCfg s fs, HasLabelGen s, MonadState s m) =>
TermLab fs l -> CfgNodeType -> m (CfgNode fs)
addCfgNode TermLab fs l
t CfgNodeType
ExitNode
  EnterExitPair fs ls
test <- m (EnterExitPair fs ls)
mtest
  EnterExitPair fs rs
succ <- m (EnterExitPair fs rs)
msucc
  EnterExitPair fs es
fail <- m (EnterExitPair fs es)
mfail
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge CfgNode fs
enterNode (EnterExitPair fs ls -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair fs ls
test)
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair fs ls -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair fs ls
test) (EnterExitPair fs rs -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair fs rs
succ)
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair fs ls -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair fs ls
test) (EnterExitPair fs es -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
enter EnterExitPair fs es
fail)
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair fs rs -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair fs rs
succ) CfgNode fs
exitNode
  (Cfg fs -> Identity (Cfg fs)) -> s -> Identity s
forall (c :: Sort) (fs :: Signature).
HasCurCfg c fs =>
Lens' c (Cfg fs)
Lens' s (Cfg fs)
cur_cfg ((Cfg fs -> Identity (Cfg fs)) -> s -> Identity s)
-> (Cfg fs -> Cfg fs) -> m ()
forall (s :: Sort) (m :: Sort -> Sort) (a :: Sort) (b :: Sort).
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
forall (fs :: Signature).
CfgNode fs -> CfgNode fs -> Cfg fs -> Cfg fs
addEdge (EnterExitPair fs es -> CfgNode fs
forall (fs :: Signature) (l :: Sort).
EnterExitPair fs l -> CfgNode fs
exit EnterExitPair fs es
fail) CfgNode fs
exitNode
  return (CfgNode fs -> CfgNode fs -> EnterExitPair fs es
forall (fs :: Signature) (l :: Sort).
CfgNode fs -> CfgNode fs -> EnterExitPair fs l
EnterExitPair CfgNode fs
enterNode CfgNode fs
exitNode)