{-# LANGUAGE LambdaCase, TupleSections #-}

module Language.EFLINT.Eval where

import Language.EFLINT.Spec
import Language.EFLINT.State

import Control.Monad
import Control.Applicative

import Data.Bool (bool)
import Data.List ((\\))
import Data.Maybe (fromJust)
import qualified Data.Map as M
import qualified Data.Set as S

data M_Subs a = M_Subs { forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs :: Spec -> State -> InputMap -> Subs -> Either RuntimeError [a] }

err :: RuntimeError -> M_Subs a 
err :: forall a. RuntimeError -> M_Subs a
err RuntimeError
re = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall a b. a -> Either a b
Left RuntimeError
re

nd :: [a] -> M_Subs a
nd :: forall a. [a] -> M_Subs a
nd [a]
vals = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return [a]
vals

results :: M_Subs a -> M_Subs [a]
results :: forall a. M_Subs a -> M_Subs [a]
results M_Subs a
n = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
n Spec
spec State
state InputMap
inpm Subs
subs

ignoreMissingInput :: M_Subs a -> M_Subs a
ignoreMissingInput :: forall a. M_Subs a -> M_Subs a
ignoreMissingInput M_Subs a
m = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> case forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
m Spec
spec State
state InputMap
inpm Subs
subs of
  Left (MissingInput Tagged
_) -> forall a b. b -> Either a b
Right []
  Either RuntimeError [a]
res                   -> Either RuntimeError [a]
res
 
bind :: Var -> Tagged -> M_Subs a -> M_Subs a
bind :: forall a. Var -> Tagged -> M_Subs a -> M_Subs a
bind Var
k Tagged
v M_Subs a
m = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm -> forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
m Spec
spec State
state InputMap
inpm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
k Tagged
v

scope_var :: Var -> M_Subs a -> M_Subs a
scope_var :: forall a. Var -> M_Subs a -> M_Subs a
scope_var Var
x M_Subs a
m = do 
  Tagged
te <- Var -> M_Subs Tagged
every_valid_subs Var
x
  forall a. Var -> Tagged -> M_Subs a -> M_Subs a
bind Var
x Tagged
te M_Subs a
m

get_type_spec :: DomId -> M_Subs TypeSpec
get_type_spec :: String -> M_Subs TypeSpec
get_type_spec String
d = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> 
                    case Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d of
                      Maybe TypeSpec
Nothing    -> forall a b. a -> Either a b
Left (InternalError -> RuntimeError
InternalError (String -> InternalError
UndeclaredType String
d))
                      Just TypeSpec
tspec -> forall a b. b -> Either a b
Right [TypeSpec
tspec]

get_dom :: DomId -> M_Subs (Domain, Term)
get_dom :: String -> M_Subs (Domain, Term)
get_dom String
d = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> 
              case Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d of
                Maybe TypeSpec
Nothing    -> forall a b. a -> Either a b
Left (InternalError -> RuntimeError
InternalError (String -> InternalError
UndeclaredType String
d))
                Just TypeSpec
tspec -> forall a b. b -> Either a b
Right [(TypeSpec -> Domain
domain TypeSpec
tspec, TypeSpec -> Term
domain_constraint TypeSpec
tspec)]

get_time :: M_Subs Int
get_time :: M_Subs Int
get_time = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return [State -> Int
time State
state]

get_subs :: M_Subs Subs
get_subs :: M_Subs Subs
get_subs = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return [Subs
subs]

modify_subs :: (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs :: forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs Subs -> Subs
mod M_Subs a
m = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm -> forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
m Spec
spec State
state InputMap
inpm forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subs -> Subs
mod 

get_spec :: M_Subs Spec 
get_spec :: M_Subs Spec
get_spec = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return [Spec
spec]

get_state :: M_Subs State
get_state :: M_Subs State
get_state = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return [State
state]

get_input :: M_Subs InputMap
get_input :: M_Subs InputMap
get_input = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return [InputMap
inpm]

get_input_assignment :: Tagged -> M_Subs Assignment
get_input_assignment :: Tagged -> M_Subs Assignment
get_input_assignment Tagged
te = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> 
  forall a b. b -> Either a b
Right [forall b a. b -> (a -> b) -> Maybe a -> b
maybe Assignment
Unknown (forall a. a -> a -> Bool -> a
bool Assignment
HoldsFalse Assignment
HoldsTrue) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Tagged
te InputMap
inpm)]

get_assignment :: Tagged -> M_Subs Assignment
get_assignment :: Tagged -> M_Subs Assignment
get_assignment te :: Tagged
te@(Elem
_,String
d) = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> 
  forall a b. b -> Either a b
Right [forall b a. b -> (a -> b) -> Maybe a -> b
maybe Assignment
Unknown Info -> Assignment
op (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Tagged
te (State -> Map Tagged Info
contents State
state))]
    where op :: Info -> Assignment
op Info
info | Info -> Bool
from_sat Info
info = Assignment
Unknown
                  | Info -> Bool
value Info
info    = Assignment
HoldsTrue
                  | Bool
otherwise     = Assignment
HoldsFalse 

instance Functor M_Subs where
  fmap :: forall a b. (a -> b) -> M_Subs a -> M_Subs b
fmap  = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM 

instance Applicative M_Subs where
  pure :: forall a. a -> M_Subs a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. M_Subs (a -> b) -> M_Subs a -> M_Subs b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad M_Subs where
  return :: forall a. a -> M_Subs a
return a
a  = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return [a
a]
  >>= :: forall a b. M_Subs a -> (a -> M_Subs b) -> M_Subs b
(>>=) M_Subs a
m a -> M_Subs b
f = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> do 
                [a]
as <- forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
m Spec
spec State
state InputMap
inpm Subs
subs
                let op :: [b] -> a -> Either RuntimeError [b]
op [b]
res a
a = (forall a. [a] -> [a] -> [a]
++[b]
res) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs (a -> M_Subs b
f a
a) Spec
spec State
state InputMap
inpm Subs
subs
                forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [b] -> a -> Either RuntimeError [b]
op [] [a]
as 

instance Alternative M_Subs where
  empty :: forall a. M_Subs a
empty     = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return []
  M_Subs a
m1 <|> :: forall a. M_Subs a -> M_Subs a -> M_Subs a
<|> M_Subs a
m2 = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> do
                        [a]
xs <- forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
m1 Spec
spec State
state InputMap
inpm Subs
subs 
                        [a]
ys <- forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
m2 Spec
spec State
state InputMap
inpm Subs
subs
                        forall (m :: * -> *) a. Monad m => a -> m a
return ([a]
xs forall a. [a] -> [a] -> [a]
++ [a]
ys)

instance MonadPlus M_Subs where

instantiate_domain :: DomId -> Domain -> M_Subs Elem
instantiate_domain :: String -> Domain -> M_Subs Elem
instantiate_domain String
d Domain
dom = case Domain
dom of
  Domain
Time          -> M_Subs Int
get_time forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
time -> forall a. [a] -> M_Subs a
nd [ Int -> Elem
Int Int
i | Int
i <- [Int
0..Int
time]]
  Domain
AnyString     -> forall a. RuntimeError -> M_Subs a
err (InternalError -> RuntimeError
InternalError forall a b. (a -> b) -> a -> b
$ String -> Domain -> InternalError
EnumerateInfiniteDomain String
d Domain
dom)
  Domain
AnyInt        -> forall a. RuntimeError -> M_Subs a
err (InternalError -> RuntimeError
InternalError forall a b. (a -> b) -> a -> b
$ String -> Domain -> InternalError
EnumerateInfiniteDomain String
d Domain
dom)
  Strings [String]
ss    -> forall a. [a] -> M_Subs a
nd [ String -> Elem
String String
s | String
s <- [String]
ss ]
  Ints [Int]
is       -> forall a. [a] -> M_Subs a
nd [ Int -> Elem
Int Int
i    | Int
i <- [Int]
is ]
  Products [Var]
xs   -> [Tagged] -> Elem
Product forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map Var -> M_Subs Tagged
every_valid_subs [Var]
xs)

