{-# LANGUAGE RecordWildCards, LambdaCase #-}

module Language.EFLINT.Interpreter (Config(..), Program(..), interpreter, initialConfig, rest_disabled, rest_enabled, get_transition, context2config, make_initial_state
                   ,OutputWriter, Output(..), getOutput
                   ,errors, violations, ex_triggers, query_ress, missing_inputs
                   ,convert_programs, collapse_programs) where

import Language.EFLINT.Eval
import Language.EFLINT.Spec
import Language.EFLINT.Saturation
import Language.EFLINT.StaticEval (compile_phrase, runStatic) 
import Language.EFLINT.State

import Control.Monad (forM, forM_, when)
import Control.Monad.Writer (Writer, tell, runWriter)
import Control.Applicative (empty)

import qualified Data.Map as M
import qualified Data.Set as S

data Program = Program Phrase 
             | PSeq Program Program
             | ProgramSkip
             deriving (Program -> Program -> Bool
(Program -> Program -> Bool)
-> (Program -> Program -> Bool) -> Eq Program
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Program -> Program -> Bool
$c/= :: Program -> Program -> Bool
== :: Program -> Program -> Bool
$c== :: Program -> Program -> Bool
Eq, Int -> Program -> ShowS
[Program] -> ShowS
Program -> String
(Int -> Program -> ShowS)
-> (Program -> String) -> ([Program] -> ShowS) -> Show Program
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Program] -> ShowS
$cshowList :: [Program] -> ShowS
show :: Program -> String
$cshow :: Program -> String
showsPrec :: Int -> Program -> ShowS
$cshowsPrec :: Int -> Program -> ShowS
Show)

data Config = Config {
        Config -> Spec
cfg_spec          :: Spec
      , Config -> State
cfg_state         :: State 
      , Config -> [Transition]
rest_transitions  :: [Transition] -- (label * enabled?) -- replaced
      , Config -> [Tagged]
rest_duties       :: [Tagged] -- replaced after ever step
      }
      deriving (Config -> Config -> Bool
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c== :: Config -> Config -> Bool
Eq)

data Output = ErrorVal Error
            | ExecutedTransition TransInfo 
            | Violation Violation
            | QueryRes QueryRes -- whether query succeed or not
            deriving (Output -> Output -> Bool
(Output -> Output -> Bool)
-> (Output -> Output -> Bool) -> Eq Output
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Output -> Output -> Bool
$c/= :: Output -> Output -> Bool
== :: Output -> Output -> Bool
$c== :: Output -> Output -> Bool
Eq, Int -> Output -> ShowS
[Output] -> ShowS
Output -> String
(Int -> Output -> ShowS)
-> (Output -> String) -> ([Output] -> ShowS) -> Show Output
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Output] -> ShowS
$cshowList :: [Output] -> ShowS
show :: Output -> String
$cshow :: Output -> String
showsPrec :: Int -> Output -> ShowS
$cshowsPrec :: Int -> Output -> ShowS
Show, ReadPrec [Output]
ReadPrec Output
Int -> ReadS Output
ReadS [Output]
(Int -> ReadS Output)
-> ReadS [Output]
-> ReadPrec Output
-> ReadPrec [Output]
-> Read Output
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Output]
$creadListPrec :: ReadPrec [Output]
readPrec :: ReadPrec Output
$creadPrec :: ReadPrec Output
readList :: ReadS [Output]
$creadList :: ReadS [Output]
readsPrec :: Int -> ReadS Output
$creadsPrec :: Int -> ReadS Output
Read)

convert_programs :: [Phrase] -> [Program]
convert_programs :: [Phrase] -> [Program]
convert_programs [Phrase]
phrases = (Phrase -> Program) -> [Phrase] -> [Program]
forall a b. (a -> b) -> [a] -> [b]
map Phrase -> Program
Program [Phrase]
phrases

collapse_programs :: [Program] -> Program
collapse_programs :: [Program] -> Program
collapse_programs [] = Program
ProgramSkip
collapse_programs [Program]
programs = ((Program -> Program -> Program) -> [Program] -> Program
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Program -> Program -> Program
PSeq [Program]
programs)

interpreter :: (InputMap, Program) -> Config -> OutputWriter (Maybe Config)
interpreter :: (InputMap, Program) -> Config -> OutputWriter (Maybe Config)
interpreter (InputMap
inpm, Program Phrase
p) Config
cfg = case M_Stc CPhrase -> Spec -> Either [String] (Spec, CPhrase)
forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic (Phrase -> M_Stc CPhrase
compile_phrase Phrase
p) (Context -> Spec
ctx_spec Context
ctx) of
    Left [String]
