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
}
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
, 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
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)
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)
]
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
, Context -> State
ctx_state :: State
, Context -> [Transition]
ctx_transitions :: [Transition]
, Context -> [Tagged]
ctx_duties :: [Tagged]
}
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
, TransInfo -> Bool
trans_forced :: Bool
, TransInfo -> Maybe Tagged
trans_actor :: Maybe Tagged
, TransInfo -> [TransInfo]
trans_syncs :: [TransInfo]
}
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 =
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