{-# LANGUAGE TupleSections #-}

module Language.EFLINT.Explorer where

import Language.EFLINT.Spec (Spec, Phrase(PSkip), ppTagged)
import Language.EFLINT.State (State, emptyInput, InputMap, TransInfo(..), Assignment(..), trans_is_action)
import Language.EFLINT.Interpreter (Program(..), Config(..), interpreter, initialConfig, Output, getOutput)
import Language.EFLINT.Print()

import qualified Language.Explorer.Pure as EI
import Language.Explorer.Monadic (revert, jump)

import Data.Tree (drawTree, Tree(..))

type Explorer = EI.Explorer Label Config [Output]

type Label = (InputMap, Program)

data Instruction = Execute [Program] InputMap
                 | ExecuteOnce Program InputMap
                 | Revert Ref Bool {- whether the revert is destructive or not -} 
                 | Display Ref  -- `last' edge leading to given ref
                 | DisplayFull Ref -- full `history', see `Path' below, for given ref
                 | ExplorationHeads -- nodes in the execution graph without outgoing edges
                 | CreateExportExploration -- create export data to recreate execution graph
                 | LoadExportExploration ExecutionGraph -- load execution graph
data Response    = ResultTrans Explorer [Output] (Config, Ref) (Config, Ref)
                 | Path Path
                 | Nodes [Node]
                 | InvalidRevert
                 | ExportExploration ExecutionGraph
                 | LoadExploration Explorer

type Ref = Int -- state identifier
type Path = [(Node, (Label, [Output]), Node)] 
type Node = (Ref, Config)

data N = N {
           N -> Ref
ref :: Ref
         , N -> Config
config :: Config
         }  
         deriving (N -> N -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: N -> N -> Bool
$c/= :: N -> N -> Bool
== :: N -> N -> Bool
$c== :: N -> N -> Bool
Eq)

data Edge = Edge {
            Edge -> Ref
source :: Ref
          , Edge -> Ref
target :: Ref
          , Edge -> PO
po     :: PO
          }  
          deriving (Edge -> Edge -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Edge -> Edge -> Bool
$c/= :: Edge -> Edge -> Bool
== :: Edge -> Edge -> Bool
$c== :: Edge -> Edge -> Bool
Eq)

data PO = PO {
          PO -> Label
label  :: Label 
        , PO -> [Output]
output :: [Output]
        }  
        deriving (PO -> PO -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PO -> PO -> Bool
$c/= :: PO -> PO -> Bool
== :: PO -> PO -> Bool
$c== :: PO -> PO -> Bool
Eq)

data ExecutionGraph = ExecutionGraph {
                      ExecutionGraph -> Ref
current :: Ref
                    , ExecutionGraph -> [N]
nodes   :: [N]
                    , ExecutionGraph -> [Edge]
edges   :: [Edge]
                    }

showTree :: Explorer -> String
showTree :: Explorer -> [Char]
showTree = Tree [Char] -> [Char]
drawTree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Char]
"#"forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p (m :: * -> *) c o. Explorer p m c o -> Tree (Ref, c)
EI.toTree

showTriggerTree :: TransInfo -> String
showTriggerTree :: TransInfo -> [Char]
showTriggerTree = Tree [Char] -> [Char]
drawTree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TransInfo -> [Char]
report forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransInfo -> Tree TransInfo
triggerTree
  where report :: TransInfo -> [Char]
report TransInfo
info = Tagged -> [Char]
ppTagged (TransInfo -> Tagged
trans_tagged TransInfo
info) forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ [Char]
whether_enabled 
--                      ++ "\n" ++ unlines (map (uncurry mod) (M.assocs (trans_assignments info)))
         where mod :: Tagged -> Assignment -> [Char]
mod Tagged
te Assignment
ass = case Assignment
ass of  Assignment
HoldsTrue -> [Char]
"+" forall a. [a] -> [a] -> [a]
++ Tagged -> [Char]
ppTagged Tagged
te
                                         Assignment