substitute_var :: Var -> M_Subs Tagged
substitute_var :: Var -> M_Subs Tagged
substitute_var Var
x = do
  Spec
spec <- M_Subs Spec
get_spec
  Subs
subs <- M_Subs Subs
get_subs
  case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Subs
subs of
    Just te :: Tagged
te@(Elem
v,String
d') -> forall (m :: * -> *) a. Monad m => a -> m a
return (Elem
v, Spec -> Var -> String
remove_decoration Spec
spec Var
x)
    Maybe Tagged
Nothing        -> forall a. RuntimeError -> M_Subs a
err (InternalError -> RuntimeError
InternalError forall a b. (a -> b) -> a -> b
$ Var -> InternalError
MissingSubstitution Var
x)

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

-- if fact/duty/event/action is of an inenumerable type, is derived with "Holds when" and is not in state,
-- then check if it is a valid instance and whether it satisfies derivation clause
-- if so, consider it to hold true
is_in_virtual_state :: Tagged -> M_Subs Bool
is_in_virtual_state :: Tagged -> M_Subs Bool
is_in_virtual_state te :: Tagged
te@(Elem
_,String
d) = do
  Spec
spec <- M_Subs Spec
get_spec
  Tagged -> M_Subs Bool
is_valid_instance Tagged
te forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
   Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
   Bool
True  -> do
    Tagged -> M_Subs Assignment
get_input_assignment Tagged
te forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     Assignment
HoldsTrue   -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
     Assignment
HoldsFalse  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
     Assignment
Unknown     -> do
      Tagged -> M_Subs Assignment
get_assignment Tagged
te forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Assignment
HoldsTrue  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       Assignment
HoldsFalse -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
       Assignment
Unknown    -> do
        Tagged -> M_Subs Bool
is_derivable Tagged
te forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
         Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
         Bool
False -> case forall a. HasCallStack => Maybe a -> a
fromJust (Spec -> String -> Maybe Bool
closed_type Spec
spec String
d) of
          Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          Bool
False -> forall a. RuntimeError -> M_Subs a
err (Tagged -> RuntimeError
MissingInput Tagged
te)

is_enabled :: Tagged -> M_Subs Bool 
is_enabled :: Tagged -> M_Subs Bool
is_enabled v :: Tagged
v@(Elem
e,String
d) = do 
  Spec
spec <- M_Subs Spec
get_spec
  Tagged -> M_Subs Bool
is_in_virtual_state Tagged
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False 
    Bool
True  -> Tagged -> M_Subs Bool
sat_conditions Tagged
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Bool
True  -> case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Kind
kind (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d) of
        Just (Act ActSpec
aspec) -> do
          (Domain
dom, Term
_) <- String -> M_Subs (Domain, Term)
get_dom String
d
          let (Product [Tagged]
args, Products [Var]
xs) = (Elem
e, Domain
dom)
          forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) forall a b. (a -> b) -> a -> b
