{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}


module Language.Explorer.Monadic
    ( Explorer
    , mkExplorer
    , mkExplorerNoSharing
    , execute
    , executeAll
    , revert
    , jump
    , toTree
    , incomingEdges
    , config
    , execEnv
    , currRef
    , leaves
    , Ref
    , Language
    , deref
    , getTrace
    , getTraces
    , getPathsFromTo
    , getPathFromTo
    , executionGraph
    , shadowExecEnv
    , eqClasses
    , initialRef
    , fromExport
    , toExport
    ) where

import Data.Graph.Inductive.Graph
import Data.Graph.Inductive.PatriciaTree
import Data.Graph.Inductive.Query
import Data.Graph.Inductive.Query.SP
import Data.Tree (Tree(..))

import qualified Data.IntMap as IntMap
import Data.List
import Data.Foldable
import Data.Maybe

type Ref = Int
type Language p m c o = (Eq p, Eq o, Monad m, Monoid o)

data Explorer programs m configs output where
    Explorer :: Language programs m configs output =>
        { Explorer programs m configs output -> Bool
shadowing :: Bool -- Shadow the exploration tree in a shadow graph.
        , Explorer programs m configs output
-> programs -> configs -> m (Maybe configs, output)
defInterp :: programs -> configs -> m (Maybe configs, output)
        , Explorer programs m configs output -> configs
config :: configs -- Cache the config
        , Explorer programs m configs output -> Ref
currRef :: Ref
        , Explorer programs m configs output -> Ref
genRef :: Ref
        , Explorer programs m configs output -> IntMap configs
cmap :: IntMap.IntMap configs
        , Explorer programs m configs output -> Gr Ref (programs, output)
execEnv :: Gr Ref (programs, output)
        , Explorer programs m configs output -> Gr [Ref] (programs, output)
shadowExecEnv :: Gr [Ref] (programs, output)
        , Explorer programs m configs output -> configs -> configs -> Bool
configEq :: configs -> configs -> Bool
        } -> Explorer programs m configs output


mkExplorer :: Language p m c o => Bool -> (c -> c -> Bool) -> (p -> c -> m (Maybe c, o)) -> c -> Explorer p m c o
mkExplorer :: Bool
-> (c -> c -> Bool)
-> (p -> c -> m (Maybe c, o))
-> c
-> Explorer p m c o
mkExplorer Bool
shadow c -> c -> Bool
shadowEq p -> c -> m (Maybe c, o)
definterp c
conf = Explorer :: forall programs (m :: * -> *) configs output.
Language programs m configs output =>
Bool
-> (programs -> configs -> m (Maybe configs, output))
-> configs
-> Ref
-> Ref
-> IntMap configs
-> Gr Ref (programs, output)
-> Gr [Ref] (programs, output)
-> (configs -> configs -> Bool)
-> Explorer programs m configs output
Explorer
    { defInterp :: p -> c -> m (Maybe c, o)
defInterp = p -> c -> m (Maybe c, o)
definterp
    , config :: c
config = c
conf
    , genRef :: Ref
genRef = Ref
1 -- Currently generate references by increasing a counter.
    , currRef :: Ref
currRef = Ref
initialRef
    , cmap :: IntMap c
cmap = [(Ref, c)] -> IntMap c
forall a. [(Ref, a)] -> IntMap a
IntMap.fromList [(Ref
initialRef, c
conf)]
    , execEnv :: Gr Ref (p, o)
execEnv = [LNode Ref] -> [LEdge (p, o)] -> Gr Ref (p, o)
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [(Ref
initialRef, Ref
initialRef)] []
    , shadowExecEnv :: Gr [Ref] (p, o)
shadowExecEnv = [LNode [Ref]] -> [LEdge (p, o)] -> Gr [Ref] (p, o)
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [(Ref
initialRef, [Ref
initialRef])] []
    , shadowing :: Bool
shadowing = Bool
shadow
    , configEq :: c -> c -> Bool
configEq = c -> c -> Bool
shadowEq
}

initialRef :: Int
initialRef :: Ref
initialRef = Ref
1

mkExplorerNoSharing :: Language p m c o  => (p -> c -> m (Maybe c, o)) -> c -> Explorer p m c o
mkExplorerNoSharing :: (p -> c -> m (Maybe c, o)) -> c -> Explorer p m c o
mkExplorerNoSharing = Bool
-> (c -> c -> Bool)
-> (p -> c -> m (Maybe c, o))
-> c
-> Explorer p m c o
forall p (m :: * -> *) c o.
Language p m c o =>
Bool
-> (c -> c -> Bool)
-> (p -> c -> m (Maybe c, o))
-> c
-> Explorer p m c o
mkExplorer Bool
False (\c
_ -> \c
_ -> Bool
False)

deref :: Explorer p m c o -> Ref -> Maybe c
deref :: Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
e Ref
r = Ref -> IntMap c -> Maybe c
forall a. Ref -> IntMap a -> Maybe a
IntMap.lookup Ref
r (Explorer p m c o -> IntMap c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
e)

findRef :: Explorer p m c o -> c -> (c -> Bool) -> Maybe (Ref, c)
findRef :: Explorer p m c o -> c -> (c -> Bool) -> Maybe (Ref, c)
findRef Explorer p m c o
e c
c c -> Bool
eq = ((Ref, c) -> Bool) -> [(Ref, c)] -> Maybe (Ref, c)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(Ref
r, c
c') -> c -> Bool
eq c
c') (IntMap c -> [(Ref, c)]
forall a. IntMap a -> [(Ref, a)]
IntMap.toList (Explorer p m c o -> IntMap c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
e))