err  -> [Output] -> WriterT [Output] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Error -> Output
ErrorVal (String -> Error
CompilationError ([String] -> String
unlines [String]
err))] WriterT [Output] Identity ()
-> OutputWriter (Maybe Config) -> OutputWriter (Maybe Config)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Config -> OutputWriter (Maybe Config)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Config
forall a. Maybe a
Nothing 
    Right (Spec
spec', CPhrase
p') -> (Context -> Config) -> Maybe Context -> Maybe Config
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context -> Config
context2config (Maybe Context -> Maybe Config)
-> WriterT [Output] Identity (Maybe Context)
-> OutputWriter (Maybe Config)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CPhrase
-> InputMap -> Context -> WriterT [Output] Identity (Maybe Context)
sem_phrase CPhrase
p' InputMap
inpm 
                          (Context
ctx{ctx_spec :: Spec
ctx_spec = Spec
spec', ctx_state :: State
ctx_state = Spec -> State -> State
rebase_and_sat Spec
spec' (Context -> State
ctx_state Context
ctx)}) 
  where ctx :: Context
ctx = Config -> Context
config2context Config
cfg
interpreter (InputMap
inpm, PSeq Program
p1 Program
p2) Config
cfg = ((InputMap, Program) -> Config -> OutputWriter (Maybe Config)
interpreter (InputMap
inpm,Program
p1) Config
cfg) OutputWriter (Maybe Config)
-> (Maybe Config -> OutputWriter (Maybe Config))
-> OutputWriter (Maybe Config)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (InputMap, Program) -> Config -> OutputWriter (Maybe Config)
interpreter (InputMap
inpm,Program
p2) (Config -> OutputWriter (Maybe Config))
-> (Maybe Config -> Config)
-> Maybe Config
-> OutputWriter (Maybe Config)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> (Config -> Config) -> Maybe Config -> Config
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Config
cfg Config -> Config
forall a. a -> a
id
interpreter (InputMap
inpm, Program
ProgramSkip) Config
cfg = Maybe Config -> OutputWriter (Maybe Config)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Config
forall a. Maybe a
Nothing

initialConfig :: Maybe (Spec, State) -> Config
initialConfig Maybe (Spec, State)
Nothing = Context -> Config
context2config (Spec -> Context
emptyContext Spec
emptySpec)
initialConfig (Just (Spec
spec,State
state)) = Context -> Config
context2config (Context -> Config) -> Context -> Config
forall a b. (a -> b) -> a -> b
$
  (Spec -> Context
emptyContext Spec
spec) { ctx_state :: State
ctx_state = State
state }

context2config :: Context -> Config
context2config :: Context -> Config
context2config Context
ctx = Config :: Spec -> State -> [Transition] -> [Tagged] -> Config
Config {
    cfg_spec :: Spec
cfg_spec    = Context -> Spec
ctx_spec Context
ctx
  , cfg_state :: State
cfg_state   = Context -> State
ctx_state Context
ctx
  , rest_transitions :: [Transition]
rest_transitions = Context -> [Transition]
ctx_transitions Context
ctx
  , rest_duties :: [Tagged]
rest_duties      = Context -> [Tagged]
ctx_duties Context
ctx
  }

config2context :: Config -> Context
config2context :: Config -> Context
config2context Config
cfg = Context :: Spec -> State -> [Transition] -> [Tagged] -> Context
Context {
    ctx_spec :: Spec
ctx_spec = Config -> Spec
cfg_spec Config
cfg
  , ctx_state :: State
ctx_state = Config -> State
cfg_state Config
cfg
  , ctx_transitions :: [Transition]
ctx_transitions = []
  , ctx_duties :: [Tagged]
ctx_duties = []
  }

