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
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  -- meta-info about components
              ,   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

-- | based union over stores, precedence HoldsTrue > HoldsFalse > Unknown
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)

-- | assumes the instance of a closed type
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)
      ]

-- 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) <- 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 --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 { 
                  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  -- 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
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

-- | Get all the TransInfo nodes in the tree represented by the given root
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 = -- trigger errors
             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