addNewPath :: Explorer p m c o -> p -> o -> c -> Explorer p m c o
addNewPath :: Explorer p m c o -> p -> o -> c -> Explorer p m c o
addNewPath Explorer p m c o
e p
p o
o c
c = Explorer p m c o
e { config :: c
config = c
c, currRef :: Ref
currRef = Ref
newref, genRef :: Ref
genRef = Ref
newref, cmap :: IntMap c
cmap = Ref -> c -> IntMap c -> IntMap c
forall a. Ref -> a -> IntMap a -> IntMap a
IntMap.insert Ref
newref c
c (Explorer p m c o -> IntMap c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
e),
     execEnv :: Gr Ref (p, o)
execEnv = LNode Ref -> Gr Ref (p, o) -> Gr Ref (p, o)
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Ref
newref, Ref
newref) (Gr Ref (p, o) -> Gr Ref (p, o)) -> Gr Ref (p, o) -> Gr Ref (p, o)
forall a b. (a -> b) -> a -> b
$ LEdge (p, o) -> Gr Ref (p, o) -> Gr Ref (p, o)
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e, Ref
newref, (p
p,o
o)) (Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
e)}
     where newref :: Ref
newref = Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
genRef Explorer p m c o
e Ref -> Ref -> Ref
forall a. Num a => a -> a -> a
+ Ref
1


findNodeRef :: Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef :: Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef Gr [Ref] (p, o)
g Ref
r = LNode [Ref] -> Ref
forall a b. (a, b) -> a
fst (LNode [Ref] -> Ref) -> LNode [Ref] -> Ref
forall a b. (a -> b) -> a -> b
$ Maybe (LNode [Ref]) -> LNode [Ref]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (LNode [Ref]) -> LNode [Ref])
-> Maybe (LNode [Ref]) -> LNode [Ref]
forall a b. (a -> b) -> a -> b
$ (LNode [Ref] -> Bool) -> [LNode [Ref]] -> Maybe (LNode [Ref])
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(Ref
_, [Ref]
rs) -> Ref
r Ref -> [Ref] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
rs) ([LNode [Ref]] -> Maybe (LNode [Ref]))
-> [LNode [Ref]] -> Maybe (LNode [Ref])
forall a b. (a -> b) -> a -> b
$ Gr [Ref] (p, o) -> [LNode [Ref]]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr [Ref] (p, o)
g


updateShadowEnv :: Language p m c o => Explorer p m c o -> (p, c, o, Ref, Ref) -> Explorer p m c o
updateShadowEnv :: Explorer p m c o -> (p, c, o, Ref, Ref) -> Explorer p m c o
updateShadowEnv Explorer p m c o
e (p
p, c
newconf, o
output, Ref
newref, Ref
oldref) =
  case Explorer p m c o -> c -> (c -> Bool) -> Maybe (Ref, c)
forall p (m :: * -> *) c o.
Explorer p m c o -> c -> (c -> Bool) -> Maybe (Ref, c)
findRef Explorer p m c o
e c
newconf (Explorer p m c o -> c -> c -> Bool
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> configs -> configs -> Bool
configEq Explorer p m c o
e c
newconf) of
    Just (Ref
r', c
_) ->
      if Gr [Ref] (p, o) -> LEdge (p, o) -> Bool
forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge Gr [Ref] (p, o)
shadowEnv (Ref
nref, Gr [Ref] (p, o) -> Ref -> Ref
forall p o. Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef Gr [Ref] (p, o)
shadowEnv Ref
r', (p
p, o
output))
        then Explorer p m c o
e
        else Explorer p m c o
e {
          shadowExecEnv :: Gr [Ref] (p, o)
shadowExecEnv = (Ref, Ref, p, o) -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall (gr :: * -> * -> *) a c d b.
DynGraph gr =>
(Ref, a, c, d) -> gr [a] b -> gr [a] b
updateLabel (Gr [Ref] (p, o) -> Ref -> Ref
forall p o. Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef Gr [Ref] (p, o)
shadowEnv Ref
r', Ref
newref, p
p, o
output) (Gr [Ref] (p, o) -> Gr [Ref] (p, o))
-> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall a b. (a -> b) -> a -> b
$ LEdge (p, o) -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Ref
nref, Gr [Ref] (p, o) -> Ref -> Ref
forall p o. Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef Gr [Ref] (p, o)
shadowEnv Ref
r', (p
p, o
output)) Gr [Ref] (p, o)
shadowEnv
        }
    Maybe (Ref, c)
Nothing -> Explorer p m c o
e {
      shadowExecEnv :: Gr [Ref] (p, o)
shadowExecEnv = LNode [Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Ref
newref, [Ref
newref]) (Gr [Ref] (p, o) -> Gr [Ref] (p, o))
-> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall a b. (a -> b) -> a -> b
$ LEdge (p, o) -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Ref
nref, Ref
newref, (p
p, o
output)) (Gr [Ref] (p, o) -> Gr [Ref] (p, o))
-> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Gr [Ref] (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr [Ref] (programs, output)
shadowExecEnv Explorer p m c o
e
    }
    where
      shadowEnv :: Gr [Ref] (p, o)
