module Language.EFLINT.State where

import Language.EFLINT.Spec

import Data.Maybe (isJust)
import qualified Data.Map as M

import Control.Applicative (empty)

data Info   = Info {
                Info -> Bool
value :: Bool
              , Info -> Bool
from_sat :: Bool -- whether assignment came from saturation process
              }
              deriving (Info -> Info -> Bool
(Info -> Info -> Bool) -> (Info -> Info -> Bool) -> Eq Info
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Info -> Info -> Bool
$c/= :: Info -> Info -> Bool
== :: Info -> Info -> Bool
$c== :: Info -> Info -> Bool
Eq, ReadPrec [Info]
ReadPrec Info
Int -> ReadS Info
ReadS [Info]
(Int -> ReadS Info)
-> ReadS [Info] -> ReadPrec Info -> ReadPrec [Info] -> Read Info
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Info]
$creadListPrec :: ReadPrec [Info]
readPrec :: ReadPrec Info
$creadPrec :: ReadPrec Info
readList :: ReadS [Info]
$creadList :: ReadS [Info]
readsPrec :: Int -> ReadS Info
$creadsPrec :: Int -> ReadS Info
Read, Int -> Info -> ShowS
[Info] -> ShowS
Info -> String
(Int -> Info -> ShowS)
-> (Info -> String) -> ([Info] -> ShowS) -> Show Info
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Info] -> ShowS
$cshowList :: [Info] -> ShowS
show :: Info -> String
$cshow :: Info -> String
showsPrec :: Int -> Info -> ShowS
$cshowsPrec :: Int -> Info -> ShowS
Show)

data State =  State {
                  State -> Map Tagged Info
contents :: M.Map Tagged Info  -- meta-info about components
              ,   State -> Int
time :: Int
              }
              deriving State -> State -> Bool
(State -> State -> Bool) -> (State -> State -> Bool) -> Eq State
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: State -> State -> Bool
$c/= :: State -> State -> Bool
== :: State -> State -> Bool
$c== :: State -> State -> Bool
Eq

data Transition = Transition {
                    Transition -> Tagged
tagged :: Tagged
                  , Transition -> Bool
exist :: Bool
                  }  
                  deriving (Eq Transition
Eq Transition
-> (Transition -> Transition -> Ordering)
-> (Transition -> Transition -> Bool)
-> (Transition -> Transition -> Bool)
-> (Transition -> Transition -> Bool)
-> (Transition -> Transition -> Bool)
-> (Transition -> Transition -> Transition)
-> (Transition -> Transition -> Transition)
-> Ord Transition
Transition -> Transition -> Bool
Transition -> Transition -> Ordering
Transition -> Transition -> Transition
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Transition -> Transition -> Transition
$cmin :: Transition -> Transition -> Transition
max :: Transition -> Transition -> Transition
$cmax :: Transition -> Transition -> Transition
>= :: Transition -> Transition -> Bool
$c>= :: Transition -> Transition -> Bool
> :: Transition -> Transition -> Bool
$c> :: Transition -> Transition -> Bool
<= :: Transition -> Transition -> Bool
$c<= :: Transition -> Transition -> Bool
< :: Transition -> Transition -> Bool
$c< :: Transition -> Transition -> Bool
compare :: Transition -> Transition -> Ordering
$ccompare :: Transition -> Transition -> Ordering
$cp1Ord :: Eq Transition
Ord, Transition -> Transition -> Bool
(Transition -> Transition -> Bool)
-> (Transition -> Transition -> Bool) -> Eq Transition
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Transition -> Transition -> Bool
$c/= :: Transition -> Transition -> Bool
== :: Transition -> Transition -> Bool
$c== :: Transition -> Transition -> Bool
Eq, Int -> Transition -> ShowS
[Transition] -> ShowS
Transition -> String
(Int -> Transition -> ShowS)
-> (Transition -> String)
-> ([Transition] -> ShowS)
-> Show Transition
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Transition] -> ShowS
$cshowList :: [Transition] -> ShowS
show :: Transition -> String
$cshow :: Transition -> String
showsPrec :: Int -> Transition -> ShowS
$cshowsPrec :: Int -> Transition -> ShowS
Show, ReadPrec [Transition]
ReadPrec Transition
Int -> ReadS Transition
ReadS [Transition]
(Int -> ReadS Transition)
-> ReadS [Transition]
-> ReadPrec Transition
-> ReadPrec [Transition]
-> Read Transition
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Transition]
$creadListPrec :: ReadPrec [Transition]
readPrec :: ReadPrec Transition
$creadPrec :: ReadPrec Transition
readList :: ReadS [Transition]
$creadList :: ReadS [Transition]
readsPrec :: Int -> ReadS Transition
$creadsPrec :: Int -> ReadS Transition
Read)