rest_enabled :: Config -> [Tagged]
rest_enabled = ((Tagged, Bool) -> Tagged) -> [(Tagged, Bool)] -> [Tagged]
forall a b. (a -> b) -> [a] -> [b]
map (Tagged, Bool) -> Tagged
forall a b. (a, b) -> a
fst ([(Tagged, Bool)] -> [Tagged])
-> (Config -> [(Tagged, Bool)]) -> Config -> [Tagged]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Tagged, Bool) -> Bool) -> [(Tagged, Bool)] -> [(Tagged, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Tagged, Bool) -> Bool
forall a b. (a, b) -> b
snd ([(Tagged, Bool)] -> [(Tagged, Bool)])
-> (Config -> [(Tagged, Bool)]) -> Config -> [(Tagged, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Transition -> (Tagged, Bool)) -> [Transition] -> [(Tagged, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map Transition -> (Tagged, Bool)
get_transition ([Transition] -> [(Tagged, Bool)])
-> (Config -> [Transition]) -> Config -> [(Tagged, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> [Transition]
rest_transitions
rest_disabled :: Config -> [Tagged]
rest_disabled = ((Tagged, Bool) -> Tagged) -> [(Tagged, Bool)] -> [Tagged]
forall a b. (a -> b) -> [a] -> [b]
map (Tagged, Bool) -> Tagged
forall a b. (a, b) -> a
fst ([(Tagged, Bool)] -> [Tagged])
-> (Config -> [(Tagged, Bool)]) -> Config -> [Tagged]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Tagged, Bool) -> Bool) -> [(Tagged, Bool)] -> [(Tagged, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Tagged, Bool) -> Bool) -> (Tagged, Bool) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged, Bool) -> Bool
forall a b. (a, b) -> b
snd) ([(Tagged, Bool)] -> [(Tagged, Bool)])
-> (Config -> [(Tagged, Bool)]) -> Config -> [(Tagged, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Transition -> (Tagged, Bool)) -> [Transition] -> [(Tagged, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map Transition -> (Tagged, Bool)
get_transition ([Transition] -> [(Tagged, Bool)])
-> (Config -> [Transition]) -> Config -> [(Tagged, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> [Transition]
rest_transitions

get_transition :: Transition -> (Tagged, Bool)
get_transition :: Transition -> (Tagged, Bool)
get_transition Transition
transition = (Transition -> Tagged
tagged Transition
transition, Transition -> Bool
exist Transition
transition)

ex_triggers :: [Output] -> [TransInfo]
ex_triggers :: [Output] -> [TransInfo]
ex_triggers = (Output -> [TransInfo]) -> [Output] -> [TransInfo]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [TransInfo]
op
 where op :: Output -> [TransInfo]
op (ExecutedTransition TransInfo
out) = [TransInfo
out]
       op Output
_ = []

violations :: [Output] -> [Violation]
violations :: [Output] -> [Violation]
violations = (Output -> [Violation]) -> [Output] -> [Violation]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [Violation]
op
 where op :: Output -> [Violation]
op (Violation Violation
v) = [Violation
v]
       op Output
_ = []

errors :: [Output] -> [Error]
errors :: [Output] -> [Error]
errors = (Output -> [Error]) -> [Output] -> [Error]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [Error]
op
  where op :: Output -> [Error]
op (ErrorVal Error
err) = [Error
err]
        op Output
_ = []

query_ress :: [Output] -> [QueryRes]
query_ress :: [Output] -> [QueryRes]
query_ress = (Output -> [QueryRes]) -> [Output] -> [QueryRes]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [QueryRes]
op
  where op :: Output -> [QueryRes]
op (QueryRes QueryRes
b) = [QueryRes
b]
        op Output
_ = []

missing_inputs :: [Output] -> [Tagged]
missing_inputs :: [Output] -> [Tagged]
missing_inputs = Set Tagged -> [Tagged]
forall a. Set a -> [a]
S.toList (Set Tagged -> [Tagged])
-> ([Output] -> Set Tagged) -> [Output] -> [Tagged]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Tagged] -> Set Tagged
forall a. Ord a => [a] -> Set a
S.fromList ([Tagged] -> Set Tagged)
-> ([Output] -> [Tagged]) -> [Output] -> Set Tagged
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Output -> [Tagged]) -> [Output] -> [Tagged]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Output -> [Tagged]
op
  where op :: Output -> [Tagged]
op (ErrorVal (RuntimeError (MissingInput Tagged
te))) = [Tagged
te]
        op Output
_ = []

type OutputWriter = Writer [Output]

getOutput :: OutputWriter a -> (a,[Output])
getOutput :: OutputWriter a -> (a, [Output])
getOutput = OutputWriter a -> (a, [Output])
forall w a. Writer w a -> (a, w)
runWriter

error_or_process :: M_Subs a -> Spec -> State -> InputMap -> ([a] -> OutputWriter (Maybe Context)) -> OutputWriter (Maybe Context)
error_or_process :: M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
error_or_process M_Subs a
ma Spec
spec State
state InputMap
inpm [a] -> WriterT [Output] Identity (Maybe Context)
fa = case M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
ma Spec
spec State
state InputMap
inpm Subs
emptySubs of
  Left RuntimeError
err  -> [Output] -> WriterT [Output] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Error -> Output
ErrorVal (Error -> Output) -> Error -> Output
forall a b. (a -> b) -> a -> b
$ RuntimeError -> Error
RuntimeError RuntimeError
err] WriterT [Output] Identity ()
-> WriterT [Output] Identity (Maybe Context)
-> WriterT [Output] Identity (Maybe Context)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Context -> WriterT [Output] Identity (Maybe Context)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Context
forall a. Maybe a
Nothing
  Right [a]
as  -> [a] -> WriterT [Output] Identity (Maybe Context)
fa [a]
as

sem_phrase :: CPhrase -> InputMap -> Context -> OutputWriter (Maybe Context)
sem_phrase :: CPhrase
-> InputMap -> Context -> WriterT [Output] Identity (Maybe Context)
sem_phrase CPhrase
p InputMap
inpm Context
c0 = case CPhrase
p of
  CPhrase
CPSkip   -> Maybe Context -> WriterT [Output] Identity (Maybe Context)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Context
forall a. Maybe a
Nothing
  CPhrase
CPOnlyDecls -> WriterT [Output] Identity (Maybe Context)
no_effect 
  CQuery Term
t -> M_Subs Value
-> Spec
-> State
-> InputMap
-> ([Value] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
error_or_process (Term -> M_Subs Value
eval Term
t) Spec
spec State
state InputMap
inpm (([Value] -> WriterT [Output] Identity (Maybe Context))
 -> WriterT [Output] Identity (Maybe Context))
-> ([Value] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a b. (a -> b) -> a -> b
$ \[Value]
vs -> do  
                 let queryRes :: QueryRes
queryRes | (Value -> Bool) -> [Value] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool -> Value
ResBool Bool
True)) [Value]
vs = QueryRes
QuerySuccess
                              | Bool
otherwise                  = QueryRes
QueryFailure
                 [Output] -> WriterT [Output] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QueryRes -> Output
QueryRes QueryRes
queryRes] WriterT [Output] Identity ()
-> WriterT [Output] Identity (Maybe Context)
-> WriterT [Output] Identity (Maybe Context)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriterT [Output] Identity (Maybe Context)
no_effect
  CCreate [Var]
vs Term
t    -> Effect -> WriterT [Output] Identity (Maybe Context)
single_effect ([Var] -> Term -> Effect
CAll [Var]
vs Term
t)
  CTerminate [Var]
vs Term
t -> Effect -> WriterT [Output] Identity (Maybe Context)
single_effect ([Var] -> Term -> Effect
TAll [Var]
vs Term
t)
  CObfuscate [Var]
vs Term
t -> Effect -> WriterT [Output] Identity (Maybe Context)
single_effect ([Var] -> Term -> Effect
OAll [Var]
vs Term
t)
  CDo Tagged
te          -> M_Subs (Either String [TransInfo])
-> Spec
-> State
-> InputMap
-> ([Either String [TransInfo]]
    -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
error_or_process (Tagged -> M_Subs (Either String [TransInfo])
trigger_or_fail Tagged
te) Spec
spec State
state InputMap
inpm [Either String [TransInfo]]
-> WriterT [Output] Identity (Maybe Context)
consider_transinfos
  CTrigger [Var]
vs Term
t -> let m_subs :: M_Subs (Either String [TransInfo])
m_subs = do  
                        [Tagged]
tes <- [Var] -> M_Subs Tagged -> M_Subs [Tagged]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
vs (M_Subs Value -> (Tagged -> M_Subs Tagged) -> M_Subs Tagged
forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return)
                        case [Tagged]
tes of 
                         (te :: Tagged
te@(Elem
_,String
d):[Tagged]
_) | Spec -> String -> Bool
triggerable Spec
spec String
d -> [TransInfo] -> Either String [TransInfo]
forall a b. b -> Either a b
Right ([TransInfo] -> Either String [TransInfo])
-> M_Subs [TransInfo] -> M_Subs (Either String [TransInfo])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Tagged] -> (Tagged -> M_Subs TransInfo) -> M_Subs [TransInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Tagged]
tes Tagged -> M_Subs TransInfo
instantiate_trans 
                                      | Bool
otherwise -> Either String [TransInfo] -> M_Subs (Either String [TransInfo])
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String [TransInfo]
forall a b. a -> Either a b
Left String
d)
                         [Tagged]
_ -> Either String [TransInfo] -> M_Subs (Either String [TransInfo])
forall (m :: * -> *) a. Monad m => a -> m a
return ([TransInfo] -> Either String [TransInfo]
forall a b. b -> Either a b
Right [])
                     in M_Subs (Either String [TransInfo])
-> Spec
-> State
-> InputMap
-> ([Either String [TransInfo]]
    -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
error_or_process M_Subs (Either String [TransInfo])
m_subs Spec
spec State
state InputMap
inpm [Either String [TransInfo]]
-> WriterT [Output] Identity (Maybe Context)
consider_transinfos
  CPDir CDirective
dir -> Store -> [CDirective] -> WriterT [Output] Identity (Maybe Context)
return_context Store
forall k a. Map k a
emptyStore [CDirective
dir] 
  CSeq CPhrase
p CPhrase
q -> CPhrase
-> InputMap -> Context -> WriterT [Output] Identity (Maybe Context)
sem_phrase CPhrase
p InputMap
inpm Context
c0 WriterT [Output] Identity (Maybe Context)
-> (Maybe Context -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (CPhrase
-> InputMap -> Context -> WriterT [Output] Identity (Maybe Context)
sem_phrase CPhrase
q InputMap
inpm (Context -> WriterT [Output] Identity (Maybe Context))
-> (Maybe Context -> Context)
-> Maybe Context
-> WriterT [Output] Identity (Maybe Context)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> (Context -> Context) -> Maybe Context -> Context
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Context
c0 Context -> Context
forall a. a -> a
id)
  where spec :: Spec
spec = Context -> Spec
ctx_spec Context
c0
        state :: State
state = Context -> State
ctx_state Context
c0

        return_context :: Store -> [CDirective] -> OutputWriter (Maybe Context)
        return_context :: Store -> [CDirective] -> WriterT [Output] Identity (Maybe Context)
return_context Store
ass [CDirective]
dirs = do  
          let duties :: [Tagged]
duties = [ Tagged
te | te :: Tagged
te@(Elem
v,String
d) <- (State -> InputMap -> [Tagged]
state_input_holds State
state' InputMap
inpm)
                            , Duty DutySpec
_ <- [Kind] -> (Kind -> [Kind]) -> Maybe Kind -> [Kind]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
:[]) ((TypeSpec -> Kind) -> Maybe TypeSpec -> Maybe Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Kind
kind (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec' String
d)) ]
          M_Subs [Violation]
-> Spec
-> State
-> InputMap
-> ([[Violation]] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
error_or_process ([Tagged] -> M_Subs [Violation]
find_duty_violations [Tagged]
duties) Spec
spec' State
state' InputMap
inpm (([[Violation]] -> WriterT [Output] Identity (Maybe Context))
 -> WriterT [Output] Identity (Maybe Context))
-> ([[Violation]] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a b. (a -> b) -> a -> b
$ \[[Violation]]
d_viols -> 
            M_Subs [Violation]
-> Spec
-> State
-> InputMap
-> ([[Violation]] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
error_or_process ([String] -> M_Subs [Violation]
find_inv_violations (Set String -> [String]
forall a. Set a -> [a]
S.toList (Set String -> [String]) -> Set String -> [String]
forall a b. (a -> b) -> a -> b
$ Spec -> Set String
invariants Spec
spec')) Spec
spec' State
state' InputMap
inpm (([[Violation]] -> WriterT [Output] Identity (Maybe Context))
 -> WriterT [Output] Identity (Maybe Context))
-> ([[Violation]] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a b. (a -> b) -> a -> b
$ \[[Violation]]
i_viols -> do
              [Output] -> WriterT [Output] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ((Violation -> Output) -> [Violation] -> [Output]
forall a b. (a -> b) -> [a] -> [b]
map Violation -> Output
Violation ([[Violation]] -> [Violation]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Violation]]
d_viols [Violation] -> [Violation] -> [Violation]
forall a. [a] -> [a] -> [a]
++ [[Violation]] -> [Violation]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Violation]]
i_viols)) 
              M_Subs [Transition]
-> Spec
-> State
-> InputMap
-> ([[Transition]] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
error_or_process M_Subs [Transition]
find_transitions Spec
spec' State
state' InputMap
inpm (([[Transition]] -> WriterT [Output] Identity (Maybe Context))
 -> WriterT [Output] Identity (Maybe Context))
-> ([[Transition]] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a b. (a -> b) -> a -> b
$ \[[Transition]]
tss ->  
                Maybe Context -> WriterT [Output] Identity (Maybe Context)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Context -> WriterT [Output] Identity (Maybe Context))
-> Maybe Context -> WriterT [Output] Identity (Maybe Context)
forall a b. (a -> b) -> a -> b
$ Context -> Maybe Context
forall a. a -> Maybe a
Just (Context -> Maybe Context) -> Context -> Maybe Context
forall a b. (a -> b) -> a -> b
$ Context
c0
                  { ctx_state :: State
ctx_state = State
state'
                  , ctx_spec :: Spec
ctx_spec = Spec
spec'
                  , ctx_transitions :: [Transition]
ctx_transitions = [[Transition]] -> [Transition]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Transition]]
tss
                  , ctx_duties :: [Tagged]
ctx_duties = [Tagged]
duties 
                  }
          where state' :: State
state' = Spec -> State -> State
rebase_and_sat Spec
spec (Store -> State -> State
make_assignments Store
ass State
state)
                spec' :: Spec
spec'  = [CDirective] -> Spec -> Spec
process_directives [CDirective]
dirs Spec
spec

        no_effect :: OutputWriter (Maybe Context)
        no_effect :: WriterT [Output] Identity (Maybe Context)
no_effect = Store -> [CDirective] -> WriterT [Output] Identity (Maybe Context)
return_context Store
forall k a. Map k a
emptyStore []

        single_effect :: Effect -> OutputWriter (Maybe Context)
        single_effect :: Effect -> WriterT [Output] Identity (Maybe Context)
single_effect Effect
eff =
          M_Subs Store
-> Spec
-> State
-> InputMap
-> ([Store] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a.
M_Subs a
-> Spec
-> State
-> InputMap
-> ([a] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
error_or_process (Effect -> M_Subs Store
eval_effect Effect
eff) Spec
spec State
state InputMap
inpm (([Store] -> WriterT [Output] Identity (Maybe Context))
 -> WriterT [Output] Identity (Maybe Context))
-> ([Store] -> WriterT [Output] Identity (Maybe Context))
-> WriterT [Output] Identity (Maybe Context)
forall a b. (a -> b) -> a -> b
$ \[Store]
stores ->
            Store -> [CDirective] -> WriterT [Output] Identity (Maybe Context)
return_context ([Store] -> Store
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions [Store]
stores) {- always just one store-} []

        trigger_or_fail :: Tagged -> M_Subs (Either DomId [TransInfo])
        trigger_or_fail :: Tagged -> M_Subs (Either String [TransInfo])
trigger_or_fail te :: Tagged
te@(Elem
_,String
d) | Spec -> String -> Bool
triggerable Spec
spec String
d = [TransInfo] -> Either String [TransInfo]
forall a b. b -> Either a b
Right ([TransInfo] -> Either String [TransInfo])
-> (TransInfo -> [TransInfo])
-> TransInfo
-> Either String [TransInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TransInfo -> [TransInfo] -> [TransInfo]
forall a. a -> [a] -> [a]
:[]) (TransInfo -> Either String [TransInfo])
-> M_Subs TransInfo -> M_Subs (Either String [TransInfo])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged -> M_Subs TransInfo
instantiate_trans Tagged
te
                                 | Bool
otherwise          = Either String [TransInfo] -> M_Subs (Either String [TransInfo])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String [TransInfo] -> M_Subs (Either String [TransInfo]))
-> Either String [TransInfo] -> M_Subs (Either String [TransInfo])
forall a b. (a -> b) -> a -> b
$ String -> Either String [TransInfo]
forall a b. a -> Either a b
Left String
d 

        consider_transinfos :: [Either String [TransInfo]]
-> WriterT [Output] Identity (Maybe Context)
consider_transinfos [Left String
d] = [Output] -> WriterT [Output] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Error -> Output
ErrorVal (String -> Error
NotTriggerable String
d)] WriterT [Output] Identity ()
-> WriterT [Output] Identity (Maybe Context)
-> WriterT [Output] Identity (Maybe Context)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriterT [Output] Identity (Maybe Context)
no_effect
        consider_transinfos [Right [TransInfo]
infos] = do
          [TransInfo]
-> (TransInfo -> WriterT [Output] Identity ())
-> WriterT [Output] Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [TransInfo]
infos ((TransInfo -> WriterT [Output] Identity ())
 -> WriterT [Output] Identity ())
-> (TransInfo -> WriterT [Output] Identity ())
-> WriterT [Output] Identity ()
forall a b. (a -> b) -> a -> b
$ \TransInfo
info -> do  [Output] -> WriterT [Output] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [TransInfo -> Output
ExecutedTransition TransInfo
info]
                                     Bool
-> WriterT [Output] Identity () -> WriterT [Output] Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TransInfo -> Bool
trans_is_action TransInfo
info Bool -> Bool -> Bool
&& TransInfo -> Bool
trans_forced TransInfo
info) 
                                       ([Output] -> WriterT [Output] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Violation -> Output
Violation (TransInfo -> Violation
TriggerViolation TransInfo
info)])
          Store -> [CDirective] -> WriterT [Output] Identity (Maybe Context)
return_context ([Store] -> Store
store_unions ((TransInfo -> Store) -> [TransInfo] -> [Store]
forall a b. (a -> b) -> [a] -> [b]
map TransInfo -> Store
trans_assignments [TransInfo]
infos)) [] 
        consider_transinfos [Either String [TransInfo]]
_ = String -> WriterT [Output] Identity (Maybe Context)
forall a. HasCallStack => String -> a
error String
"ASSERT: consider_transinfos"

find_inv_violations :: [DomId] -> M_Subs [Violation]
find_inv_violations :: [String] -> M_Subs [Violation]
find_inv_violations [String]
ds = do 
  Spec
spec <- M_Subs Spec
get_spec 
  [String] -> (String -> M_Subs Violation) -> M_Subs [Violation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [String]
ds ((String -> M_Subs Violation) -> M_Subs [Violation])
-> (String -> M_Subs Violation) -> M_Subs [Violation]
forall a b. (a -> b) -> a -> b
$ \String
d -> do
    let term :: Term
term = [Var] -> Term -> Term
Exists [String -> String -> Var
Var String
d String
""] (Term -> Term
Present (Var -> Term
Ref (String -> String -> Var
Var String
d String
"")))
    M_Subs () -> M_Subs ()
forall a. M_Subs a -> M_Subs a
ignoreMissingInput (M_Subs Value -> M_Subs ()
checkFalse (Term -> M_Subs Value
eval Term
term))
    Violation -> M_Subs Violation
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Violation
InvariantViolation String
d)

find_duty_violations :: [Tagged] -> M_Subs [Violation]
find_duty_violations :: [Tagged] -> M_Subs [Violation]
find_duty_violations [Tagged]
tes = do 
  Spec
spec <- M_Subs Spec
get_spec 
  [Tagged] -> (Tagged -> M_Subs Violation) -> M_Subs [Violation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Tagged]
tes ((Tagged -> M_Subs Violation) -> M_Subs [Violation])
-> (Tagged -> M_Subs Violation) -> M_Subs [Violation]
forall a b. (a -> b) -> a -> b
$ \te :: Tagged
te@(Elem
_,String
d) -> do
    M_Subs Bool -> M_Subs Bool
forall a. M_Subs a -> M_Subs a
ignoreMissingInput (Tagged -> Maybe [Term] -> M_Subs Bool
eval_violation_condition Tagged
te (Spec -> String -> Maybe [Term]
find_violation_cond Spec
spec String
d)) M_Subs Bool -> (Bool -> M_Subs Violation) -> M_Subs Violation
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
      Bool
True  -> Violation -> M_Subs Violation
forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> Violation
DutyViolation Tagged
te)
      Bool
False -> M_Subs Violation
forall (f :: * -> *) a. Alternative f => f a
empty 
 
find_transitions :: M_Subs [Transition]
find_transitions :: M_Subs [Transition]
find_transitions = do
  Spec
spec <- M_Subs Spec
get_spec 
  [[Transition]] -> [Transition]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Transition]] -> [Transition])