shadowEnv = Explorer p m c o -> Gr [Ref] (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr [Ref] (programs, output)
shadowExecEnv Explorer p m c o
e
      nref :: Ref
nref = Gr [Ref] (p, o) -> Ref -> Ref
forall p o. Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef Gr [Ref] (p, o)
shadowEnv Ref
oldref
      updateLabel :: (Ref, a, c, d) -> gr [a] b -> gr [a] b
updateLabel (Ref
target, a
add_to_label, c
p, d
output) gr [a] b
gr =
        case Ref -> gr [a] b -> Decomp gr [a] b
forall (gr :: * -> * -> *) a b.
Graph gr =>
Ref -> gr a b -> Decomp gr a b
match Ref
target gr [a] b
gr of
          (Just (Adj b
toadj, Ref
node, [a]
label, Adj b
fromadj), gr [a] b
decomgr) -> (Adj b
toadj, Ref
node, a
add_to_label a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
label, Adj b
fromadj) Context [a] b -> gr [a] b -> gr [a] b
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
Context a b -> gr a b -> gr a b
& gr [a] b
decomgr
          Decomp gr [a] b
_ -> [Char] -> gr [a] b
forall a. HasCallStack => [Char] -> a
error [Char]
"Shadow execution environment is inconsistent."


updateExecEnvs :: Language p m c o => Explorer p m c o -> (p, c, o) -> Explorer p m c o
updateExecEnvs :: Explorer p m c o -> (p, c, o) -> Explorer p m c o
updateExecEnvs Explorer p m c o
e (p
p, c
newconf, o
output)
  | Explorer p m c o -> Bool
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Bool
shadowing Explorer p m c o
e = Explorer p m c o -> p -> o -> c -> Explorer p m c o
forall p (m :: * -> *) c o.
Explorer p m c o -> p -> o -> c -> Explorer p m c o
addNewPath (Explorer p m c o -> (p, c, o, Ref, Ref) -> Explorer p m c o
forall p (m :: * -> *) c o.
Language p m c o =>
Explorer p m c o -> (p, c, o, Ref, Ref) -> Explorer p m c o
updateShadowEnv Explorer p m c o
e (p
p, c
newconf, o
output, (Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
newexplorer), (Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e))) p
p o
output c
newconf
  | Bool
otherwise = Explorer p m c o
newexplorer
  where
    newexplorer :: Explorer p m c o
newexplorer = Explorer p m c o -> p -> o -> c -> Explorer p m c o
forall p (m :: * -> *) c o.
Explorer p m c o -> p -> o -> c -> Explorer p m c o
addNewPath Explorer p m c o
e p
p o
output c
newconf

execute :: Language p m c o =>  p -> Explorer p m c o -> m (Explorer p m c o, o)
execute :: p -> Explorer p m c o -> m (Explorer p m c o, o)
execute p
p Explorer p m c o
e =
  do (Maybe c
mcfg, o
o) <- Explorer p m c o -> p -> c -> m (Maybe c, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output
-> programs -> configs -> m (Maybe configs, output)
defInterp Explorer p m c o
e p
p (Explorer p m c o -> c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> configs
config Explorer p m c o
e)
     case Maybe c
mcfg of
       Just c
cfg -> (Explorer p m c o, o) -> m (Explorer p m c o, o)
forall (m :: * -> *) a. Monad m => a -> m a
return (Explorer p m c o -> (p, c, o) -> Explorer p m c o
forall p (m :: * -> *) c o.
Language p m c o =>
Explorer p m c o -> (p, c, o) -> Explorer p m c o
updateExecEnvs Explorer p m c o
e (p
p, c
cfg, o
o), o
o)
       Maybe c
Nothing  -> (Explorer p m c o, o) -> m (Explorer p m c o, o)
forall (m :: * -> *) a. Monad m => a -> m a
return (Explorer p m c o
e, o
o)

executeAll :: Language p m c o => [p] -> Explorer p m c o -> m (Explorer p m c o, o)
executeAll :: [p] -> Explorer p m c o -> m (Explorer p m c o, o)
executeAll [p]
ps Explorer p m c o
exp = ((Explorer p m c o, o) -> p -> m (Explorer p m c o, o))
-> (Explorer p m c o, o) -> [p] -> m (Explorer p m c o, o)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (Explorer p m c o, o) -> p -> m (Explorer p m c o, o)
forall (m :: * -> *) p b c.
(Monad m, Eq p, Eq b, Monoid b) =>
(Explorer p m c b, b) -> p -> m (Explorer p m c b, b)
executeCollect (Explorer p m c o
exp, o
forall a. Monoid a => a
mempty) [p]
ps
  where executeCollect :: (Explorer p m c b, b) -> p -> m (Explorer p m c b, b)
executeCollect (Explorer p m c b
exp, b
out) p
p = do (Explorer p m c b
res, b
out') <- p -> Explorer p m c b -> m (Explorer p m c b, b)
forall p (m :: * -> *) c o.
Language p m c o =>
p -> Explorer p m c o -> m (Explorer p m c o, o)
execute p
p Explorer p m c b
exp
                                         (Explorer p m c b, b) -> m (Explorer p m c b, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Explorer p m c b
res, b
out b -> b -> b
forall a. Monoid a => a -> a -> a
`mappend` b
out')

deleteMap :: [Ref] -> IntMap.IntMap a -> IntMap.IntMap a
deleteMap :: [Ref] -> IntMap a -> IntMap a
deleteMap [Ref]
xs IntMap a
m = (IntMap a -> Ref -> IntMap a) -> IntMap a -> [Ref] -> IntMap a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Ref -> IntMap a -> IntMap a) -> IntMap a -> Ref -> IntMap a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Ref -> IntMap a -> IntMap a
forall a. Ref -> IntMap a -> IntMap a
IntMap.delete) IntMap a
m [Ref]
xs


deleteFromShadowEnv :: [(Ref, Ref)] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv :: [LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv [(Ref
l, Ref
r)] Gr [Ref] po
gr = case Ref -> Gr [Ref] po -> Decomp Gr [Ref] po
forall (gr :: * -> * -> *) a b.
Graph gr =>
Ref -> gr a b -> Decomp gr a b
match Ref
r Gr [Ref] po
gr of
  (Just (Adj po
toadj, Ref
node, [Ref]
label, Adj po
fromadj), Gr [Ref] po
decomgr) -> (Adj po
toadj, Ref
node, [Ref]
label [Ref] -> [Ref] -> [Ref]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Ref
l], Adj po
fromadj) Context [Ref] po -> Gr [Ref] po -> Gr [Ref] po
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
Context a b -> gr a b -> gr a b
& Gr [Ref] po
decomgr
  Decomp Gr [Ref] po
_ -> [Char] -> Gr [Ref] po
forall a. HasCallStack => [Char] -> a
error [Char]
"Inconsistent shadow env."
deleteFromShadowEnv (LNode Ref
x:[LNode Ref]
xs) Gr [Ref] po
gr = [LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
forall po. [LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv [LNode Ref]
xs ([LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
forall po. [LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv [LNode Ref
x] Gr [Ref] po
gr)

cleanEdges :: [Ref] -> [(Ref, Ref, (p, o))] -> [(Ref, Ref, (p, o))]
cleanEdges :: [Ref] -> [(Ref, Ref, (p, o))] -> [(Ref, Ref, (p, o))]
cleanEdges [Ref]
ref [(Ref, Ref, (p, o))]
edg = ((Ref, Ref, (p, o)) -> Bool)
-> [(Ref, Ref, (p, o))] -> [(Ref, Ref, (p, o))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ref
s, Ref
t, (p, o)
l) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Ref
t Ref -> [Ref] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
ref) [(Ref, Ref, (p, o))]
edg

cleanShadowEnv :: Bool -> [Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
cleanShadowEnv :: Bool -> [Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
cleanShadowEnv Bool
False [Ref]
_ Gr [Ref] (p, o)
g = Gr [Ref] (p, o)
g
cleanShadowEnv Bool
True [Ref]
nds Gr [Ref] (p, o)
g = Gr [Ref] (p, o)
shadowEnv''
  where
    shadowEnv' :: Gr [Ref] (p, o)
shadowEnv' = [LNode Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall po. [LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv ((Ref -> LNode Ref) -> [Ref] -> [LNode Ref]
forall a b. (a -> b) -> [a] -> [b]
map (\Ref
r -> (Ref
r, Gr [Ref] (p, o) -> Ref -> Ref
forall p o. Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef Gr [Ref] (p, o)
g Ref
r)) [Ref]
nds) Gr [Ref] (p, o)
g
    nodesToDel' :: [Ref]
nodesToDel' = (LNode [Ref] -> Ref) -> [LNode [Ref]] -> [Ref]
forall a b. (a -> b) -> [a] -> [b]
map LNode [Ref] -> Ref
forall a b. (a, b) -> a
fst ((LNode [Ref] -> Bool) -> [LNode [Ref]] -> [LNode [Ref]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ref
r, [Ref]
labels) -> [Ref]
labels [Ref] -> [Ref] -> Bool
forall a. Eq a => a -> a -> Bool
== []) ([LNode [Ref]] -> [LNode [Ref]]) -> [LNode [Ref]] -> [LNode [Ref]]
forall a b. (a -> b) -> a -> b
$ Gr [Ref] (p, o) -> [LNode [Ref]]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (Gr [Ref] (p, o)
shadowEnv'))
    edgesToDel' :: [LNode Ref]
edgesToDel' = (LNode Ref -> Bool) -> [LNode Ref] -> [LNode Ref]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ref
s, Ref
t) -> Ref
s Ref -> [Ref] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
nodesToDel' Bool -> Bool -> Bool
|| Ref
t Ref -> [Ref] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
nodesToDel') (Gr [Ref] (p, o) -> [LNode Ref]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode Ref]
edges Gr [Ref] (p, o)
shadowEnv')
    shadowEnv'' :: Gr [Ref] (p, o)
shadowEnv'' = ([LNode Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
[LNode Ref] -> gr a b -> gr a b
delEdges [LNode Ref]
edgesToDel' (Gr [Ref] (p, o) -> Gr [Ref] (p, o))
-> (Gr [Ref] (p, o) -> Gr [Ref] (p, o))
-> Gr [Ref] (p, o)
-> Gr [Ref] (p, o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall (gr :: * -> * -> *) a b.
Graph gr =>
[Ref] -> gr a b -> gr a b
delNodes [Ref]
nodesToDel') Gr [Ref] (p, o)
shadowEnv'

data RevertableStatus = ContinueRevert | StopRevert deriving Ref -> RevertableStatus -> ShowS
[RevertableStatus] -> ShowS
RevertableStatus -> [Char]
(Ref -> RevertableStatus -> ShowS)
-> (RevertableStatus -> [Char])
-> ([RevertableStatus] -> ShowS)
-> Show RevertableStatus
forall a.
(Ref -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [RevertableStatus] -> ShowS
$cshowList :: [RevertableStatus] -> ShowS
show :: RevertableStatus -> [Char]
$cshow :: RevertableStatus -> [Char]
showsPrec :: Ref -> RevertableStatus -> ShowS
$cshowsPrec :: Ref -> RevertableStatus -> ShowS
Show

findRevertableNodes :: gr a b -> Ref -> Ref -> [Ref]
findRevertableNodes gr a b
gr Ref
source Ref
target =
  case gr a b -> Ref -> Ref -> Maybe Ref
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Ref -> Ref -> Maybe Ref
findNextNodeInPath gr a b
gr Ref
source Ref
target of
    (Just Ref
node) -> ([Ref], RevertableStatus) -> [Ref]
forall a b. (a, b) -> a
fst (([Ref], RevertableStatus) -> [Ref])
-> ([Ref], RevertableStatus) -> [Ref]
forall a b. (a -> b) -> a -> b
$ gr a b -> Ref -> Ref -> ([Ref], RevertableStatus)
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Ref -> Ref -> ([Ref], RevertableStatus)
findRevertableNodes' gr a b
gr Ref
node Ref
target
    Maybe Ref
Nothing     -> []
  where
    findNextNodeInPath :: gr a b -> Ref -> Ref -> Maybe Ref
findNextNodeInPath gr a b
gr Ref
source Ref
target = (Ref -> Bool) -> [Ref] -> Maybe Ref
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\Ref
n -> Ref
target Ref -> [Ref] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Ref -> gr a b -> [Ref]
forall (gr :: * -> * -> *) a b. Graph gr => Ref -> gr a b -> [Ref]
reachable Ref
n gr a b
gr)) (gr a b -> Ref -> [Ref]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Ref -> [Ref]
suc gr a b
gr Ref
source)
    findRevertableNodes' :: gr a b -> Ref -> Ref -> ([Ref], RevertableStatus)
findRevertableNodes' gr a b
gr Ref
source Ref
target
      | Ref
source Ref -> Ref -> Bool
forall a. Eq a => a -> a -> Bool
== Ref
target = if gr a b -> Ref -> Ref
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Ref -> Ref
outdeg gr a b
gr Ref
source Ref -> Ref -> Bool
forall a. Ord a => a -> a -> Bool
> Ref
1 then ([], RevertableStatus
StopRevert) else ([Ref
source], RevertableStatus
ContinueRevert)
      | Bool
otherwise = case gr a b -> Ref -> Ref -> Maybe Ref
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Ref -> Ref -> Maybe Ref
findNextNodeInPath gr a b
gr Ref
source Ref
target of
        (Just Ref
node) -> case gr a b -> Ref -> Ref -> ([Ref], RevertableStatus)
findRevertableNodes' gr a b
gr Ref
node Ref
target of
          ([Ref]
res, RevertableStatus
StopRevert) -> ([Ref]
res, RevertableStatus
StopRevert)
          ([Ref]
res, RevertableStatus
ContinueRevert) -> if gr a b -> Ref -> Ref
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Ref -> Ref
outdeg gr a b
gr Ref
source Ref -> Ref -> Bool
forall a. Ord a => a -> a -> Bool
> Ref
1 then ([Ref]
res, RevertableStatus
StopRevert) else (Ref
source Ref -> [Ref] -> [Ref]
forall a. a -> [a] -> [a]
: [Ref]
res, RevertableStatus
ContinueRevert)
        Maybe Ref
Nothing -> ([], RevertableStatus
ContinueRevert)

revert :: Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
revert :: Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
revert Ref
r Explorer p m c o
e
  | Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e Ref -> [Ref] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
reachNodes =
      Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
forall p (m :: * -> *) c o.
Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
jump Ref
r Explorer p m c o
e Maybe (Explorer p m c o)
-> (Explorer p m c o -> Maybe (Explorer p m c o))
-> Maybe (Explorer p m c o)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Explorer p m c o
e' -> Explorer p m c o -> Maybe (Explorer p m c o)
forall (m :: * -> *) a. Monad m => a -> m a
return (Explorer p m c o -> Maybe (Explorer p m c o))
-> Explorer p m c o -> Maybe (Explorer p m c o)
forall a b. (a -> b) -> a -> b
$ Explorer p m c o
e' { execEnv :: Gr Ref (p, o)
execEnv = [LNode Ref] -> [LEdge (p, o)] -> Gr Ref (p, o)
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph ([Ref] -> [Ref] -> [LNode Ref]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ref]
remainNodes [Ref]
remainNodes) ([LEdge (p, o)] -> Gr Ref (p, o))
-> [LEdge (p, o)] -> Gr Ref (p, o)
forall a b. (a -> b) -> a -> b
$ [Ref] -> [LEdge (p, o)] -> [LEdge (p, o)]
forall p o. [Ref] -> [(Ref, Ref, (p, o))] -> [(Ref, Ref, (p, o))]
cleanEdges [Ref]
reachNodes (Gr Ref (p, o) -> [LEdge (p, o)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Gr Ref (p, o) -> [LEdge (p, o)])
-> Gr Ref (p, o) -> [LEdge (p, o)]
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
e')
                                      ,  cmap :: IntMap c
cmap = [Ref] -> IntMap c -> IntMap c
forall a. [Ref] -> IntMap a -> IntMap a
deleteMap [Ref]
reachNodes (Explorer p m c o -> IntMap c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
e')
                                      , shadowExecEnv :: Gr [Ref] (p, o)
shadowExecEnv = Bool -> [Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
forall p o. Bool -> [Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
cleanShadowEnv (Explorer p m c o -> Bool
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Bool
shadowing Explorer p m c o
e') [Ref]
reachNodes (Explorer p m c o -> Gr [Ref] (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr [Ref] (programs, output)
shadowExecEnv Explorer p m c o
e')}
  | Bool
otherwise = Maybe (Explorer p m c o)
forall a. Maybe a
Nothing
  where
    reachNodes :: [Ref]
reachNodes = Gr Ref (p, o) -> Ref -> Ref -> [Ref]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Ref -> Ref -> [Ref]
findRevertableNodes Gr Ref (p, o)
gr Ref
r (Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e)
    remainNodes :: [Ref]
remainNodes = Gr Ref (p, o) -> [Ref]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Ref]
nodes Gr Ref (p, o)
gr [Ref] -> [Ref] -> [Ref]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Ref]
reachNodes
    gr :: Gr Ref (p, o)
gr = Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
e

jump :: Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
jump :: Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
jump Ref
r Explorer p m c o
e = case Explorer p m c o -> Ref -> Maybe c
forall p (m :: * -> *) c o. Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
e Ref
r of
             (Just c
c) -> Explorer p m c o -> Maybe (Explorer p m c o)
forall (m :: * -> *) a. Monad m => a -> m a
return (Explorer p m c o -> Maybe (Explorer p m c o))
-> Explorer p m c o -> Maybe (Explorer p m c o)
forall a b. (a -> b) -> a -> b
$ Explorer p m c o
e { config :: c
config = c
c, currRef :: Ref
currRef = Ref
r }
             Maybe c
Nothing -> Maybe (Explorer p m c o)
forall a. Maybe a
Nothing

toTree :: Explorer p m c o -> Tree (Ref, c)
toTree :: Explorer p m c o -> Tree (Ref, c)
toTree Explorer p m c o
exp = Ref -> Tree (Ref, c)
mkTree Ref
initialRef
  where graph :: Gr Ref (p, o)
graph = Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
exp
        target :: (a, b, c) -> b
target (a
_, b
r, c
_) = b
r
        mkTree :: Ref -> Tree (Ref, c)
mkTree Ref
r = (Ref, c) -> Forest (Ref, c) -> Tree (Ref, c)
forall a. a -> Forest a -> Tree a
Node (Ref
r, Explorer p m c o -> IntMap c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
exp IntMap c -> Ref -> c
forall a. IntMap a -> Ref -> a
IntMap.! Ref
r) (((Ref, Ref, (p, o)) -> Tree (Ref, c))
-> [(Ref, Ref, (p, o))] -> Forest (Ref, c)
forall a b. (a -> b) -> [a] -> [b]
map (Ref -> Tree (Ref, c)
mkTree (Ref -> Tree (Ref, c))
-> ((Ref, Ref, (p, o)) -> Ref)
-> (Ref, Ref, (p, o))
-> Tree (Ref, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ref, Ref, (p, o)) -> Ref
forall a b c. (a, b, c) -> b
target) (Gr Ref (p, o) -> Ref -> [(Ref, Ref, (p, o))]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Ref -> [LEdge b]
out Gr Ref (p, o)
graph Ref
r))


incomingEdges :: Ref -> Explorer p m c o -> [((Ref, c), (p, o), (Ref, c))]
incomingEdges :: Ref -> Explorer p m c o -> [((Ref, c), (p, o), (Ref, c))]
incomingEdges Ref
ref Explorer p m c o
e = ((Ref, Ref, (p, o))
 -> [((Ref, c), (p, o), (Ref, c))]
 -> [((Ref, c), (p, o), (Ref, c))])
-> [((Ref, c), (p, o), (Ref, c))]
-> [(Ref, Ref, (p, o))]
-> [((Ref, c), (p, o), (Ref, c))]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Ref
s, Ref
t, (p, o)
l) [((Ref, c), (p, o), (Ref, c))]
acc ->  [((Ref
s, Ref -> c
unpack Ref
s), (p, o)
l, (Ref
t, Ref -> c
unpack Ref
t))] [((Ref, c), (p, o), (Ref, c))]
-> [((Ref, c), (p, o), (Ref, c))] -> [((Ref, c), (p, o), (Ref, c))]
forall a. [a] -> [a] -> [a]
++ [((Ref, c), (p, o), (Ref, c))]
acc) [] (((Ref, Ref, (p, o)) -> Bool)
-> [(Ref, Ref, (p, o))] -> [(Ref, Ref, (p, o))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ref
_, Ref
t, (p, o)
_) -> Ref
t Ref -> Ref -> Bool
forall a. Eq a => a -> a -> Bool
== Ref
ref) (Gr Ref (p, o) -> [(Ref, Ref, (p, o))]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
e)))
  where
    unpack :: Ref -> c
unpack Ref
ref = Maybe c -> c
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe c -> c) -> Maybe c -> c
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Ref -> Maybe c
forall p (m :: * -> *) c o. Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
e Ref
ref

getTrace :: Explorer p m c o -> [((Ref, c), (p, o), (Ref, c))]
getTrace :: Explorer p m c o -> [((Ref, c), (p, o), (Ref, c))]
getTrace Explorer p m c o
e = Explorer p m c o -> Ref -> Ref -> [((Ref, c), (p, o), (Ref, c))]
forall p (m :: * -> *) c o.
Explorer p m c o -> Ref -> Ref -> [((Ref, c), (p, o), (Ref, c))]
getPathFromTo Explorer p m c o
e Ref
initialRef (Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e)

getTraces :: Explorer p m c o -> [[((Ref, c), (p, o), (Ref, c))]]
getTraces :: Explorer p m c o -> [[((Ref, c), (p, o), (Ref, c))]]
getTraces Explorer p m c o
e = Explorer p m c o -> Ref -> Ref -> [[((Ref, c), (p, o), (Ref, c))]]
forall p (m :: * -> *) c o.
Explorer p m c o -> Ref -> Ref -> [[((Ref, c), (p, o), (Ref, c))]]
getPathsFromTo Explorer p m c o
e Ref
initialRef (Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e)


mapOut :: Explorer p m c o -> Gr Ref (p, o) -> [Ref] -> Ref -> (Ref, Ref, (p,o)) -> Maybe [[((Ref, c), (p, o), (Ref, c))]]
mapOut :: Explorer p m c o
-> Gr Ref (p, o)
-> [Ref]
-> Ref
-> (Ref, Ref, (p, o))
-> Maybe [[((Ref, c), (p, o), (Ref, c))]]
mapOut Explorer p m c o
exp Gr Ref (p, o)
gr [Ref]
visited Ref
goal (Ref
s, Ref
t, (p
l, o
o))
  | Ref
goal Ref -> Ref -> Bool
forall a. Eq a => a -> a -> Bool
== Ref
t = [[((Ref, c), (p, o), (Ref, c))]]
-> Maybe [[((Ref, c), (p, o), (Ref, c))]]
forall a. a -> Maybe a
Just ([[((Ref, c), (p, o), (Ref, c))]]
 -> Maybe [[((Ref, c), (p, o), (Ref, c))]])
-> [[((Ref, c), (p, o), (Ref, c))]]
-> Maybe [[((Ref, c), (p, o), (Ref, c))]]
forall a b. (a -> b) -> a -> b
$ [[((Ref
s, Ref -> c
unpack Ref
s), (p
l, o
o), (Ref
t, Ref -> c
unpack Ref
t))]] [[((Ref, c), (p, o), (Ref, c))]]
-> [[((Ref, c), (p, o), (Ref, c))]]
-> [[((Ref, c), (p, o), (Ref, c))]]
forall a. [a] -> [a] -> [a]
++ [[((Ref, c), (p, o), (Ref, c))]]
explore
  | Bool
otherwise = case Ref
t Ref -> [Ref] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
visited of
                  Bool
True -> Maybe [[((Ref, c), (p, o), (Ref, c))]]
forall a. Maybe a
Nothing
                  Bool
False -> [[((Ref, c), (p, o), (Ref, c))]]
-> Maybe [[((Ref, c), (p, o), (Ref, c))]]
forall a. a -> Maybe a
Just [[((Ref, c), (p, o), (Ref, c))]]
explore
  where
    explore :: [[((Ref, c), (p, o), (Ref, c))]]
explore = ([((Ref, c), (p, o), (Ref, c))] -> [((Ref, c), (p, o), (Ref, c))])
-> [[((Ref, c), (p, o), (Ref, c))]]
-> [[((Ref, c), (p, o), (Ref, c))]]
forall a b. (a -> b) -> [a] -> [b]
map ((:)((Ref
s, Ref -> c
unpack Ref
s), (p
l, o
o), (Ref
t, Ref -> c
unpack Ref
t))) ([[[((Ref, c), (p, o), (Ref, c))]]]
-> [[((Ref, c), (p, o), (Ref, c))]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[((Ref, c), (p, o), (Ref, c))]]]
 -> [[((Ref, c), (p, o), (Ref, c))]])
-> [[[((Ref, c), (p, o), (Ref, c))]]]
-> [[((Ref, c), (p, o), (Ref, c))]]
forall a b. (a -> b) -> a -> b
$ [Maybe [[((Ref, c), (p, o), (Ref, c))]]]
-> [[[((Ref, c), (p, o), (Ref, c))]]]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe [[((Ref, c), (p, o), (Ref, c))]]]
 -> [[[((Ref, c), (p, o), (Ref, c))]]])
-> [Maybe [[((Ref, c), (p, o), (Ref, c))]]]
-> [[[((Ref, c), (p, o), (Ref, c))]]]
forall a b. (a -> b) -> a -> b
$ ((Ref, Ref, (p, o)) -> Maybe [[((Ref, c), (p, o), (Ref, c))]])
-> [(Ref, Ref, (p, o))] -> [Maybe [[((Ref, c), (p, o), (Ref, c))]]]
forall a b. (a -> b) -> [a] -> [b]
map (Explorer p m c o
-> Gr Ref (p, o)
-> [Ref]
-> Ref
-> (Ref, Ref, (p, o))
-> Maybe [[((Ref, c), (p, o), (Ref, c))]]
forall p (m :: * -> *) c o.
Explorer p m c o
-> Gr Ref (p, o)
-> [Ref]
-> Ref
-> (Ref, Ref, (p, o))
-> Maybe [[((Ref, c), (p, o), (Ref, c))]]
mapOut Explorer p m c o
exp Gr Ref (p, o)
gr (Ref
t Ref -> [Ref] -> [Ref]
forall a. a -> [a] -> [a]
: [Ref]
visited) Ref
goal) (Gr Ref (p, o) -> Ref -> [(Ref, Ref, (p, o))]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Ref -> [LEdge b]
out Gr Ref (p, o)
gr Ref
t))
    unpack :: Ref -> c
unpack Ref
ref = Maybe c -> c
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe c -> c) -> Maybe c -> c
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Ref -> Maybe c
forall p (m :: * -> *) c o. Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
exp Ref
ref


getPathsFromTo :: Explorer p m c o -> Ref -> Ref -> [[((Ref, c), (p, o), (Ref, c))]]
getPathsFromTo :: Explorer p m c o -> Ref -> Ref -> [[((Ref, c), (p, o), (Ref, c))]]
getPathsFromTo Explorer p m c o
exp Ref
from Ref
to = [[[((Ref, c), (p, o), (Ref, c))]]]
-> [[((Ref, c), (p, o), (Ref, c))]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[((Ref, c), (p, o), (Ref, c))]]]
 -> [[((Ref, c), (p, o), (Ref, c))]])