type InputMap = M.Map Tagged Bool

type Store = M.Map Tagged Assignment 

data Assignment = HoldsTrue
                | HoldsFalse
                | Unknown
                deriving (Assignment -> Assignment -> Bool
(Assignment -> Assignment -> Bool)
-> (Assignment -> Assignment -> Bool) -> Eq Assignment
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Assignment -> Assignment -> Bool
$c/= :: Assignment -> Assignment -> Bool
== :: Assignment -> Assignment -> Bool
$c== :: Assignment -> Assignment -> Bool
Eq, Eq Assignment
Eq Assignment
-> (Assignment -> Assignment -> Ordering)
-> (Assignment -> Assignment -> Bool)
-> (Assignment -> Assignment -> Bool)
-> (Assignment -> Assignment -> Bool)
-> (Assignment -> Assignment -> Bool)
-> (Assignment -> Assignment -> Assignment)
-> (Assignment -> Assignment -> Assignment)
-> Ord Assignment
Assignment -> Assignment -> Bool
Assignment -> Assignment -> Ordering
Assignment -> Assignment -> Assignment
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Assignment -> Assignment -> Assignment
$cmin :: Assignment -> Assignment -> Assignment
max :: Assignment -> Assignment -> Assignment
$cmax :: Assignment -> Assignment -> Assignment
>= :: Assignment -> Assignment -> Bool
$c>= :: Assignment -> Assignment -> Bool
> :: Assignment -> Assignment -> Bool
$c> :: Assignment -> Assignment -> Bool
<= :: Assignment -> Assignment -> Bool
$c<= :: Assignment -> Assignment -> Bool
< :: Assignment -> Assignment -> Bool
$c< :: Assignment -> Assignment -> Bool
compare :: Assignment -> Assignment -> Ordering
$ccompare :: Assignment -> Assignment -> Ordering
$cp1Ord :: Eq Assignment
Ord, Int -> Assignment -> ShowS
[Assignment] -> ShowS
Assignment -> String
(Int -> Assignment -> ShowS)
-> (Assignment -> String)
-> ([Assignment] -> ShowS)
-> Show Assignment
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Assignment] -> ShowS
$cshowList :: [Assignment] -> ShowS
show :: Assignment -> String
$cshow :: Assignment -> String
showsPrec :: Int -> Assignment -> ShowS
$cshowsPrec :: Int -> Assignment -> ShowS
Show, ReadPrec [Assignment]
ReadPrec Assignment
Int -> ReadS Assignment
ReadS [Assignment]
(Int -> ReadS Assignment)
-> ReadS [Assignment]
-> ReadPrec Assignment
-> ReadPrec [Assignment]
-> Read Assignment
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Assignment]
$creadListPrec :: ReadPrec [Assignment]
readPrec :: ReadPrec Assignment
$creadPrec :: ReadPrec Assignment
readList :: ReadS [Assignment]
$creadList :: ReadS [Assignment]
readsPrec :: Int -> ReadS Assignment
$creadsPrec :: Int -> ReadS Assignment
Read)

emptyInput :: InputMap
emptyInput :: InputMap
emptyInput = InputMap
forall k a. Map k a
M.empty

emptyStore :: Map k a
emptyStore = Map k a
forall k a. Map k a
M.empty

-- | based union over stores, precedence HoldsTrue > HoldsFalse > Unknown
store_union :: Store -> Store -> Store
store_union :: Store -> Store -> Store
store_union = (Assignment -> Assignment -> Assignment) -> Store -> Store -> Store
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Assignment -> Assignment -> Assignment
op
  where op :: Assignment -> Assignment -> Assignment
op Assignment
HoldsTrue Assignment
_      = Assignment
HoldsTrue
        op Assignment
_ Assignment
HoldsTrue      = Assignment
HoldsTrue
        op Assignment
HoldsFalse Assignment
_     = Assignment
HoldsFalse
        op Assignment
_ Assignment
HoldsFalse     = Assignment
HoldsFalse
        op Assignment
Unknown Assignment
Unknown  = Assignment
Unknown
store_unions :: [Store] -> Store
store_unions :: [Store] -> Store
store_unions = (Store -> Store -> Store) -> Store -> [Store] -> Store
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Store -> Store -> Store
store_union Store
forall k a. Map k a
emptyStore

make_assignments :: Store -> State -> State
make_assignments :: Store -> State -> State
make_assignments = (State -> Store -> State) -> Store -> State -> State
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Tagged -> Assignment -> State -> State) -> State -> Store -> State
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey Tagged -> Assignment -> State -> State
op)
  where op :: Tagged -> Assignment -> State -> State
