{-# LANGUAGE GADTs #-}

module Language.Explorer.Monadic
    ( Explorer
    , execute
    , executeAll
    , revert
    , dynamicRevert
    , toTree
    , incomingEdges
    , mkExplorerStack
    , mkExplorerTree
    , mkExplorerGraph
    , mkExplorerGSS
    , config
    , execEnv
    , currRef
    , leaves
    , Ref
    , deref
    , getTrace
    , getTraces
    , getPathsFromTo
    , getPathFromTo
    , executionGraph
    ) 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

data Explorer programs m configs output where
    Explorer :: (Show programs, Eq programs, Eq configs, Monad m, Monoid output) =>
        { Explorer programs m configs output -> Bool
sharing :: Bool
        , Explorer programs m configs output -> Bool
backTracking :: Bool
        , 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

mkExplorer :: (Show a, Eq a, Eq b, Monad m, Monoid o) =>
  Bool -> Bool -> (a -> b -> m (Maybe b,o)) -> b -> Explorer a m b o
mkExplorer :: Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorer Bool
share Bool
backtrack a -> b -> m (Maybe b, o)
definterp b
conf = Explorer :: forall programs configs (m :: * -> *) output.
(Show programs, Eq programs, Eq configs, Monad m, Monoid output) =>
Bool
-> Bool
-> (programs -> configs -> m (Maybe configs, output))
-> configs
-> Ref
-> Ref
-> IntMap configs
-> Gr Ref (programs, output)
-> Explorer programs m configs output
Explorer
    { defInterp :: a -> b -> m (Maybe b, o)
defInterp = a -> b -> m (Maybe b, o)
definterp
    , config :: b
config = b
conf
    , genRef :: Ref
genRef = Ref
1 -- Currently generate references by increasing a counter.
    , currRef :: Ref
currRef = Ref
initialRef
    , cmap :: IntMap b
cmap = [(Ref, b)] -> IntMap b
forall a. [(Ref, a)] -> IntMap a
IntMap.fromList [(Ref
initialRef, b
conf)]
    , execEnv :: Gr Ref (a, o)
execEnv = [LNode Ref] -> [LEdge (a, o)] -> Gr Ref (a, o)
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [(Ref
initialRef, Ref
initialRef)] []
    , sharing :: Bool
sharing = Bool
share
    , backTracking :: Bool
backTracking = Bool
backtrack
}

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

mkExplorerStack, mkExplorerTree, mkExplorerGraph, mkExplorerGSS :: (Show a, Eq a, Eq b, Monad m, Monoid o) => (a -> b -> m (Maybe b,o)) -> b -> Explorer a m b o
mkExplorerStack :: (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorerStack = Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
forall a b (m :: * -> *) o.
(Show a, Eq a, Eq b, Monad m, Monoid o) =>
Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorer Bool
False Bool
True
mkExplorerTree :: (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorerTree  = Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
forall a b (m :: * -> *) o.
(Show a, Eq a, Eq b, Monad m, Monoid o) =>
Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorer Bool
False Bool
False
mkExplorerGraph :: (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorerGraph = Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
forall a b (m :: * -> *) o.
(Show a, Eq a, Eq b, Monad m, Monoid o) =>
Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorer Bool
True Bool
False
mkExplorerGSS :: (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorerGSS   = Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
forall a b (m :: * -> *) o.
(Show a, Eq a, Eq b, Monad m, Monoid o) =>
Bool -> Bool -> (a -> b -> m (Maybe b, o)) -> b -> Explorer a m b o
mkExplorer Bool
True Bool
True

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 :: Eq c => Explorer p m c o -> c -> Maybe (Ref, c)
findRef :: Explorer p m c o -> c -> Maybe (Ref, c)
findRef Explorer p m c o
e c
c = ((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
c' c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== 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

updateConf :: (Eq c, Eq p, Eq o) => Explorer p m c o -> (p, c, o) -> Explorer p m c o
updateConf :: Explorer p m c o -> (p, c, o) -> Explorer p m c o
updateConf Explorer p m c o
e (p
p, c
newconf, o
output) =
    if Explorer p m c o -> Bool
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Bool
sharing Explorer p m c o
e
        then case Explorer p m c o -> c -> Maybe (Ref, c)
forall c p (m :: * -> *) o.
Eq c =>
Explorer p m c o -> c -> Maybe (Ref, c)
findRef Explorer p m c o
e c
newconf of
            Just (Ref
r, c
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 (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) (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
r, (p
p,o
output))
                    then Explorer p m c o
e  { config :: c
config = c
newconf, currRef :: Ref
currRef = Ref
r }
                    else Explorer p m c o
e  { config :: c
config = c
newconf, currRef :: Ref
currRef = Ref
r
                            , execEnv :: Gr Ref (p, o)
execEnv = 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
r, (p
p,o
output)) (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) }
            Maybe (Ref, c)
Nothing -> 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
        else 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 :: (Eq c, Eq p, Eq o, Monad m, Monoid 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, o) -> m (Explorer p m c o, o))
-> (Explorer p m c o, o) -> m (Explorer p m c o, o)
forall a b. (a -> b) -> a -> b
$ (Explorer p m c o -> (p, c, o) -> Explorer p m c o
forall c p o (m :: * -> *).
(Eq c, Eq p, Eq o) =>
Explorer p m c o -> (p, c, o) -> Explorer p m c o
updateConf 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 :: (Eq c, Eq p, Eq o, Monad m, Monoid 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 :: * -> *) c p b.
(Monad m, Eq c, 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 c p o (m :: * -> *).
(Eq c, Eq p, Eq o, Monad m, Monoid 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

dynamicRevert :: Bool -> Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
dynamicRevert :: Bool -> Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
dynamicRevert Bool
backtrack Ref
r Explorer p m c o
e =
  case 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) of
    Just c
c | Bool
backtrack -> Explorer p m c o -> Maybe (Explorer p m c o)
forall a. a -> Maybe a
Just Explorer p m c o
e { execEnv :: Gr Ref (p, o)
execEnv = Gr Ref (p, o)
execEnv', currRef :: Ref
currRef = Ref
r, config :: c
config = c
c, cmap :: IntMap c
cmap = IntMap c
cmap'}
           | Bool
otherwise -> Explorer p m c o -> Maybe (Explorer p m c o)
forall a. a -> Maybe a
Just Explorer p m c o
e { currRef :: Ref
currRef = Ref
r, config :: c
config = c
c }
    Maybe c
Nothing            -> Maybe (Explorer p m c o)
forall a. Maybe a
Nothing
    where nodesToDel :: [Ref]
nodesToDel = Ref -> Gr Ref (p, o) -> [Ref]
forall (gr :: * -> * -> *) a b. Graph gr => Ref -> gr a b -> [Ref]
reachable Ref
r (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) [Ref] -> [Ref] -> [Ref]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Ref
r]
          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 (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))
          execEnv' :: Gr Ref (p, o)
execEnv'   = ([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) (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]
nodesToDel (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)


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 = Bool -> Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
forall p (m :: * -> *) c o.
Bool -> Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
dynamicRevert (Explorer p m c o -> Bool
forall programs (m :: * -> *) configs output.
Explorer programs m configs output -> Bool
backTracking Explorer p m c o
e) Ref
r Explorer p m c o
e


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


transformToRealGraph :: Gr Ref p -> Gr Ref Int
transformToRealGraph :: Gr Ref p -> Gr Ref Ref
transformToRealGraph Gr Ref p
g = [LNode Ref] -> [LEdge Ref] -> Gr Ref Ref
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph (Gr Ref p -> [LNode Ref]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr Ref p
g) ((LNode Ref -> LEdge Ref) -> [LNode Ref] -> [LEdge Ref]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ref
s, Ref
t) -> (Ref
s, Ref
t, Ref
1)) (Gr Ref p -> [LNode Ref]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode Ref]
edges Gr Ref p
g))

transformToPairs :: [Ref] -> [(Ref, Ref)]
transformToPairs :: [Ref] -> [LNode Ref]
transformToPairs (Ref
s:Ref
t:[Ref]
xs) = (Ref
s, Ref
t) LNode Ref -> [LNode Ref] -> [LNode Ref]
forall a. a -> [a] -> [a]
: [Ref] -> [LNode Ref]
transformToPairs (Ref
tRef -> [Ref] -> [Ref]
forall a. a -> [a] -> [a]
:[Ref]
xs)
transformToPairs [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, [Ref], [((Ref, c), (p, o), (Ref, c))])
executionGraph :: Explorer p m c o -> (Ref, [Ref], [((Ref, c), (p, o), (Ref, c))])
executionGraph Explorer p m c o
exp =
  (Ref
curr, [Ref]
nodes, [((Ref, c), (p, o), (Ref, c))]
edges)
  where
    curr :: Ref
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
    nodes :: [Ref]
nodes = (LNode Ref -> Ref) -> [LNode Ref] -> [Ref]
forall a b. (a -> b) -> [a] -> [b]
map LNode Ref -> Ref
forall a b. (a, b) -> a
fst (Gr Ref (p, o) -> [LNode Ref]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes (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))
    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]
leave_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)
    leave_nodes :: [Ref]
leave_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