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