op Tagged
te Assignment
HoldsTrue   = Tagged -> State -> State
create Tagged
te
        op Tagged
te Assignment
HoldsFalse  = Tagged -> State -> State
terminate Tagged
te
        op Tagged
te Assignment
Unknown     = Tagged -> State -> State
obfuscate Tagged
te

derive :: Tagged -> State -> State
derive :: Tagged -> State -> State
derive Tagged
te State
s = State
s { contents :: Map Tagged Info
contents = (Maybe Info -> Maybe Info)
-> Tagged -> Map Tagged Info -> Map Tagged Info
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter Maybe Info -> Maybe Info
adj Tagged
te (State -> Map Tagged Info
contents State
s) }
  where adj :: Maybe Info -> Maybe Info
adj Maybe Info
Nothing     = Info -> Maybe Info
forall a. a -> Maybe a
Just (Info -> Maybe Info) -> Info -> Maybe Info
forall a b. (a -> b) -> a -> b
$ Info :: Bool -> Bool -> Info
Info{ value :: Bool
value = Bool
True, from_sat :: Bool
from_sat = Bool
True }
        adj (Just Info
info) = Info -> Maybe Info
forall a. a -> Maybe a
Just Info
info

derive_all :: [Tagged] -> State -> State
derive_all :: [Tagged] -> State -> State
derive_all = (State -> [Tagged] -> State) -> [Tagged] -> State -> State
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Tagged -> State -> State) -> State -> [Tagged] -> State
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Tagged -> State -> State
derive)

create :: Tagged -> State -> State
create :: Tagged -> State -> State
create Tagged
te State
s = State
s { contents :: Map Tagged Info
contents = Tagged -> Info -> Map Tagged Info -> Map Tagged Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Tagged
te Info :: Bool -> Bool -> Info
Info{ value :: Bool
value = Bool
True, from_sat :: Bool
from_sat = Bool
False } (State -> Map Tagged Info
contents State
s) }

create_all :: [Tagged] -> State -> State
create_all :: [Tagged] -> State -> State
create_all = (State -> [Tagged] -> State) -> [Tagged] -> State -> State
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Tagged -> State -> State) -> State -> [Tagged] -> State
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Tagged -> State -> State
create)

terminate :: Tagged -> State -> State
terminate :: Tagged -> State -> State
terminate Tagged
te State
s = State
s { contents :: Map Tagged Info
contents = Tagged -> Info -> Map Tagged Info -> Map Tagged Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Tagged
te Info :: Bool -> Bool -> Info
Info{ value :: Bool
value = Bool
False, from_sat :: Bool
from_sat = Bool
False } (State -> Map Tagged Info
contents State
s) }

terminate_all :: [Tagged] -> State -> State
terminate_all :: [Tagged] -> State -> State
terminate_all = (State -> [Tagged] -> State) -> [Tagged] -> State -> State
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Tagged -> State -> State) -> State -> [Tagged] -> State
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Tagged -> State -> State
terminate)

obfuscate :: Tagged -> State -> State
obfuscate :: Tagged -> State -> State
obfuscate Tagged
te State
s = State
s { contents :: Map Tagged Info
contents = Tagged -> Map Tagged Info -> Map Tagged Info
forall k a. Ord k => k -> Map k a -> Map k a
M.delete Tagged
te (State -> Map Tagged Info
contents State
s) }

obfuscate_all :: [Tagged] -> State -> State
obfuscate_all :: [Tagged] -> State -> State
obfuscate_all = (State -> [Tagged] -> State) -> [Tagged] -> State -> State
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Tagged -> State -> State) -> State -> [Tagged] -> State
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Tagged -> State -> State
obfuscate)

-- | assumes the instance of a closed type
holds :: Tagged -> State -> Bool
holds :: Tagged -> State -> Bool
holds Tagged
te State
s = Bool -> (Info -> Bool) -> Maybe Info -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
==Bool
True) (Bool -> Bool) -> (Info -> Bool) -> Info -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Info -> Bool
value) (Tagged -> Map Tagged Info -> Maybe Info
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Tagged
te (State -> Map Tagged Info
contents State
s))

emptyState :: State
emptyState = State :: Map Tagged Info -> Int -> State
State { contents :: Map Tagged Info
contents = Map Tagged Info
forall k a. Map k a
M.empty, time :: Int
time = Int
0 }

increment_time :: State -> State
increment_time State
state = State
state { time :: Int
time = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (State -> Int
time State
state) }

instance Show State where
  show :: State -> String