$ do
            [TransInfo]
sync_infos <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Sync -> M_Subs [TransInfo]
eval_sync (ActSpec -> [Sync]
syncs ActSpec
aspec) 
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransInfo -> Bool
trans_forced) [TransInfo]
sync_infos)
        Maybe Kind
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

is_valid_instance :: Tagged -> M_Subs Bool
is_valid_instance :: Tagged -> M_Subs Bool
is_valid_instance te :: Tagged
te@(Elem
e,String
d) = do 
  (Domain
dom, Term
dom_filter) <- String -> M_Subs (Domain, Term)
get_dom String
d 
  let bindings :: Subs
bindings = case (Domain
dom,Elem
e) of (Products [Var]
xs, Product [Tagged]
args) -> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
                                 (Domain, Elem)
_ -> forall k a. k -> a -> Map k a
M.singleton (String -> Var
no_decoration String
d) Tagged
te
  let check_constraint :: M_Subs Bool
check_constraint = forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) (forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
dom_filter) forall (m :: * -> *) a. Monad m => a -> m a
return)
  case (Elem
e, Domain
dom) of 
    (Int Int
i, Ints [Int]
is) | Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
is -> M_Subs Bool
check_constraint
    (Int Int
i, Domain
AnyInt) -> M_Subs Bool
check_constraint
    (String String
s, Strings [String]
ss) | String
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
ss -> M_Subs Bool
check_constraint
    (String String
s, Domain
AnyString) -> M_Subs Bool
check_constraint
    (Product [Tagged]
args, Products [Var]
params) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tagged]
args forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
params ->
      forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Tagged -> M_Subs Bool
is_valid_instance [Tagged]
args forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        Bool
True  -> M_Subs Bool
check_constraint 
    (Elem, Domain)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

is_derivable :: Tagged -> M_Subs Bool
is_derivable :: Tagged -> M_Subs Bool
is_derivable te :: Tagged
te@(Elem
e,String
d) = Tagged -> M_Subs Bool -> M_Subs Bool
derivation_closure_on Tagged
te forall a b. (a -> b) -> a -> b
$ do
  Spec
spec <- M_Subs Spec
get_spec
  (Domain
dom, Term
_) <- String -> M_Subs (Domain, Term)
get_dom String
d
  let bindings :: Subs
bindings = case (Domain
dom,Elem
e) of (Products [Var]
xs, Product [Tagged]
args) -> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
                                 (Domain, Elem)
_ -> forall k a. k -> a -> Map k a
M.singleton (String -> Var
no_decoration String
d) Tagged
te
  let consider_clause :: Derivation -> M_Subs Bool
