{-# 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 =>
        { forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Bool
shadowing :: Bool -- Shadow the exploration tree in a shadow graph.
        , forall programs (m :: * -> *) configs output.
Explorer programs m configs output
-> programs -> configs -> m (Maybe configs, output)
defInterp :: programs -> configs -> m (Maybe configs, output)
        , forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> configs
config :: configs -- Cache the config
        , forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef :: Ref
        , forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
genRef :: Ref
        , forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap :: IntMap.IntMap configs
        , forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr Ref (programs, output)
execEnv :: Gr Ref (programs, output)
        , forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr [Ref] (programs, output)
shadowExecEnv :: Gr [Ref] (programs, output)
        , forall programs (m :: * -> *) configs 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 :: 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
shadow c -> c -> Bool
shadowEq p -> c -> m (Maybe c, o)
definterp c
conf = 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 = forall a. [(Ref, a)] -> IntMap a
IntMap.fromList [(Ref
initialRef, c
conf)]
    , execEnv :: Gr Ref (p, o)
execEnv = forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [(Ref
initialRef, Ref
initialRef)] []
    , shadowExecEnv :: Gr [Ref] (p, o)
shadowExecEnv = 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 :: forall p (m :: * -> *) c o.
Language p m c o =>
(p -> c -> m (Maybe c, o)) -> c -> Explorer p m c o
mkExplorerNoSharing = 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 :: forall p (m :: * -> *) c o. Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
e Ref
r = forall a. Ref -> IntMap a -> Maybe a
IntMap.lookup Ref
r (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 :: forall p (m :: * -> *) c o.
Explorer p m c o -> c -> (c -> Bool) -> Maybe (Ref, c)
findRef Explorer p m c o
e c
c c -> Bool
eq = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(Ref
r, c
c') -> c -> Bool
eq c
c') (forall a. IntMap a -> [(Ref, a)]
IntMap.toList (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 :: 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
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 = forall a. Ref -> a -> IntMap a -> IntMap a
IntMap.insert Ref
newref c
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 = forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Ref
newref, Ref
newref) forall a b. (a -> b) -> a -> b
$ forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e, Ref
newref, (p
p,o
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 = forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
genRef Explorer p m c o
e forall a. Num a => a -> a -> a
+ Ref
1


findNodeRef :: Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef :: forall p o. Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef Gr [Ref] (p, o)
g Ref
r = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(Ref
_, [Ref]
rs) -> Ref
r forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
rs) forall a b. (a -> b) -> a -> b
$ 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 :: 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, Ref
newref, Ref
oldref) =
  case 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 (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 forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge Gr [Ref] (p, o)
shadowEnv (Ref
nref, 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 = forall {gr :: * -> * -> *} {a} {c} {d} {b}.
DynGraph gr =>
(Ref, a, c, d) -> gr [a] b -> gr [a] b
updateLabel (forall p o. Gr [Ref] (p, o) -> Ref -> Ref
findNodeRef Gr [Ref] (p, o)
shadowEnv Ref
r', Ref
newref, p
p, o
output) forall a b. (a -> b) -> a -> b
$ forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Ref
nref, 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 = forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Ref
newref, [Ref
newref]) forall a b. (a -> b) -> a -> b
$ forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Ref
nref, Ref
newref, (p
p, o
output)) forall a b. (a -> b) -> a -> b
$ 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 = forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr [Ref] (programs, output)
shadowExecEnv Explorer p m c o
e
      nref :: Ref
nref = 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 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 forall a. a -> [a] -> [a]
: [a]
label, Adj b
fromadj) forall (gr :: * -> * -> *) a b.
DynGraph gr =>
Context a b -> gr a b -> gr a b
& gr [a] b
decomgr
          (MContext [a] b, 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 :: 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
newconf, o
output)
  | forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Bool
shadowing Explorer p m c o
e = forall p (m :: * -> *) c o.
Explorer p m c o -> p -> o -> c -> Explorer p m c o
addNewPath (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, (forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
newexplorer), (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 = 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 :: 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 o
e =
  do (Maybe c
mcfg, o
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 (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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (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  -> 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 :: forall p (m :: * -> *) c o.
Language p m c o =>
[p] -> Explorer p m c o -> m (Explorer p m c o, o)
executeAll [p]
ps Explorer p m c o
exp = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM 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, 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') <- 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
                                         forall (m :: * -> *) a. Monad m => a -> m a
return (Explorer p m c b
res, b
out forall a. Monoid a => a -> a -> a
`mappend` b
out')

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


deleteFromShadowEnv :: [(Ref, Ref)] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv :: forall po. [LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv [(Ref
l, Ref
r)] Gr [Ref] po
gr = case 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 forall a. Eq a => [a] -> [a] -> [a]
\\ [Ref
l], Adj po
fromadj) forall (gr :: * -> * -> *) a b.
DynGraph gr =>
Context a b -> gr a b -> gr a b
& Gr [Ref] po
decomgr
  (MContext [Ref] po, Gr [Ref] po)
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Inconsistent shadow env."
deleteFromShadowEnv (LNode Ref
x:[LNode Ref]
xs) Gr [Ref] po
gr = forall po. [LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv [LNode Ref]
xs (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 :: forall p o. [Ref] -> [(Ref, Ref, (p, o))] -> [(Ref, Ref, (p, o))]
cleanEdges [Ref]
ref [(Ref, Ref, (p, o))]
edg = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ref
s, Ref
t, (p, o)
l) -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Ref
t 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 :: forall p o. 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' = forall po. [LNode Ref] -> Gr [Ref] po -> Gr [Ref] po
deleteFromShadowEnv (forall a b. (a -> b) -> [a] -> [b]
map (\Ref
r -> (Ref
r, 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' = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ref
r, [Ref]
labels) -> [Ref]
labels forall a. Eq a => a -> a -> Bool
== []) forall a b. (a -> b) -> a -> b
$ forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (Gr [Ref] (p, o)
shadowEnv'))
    edgesToDel' :: [LNode Ref]
edgesToDel' = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ref
s, Ref
t) -> Ref
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
nodesToDel' Bool -> Bool -> Bool
|| Ref
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
nodesToDel') (forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode Ref]
edges Gr [Ref] (p, o)
shadowEnv')
    shadowEnv'' :: Gr [Ref] (p, o)
shadowEnv'' = (forall (gr :: * -> * -> *) a b.
DynGraph gr =>
[LNode Ref] -> gr a b -> gr a b
delEdges [LNode Ref]
edgesToDel' forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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]
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 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) -> forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\Ref
n -> Ref
target forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (forall (gr :: * -> * -> *) a b. Graph gr => Ref -> gr a b -> [Ref]
reachable Ref
n gr a b
gr)) (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 forall a. Eq a => a -> a -> Bool
== Ref
target = if forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Ref -> Ref
outdeg gr a b
gr Ref
source forall a. Ord a => a -> a -> Bool
> Ref
1 then ([], RevertableStatus
StopRevert) else ([Ref
source], RevertableStatus
ContinueRevert)
      | Bool
otherwise = case 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 forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> Ref -> Ref
outdeg gr a b
gr Ref
source forall a. Ord a => a -> a -> Bool
> Ref
1 then ([Ref]
res, RevertableStatus
StopRevert) else (Ref
source 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 :: forall p (m :: * -> *) c o.
Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
revert Ref
r Explorer p m c o
e
  | forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
reachNodes =
      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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Explorer p m c o
e' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Explorer p m c o
e' { execEnv :: Gr Ref (p, o)
execEnv = forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph (forall a b. [a] -> [b] -> [(a, b)]
zip [Ref]
remainNodes [Ref]
remainNodes) forall a b. (a -> b) -> a -> b
$ forall p o. [Ref] -> [(Ref, Ref, (p, o))] -> [(Ref, Ref, (p, o))]
cleanEdges [Ref]
reachNodes (forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges forall a b. (a -> b) -> a -> b
$ 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 = forall a. [Ref] -> IntMap a -> IntMap a
deleteMap [Ref]
reachNodes (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 = forall p o. Bool -> [Ref] -> Gr [Ref] (p, o) -> Gr [Ref] (p, o)
cleanShadowEnv (forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Bool
shadowing Explorer p m c o
e') [Ref]
reachNodes (forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Gr [Ref] (programs, output)
shadowExecEnv Explorer p m c o
e')}
  | Bool
otherwise = forall a. Maybe a
Nothing
  where
    reachNodes :: [Ref]
reachNodes = forall {gr :: * -> * -> *} {a} {b}.
Graph gr =>
gr a b -> Ref -> Ref -> [Ref]
findRevertableNodes Gr Ref (p, o)
gr Ref
r (forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
e)
    remainNodes :: [Ref]
remainNodes = forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Ref]
nodes Gr Ref (p, o)
gr forall a. Eq a => [a] -> [a] -> [a]
\\ [Ref]
reachNodes
    gr :: Gr Ref (p, o)
gr = 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 :: 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 = case 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) -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> forall a. Maybe a
Nothing

toTree :: Explorer p m c o -> Tree (Ref, c)
toTree :: forall p (m :: * -> *) c o. 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 = 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 = forall a. a -> [Tree a] -> Tree a
Node (Ref
r, forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
exp forall a. IntMap a -> Ref -> a
IntMap.! Ref
r) (forall a b. (a -> b) -> [a] -> [b]
map (Ref -> Tree (Ref, c)
mkTree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {b} {c}. (a, b, c) -> b
target) (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 :: forall p (m :: * -> *) c o.
Ref -> Explorer p m c o -> [((Ref, c), (p, o), (Ref, c))]
incomingEdges Ref
ref Explorer p m c o
e = 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))] forall a. [a] -> [a] -> [a]
++ [((Ref, c), (p, o), (Ref, c))]
acc) [] (forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ref
_, Ref
t, (p, o)
_) -> Ref
t forall a. Eq a => a -> a -> Bool
== Ref
ref) (forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (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 = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ 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 :: forall p (m :: * -> *) c o.
Explorer p m c o -> [((Ref, c), (p, o), (Ref, c))]
getTrace Explorer p m c o
e = 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 (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 :: forall p (m :: * -> *) c o.
Explorer p m c o -> [[((Ref, c), (p, o), (Ref, c))]]
getTraces Explorer p m c o
e = 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 (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 :: 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]
visited Ref
goal (Ref
s, Ref
t, (p
l, o
o))
  | Ref
goal forall a. Eq a => a -> a -> Bool
== Ref
t = forall a. a -> Maybe a
Just 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))]] forall a. [a] -> [a] -> [a]
++ [[((Ref, c), (p, o), (Ref, c))]]
explore
  | Bool
otherwise = case Ref
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ref]
visited of
                  Bool
True -> forall a. Maybe a
Nothing
                  Bool
False -> forall a. a -> Maybe a
Just [[((Ref, c), (p, o), (Ref, c))]]
explore
  where
    explore :: [[((Ref, c), (p, o), (Ref, c))]]
explore = 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))) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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 forall a. a -> [a] -> [a]
: [Ref]
visited) Ref
goal) (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 = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ 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 :: 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 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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 (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) (forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Ref -> [LEdge b]
out (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 :: forall p (m :: * -> *) c o.
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 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 :: forall p (m :: * -> *) c o.
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 = (forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
exp, forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> configs
config Explorer p m c o
exp)
    nodes :: [(Ref, c)]
nodes = forall a. IntMap a -> [(Ref, a)]
IntMap.toList forall a b. (a -> b) -> a -> b
$ 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 = forall a b. (a -> b) -> [a] -> [b]
map (\(Ref
s, Ref
t, (p, o)
p) -> ((Ref
s, forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ 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, forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall p (m :: * -> *) c o. Explorer p m c o -> Ref -> Maybe c
deref Explorer p m c o
exp Ref
t)) ) (forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges (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 :: forall p (m :: * -> *) c o. Explorer p m c o -> [(Ref, c)]
leaves Explorer p m c o
exp = forall a b. (a -> b) -> [a] -> [b]
map Ref -> (Ref, c)
refToPair [Ref]
leaf_nodes
  where
    env :: Gr Ref (p, o)
env = 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, forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ 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 = forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Ref]
nodes forall a b. (a -> b) -> a -> b
$ forall (gr :: * -> * -> *) a b.
DynGraph gr =>
(Ref -> Bool) -> gr a b -> gr a b
nfilter (\Ref
n -> (forall a. Eq a => a -> a -> Bool
==Ref
0) forall a b. (a -> b) -> a -> b
$ 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 :: forall p (m :: * -> *) c o.
Explorer p m c o -> (Ref, [(Ref, c)], [(Ref, Ref, (p, o))])
toExport Explorer p m c o
exp = (forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Ref
currRef Explorer p m c o
exp, forall a. IntMap a -> [(Ref, a)]
IntMap.toList forall a b. (a -> b) -> a -> b
$ forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> IntMap configs
cmap Explorer p m c o
exp, forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges forall a b. (a -> b) -> a -> b
$ 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 :: forall p (m :: * -> *) c o.
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 = forall {a} {b}. Ord a => [(a, b)] -> a
findMax [(Ref, c)]
nds,
                                         config :: c
config = forall {a} {b}. Eq a => a -> [(a, b)] -> b
findCurrentConf Ref
curr [(Ref, c)]
nds,
                                         currRef :: Ref
currRef = Ref
curr,
                                         cmap :: IntMap c
cmap = forall a. [(Ref, a)] -> IntMap a
IntMap.fromList [(Ref, c)]
nds,
                                         execEnv :: Gr Ref (p, o)
execEnv = forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph (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 = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(a, b)]
l
        findCurrentConf :: a -> [(a, b)] -> b
findCurrentConf a
curr [(a, b)]
nds = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
curr [(a, b)]
nds of
                                     Just b
conf -> b
conf
                                     Maybe b
Nothing   -> forall a. HasCallStack => [Char] -> a
error [Char]
"no config found"

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