show State
state = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ 
      [ Tagged -> String
show_component Tagged
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show (Info -> Bool
value Info
m)
      | (Tagged
c,Info
m) <- Map Tagged Info -> [(Tagged, Info)]
forall k a. Map k a -> [(k, a)]
M.assocs (State -> Map Tagged Info
contents State
state)
      ]

-- instance ToJSON State where
-- toJSON state = toJSON (map TaggedJSON (state_holds state)) 

state_holds :: State -> [Tagged]
state_holds :: State -> [Tagged]
state_holds State
state = [ Tagged
te | (Tagged
te, Info
m) <- Map Tagged Info -> [(Tagged, Info)]
forall k a. Map k a -> [(k, a)]
M.assocs (State -> Map Tagged Info
contents State
state), Bool
True Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Info -> Bool
value Info
m ]

state_input_holds :: State -> InputMap -> [Tagged]
state_input_holds :: State -> InputMap -> [Tagged]
state_input_holds State
state InputMap
inpm = State -> [Tagged]
state_holds State
state [Tagged] -> [Tagged] -> [Tagged]
forall a. [a] -> [a] -> [a]
++ InputMap -> [Tagged]
input_holds InputMap
inpm

state_not_holds :: State -> [Tagged]
state_not_holds :: State -> [Tagged]
state_not_holds State
state = [ Tagged
te | (Tagged
te, Info
m) <- Map Tagged Info -> [(Tagged, Info)]
forall k a. Map k a -> [(k, a)]
M.assocs (State -> Map Tagged Info
contents State
state), Bool
False Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Info -> Bool
value Info
m ]

input_holds :: InputMap -> [Tagged]
input_holds :: InputMap -> [Tagged]
input_holds InputMap
inpm = [ Tagged
te |  (Tagged
te, Bool
True) <- InputMap -> [(Tagged, Bool)]
forall k a. Map k a -> [(k, a)]
M.assocs InputMap
inpm ]

data Context = Context {
                  Context -> Spec
ctx_spec        :: Spec --mutable 
                , Context -> State
ctx_state       :: State --mutable 
                , Context -> [Transition]
ctx_transitions :: [Transition] -- (label * enabled?) -- replaceable
                , Context -> [Tagged]
ctx_duties      :: [Tagged] -- replaceable
                }

-- mutable means c0 ; c1 results in c1 adding to c0 with possible override
-- appendable means c0 ; c1 results in effects of c0 and c1 being concatenated
-- replaceable means c0 ; c1 results in effect of c1

emptyContext :: Spec -> Context
emptyContext Spec
spec = 
               Context :: Spec -> State -> [Transition] -> [Tagged] -> Context
Context { 
                  ctx_spec :: Spec
ctx_spec = Spec
spec
                , ctx_state :: State
ctx_state = State
emptyState
                , ctx_transitions :: [Transition]
ctx_transitions = [Transition]
forall (f :: * -> *) a. Alternative f => f a
empty
                , ctx_duties :: [Tagged]
ctx_duties = [Tagged]
forall (f :: * -> *) a. Alternative f => f a
empty }