consider_clause Derivation
deriv = case Derivation
deriv of 
          Dv [Var]
xs Term
dvt -> do [Tagged]
tes <- forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) 
                                   (forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach ([Var]
xs forall a. Eq a => [a] -> [a] -> [a]
\\ forall k a. Map k a -> [k]
M.keys Subs
bindings) (forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
dvt) forall (m :: * -> *) a. Monad m => a -> m a
return))
                          forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged
te forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Tagged]
tes) -- valid instance and in DV
          HoldsWhen Term
t -> forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) (forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t) forall (m :: * -> *) a. Monad m => a -> m a
return )
  case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> [Derivation]
derivation (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d) of 
    Maybe [Derivation]
Nothing  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just [Derivation]
dvs -> (forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Derivation -> M_Subs Bool
consider_clause [Derivation]
dvs) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
                  Bool
True  -> Tagged -> M_Subs Bool
sat_conditions Tagged
te
                  Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

derivation_closure_on :: Tagged -> M_Subs Bool -> M_Subs Bool
derivation_closure_on :: Tagged -> M_Subs Bool -> M_Subs Bool
derivation_closure_on Tagged
te M_Subs Bool
m = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Tagged
te (State -> Map Tagged Info
contents State
state) of
  Just Info
info -> forall (m :: * -> *) a. Monad m => a -> m a
return [Info -> Bool
value Info
info]
  Maybe Info
Nothing   -> forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs Bool
m Spec
spec (State -> State
mod State
state) InputMap
inpm Subs
subs
  where mod :: State -> State
mod 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
True }) (State -> Map Tagged Info
contents State
s) }

sat_conditions :: Tagged -> M_Subs Bool
sat_conditions :: Tagged -> M_Subs Bool
sat_conditions te :: Tagged
te@(Elem
v,String
d) = 
  Tagged -> M_Subs Bool
is_valid_instance Tagged
te forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case  
    Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Bool
True  -> do
      TypeSpec
tspec <- String -> M_Subs TypeSpec
get_type_spec String
d
      (Domain
dom, Term
_) <- String -> M_Subs (Domain, Term)
get_dom String
d
      let bindings :: Subs
bindings = case (Domain
dom,Elem
v) of (Products [Var]
xs, Product [Tagged]
args) -> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
                                     (Domain, Elem)
_ -> forall k a. k -> a -> Map k a
M.singleton (String -> Var
no_decoration String
d) Tagged
te
      forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) (forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> M_Subs Value
eval) (TypeSpec -> [Term]
conditions TypeSpec
tspec))

is_violated :: Tagged -> M_Subs Bool
is_violated :: Tagged -> M_Subs Bool
is_violated te :: Tagged
te@(Elem
_,String
d) = Bool -> Bool -> Bool
(&&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged -> M_Subs Bool
is_in_virtual_state Tagged
te forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tagged -> M_Subs Bool
violation_condition Tagged
te
 where violation_condition :: Tagged -> M_Subs Bool
violation_condition Tagged
te = do 
        Spec
spec <- M_Subs Spec
get_spec 
        Tagged -> Maybe [Term] -> M_Subs Bool
eval_violation_condition Tagged
te (Spec -> String -> Maybe [Term]
find_violation_cond Spec
spec String
d)

eval_violation_condition :: Tagged -> Maybe [Term] -> M_Subs Bool
eval_violation_condition :: Tagged -> Maybe [Term] -> M_Subs Bool
eval_violation_condition te :: Tagged
te@(Elem
v,String
d) Maybe [Term]
mconds = do
  (Domain
dom, Term
_) <- String -> M_Subs (Domain, Term)
get_dom String
d
  let Products [Var]
xs = Domain
dom
      Product [Tagged]
args = Elem
v
  forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) 
    (forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> Term
BoolLit Bool
False) (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Term -> Term -> Term
Or (Bool -> Term
BoolLit Bool
False)) Maybe [Term]
mconds)) forall (m :: * -> *) a. Monad m => a -> m a
return)


syncTransInfos :: [TransInfo] -> (Store, Bool {- forced? -})
syncTransInfos :: [TransInfo] -> (Store, Bool)
syncTransInfos = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TransInfo -> (Store, Bool) -> (Store, Bool)
op (forall {k} {a}. Map k a
emptyStore, Bool
False)
  where op :: TransInfo -> (Store, Bool) -> (Store, Bool)