-> M_Subs [[Transition]] -> M_Subs [Transition]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((String, Either EventSpec ActSpec) -> M_Subs [Transition])
-> [(String, Either EventSpec ActSpec)] -> M_Subs [[Transition]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String, Either EventSpec ActSpec) -> M_Subs [Transition]
forall b. (String, b) -> M_Subs [Transition]
gen_trans (Spec -> [(String, Either EventSpec ActSpec)]
trigger_decls Spec
spec)
  where gen_trans :: (String, b) -> M_Subs [Transition]
gen_trans (String
d,b
_) = M_Subs Transition -> M_Subs [Transition]
forall a. M_Subs a -> M_Subs [a]
results (M_Subs Transition -> M_Subs [Transition])
-> M_Subs Transition -> M_Subs [Transition]
forall a b. (a -> b) -> a -> b
$ M_Subs Transition -> M_Subs Transition
forall a. M_Subs a -> M_Subs a
ignoreMissingInput (M_Subs Transition -> M_Subs Transition)
-> M_Subs Transition -> M_Subs Transition
forall a b. (a -> b) -> a -> b
$ do
          Tagged
tagged <- Var -> M_Subs Tagged
every_possible_subs (String -> Var
no_decoration String
d)
          Bool
exist  <- Tagged -> M_Subs Bool
is_in_virtual_state Tagged
tagged
          Transition -> M_Subs Transition