data TransInfo = TransInfo {
                  TransInfo -> Tagged
trans_tagged      :: Tagged 
                , TransInfo -> Store
trans_assignments :: Store  -- includes sync'ed effects
                , TransInfo -> Bool
trans_forced      :: Bool -- whether this or a sync'ed transition is not enabled was forced (i.e. was not enabled)
                , TransInfo -> Maybe Tagged
trans_actor       :: Maybe Tagged
                , TransInfo -> [TransInfo]
trans_syncs       :: [TransInfo] -- the transitions this transitions sync'ed with 
                }
                deriving (TransInfo -> TransInfo -> Bool
(TransInfo -> TransInfo -> Bool)
-> (TransInfo -> TransInfo -> Bool) -> Eq TransInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TransInfo -> TransInfo -> Bool
$c/= :: TransInfo -> TransInfo -> Bool
== :: TransInfo -> TransInfo -> Bool
$c== :: TransInfo -> TransInfo -> Bool
Eq, Eq TransInfo
Eq TransInfo
-> (TransInfo -> TransInfo -> Ordering)
-> (TransInfo -> TransInfo -> Bool)
-> (TransInfo -> TransInfo -> Bool)
-> (TransInfo -> TransInfo -> Bool)
-> (TransInfo -> TransInfo -> Bool)
-> (TransInfo -> TransInfo -> TransInfo)
-> (TransInfo -> TransInfo -> TransInfo)
-> Ord TransInfo
TransInfo -> TransInfo -> Bool
TransInfo -> TransInfo -> Ordering
TransInfo -> TransInfo -> TransInfo
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TransInfo -> TransInfo -> TransInfo
$cmin :: TransInfo -> TransInfo -> TransInfo
max :: TransInfo -> TransInfo -> TransInfo
$cmax :: TransInfo -> TransInfo -> TransInfo
>= :: TransInfo -> TransInfo -> Bool
$c>= :: TransInfo -> TransInfo -> Bool
> :: TransInfo -> TransInfo -> Bool
$c> :: TransInfo -> TransInfo -> Bool
<= :: TransInfo -> TransInfo -> Bool
$c<= :: TransInfo -> TransInfo -> Bool
< :: TransInfo -> TransInfo -> Bool
$c< :: TransInfo -> TransInfo -> Bool
compare :: TransInfo -> TransInfo -> Ordering
$ccompare :: TransInfo -> TransInfo -> Ordering
$cp1Ord :: Eq TransInfo
Ord, Int -> TransInfo -> ShowS
[TransInfo] -> ShowS
TransInfo -> String
(Int -> TransInfo -> ShowS)
-> (TransInfo -> String)
-> ([TransInfo] -> ShowS)
-> Show TransInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TransInfo] -> ShowS
$cshowList :: [TransInfo] -> ShowS
show :: TransInfo -> String
$cshow :: TransInfo -> String
showsPrec :: Int -> TransInfo -> ShowS
$cshowsPrec :: Int -> TransInfo -> ShowS
Show, ReadPrec [TransInfo]
ReadPrec TransInfo
Int -> ReadS TransInfo
ReadS [TransInfo]
(Int -> ReadS TransInfo)
-> ReadS [TransInfo]
-> ReadPrec TransInfo
-> ReadPrec [TransInfo]
-> Read TransInfo
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [TransInfo]
$creadListPrec :: ReadPrec [TransInfo]
readPrec :: ReadPrec TransInfo
$creadPrec :: ReadPrec TransInfo
readList :: ReadS [TransInfo]
$creadList :: ReadS [TransInfo]
readsPrec :: Int -> ReadS TransInfo
$creadsPrec :: Int -> ReadS TransInfo
Read) 

trans_is_action :: TransInfo -> Bool
trans_is_action :: TransInfo -> Bool
trans_is_action = Maybe Tagged -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Tagged -> Bool)
-> (TransInfo -> Maybe Tagged) -> TransInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransInfo -> Maybe Tagged
trans_actor

data Violation = DutyViolation      Tagged
               | TriggerViolation   TransInfo 
               | InvariantViolation DomId
               deriving (Eq Violation
Eq Violation
-> (Violation -> Violation -> Ordering)
-> (Violation -> Violation -> Bool)
-> (Violation -> Violation -> Bool)
-> (Violation -> Violation -> Bool)
-> (Violation -> Violation -> Bool)
-> (Violation -> Violation -> Violation)
-> (Violation -> Violation -> Violation)
-> Ord Violation
Violation -> Violation -> Bool
Violation -> Violation -> Ordering
Violation -> Violation -> Violation
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Violation -> Violation -> Violation
$cmin :: Violation -> Violation -> Violation
max :: Violation -> Violation -> Violation
$cmax :: Violation -> Violation -> Violation
>= :: Violation -> Violation -> Bool
$c>= :: Violation -> Violation -> Bool
> :: Violation -> Violation -> Bool
$c> :: Violation -> Violation -> Bool
<= :: Violation -> Violation -> Bool
$c<= :: Violation -> Violation -> Bool
< :: Violation -> Violation -> Bool
$c< :: Violation -> Violation -> Bool
compare :: Violation -> Violation -> Ordering
$ccompare :: Violation -> Violation -> Ordering
$cp1Ord :: Eq Violation
Ord, Violation -> Violation -> Bool
(Violation -> Violation -> Bool)
-> (Violation -> Violation -> Bool) -> Eq Violation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Violation -> Violation -> Bool
$c/= :: Violation -> Violation -> Bool
== :: Violation -> Violation -> Bool
$c== :: Violation -> Violation -> Bool
Eq, Int -> Violation -> ShowS
[Violation] -> ShowS
Violation -> String
(Int -> Violation -> ShowS)
-> (Violation -> String)
-> ([Violation] -> ShowS)
-> Show Violation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Violation] -> ShowS
$cshowList :: [Violation] -> ShowS
show :: Violation -> String
$cshow :: Violation -> String
showsPrec :: Int -> Violation -> ShowS
$cshowsPrec :: Int -> Violation -> ShowS
Show, ReadPrec [Violation]
ReadPrec Violation
Int -> ReadS Violation
ReadS [Violation]
(Int -> ReadS Violation)
-> ReadS [Violation]
-> ReadPrec Violation
-> ReadPrec [Violation]
-> Read Violation
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Violation]
$creadListPrec :: ReadPrec [Violation]
readPrec :: ReadPrec Violation
$creadPrec :: ReadPrec Violation
readList :: ReadS [Violation]
$creadList :: ReadS [Violation]
readsPrec :: Int -> ReadS Violation
$creadsPrec :: Int -> ReadS Violation
Read) 