op (TransInfo Tagged
te Store
ass Bool
is_f Maybe Tagged
is_a [TransInfo]
tes) (Store
ass',Bool
is_f') = 
          (Store
ass Store -> Store -> Store
`store_union` Store
ass', Bool
is_f Bool -> Bool -> Bool
|| Bool
is_f')

instantiate_trans :: Tagged -> M_Subs TransInfo
instantiate_trans :: Tagged -> M_Subs TransInfo
instantiate_trans = Set Tagged -> Tagged -> M_Subs TransInfo
instantiate_trans' forall a. Set a
S.empty

instantiate_trans' :: S.Set Tagged -> Tagged -> M_Subs TransInfo
instantiate_trans' :: Set Tagged -> Tagged -> M_Subs TransInfo
instantiate_trans' Set Tagged
done' te :: Tagged
te@(Elem
v,String
d) 
  | Tagged
te forall a. Ord a => a -> Set a -> Bool
`S.member` Set Tagged
done' = forall (f :: * -> *) a. Alternative f => f a
empty
  | Bool
otherwise           = do 
  TypeSpec
tspec <- String -> M_Subs TypeSpec
get_type_spec String
d
  Bool
is_enabled <- Tagged -> M_Subs Bool
is_enabled Tagged
te 
  case TypeSpec -> Kind
kind TypeSpec
tspec of 
      Fact FactSpec
_      -> forall (f :: * -> *) a. Alternative f => f a
empty
      Duty DutySpec
_      -> forall (f :: * -> *) a. Alternative f => f a
empty 
      Act ActSpec
aspec   -> forall {t :: * -> *}.
Traversable t =>
Tagged
-> Maybe Tagged -> Bool -> [Effect] -> t Sync -> M_Subs TransInfo
do_transition Tagged
te Maybe Tagged
actor Bool
is_enabled (ActSpec -> [Effect]
effects ActSpec
aspec) (ActSpec -> [Sync]
syncs ActSpec
aspec)
      Event EventSpec
espec -> forall {t :: * -> *}.
Traversable t =>
Tagged
-> Maybe Tagged -> Bool -> [Effect] -> t Sync -> M_Subs TransInfo
do_transition Tagged
te forall a. Maybe a
Nothing Bool
is_enabled (EventSpec -> [Effect]
event_effects EventSpec
espec) (EventSpec -> [Sync]
event_syncs EventSpec
espec)
  where done :: Set Tagged
done = Tagged
te forall a. Ord a => a -> Set a -> Set a
`S.insert` Set Tagged
done'
        do_transition :: Tagged
-> Maybe Tagged -> Bool -> [Effect] -> t Sync -> M_Subs TransInfo
do_transition te :: Tagged
te@(Elem
v,String
d) Maybe Tagged
mActor Bool
is_enabled [Effect]
effects t Sync
ss = do 
          (Domain
dom, Term
_) <- String -> M_Subs (Domain, Term)
get_dom String
d
          let Products [Var]
xs = Domain
dom
          let Product [Tagged]
args = Elem
v
          forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) forall a b. (a -> b) -> a -> b
$ do
            [TransInfo]
sync_infos <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Set Tagged -> Sync -> M_Subs [TransInfo]
eval_sync' Set Tagged
done) t Sync
ss 
            let (Store
ss_ass,Bool
any_f) = [TransInfo] -> (Store, Bool)
syncTransInfos [TransInfo]
sync_infos
            Store
ass' <- [Store] -> Store
store_unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Effect -> M_Subs Store
eval_effect [Effect]
effects
            let ass :: Store
ass = Store
ass' Store -> Store -> Store
`store_union` Store
ss_ass
            forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> Store -> Bool -> Maybe Tagged -> [TransInfo] -> TransInfo
TransInfo Tagged
te Store
ass (Bool
any_f Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
is_enabled) Maybe Tagged
mActor [TransInfo]
sync_infos)
        actor :: Maybe Tagged
actor = case Elem
v of Product (Tagged
a:[Tagged]
objs) -> forall a. a -> Maybe a
Just Tagged
a
                          Elem
_                -> forall a. Maybe a
Nothing

eval_sync :: Sync -> M_Subs [TransInfo]
eval_sync :: Sync -> M_Subs [TransInfo]
eval_sync = Set Tagged -> Sync -> M_Subs [TransInfo]
eval_sync' forall a. Set a
S.empty

eval_sync' :: S.Set Tagged -> Sync -> M_Subs [TransInfo]
eval_sync' :: Set Tagged -> Sync -> M_Subs [TransInfo]
eval_sync' Set Tagged
done (Sync [Var]
xs Term
t) = forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) (Set Tagged -> Tagged -> M_Subs TransInfo
instantiate_trans' Set Tagged
done))

