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
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]
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 -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Info] -> ShowS
$cshowList :: [Info] -> ShowS
show :: Info -> [Char]
$cshow :: Info -> [Char]
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
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
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
Ord, Transition -> Transition -> Bool
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 -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Transition] -> ShowS
$cshowList :: [Transition] -> ShowS
show :: Transition -> [Char]
$cshow :: Transition -> [Char]
showsPrec :: Int -> Transition -> ShowS
$cshowsPrec :: Int -> Transition -> ShowS
Show, ReadPrec [Transition]
ReadPrec Transition
Int -> ReadS Transition
ReadS [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
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
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
Ord, Int -> Assignment -> ShowS
[Assignment] -> ShowS
Assignment -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Assignment] -> ShowS
$cshowList :: [Assignment] -> ShowS
show :: Assignment -> [Char]
$cshow :: Assignment -> [Char]
showsPrec :: Int -> Assignment -> ShowS
$cshowsPrec :: Int -> Assignment -> ShowS
Show, ReadPrec [Assignment]
ReadPrec Assignment
Int -> ReadS Assignment
ReadS [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 = forall k a. Map k a
M.empty
emptyStore :: Map k a
emptyStore = forall k a. Map k a
M.empty
store_union :: Store -> Store -> Store
store_union :: Store -> Store -> Store
store_union = 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Store -> Store -> Store
store_union forall k a. Map k a
emptyStore
make_assignments :: Spec -> Store -> State -> State
make_assignments :: Spec -> Store -> State -> State
make_assignments Spec
spec = forall a b c. (a -> b -> c) -> b -> a -> c
flip (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 te :: Tagged
te@(Elem
_,[Char]
d) Assignment
HoldsTrue | Spec -> [Char] -> Bool
is_var Spec
spec [Char]
d = Tagged -> State -> State
var_assignment Tagged
te
| Spec -> [Char] -> Bool
is_function Spec
spec [Char]
d = Tagged -> State -> State
function_assignment Tagged
te
| Bool
otherwise = 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
create :: Tagged -> State -> State
create :: Tagged -> State -> State
create Tagged
te State
s = State
s { contents :: Map Tagged Info
contents = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Tagged
te Info{ value :: Bool
value = Bool
True, from_sat :: Bool
from_sat = Bool
False } (State -> Map Tagged Info
contents State
s) }
terminate :: Tagged -> State -> State
terminate :: Tagged -> State -> State
terminate Tagged
te State
s = State
s { contents :: Map Tagged Info
contents = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Tagged
te Info{ value :: Bool
value = Bool
False, from_sat :: Bool
from_sat = Bool
False } (State -> Map Tagged Info
contents State
s) }
obfuscate :: Tagged -> State -> State
obfuscate :: Tagged -> State -> State
obfuscate Tagged
te State
s = State
s { contents :: Map Tagged Info
contents = forall k a. Ord k => k -> Map k a -> Map k a
M.delete Tagged
te (State -> Map Tagged Info
contents State
s) }
var_assignment :: Tagged -> State -> State
var_assignment :: Tagged -> State -> State
var_assignment te :: Tagged
te@(Elem
_,[Char]
d) State
s = Tagged -> State -> State
create Tagged
te forall a b. (a -> b) -> a -> b
$ State
s { contents :: Map Tagged Info
contents = forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey forall {a}. (a, [Char]) -> Info -> Info
op (State -> Map Tagged Info
contents State
s) }
where op :: (a, [Char]) -> Info -> Info
op te :: (a, [Char])
te@(a
_,[Char]
d') Info
i | [Char]
d forall a. Eq a => a -> a -> Bool
== [Char]
d' = Info
i { value :: Bool
value = Bool
False, from_sat :: Bool
from_sat = Bool
False }
| Bool
otherwise = Info
i
function_assignment :: Tagged -> State -> State
function_assignment :: Tagged -> State -> State
function_assignment te :: Tagged
te@(Product [Tagged
f,Tagged
t], [Char]
d) State
s =
Tagged -> State -> State
create Tagged
te forall a b. (a -> b) -> a -> b
$ State
s { contents :: Map Tagged Info
contents = forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey Tagged -> Info -> Info
op (State -> Map Tagged Info
contents State
s) }
where op :: Tagged -> Info -> Info
op (Product [Tagged
f',Tagged
t'], [Char]
d') Info
i | [Char]
d forall a. Eq a => a -> a -> Bool
== [Char]
d' Bool -> Bool -> Bool
&& Tagged
f forall a. Eq a => a -> a -> Bool
== Tagged
f' = Info
i { value :: Bool
value = Bool
False, from_sat :: Bool
from_sat = Bool
False }
op Tagged
_ Info
i = Info
i
function_assignment Tagged
_ State
s = State
s
derive :: Tagged -> State -> State
derive :: Tagged -> State -> State
derive Tagged
te State
s = State
s { contents :: Map Tagged Info
contents = 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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Info{ value :: Bool
value = Bool
True, from_sat :: Bool
from_sat = Bool
True }
adj (Just Info
info) = forall a. a -> Maybe a
Just Info
info
derive_all :: [Tagged] -> State -> State
derive_all :: [Tagged] -> State -> State
derive_all = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Tagged -> State -> State
derive)
holds :: Tagged -> State -> Bool
holds :: Tagged -> State -> Bool
holds Tagged
te State
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((forall a. Eq a => a -> a -> Bool
==Bool
True) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Info -> Bool
value) (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 { contents :: Map Tagged Info
contents = 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 forall a. Num a => a -> a -> a
+ (State -> Int
time State
state) }
instance Show State where
show :: State -> [Char]
show State
state = [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$
[ Tagged -> [Char]
show_component Tagged
c forall a. [a] -> [a] -> [a]
++ [Char]
" = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Info -> Bool
value Info
m)
| (Tagged
c,Info
m) <- 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) <- forall k a. Map k a -> [(k, a)]
M.assocs (State -> Map Tagged Info
contents State
state), Bool
True 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 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) <- forall k a. Map k a -> [(k, a)]
M.assocs (State -> Map Tagged Info
contents State
state), Bool
False 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) <- 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 {
ctx_spec :: Spec
ctx_spec = Spec
spec
, ctx_state :: State
ctx_state = State
emptyState
, ctx_transitions :: [Transition]
ctx_transitions = forall (f :: * -> *) a. Alternative f => f a
empty
, ctx_duties :: [Tagged]
ctx_duties = 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
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
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
Ord, Int -> TransInfo -> ShowS
[TransInfo] -> ShowS
TransInfo -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TransInfo] -> ShowS
$cshowList :: [TransInfo] -> ShowS
show :: TransInfo -> [Char]
$cshow :: TransInfo -> [Char]
showsPrec :: Int -> TransInfo -> ShowS
$cshowsPrec :: Int -> TransInfo -> ShowS
Show, ReadPrec [TransInfo]
ReadPrec TransInfo
Int -> ReadS TransInfo
ReadS [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 = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransInfo -> Maybe Tagged
trans_actor
trans_all_infos :: TransInfo -> [TransInfo]
trans_all_infos :: TransInfo -> [TransInfo]
trans_all_infos TransInfo
info = TransInfo
info forall a. a -> [a] -> [a]
: forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TransInfo -> [TransInfo]
trans_all_infos (TransInfo -> [TransInfo]
trans_syncs TransInfo
info)
data Violation = DutyViolation Tagged
| TriggerViolation TransInfo
| InvariantViolation DomId
deriving (Eq 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
Ord, Violation -> Violation -> Bool
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 -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Violation] -> ShowS
$cshowList :: [Violation] -> ShowS
show :: Violation -> [Char]
$cshow :: Violation -> [Char]
showsPrec :: Int -> Violation -> ShowS
$cshowsPrec :: Int -> Violation -> ShowS
Show, ReadPrec [Violation]
ReadPrec Violation
Int -> ReadS Violation
ReadS [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
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
Ord, QueryRes -> QueryRes -> Bool
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 -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [QueryRes] -> ShowS
$cshowList :: [QueryRes] -> ShowS
show :: QueryRes -> [Char]
$cshow :: QueryRes -> [Char]
showsPrec :: Int -> QueryRes -> ShowS
$cshowsPrec :: Int -> QueryRes -> ShowS
Show, ReadPrec [QueryRes]
ReadPrec QueryRes
Int -> ReadS QueryRes
ReadS [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 DomId
| CompilationError String
| RuntimeError RuntimeError
deriving (Error -> Error -> Bool
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
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
Ord, Int -> Error -> ShowS
[Error] -> ShowS
Error -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Error] -> ShowS
$cshowList :: [Error] -> ShowS
show :: Error -> [Char]
$cshow :: Error -> [Char]
showsPrec :: Int -> Error -> ShowS
$cshowsPrec :: Int -> Error -> ShowS
Show, ReadPrec [Error]
ReadPrec Error
Int -> ReadS Error
ReadS [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
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
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
Ord, Int -> RuntimeError -> ShowS
[RuntimeError] -> ShowS
RuntimeError -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [RuntimeError] -> ShowS
$cshowList :: [RuntimeError] -> ShowS
show :: RuntimeError -> [Char]
$cshow :: RuntimeError -> [Char]
showsPrec :: Int -> RuntimeError -> ShowS
$cshowsPrec :: Int -> RuntimeError -> ShowS
Show, ReadPrec [RuntimeError]
ReadPrec RuntimeError
Int -> ReadS RuntimeError
ReadS [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
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
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
Ord, Int -> InternalError -> ShowS
[InternalError] -> ShowS
InternalError -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [InternalError] -> ShowS
$cshowList :: [InternalError] -> ShowS
show :: InternalError -> [Char]
$cshow :: InternalError -> [Char]
showsPrec :: Int -> InternalError -> ShowS
$cshowsPrec :: Int -> InternalError -> ShowS
Show, ReadPrec [InternalError]
ReadPrec InternalError
Int -> ReadS InternalError
ReadS [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 -> [Char]
print_error (NotTriggerable [Char]
d) = [Char]
"not a triggerable (act- or event-) type: " forall a. [a] -> [a] -> [a]
++ [Char]
d
print_error (CompilationError [Char]
err) = [Char]
err
print_error (RuntimeError RuntimeError
err) = RuntimeError -> [Char]
print_runtime_error RuntimeError
err
print_runtime_error :: RuntimeError -> String
print_runtime_error :: RuntimeError -> [Char]
print_runtime_error (MissingInput Tagged
te) = [Char]
"missing input assignment for: " forall a. [a] -> [a] -> [a]
++ Tagged -> [Char]
ppTagged Tagged
te
print_runtime_error (InternalError InternalError
err) = [Char]
"INTERNAL ERROR " forall a. [a] -> [a] -> [a]
++ InternalError -> [Char]
print_internal_error InternalError
err
print_internal_error :: InternalError -> String
print_internal_error :: InternalError -> [Char]
print_internal_error (EnumerateInfiniteDomain [Char]
d Domain
AnyString) = [Char]
"cannot enumerate all strings of type: " forall a. [a] -> [a] -> [a]
++ [Char]
d
print_internal_error (EnumerateInfiniteDomain [Char]
d Domain
AnyInt) = [Char]
"cannot enumerate all integers of type: " forall a. [a] -> [a] -> [a]
++ [Char]
d
print_internal_error (EnumerateInfiniteDomain [Char]
d Domain
_) = [Char]
"cannot enumerate all instances of type: " forall a. [a] -> [a] -> [a]
++ [Char]
d
print_internal_error (MissingSubstitution (Var [Char]
base [Char]
dec)) = [Char]
"variable " forall a. [a] -> [a] -> [a]
++ [Char]
base forall a. [a] -> [a] -> [a]
++ [Char]
dec forall a. [a] -> [a] -> [a]
++ [Char]
" not bound"
print_internal_error (PrimitiveApplication [Char]
d) = [Char]
"application of primitive type: " forall a. [a] -> [a] -> [a]
++ [Char]
d
print_internal_error (UndeclaredType [Char]
d) = [Char]
"undeclared type: " forall a. [a] -> [a] -> [a]
++ [Char]
d