data QueryRes = QuerySuccess
              | QueryFailure
              deriving (Eq QueryRes
Eq QueryRes
-> (QueryRes -> QueryRes -> Ordering)
-> (QueryRes -> QueryRes -> Bool)
-> (QueryRes -> QueryRes -> Bool)
-> (QueryRes -> QueryRes -> Bool)
-> (QueryRes -> QueryRes -> Bool)
-> (QueryRes -> QueryRes -> QueryRes)
-> (QueryRes -> QueryRes -> QueryRes)
-> Ord QueryRes
QueryRes -> QueryRes -> Bool
QueryRes -> QueryRes -> Ordering
QueryRes -> QueryRes -> QueryRes
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: QueryRes -> QueryRes -> QueryRes
$cmin :: QueryRes -> QueryRes -> QueryRes
max :: QueryRes -> QueryRes -> QueryRes
$cmax :: QueryRes -> QueryRes -> QueryRes
>= :: QueryRes -> QueryRes -> Bool
$c>= :: QueryRes -> QueryRes -> Bool
> :: QueryRes -> QueryRes -> Bool
$c> :: QueryRes -> QueryRes -> Bool
<= :: QueryRes -> QueryRes -> Bool
$c<= :: QueryRes -> QueryRes -> Bool
< :: QueryRes -> QueryRes -> Bool
$c< :: QueryRes -> QueryRes -> Bool
compare :: QueryRes -> QueryRes -> Ordering
$ccompare :: QueryRes -> QueryRes -> Ordering
$cp1Ord :: Eq QueryRes
Ord, QueryRes -> QueryRes -> Bool
(QueryRes -> QueryRes -> Bool)
-> (QueryRes -> QueryRes -> Bool) -> Eq QueryRes
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QueryRes -> QueryRes -> Bool
$c/= :: QueryRes -> QueryRes -> Bool
== :: QueryRes -> QueryRes -> Bool
$c== :: QueryRes -> QueryRes -> Bool
Eq, Int -> QueryRes -> ShowS
[QueryRes] -> ShowS
QueryRes -> String
(Int -> QueryRes -> ShowS)
-> (QueryRes -> String) -> ([QueryRes] -> ShowS) -> Show QueryRes
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QueryRes] -> ShowS
$cshowList :: [QueryRes] -> ShowS
show :: QueryRes -> String
$cshow :: QueryRes -> String
showsPrec :: Int -> QueryRes -> ShowS
$cshowsPrec :: Int -> QueryRes -> ShowS
Show, ReadPrec [QueryRes]
ReadPrec QueryRes
Int -> ReadS QueryRes
ReadS [QueryRes]
(Int -> ReadS QueryRes)
-> ReadS [QueryRes]
-> ReadPrec QueryRes
-> ReadPrec [QueryRes]
-> Read QueryRes
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [QueryRes]
$creadListPrec :: ReadPrec [QueryRes]
readPrec :: ReadPrec QueryRes
$creadPrec :: ReadPrec QueryRes
readList :: ReadS [QueryRes]
$creadList :: ReadS [QueryRes]
readsPrec :: Int -> ReadS QueryRes
$creadsPrec :: Int -> ReadS QueryRes
Read)