eval_effect :: Effect -> M_Subs Store
eval_effect :: Effect -> M_Subs Store
eval_effect (CAll [Var]
xs Term
t) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (,Assignment
HoldsTrue) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) forall (m :: * -> *) a. Monad m => a -> m a
return)
eval_effect (TAll [Var]
xs Term
t) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (,Assignment
HoldsFalse) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) forall (m :: * -> *) a. Monad m => a -> m a
return)
eval_effect (OAll [Var]
xs Term
t) = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (,Assignment
Unknown) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) forall (m :: * -> *) a. Monad m => a -> m a
return)

get_kind :: DomId -> M_Subs Kind
get_kind :: String -> M_Subs Kind
get_kind String
d = forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (forall a. a -> [a] -> [a]
:[]) (Spec -> String -> Maybe Kind
find_kind Spec
spec String
d) 
  where find_kind :: Spec -> DomId -> Maybe Kind 
        find_kind :: Spec -> String -> Maybe Kind
find_kind Spec
spec String
d = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Kind
kind (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d)

whenBool :: M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool :: forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool M_Subs Value
m Bool -> M_Subs a
f = M_Subs Value
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResBool Bool
b -> Bool -> M_Subs a
f Bool
b
                           Value
_         -> forall (f :: * -> *) a. Alternative f => f a
empty

checkTrue :: M_Subs Value -> M_Subs () 
checkTrue :: M_Subs Value -> M_Subs ()
checkTrue M_Subs Value
m = M_Subs Value
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResBool Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return () 
                          Value
_            -> forall (f :: * -> *) a. Alternative f => f a
empty

checkFalse :: M_Subs Value -> M_Subs () 
checkFalse :: M_Subs Value -> M_Subs ()
checkFalse M_Subs Value
m = M_Subs Value
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResBool Bool
False  -> forall (m :: * -> *) a. Monad m => a -> m a
return () 
                           Value
_              -> forall (f :: * -> *) a. Alternative f => f a
empty


whenInt :: M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt :: forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt M_Subs Value
m Int -> M_Subs a
f = M_Subs Value
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResInt Int
v -> Int -> M_Subs a
f Int
v
                          Value
_        -> forall (f :: * -> *) a. Alternative f => f a
empty

whenInts :: M_Subs Value -> ([Int] -> M_Subs a) -> M_Subs a
whenInts :: forall a. M_Subs Value -> ([Int] -> M_Subs a) -> M_Subs a
whenInts M_Subs Value
m [Int] -> M_Subs a
f = forall a. M_Subs a -> M_Subs [a]
results M_Subs Value
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Int] -> M_Subs a
f

whenTagged :: M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged :: forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged M_Subs Value
m Tagged -> M_Subs a
f = M_Subs Value
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResTagged Tagged
v  -> Tagged -> M_Subs a
f Tagged
v
                             Value
_            -> forall (f :: * -> *) a. Alternative f => f a
empty

whenTaggedHolds :: M_Subs Value -> (Tagged -> M_Subs b) -> M_Subs b
whenTaggedHolds M_Subs Value
m Tagged -> M_Subs b
f = M_Subs Value
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResTagged Tagged
v -> Tagged -> M_Subs Bool
is_in_virtual_state Tagged
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                                                   Bool
True  -> Tagged -> M_Subs b
f Tagged
v
                                                   Bool
False -> forall (f :: * -> *) a. Alternative f => f a
empty
                                  Value
_           -> forall (f :: * -> *) a. Alternative f => f a
empty

whenString :: M_Subs Value -> (String -> M_Subs a) -> M_Subs a
whenString :: forall a. M_Subs Value -> (String -> M_Subs a) -> M_Subs a
whenString M_Subs Value
m String -> M_Subs a
f = M_Subs Value
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResString String
s  -> String -> M_Subs a
f String
s
                             Value
_            -> forall (f :: * -> *) a. Alternative f => f a
empty

eval :: Term -> M_Subs Value
eval :: Term -> M_Subs Value
eval Term
t0 = case Term
t0 of
  Term
CurrentTime -> Int -> Value
ResInt forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> M_Subs Int
get_time
  StringLit String
s -> forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Value
ResString String
s)
  BoolLit Bool
b   -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool Bool
b)
  IntLit Int
i    -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt Int
i)
  Ref Var
x       -> Tagged -> Value
ResTagged forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> M_Subs Tagged
substitute_var Var
x
  App String
d Arguments
params-> do (Domain
dom,Term
dom_filter) <- String -> M_Subs (Domain, Term)
get_dom String
d
                    case Domain