forall (m :: * -> *) a. Monad m => a -> m a
return Transition :: Tagged -> Bool -> Transition
Transition{Bool
Tagged
exist :: Bool
tagged :: Tagged
exist :: Bool
tagged :: Tagged
..}

every_possible_subs :: Var -> M_Subs Tagged
every_possible_subs :: Var -> M_Subs Tagged
every_possible_subs Var
x = do
    Spec
spec <- M_Subs Spec
get_spec
    let d :: String
d = Spec -> Var -> String
remove_decoration Spec
spec Var
x
    (Domain
dom, Term
_) <- String -> M_Subs (Domain, Term)
get_dom String
d
    if Spec -> Domain -> Bool
enumerable Spec
spec Domain
dom then String -> M_Subs Tagged
generate_instances String
d
                           else String -> M_Subs Tagged
every_available_subs String
d
 where generate_instances :: String -> M_Subs Tagged
generate_instances String
d = do
          (Domain
dom, Term
dom_filter) <- String -> M_Subs (Domain, Term)
get_dom String
d
          Elem
e <- String -> Domain -> M_Subs Elem
instantiate_domain String
d Domain
dom
          let bindings :: Subs
bindings = case (Domain
dom,Elem
e) of (Products [Var]
xs, Product [Tagged]
args) -> [(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
                                         (Domain, Elem)
_ -> Var -> Tagged -> Subs
forall k a. k -> a -> Map k a
M.singleton (String -> Var
no_decoration String
d) (Elem
e,String
d) 
          (Subs -> Subs) -> M_Subs () -> M_Subs ()
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) (M_Subs Value -> M_Subs ()
checkTrue (Term -> M_Subs Value
eval Term
dom_filter))
          Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return (Elem
e,String
d)
       every_available_subs :: String -> M_Subs Tagged
every_available_subs String
d = do
          (Domain
dom, Term
dom_filter) <- String -> M_Subs (Domain, Term)
get_dom String
d
          case Domain
dom of
            Products [Var]
xs -> do
              [Tagged]
args <- [M_Subs Tagged] -> M_Subs [Tagged]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Var -> M_Subs Tagged) -> [Var] -> [M_Subs Tagged]
forall a b. (a -> b) -> [a] -> [b]
map Var -> M_Subs Tagged
every_possible_subs [Var]
xs)
              (Subs -> Subs) -> M_Subs () -> M_Subs ()
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` ([(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) (M_Subs Value -> M_Subs ()
checkTrue (Term -> M_Subs Value
eval Term
dom_filter))
              Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return ([Tagged] -> Elem
Product [Tagged]
args, String
d)
            Domain
_ -> do
              State
state <- M_Subs State
get_state
              InputMap
input <- M_Subs InputMap
get_input
              [Tagged] -> M_Subs Tagged
forall a. [a] -> M_Subs a
nd ([Tagged] -> M_Subs Tagged) -> [Tagged] -> M_Subs Tagged
forall a b. (a -> b) -> a -> b
$  [ Tagged
te | te :: Tagged
te@(Elem
v,String
d') <- State -> InputMap -> [Tagged]
state_input_holds State
state InputMap
input, String
d' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
d ]

make_initial_state :: Spec -> Initialiser -> State
make_initial_state :: Spec -> Initialiser -> State
make_initial_state Spec
spec Initialiser
inits = do
  case M_Subs Store
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [Store]
forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs ([Store] -> Store
store_unions ([Store] -> Store) -> M_Subs [Store] -> M_Subs Store
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Effect -> M_Subs Store) -> Initialiser -> M_Subs [Store]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Effect -> M_Subs Store
eval_effect Initialiser
inits) Spec
spec State
emptyState InputMap
emptyInput Subs
emptySubs of
    Left RuntimeError
err -> String -> State
forall a. HasCallStack => String -> a
error (RuntimeError -> String
print_runtime_error RuntimeError
err)
    Right [Store]
res -> case [Store]
res of 
      []    -> String -> State
forall a. HasCallStack => String -> a
error String
"failed to initialise state"
      [Store
sto] -> Spec -> State -> State
rebase_and_sat Spec
spec (Store -> State -> State
make_assignments Store
sto State
emptyState)
      [Store]
_     -> String -> State
forall a. HasCallStack => String -> a
error String
"non-deterministic state initialisation"