data Error = -- trigger errors
             NotTriggerable Tagged
           | NonDeterministicTransition
           | CompilationError String
           | RuntimeError RuntimeError
           deriving (Error -> Error -> Bool
(Error -> Error -> Bool) -> (Error -> Error -> Bool) -> Eq Error
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Error -> Error -> Bool
$c/= :: Error -> Error -> Bool
== :: Error -> Error -> Bool
$c== :: Error -> Error -> Bool
Eq, Eq Error
Eq Error
-> (Error -> Error -> Ordering)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Error)
-> (Error -> Error -> Error)
-> Ord Error
Error -> Error -> Bool
Error -> Error -> Ordering
Error -> Error -> Error
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Error -> Error -> Error
$cmin :: Error -> Error -> Error
max :: Error -> Error -> Error
$cmax :: Error -> Error -> Error
>= :: Error -> Error -> Bool
$c>= :: Error -> Error -> Bool
> :: Error -> Error -> Bool
$c> :: Error -> Error -> Bool
<= :: Error -> Error -> Bool
$c<= :: Error -> Error -> Bool
< :: Error -> Error -> Bool
$c< :: Error -> Error -> Bool
compare :: Error -> Error -> Ordering
$ccompare :: Error -> Error -> Ordering
$cp1Ord :: Eq Error
Ord, Int -> Error -> ShowS
[Error] -> ShowS
Error -> String
(Int -> Error -> ShowS)
-> (Error -> String) -> ([Error] -> ShowS) -> Show Error
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Error] -> ShowS
$cshowList :: [Error] -> ShowS
show :: Error -> String
$cshow :: Error -> String
showsPrec :: Int -> Error -> ShowS
$cshowsPrec :: Int -> Error -> ShowS
Show, ReadPrec [Error]
ReadPrec Error
Int -> ReadS Error
ReadS [Error]
(Int -> ReadS Error)
-> ReadS [Error]
-> ReadPrec Error
-> ReadPrec [Error]
-> Read Error
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Error]
$creadListPrec :: ReadPrec [Error]
readPrec :: ReadPrec Error
$creadPrec :: ReadPrec Error
readList :: ReadS [Error]
$creadList :: ReadS [Error]
readsPrec :: Int -> ReadS Error
$creadsPrec :: Int -> ReadS Error
Read) 

data RuntimeError
      = MissingInput Tagged 
      | InternalError InternalError
      deriving (RuntimeError -> RuntimeError -> Bool
(RuntimeError -> RuntimeError -> Bool)
-> (RuntimeError -> RuntimeError -> Bool) -> Eq RuntimeError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RuntimeError -> RuntimeError -> Bool
$c/= :: RuntimeError -> RuntimeError -> Bool
== :: RuntimeError -> RuntimeError -> Bool
$c== :: RuntimeError -> RuntimeError -> Bool
Eq, Eq RuntimeError
Eq RuntimeError
-> (RuntimeError -> RuntimeError -> Ordering)
-> (RuntimeError -> RuntimeError -> Bool)
-> (RuntimeError -> RuntimeError -> Bool)
-> (RuntimeError -> RuntimeError -> Bool)
-> (RuntimeError -> RuntimeError -> Bool)
-> (RuntimeError -> RuntimeError -> RuntimeError)
-> (RuntimeError -> RuntimeError -> RuntimeError)
-> Ord RuntimeError
RuntimeError -> RuntimeError -> Bool
RuntimeError -> RuntimeError -> Ordering
RuntimeError -> RuntimeError -> RuntimeError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RuntimeError -> RuntimeError -> RuntimeError
$cmin :: RuntimeError -> RuntimeError -> RuntimeError
max :: RuntimeError -> RuntimeError -> RuntimeError
$cmax :: RuntimeError -> RuntimeError -> RuntimeError
>= :: RuntimeError -> RuntimeError -> Bool
$c>= :: RuntimeError -> RuntimeError -> Bool
> :: RuntimeError -> RuntimeError -> Bool
$c> :: RuntimeError -> RuntimeError -> Bool
<= :: RuntimeError -> RuntimeError -> Bool
$c<= :: RuntimeError -> RuntimeError -> Bool
< :: RuntimeError -> RuntimeError -> Bool
$c< :: RuntimeError -> RuntimeError -> Bool
compare :: RuntimeError -> RuntimeError -> Ordering
$ccompare :: RuntimeError -> RuntimeError -> Ordering
$cp1Ord :: Eq RuntimeError
Ord, Int -> RuntimeError -> ShowS
[RuntimeError] -> ShowS
RuntimeError -> String
(Int -> RuntimeError -> ShowS)
-> (RuntimeError -> String)
-> ([RuntimeError] -> ShowS)
-> Show RuntimeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RuntimeError] -> ShowS
$cshowList :: [RuntimeError] -> ShowS
show :: RuntimeError -> String
$cshow :: RuntimeError -> String
showsPrec :: Int -> RuntimeError -> ShowS
$cshowsPrec :: Int -> RuntimeError -> ShowS
Show, ReadPrec [RuntimeError]
ReadPrec RuntimeError
Int -> ReadS RuntimeError
ReadS [RuntimeError]
(Int -> ReadS RuntimeError)
-> ReadS [RuntimeError]
-> ReadPrec RuntimeError
-> ReadPrec [RuntimeError]
-> Read RuntimeError
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [RuntimeError]
$creadListPrec :: ReadPrec [RuntimeError]
readPrec :: ReadPrec RuntimeError
$creadPrec :: ReadPrec RuntimeError
readList :: ReadS [RuntimeError]
$creadList :: ReadS [RuntimeError]
readsPrec :: Int -> ReadS RuntimeError
$creadsPrec :: Int -> ReadS RuntimeError
Read) 