dom of 
                      Products [Var]
xs -> do 
                        let replacements :: [(Var, Term)]
replacements = [Var] -> Arguments -> [(Var, Term)]
make_substitutions_of [Var]
xs Arguments
params
                        [(Var, Tagged)]
tes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Var
x,Term
t) -> forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var
x,))) [(Var, Term)]
replacements
                        [Tagged]
args <- forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Var, Tagged)]
tes) (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Var -> M_Subs Tagged
substitute_var [Var]
xs)
                        forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) forall a b. (a -> b) -> a -> b
$ do
                          M_Subs Value -> M_Subs ()
checkTrue (Term -> M_Subs Value
eval Term
dom_filter)
                          forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> Value
ResTagged ([Tagged] -> Elem
Product [Tagged]
args, String
d))
                      Domain
_           -> forall a. RuntimeError -> M_Subs a
err (InternalError -> RuntimeError
InternalError forall a b. (a -> b) -> a -> b
$ String -> InternalError
PrimitiveApplication String
d)
  Tag Term
t String
d     -> Term -> M_Subs Value
eval Term
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b c. (a -> b -> c) -> b -> a -> c
flip Value -> String -> M_Subs Value
tag String
d
  Untag Term
t     -> Term -> M_Subs Value
eval Term
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> M_Subs Value
untag
  Not Term
t       -> forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t) forall a b. (a -> b) -> a -> b
$ \Bool
b -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Bool -> Bool
not Bool
b))
  And Term
t1 Term
t2   -> forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \case 
                    Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool Bool
False)
                    Bool
True  -> forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t2) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Value
ResBool) 
  Or  Term
t1 Term
t2   -> forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \case 
                    Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool Bool
True)
                    Bool
False -> forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t2) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Value
ResBool)
--  And t1 t2   -> whenBool (eval t1) $ \b1 -> whenBool (eval t2) (\b2 -> return (ResBool (and [b1,b2])))
--  Or  t1 t2   -> whenBool (eval t1) $ \b1 -> whenBool (eval t2) (\b2 -> return (ResBool (or [b1,b2])))
  Leq  Term
t1 Term
t2  -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Int
v1 forall a. Ord a => a -> a -> Bool
<= Int
v2)))
  Le   Term
t1 Term
t2  -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Int
v1 forall a. Ord a => a -> a -> Bool
< Int
v2)))
  Geq  Term
t1 Term
t2  -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Int
v1 forall a. Ord a => a -> a -> Bool
>= Int
v2)))
  Ge   Term
t1 Term
t2  -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Int
v1 forall a. Ord a => a -> a -> Bool
> Int
v2)))
  Mult  Term
t1 Term
t2 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 forall a. Num a => a -> a -> a
* Int
v2)))
  Mod  Term
t1 Term
t2  -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 forall a. Integral a => a -> a -> a
`mod` Int
v2)))
  Div  Term
t1 Term
t2  -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 forall a. Integral a => a -> a -> a
`div` Int
v2)))
  Sub  Term
t1 Term
t2  -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 forall a. Num a => a -> a -> a
- Int
v2)))
  Add  Term
t1 Term
t2  -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt  (Term -> M_Subs Value
eval Term
t1) forall a b. (a -> b) -> a -> b
$ \Int
v1 -> forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 forall a. Num a => a -> a -> a
+ Int
v2)))
  Eq  Term
t1 Term
t2   -> ((Bool -> Value
ResBool forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => a -> a -> Bool
(==)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> M_Subs Value
eval Term
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> M_Subs Value
eval Term
t2
  Neq Term
t1 Term
t2   -> ((Bool -> Value
ResBool forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => a -> a -> Bool
(/=)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> M_Subs Value
eval Term
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> M_Subs Value
eval Term
t2

  Sum [Var]
xs Term
t1   -> Int -> Value
ResInt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) forall (m :: * -> *) a. Monad m => a -> m a
return)
  Count [Var]
xs Term
t1 -> Int -> Value
ResInt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (Term -> M_Subs Value
eval Term
t1)
  Max [Var]
xs Term
t1   -> Int -> Value
ResInt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\[Int]
xs -> if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
xs then Int
0 else forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) forall (m :: * -> *) a. Monad m => a -> m a
return)
  Min [Var]
xs Term
t1   -> Int -> Value
ResInt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\[Int]
xs -> if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
xs then Int
0 else forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Int]
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) forall (m :: * -> *) a. Monad m => a -> m a
return)
  When Term