-> [[[((Ref, c), (p, o), (Ref, c))]]]
-> [[((Ref, c), (p, o), (Ref, c))]]
forall a b. (a -> b) -> a -> b
$ [Maybe [[((Ref, c), (p, o), (Ref, c))]]]
-> [[[((Ref, c), (p, o), (Ref, c))]]]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe [[((Ref, c), (p, o), (Ref, c))]]]
 -> [[[((Ref, c), (p, o), (Ref, c))]]])
-> [Maybe [[((Ref, c), (p, o), (Ref, c))]]]
-> [[[((Ref, c), (p, o), (Ref, c))]]]
forall a b. (a -> b) -> a -> b
$ ((Ref, Ref, (p, o)) -> Maybe [[((Ref, c), (p, o), (Ref, c))]])
-> [(Ref, Ref, (p, o))] -> [Maybe [[((Ref, c), (p, o), (Ref, c))]]]
forall a b. (a -> b) -> [a] -> [b]
map (Explorer p m c o
-> Gr Ref (p, o)
-> [Ref]
-> Ref
-> (Ref, Ref, (p, o))
-> Maybe [[((Ref, c), (p, o), (Ref, c))]]
forall p (m :: * -> *) c o.
Explorer p m c o
-> Gr Ref (p, o)
-> [Ref]
-> Ref
-> (Ref, Ref, (p, o))
-> Maybe [[((Ref, c), (p, o), (Ref, c))]]
mapOut Explorer p m c o
exp (Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
exp) [Ref
from] Ref
to) (Gr Ref (p, o) -> Ref -> [(Ref, Ref, (p, o))]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Ref -> [LEdge b]
out (Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
exp) Ref
from)