data InternalError 
      = EnumerateInfiniteDomain DomId Domain 
      | MissingSubstitution Var
      | PrimitiveApplication DomId
      | UndeclaredType DomId 
      deriving (InternalError -> InternalError -> Bool
(InternalError -> InternalError -> Bool)
-> (InternalError -> InternalError -> Bool) -> Eq InternalError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InternalError -> InternalError -> Bool
$c/= :: InternalError -> InternalError -> Bool
== :: InternalError -> InternalError -> Bool
$c== :: InternalError -> InternalError -> Bool
Eq, Eq InternalError
Eq InternalError
-> (InternalError -> InternalError -> Ordering)
-> (InternalError -> InternalError -> Bool)
-> (InternalError -> InternalError -> Bool)
-> (InternalError -> InternalError -> Bool)
-> (InternalError -> InternalError -> Bool)
-> (InternalError -> InternalError -> InternalError)
-> (InternalError -> InternalError -> InternalError)
-> Ord InternalError
InternalError -> InternalError -> Bool
InternalError -> InternalError -> Ordering
InternalError -> InternalError -> InternalError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: InternalError -> InternalError -> InternalError
$cmin :: InternalError -> InternalError -> InternalError
max :: InternalError -> InternalError -> InternalError
$cmax :: InternalError -> InternalError -> InternalError
>= :: InternalError -> InternalError -> Bool
$c>= :: InternalError -> InternalError -> Bool
> :: InternalError -> InternalError -> Bool
$c> :: InternalError -> InternalError -> Bool
<= :: InternalError -> InternalError -> Bool
$c<= :: InternalError -> InternalError -> Bool
< :: InternalError -> InternalError -> Bool
$c< :: InternalError -> InternalError -> Bool
compare :: InternalError -> InternalError -> Ordering
$ccompare :: InternalError -> InternalError -> Ordering
$cp1Ord :: Eq InternalError
Ord, Int -> InternalError -> ShowS
[InternalError] -> ShowS
InternalError -> String
(Int -> InternalError -> ShowS)
-> (InternalError -> String)
-> ([InternalError] -> ShowS)
-> Show InternalError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InternalError] -> ShowS
$cshowList :: [InternalError] -> ShowS
show :: InternalError -> String
$cshow :: InternalError -> String
showsPrec :: Int -> InternalError -> ShowS
$cshowsPrec :: Int -> InternalError -> ShowS
Show, ReadPrec [InternalError]
ReadPrec InternalError
Int -> ReadS InternalError
ReadS [InternalError]
(Int -> ReadS InternalError)
-> ReadS [InternalError]
-> ReadPrec InternalError
-> ReadPrec [InternalError]
-> Read InternalError
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [InternalError]
$creadListPrec :: ReadPrec [InternalError]
readPrec :: ReadPrec InternalError
$creadPrec :: ReadPrec InternalError
readList :: ReadS [InternalError]
$creadList :: ReadS [InternalError]
readsPrec :: Int -> ReadS InternalError
$creadsPrec :: Int -> ReadS InternalError
Read)

print_error :: Error -> String
print_error :: Error -> String
print_error (NotTriggerable Tagged
te) = String
"not a triggerable instance: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Tagged -> String
ppTagged Tagged
te
print_error (Error
NonDeterministicTransition) = String
"non-deterministic transition attempt"
print_error (CompilationError String
err) = String
err
print_error (RuntimeError RuntimeError
err) = RuntimeError -> String
print_runtime_error RuntimeError
err

print_runtime_error :: RuntimeError -> String
print_runtime_error :: RuntimeError -> String
print_runtime_error (MissingInput Tagged
te) = String
"missing input assignment for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Tagged -> String
ppTagged Tagged
te
print_runtime_error (InternalError InternalError
err) = String
"INTERNAL ERROR " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InternalError -> String
print_internal_error InternalError
err

print_internal_error :: InternalError -> String
print_internal_error :: InternalError -> String
print_internal_error (EnumerateInfiniteDomain String
d Domain
AnyString) = String
"cannot enumerate all strings of type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d
print_internal_error (EnumerateInfiniteDomain String
d Domain
AnyInt) = String
"cannot enumerate all integers of type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d
print_internal_error (EnumerateInfiniteDomain String
d Domain
_) = String
"cannot enumerate all instances of type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d
print_internal_error (MissingSubstitution (Var String
base String
dec)) = String
"variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
base String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
dec String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not bound"
print_internal_error (PrimitiveApplication String
d) = String
"application of primitive type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d
print_internal_error (UndeclaredType String
d) = String
"undeclared type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d