t1 Term
t2  -> -- order matters because of constraint that equal variables have equal instantiations
                 -- however, with renaming some of these constraints can be lifted
                 -- this modification propagates in the same order as the evaluation order
                 Term -> M_Subs Value
eval Term
t1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value
v1 -> forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t2) (\case Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return Value
v1
                                                              Bool
False -> forall (f :: * -> *) a. Alternative f => f a
empty)
                 {- whenBool (eval t2) $ \case  True  -> eval t1 
                                              False -> empty-}
  Present Term
t1  -> forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t1) (\Tagged
v -> Bool -> Value
ResBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged -> M_Subs Bool
is_in_virtual_state Tagged
v)
  Violated Term
t1 -> forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t1) (\Tagged
v -> Bool -> Value
ResBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged -> M_Subs Bool
is_violated Tagged
v)
  Enabled Term
t1  -> forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t1) (\Tagged
v -> Bool -> Value
ResBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged -> M_Subs Bool
is_enabled Tagged
v)
  Exists [Var]
xs Term
t -> Bool -> Value
ResBool forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. M_Subs a -> M_Subs [a]
results (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Var -> M_Subs a -> M_Subs a
scope_var (M_Subs Value -> M_Subs ()
checkTrue (Term -> M_Subs Value
eval Term
t)) [Var]
xs) 
  Forall [Var]
xs Term
t -> Bool -> Value
ResBool forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. M_Subs a -> M_Subs [a]
results (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Var -> M_Subs a -> M_Subs a
scope_var (forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t) forall (m :: * -> *) a. Monad m => a -> m a
return) [Var]
xs)

  Project Term
t Var
x -> forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval (Term
t)) forall a b. (a -> b) -> a -> b
$ \te :: Tagged
te@(Elem
e,String
d) -> case Elem
e of 
                    Product [Tagged]
tes -> do (Domain
dom, Term
_) <- String -> M_Subs (Domain, Term)
get_dom String
d
                                      case Domain
dom of Products [Var]
rs | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tagged]
tes forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
rs -> 
                                                    case forall {a} {b}. (Num a, Enum a, Eq b) => b -> [b] -> Maybe a
elemIndex Var
x [Var]
rs of
                                                      Maybe Int
Nothing -> forall (f :: * -> *) a. Alternative f => f a
empty
                                                      Just Int
j  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> Value
ResTagged ([Tagged]
tes forall a. [a] -> Int -> a
!! Int
j))
                                                  Domain
_ -> forall (f :: * -> *) a. Alternative f => f a
empty
                    Elem
_ -> forall (f :: * -> *) a. Alternative f => f a
empty
    where elemIndex :: b -> [b] -> Maybe a
elemIndex b
x [b]
rs = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. a -> b -> Maybe a
op [a
0..] [b]
rs)
            where op :: a -> b -> Maybe a
op a
j b
y | b
x forall a. Eq a => a -> a -> Bool
== b
y    = forall a. a -> Maybe a
Just a
j
                         | Bool
otherwise = forall a. Maybe a
Nothing


foreach :: [Var] -> M_Subs a -> M_Subs [a]
foreach :: forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs M_Subs a
m = forall a. M_Subs a -> M_Subs [a]
results (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Var -> M_Subs a -> M_Subs a
scope_var M_Subs a
m [Var]
xs)

tag :: Value -> DomId -> M_Subs Value
tag :: Value -> String -> M_Subs Value
tag (ResInt Int
i) String
d        = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Tagged -> Value
ResTagged (Int -> Elem
Int Int
i,String
d)
tag (ResString String
s) String
d     = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Tagged -> Value
ResTagged (String -> Elem
String String
s, String
d)
tag (ResTagged (Elem
v,String
_)) String
d = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Tagged -> Value
ResTagged (Elem
v,String
d)
tag (ResBool Bool
b) String
_       = forall (f :: * -> *) a. Alternative f => f a
empty

untag :: Value -> M_Subs Value
untag :: Value -> M_Subs Value
untag (ResTagged (Int Int
i, String
d))      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Value
ResInt Int
i
untag (ResTagged (String String
s, String
d))   = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Value
ResString String
s
untag (ResTagged (Product [Tagged]
_, String
_))  = forall (f :: * -> *) a. Alternative f => f a
empty
untag (ResBool Bool
_)                 = forall (f :: * -> *) a. Alternative f => f a
empty
untag (ResInt Int
_)                  = forall (f :: * -> *) a. Alternative f => f a
empty
untag (ResString String
_)               = forall (f :: * -> *) a. Alternative f => f a
empty