getPathFromTo :: Explorer p m c o -> Ref -> Ref -> [((Ref, c), (p, o), (Ref, c))]
getPathFromTo :: Explorer p m c o -> Ref -> Ref -> [((Ref, c), (p, o), (Ref, c))]
getPathFromTo Explorer p m c o
exp Ref
from Ref
to =
  case Explorer p m c o -> Ref -> Ref -> [[((Ref, c), (p, o), (Ref, c))]]
forall p (m :: * -> *) c o.
Explorer p m c o -> Ref -> Ref -> [[((Ref, c), (p, o), (Ref, c))]]
getPathsFromTo Explorer p m c o
exp Ref
from Ref
to of
    [] -> []
    ([((Ref, c), (p, o), (Ref, c))]
x:[[((Ref, c), (p, o), (Ref, c))]]
_) -> [((Ref, c), (p, o), (Ref, c))]
x



executionGraph :: Explorer p m c o -> ((Ref, c), [(Ref, c)], [((Ref, c), (p, o), (Ref, c))])
executionGraph :: Explorer p m c o
-> ((Ref, c), [(Ref, c)], [((Ref, c), (p, o), (Ref, c))])
executionGraph Explorer p m c o
exp =
  ((Ref, c)
curr, [(Ref, c)]
nodes, [((Ref, c), (p, o), (Ref, c))]
edges)
  where
    curr :: (Ref, c)
