{-# 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
, 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
, 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))
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