HoldsFalse -> [Char]
"-" forall a. [a] -> [a] -> [a]
++ Tagged -> [Char]
ppTagged Tagged
te
                                         Assignment
Unknown -> [Char]
"~" forall a. [a] -> [a] -> [a]
++ Tagged -> [Char]
ppTagged Tagged
te
               whether_enabled :: [Char]
whether_enabled | Bool -> Bool
not (TransInfo -> Bool
trans_is_action TransInfo
info) = [Char]
""
                               | TransInfo -> Bool
trans_forced TransInfo
info          = [Char]
"(DISABLED)"
                               | Bool
otherwise                  = [Char]
"(ENABLED)"

triggerTree :: TransInfo -> Tree TransInfo 
triggerTree :: TransInfo -> Tree TransInfo
triggerTree TransInfo
t = forall a. a -> [Tree a] -> Tree a
Node TransInfo
t (forall a b. (a -> b) -> [a] -> [b]
map TransInfo -> Tree TransInfo
triggerTree (TransInfo -> [TransInfo]
trans_syncs TransInfo
t))

get_last_edge :: Explorer -> Ref -> ((Ref, Config), (Label, [Output]), (Ref, Config))
get_last_edge :: Explorer
-> Ref -> ((Ref, Config), (Label, [Output]), (Ref, Config))
get_last_edge Explorer
exp Ref
cr = case forall a. [a] -> [a]
reverse (forall p c o.
Explorer p c o -> Ref -> Ref -> [((Ref, c), (p, o), (Ref, c))]
EI.getPathFromTo Explorer
exp Ref
1 Ref
cr) of
  (((Ref, Config), (Label, [Output]), (Ref, Config))
edge:[((Ref, Config), (Label, [Output]), (Ref, Config))]
_) -> ((Ref, Config), (Label, [Output]), (Ref, Config))
edge 
  [((Ref, Config), (Label, [Output]), (Ref, Config))]
_ -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. HasCallStack => [Char] -> a
error ([Char]
"ASSERT: get_last_edge1")) (\Config
cfg -> ((Ref
cr,Config
cfg), ((Map Tagged Bool
emptyInput, Phrase -> Program
Program Phrase
PSkip),[]), (Ref
cr,Config
cfg))) (forall p c o. Explorer p c o -> Ref -> Maybe c
EI.deref Explorer
exp Ref
cr) 
        
init_tree_explorer, init_graph_explorer :: Maybe (Spec,State) -> Explorer
init_tree_explorer :: Maybe (Spec, State) -> Explorer
init_tree_explorer = forall p c o.
PureLanguage p c o =>
Bool
-> (c -> c -> Bool)
-> (p -> c -> (Maybe c, o))
-> c
-> Explorer p c o
EI.mkExplorer Bool
False (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Bool
False) Label -> Config -> (Maybe Config, [Output])
defInterpreter forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Spec, State) -> Config
initialConfig
init_graph_explorer :: Maybe (Spec, State) -> Explorer
init_graph_explorer = forall p c o.
PureLanguage p c o =>
Bool
-> (c -> c -> Bool)
-> (p -> c -> (Maybe c, o))
-> c
-> Explorer p c o
EI.mkExplorer Bool
True forall a. Eq a => a -> a -> Bool
(==) Label -> Config -> (Maybe Config, [Output])
defInterpreter forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Spec, State) -> Config
initialConfig

defInterpreter :: Label -> Config -> (Maybe Config, [Output])
defInterpreter Label
p Config
c = forall a. OutputWriter a -> (a, [Output])
getOutput forall a b. (a -> b) -> a -> b
$ Label -> Config -> OutputWriter (Maybe Config)
interpreter Label
p Config
c

run_ :: Explorer -> Instruction -> Response
run_ :: Explorer -> Instruction -> Response
run_ Explorer
exp Instruction
instr = case Instruction
instr of 
  Execute [Program]