curr = (Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
exp, Explorer p m c o -> c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> configs
config Explorer p m c o
exp)
    nodes :: [(Ref, c)]
nodes = IntMap c -> [(Ref, c)]
forall a. IntMap a -> [(Ref, a)]
IntMap.toList (IntMap c -> [(Ref, c)]) -> IntMap c -> [(Ref, c)]
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> IntMap c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
exp
    edges :: [((Ref, c), (p, o), (Ref, c))]
edges = ((Ref, Ref, (p, o)) -> ((Ref, c), (p, o), (Ref, c)))
-> [(Ref, Ref, (p, o))] -> [((Ref, c), (p, o), (Ref, c))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ref
s, Ref
t, (p, o)
p) -> ((Ref
s, Maybe c -> c
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe c -> c) -> Maybe c -> c
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Ref -> Maybe c
forall p (m :: * -> *) c o. Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
exp Ref
s), (p, o)
p, (Ref
t, Maybe c -> c
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe c -> c) -> Maybe c -> c
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Ref -> Maybe c
forall p (m :: * -> *) c o. Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
exp Ref
t)) ) (Gr Ref (p, o) -> [(Ref, Ref, (p, o))]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
exp))

{-|
  Returns all configurations that have not been the source for an execute action.
  This corresponds to leaves in a tree or nodes without an outbound-edge in a graph.
-}
leaves :: Explorer p m c o -> [(Ref, c)]
leaves :: Explorer p m c o -> [(Ref, c)]
leaves Explorer p m c o
exp = (Ref -> (Ref, c)) -> [Ref] -> [(Ref, c)]
forall a b. (a -> b) -> [a] -> [b]
map Ref -> (Ref, c)
refToPair [Ref]
leaf_nodes
  where
    env :: Gr Ref (p, o)
env = Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
exp
    refToPair :: Ref -> (Ref, c)
refToPair = \Ref
r -> (Ref
r, Maybe c -> c
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe c -> c) -> Maybe c -> c
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Ref -> Maybe c
forall p (m :: * -> *) c o. Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
exp Ref
r)
    leaf_nodes :: [Ref]
leaf_nodes = Gr Ref (p, o) -> [Ref]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Ref]
nodes (Gr Ref (p, o) -> [Ref]) -> Gr Ref (p, o) -> [Ref]
forall a b. (a -> b) -> a -> b
$ (Ref -> Bool) -> Gr Ref (p, o) -> Gr Ref (p, o)
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
(Ref -> Bool) -> gr a b -> gr a b
nfilter (\Ref
n -> (Ref -> Ref -> Bool
forall a. Eq a => a -> a -> Bool
==Ref
0) (Ref -> Bool) -> Ref -> Bool
forall a b. (a -> b) -> a -> b
$ Gr Ref (p, o) -> Ref -> Ref
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Ref -> Ref
outdeg Gr Ref (p, o)
env Ref
n) Gr Ref (p, o)
env


toExport :: Explorer p m c o -> (Ref, [(Ref, c)], [(Ref, Ref, (p, o))])
toExport :: Explorer p m c o -> (Ref, [(Ref, c)], [(Ref, Ref, (p, o))])
toExport Explorer p m c o
exp = (Explorer p m c o -> Ref
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
exp, IntMap c -> [(Ref, c)]
forall a. IntMap a -> [(Ref, a)]
IntMap.toList (IntMap c -> [(Ref, c)]) -> IntMap c -> [(Ref, c)]
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> IntMap c
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
exp, Gr Ref (p, o) -> [(Ref, Ref, (p, o))]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (Gr Ref (p, o) -> [(Ref, Ref, (p, o))])
-> Gr Ref (p, o) -> [(Ref, Ref, (p, o))]
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Gr Ref (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv Explorer p m c o
exp)

fromExport :: Explorer p m c o -> (Ref, [(Ref, c)], [(Ref, Ref, (p, o))]) -> Explorer p m c o
fromExport :: Explorer p m c o
-> (Ref, [(Ref, c)], [(Ref, Ref, (p, o))]) -> Explorer p m c o
fromExport Explorer p m c o
exp (Ref
curr, [(Ref, c)]
nds, [(Ref, Ref, (p, o))]
edgs) = Explorer p m c o
exp { genRef :: Ref
genRef = [(Ref, c)] -> Ref
forall a b. Ord a => [(a, b)] -> a
findMax [(Ref, c)]
nds,
                                         config :: c
config = Ref -> [(Ref, c)] -> c
forall a p. Eq a => a -> [(a, p)] -> p
findCurrentConf Ref
curr [(Ref, c)]
nds,
                                         currRef :: Ref
currRef = Ref
curr,
                                         cmap :: IntMap c
cmap = [(Ref, c)] -> IntMap c
forall a. [(Ref, a)] -> IntMap a
IntMap.fromList [(Ref, c)]
nds,
                                         execEnv :: Gr Ref (p, o)
execEnv = [LNode Ref] -> [(Ref, Ref, (p, o))] -> Gr Ref (p, o)
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph (((Ref, c) -> LNode Ref) -> [(Ref, c)] -> [LNode Ref]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ref
x, c
_) -> (Ref
x, Ref
x)) [(Ref, c)]
nds) [(Ref, Ref, (p, o))]
edgs }
  where findMax :: [(a, b)] -> a
findMax [(a, b)]
l = [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ ((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst [(a, b)]
l
        findCurrentConf :: a -> [(a, p)] -> p
findCurrentConf a
curr [(a, p)]
nds = case a -> [(a, p)] -> Maybe p
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
curr [(a, p)]
nds of
                                     Just p
conf -> p
conf
                                     Maybe p
Nothing   -> [Char] -> p
forall a. HasCallStack => [Char] -> a
error [Char]
"no config found"

eqClasses :: Explorer p m c o -> [[Ref]]
eqClasses :: Explorer p m c o -> [[Ref]]
eqClasses Explorer p m c o
expl = (LNode [Ref] -> [Ref]) -> [LNode [Ref]] -> [[Ref]]
forall a b. (a -> b) -> [a] -> [b]
map LNode [Ref] -> [Ref]
forall a b. (a, b) -> b
snd ([LNode [Ref]] -> [[Ref]]) -> [LNode [Ref]] -> [[Ref]]
forall a b. (a -> b) -> a -> b
$ Gr [Ref] (p, o) -> [LNode [Ref]]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (Gr [Ref] (p, o) -> [LNode [Ref]])
-> Gr [Ref] (p, o) -> [LNode [Ref]]
forall a b. (a -> b) -> a -> b
$ Explorer p m c o -> Gr [Ref] (p, o)
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr [Ref] (programs, output)
shadowExecEnv Explorer p m c o
expl