ps Map Tagged Bool
inpm -> 
    let (Explorer
exp',[Output]
outs) = forall p c o.
PureLanguage p c o =>
[p] -> Explorer p c o -> (Explorer p c o, o)
EI.executeAll (forall a b. (a -> b) -> [a] -> [b]
map (Map Tagged Bool
inpm,) [Program]
ps) Explorer
exp
        cfg' :: Config
cfg'        = forall a b o. Explorer a b o -> b
EI.config Explorer
exp'
        ref' :: Ref
ref'        = forall a b o. Explorer a b o -> Ref
EI.currRef Explorer
exp'
    in Explorer -> [Output] -> (Config, Ref) -> (Config, Ref) -> Response
ResultTrans Explorer
exp' [Output]
outs (forall a b o. Explorer a b o -> b
EI.config Explorer
exp, forall a b o. Explorer a b o -> Ref
EI.currRef Explorer
exp) (Config
cfg', Ref
ref')
  ExecuteOnce Program
ps Map Tagged Bool
inpm -> 
    let (Explorer
exp',[Output]
outs) = forall p c o.
PureLanguage p c o =>
p -> Explorer p c o -> (Explorer p c o, o)
EI.execute (Map Tagged Bool
inpm,Program
ps) Explorer
exp
        cfg' :: Config
cfg'        = forall a b o. Explorer a b o -> b
EI.config Explorer
exp'
        ref' :: Ref
ref'        = forall a b o. Explorer a b o -> Ref
EI.currRef Explorer
exp'
    in Explorer -> [Output] -> (Config, Ref) -> (Config, Ref) -> Response
ResultTrans Explorer
exp' [Output]
outs (forall a b o. Explorer a b o -> b
EI.config Explorer
exp, forall a b o. Explorer a b o -> Ref
EI.currRef Explorer
exp) (Config
cfg', Ref
ref')
  Revert Ref
r Bool
d -> case (if Bool
d then forall p (m :: * -> *) c o.
Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
revert else forall p (m :: * -> *) c o.
Ref -> Explorer p m c o -> Maybe (Explorer p m c o)
jump) Ref
r Explorer
exp of 
    Maybe Explorer
Nothing   -> Response
InvalidRevert
    Just Explorer
exp'  -> Explorer -> [Output] -> (Config, Ref) -> (Config, Ref) -> Response
ResultTrans Explorer
exp' [] (forall a b o. Explorer a b o -> b
EI.config Explorer
exp, forall a b o. Explorer a b o -> Ref
EI.currRef Explorer
exp) (forall a b o. Explorer a b o -> b
EI.config Explorer
exp', forall a b o. Explorer a b o -> Ref
EI.currRef Explorer
exp')
  Display Ref
id -> Explorer -> [Output] -> (Config, Ref) -> (Config, Ref) -> Response
ResultTrans Explorer
exp [Output]
out (Config
from, Ref
pr) (Config
to, Ref
cr)
    where ((Ref
pr,Config
from), (Label
_,[Output]
out), (Ref
cr, Config
to)) = Explorer
-> Ref -> ((Ref, Config), (Label, [Output]), (Ref, Config))
get_last_edge Explorer
exp Ref
id
  DisplayFull Ref
id -> [((Ref, Config), (Label, [Output]), (Ref, Config))] -> Response
Path forall a b. (a -> b) -> a -> b
$ forall p c o.
Explorer p c o -> Ref -> Ref -> [((Ref, c), (p, o), (Ref, c))]
EI.getPathFromTo Explorer
exp Ref
1 Ref
id
  Instruction
ExplorationHeads -> [(Ref, Config)] -> Response
Nodes forall a b. (a -> b) -> a -> b
$ forall p c o. Explorer p c o -> [(Ref, c)]
EI.leaves Explorer
exp
  Instruction
CreateExportExploration -> ExecutionGraph -> Response
ExportExploration forall a b. (a -> b) -> a -> b
$ (Ref, [(Ref, Config)], [(Ref, Ref, (Label, [Output]))])
-> ExecutionGraph
convertToGraph (forall p c o.
Explorer p c o -> (Ref, [(Ref, c)], [(Ref, Ref, (p, o))])
EI.toExport Explorer
exp)
  LoadExportExploration ExecutionGraph
graph -> Explorer -> Response
LoadExploration forall a b. (a -> b) -> a -> b
$ forall p c o.
Explorer p c o
-> (Ref, [(Ref, c)], [(Ref, Ref, (p, o))]) -> Explorer p c o
EI.fromExport Explorer
exp (ExecutionGraph
-> (Ref, [(Ref, Config)], [(Ref, Ref, (Label, [Output]))])
convertFromGraph ExecutionGraph
graph)

convertToGraph :: (Ref, [(Ref, Config)], [(Ref, Ref, (Label, [Output]))]) -> ExecutionGraph
convertToGraph :: (Ref, [(Ref, Config)], [(Ref, Ref, (Label, [Output]))])
-> ExecutionGraph
convertToGraph (Ref
cid, [(Ref, Config)]
nodes, [(Ref, Ref, (Label, [Output]))]
edges) = ExecutionGraph{current :: Ref
current=Ref
cid, nodes :: [N]
nodes=(forall a b. (a -> b) -> [a] -> [b]
map (Ref, Config) -> N
convertToN [(Ref, Config)]
nodes), edges :: [Edge]
edges=(forall a b. (a -> b) -> [a] -> [b]
map (Ref, Ref, (Label, [Output])) -> Edge
convertToEdges [(Ref, Ref, (Label, [Output]))]
edges)}

convertFromGraph :: ExecutionGraph -> (Ref, [(Ref, Config)], [(Ref, Ref, (Label, [Output]))])
convertFromGraph :: ExecutionGraph
-> (Ref, [(Ref, Config)], [(Ref, Ref, (Label, [Output]))])
convertFromGraph ExecutionGraph
graph = (ExecutionGraph -> Ref
current ExecutionGraph
graph, forall a b. (a -> b) -> [a] -> [b]
map N -> (Ref, Config)
convertFromN (ExecutionGraph -> [N]
nodes ExecutionGraph
graph), forall a b. (a -> b) -> [a] -> [b]
map Edge -> (Ref, Ref, (Label, [Output]))
convertFromEdges (ExecutionGraph -> [Edge]
edges ExecutionGraph
graph))

convertToN :: (Ref, Config) -> N
convertToN :: (Ref, Config) -> N
convertToN (Ref
r, Config
c) = N{ref :: Ref
ref=Ref
r, config :: Config
config=Config
c}

convertFromN :: N -> (Ref, Config) 
convertFromN :: N -> (Ref, Config)
convertFromN N
n = (N -> Ref
ref N
n, N -> Config
config N
n)

convertToEdges :: (Ref, Ref, (Label, [Output])) -> Edge
convertToEdges :: (Ref, Ref, (Label, [Output])) -> Edge
convertToEdges (Ref
sid, Ref
tid, (Label
p, [Output]
o)) = Edge{source :: Ref
source=Ref
sid, target :: Ref
target=Ref
tid, po :: PO
po=PO{label :: Label
label=Label
p, output :: [Output]
output=[Output]
o}}

convertFromEdges :: Edge -> (Ref, Ref, (Label, [Output]))
convertFromEdges :: Edge -> (Ref, Ref, (Label, [Output]))
convertFromEdges Edge
edge = (Edge -> Ref
source Edge
edge, Edge -> Ref
target Edge
edge, PO -> (Label, [Output])
convertFromPO (Edge -> PO
po Edge
edge))

convertFromPO :: PO -> (Label, [Output])
convertFromPO :: PO -> (Label, [Output])
convertFromPO PO
po = (PO -> Label
label PO
po, PO -> [Output]
output PO
po)