{-# 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
data M_Subs a = M_Subs { M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs :: Spec -> State -> InputMap -> Subs -> Either RuntimeError [a] }
err :: RuntimeError -> M_Subs a
err :: RuntimeError -> M_Subs a
err RuntimeError
re = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> RuntimeError -> Either RuntimeError [a]
forall a b. a -> Either a b
Left RuntimeError
re
nd :: [a] -> M_Subs a
nd :: [a] -> M_Subs a
nd [a]
vals = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [a] -> Either RuntimeError [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
vals
results :: M_Subs a -> M_Subs [a]
results :: M_Subs a -> M_Subs [a]
results M_Subs a
n = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [[a]])
-> M_Subs [a]
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [[a]])
-> M_Subs [a])
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [[a]])
-> M_Subs [a]
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> ([a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[]) ([a] -> [[a]])
-> Either RuntimeError [a] -> Either RuntimeError [[a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
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 :: M_Subs a -> M_Subs a
ignoreMissingInput M_Subs a
m = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> case M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
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
_) -> [a] -> Either RuntimeError [a]
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 :: Var -> Tagged -> M_Subs a -> M_Subs a
bind Var
k Tagged
v M_Subs a
m = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm -> M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
m Spec
spec State
state InputMap
inpm (Subs -> Either RuntimeError [a])
-> (Subs -> Subs) -> Subs -> Either RuntimeError [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Tagged -> Subs -> Subs
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 :: 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
Var -> Tagged -> M_Subs a -> M_Subs a
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 :: DomId -> M_Subs TypeSpec
get_type_spec DomId
d = (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [TypeSpec])
-> M_Subs TypeSpec
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec
-> State -> InputMap -> Subs -> Either RuntimeError [TypeSpec])
-> M_Subs TypeSpec)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [TypeSpec])
-> M_Subs TypeSpec
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs ->
case Spec -> DomId -> Maybe TypeSpec
find_decl Spec
spec DomId
d of
Maybe TypeSpec
Nothing -> RuntimeError -> Either RuntimeError [TypeSpec]
forall a b. a -> Either a b
Left (InternalError -> RuntimeError
InternalError (DomId -> InternalError
UndeclaredType DomId
d))
Just TypeSpec
tspec -> [TypeSpec] -> Either RuntimeError [TypeSpec]
forall a b. b -> Either a b
Right [TypeSpec
tspec]
get_dom :: DomId -> M_Subs (Domain, Term)
get_dom :: DomId -> M_Subs (Domain, Term)
get_dom DomId
d = (Spec
-> State
-> InputMap
-> Subs
-> Either RuntimeError [(Domain, Term)])
-> M_Subs (Domain, Term)
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec
-> State
-> InputMap
-> Subs
-> Either RuntimeError [(Domain, Term)])
-> M_Subs (Domain, Term))
-> (Spec
-> State
-> InputMap
-> Subs
-> Either RuntimeError [(Domain, Term)])
-> M_Subs (Domain, Term)
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs ->
case Spec -> DomId -> Maybe TypeSpec
find_decl Spec
spec DomId
d of
Maybe TypeSpec
Nothing -> RuntimeError -> Either RuntimeError [(Domain, Term)]
forall a b. a -> Either a b
Left (InternalError -> RuntimeError
InternalError (DomId -> InternalError
UndeclaredType DomId
d))
Just TypeSpec
tspec -> [(Domain, Term)] -> Either RuntimeError [(Domain, Term)]
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 = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [Int])
-> M_Subs Int
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [Int])
-> M_Subs Int)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [Int])
-> M_Subs Int
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [Int] -> Either RuntimeError [Int]
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 = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [Subs])
-> M_Subs Subs
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [Subs])
-> M_Subs Subs)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Subs])
-> M_Subs Subs
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [Subs] -> Either RuntimeError [Subs]
forall (m :: * -> *) a. Monad m => a -> m a
return [Subs
subs]
modify_subs :: (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs :: (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs Subs -> Subs
mod M_Subs a
m = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm -> M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs a
m Spec
spec State
state InputMap
inpm (Subs -> Either RuntimeError [a])
-> (Subs -> Subs) -> Subs -> Either RuntimeError [a]
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 = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [Spec])
-> M_Subs Spec
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [Spec])
-> M_Subs Spec)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Spec])
-> M_Subs Spec
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [Spec] -> Either RuntimeError [Spec]
forall (m :: * -> *) a. Monad m => a -> m a
return [Spec
spec]
get_state :: M_Subs State
get_state :: M_Subs State
get_state = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [State])
-> M_Subs State
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [State])
-> M_Subs State)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [State])
-> M_Subs State
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [State] -> Either RuntimeError [State]
forall (m :: * -> *) a. Monad m => a -> m a
return [State
state]
get_input :: M_Subs InputMap
get_input :: M_Subs InputMap
get_input = (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [InputMap])
-> M_Subs InputMap
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec
-> State -> InputMap -> Subs -> Either RuntimeError [InputMap])
-> M_Subs InputMap)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [InputMap])
-> M_Subs InputMap
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [InputMap] -> Either RuntimeError [InputMap]
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 = (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Assignment])
-> M_Subs Assignment
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Assignment])
-> M_Subs Assignment)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Assignment])
-> M_Subs Assignment
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs ->
[Assignment] -> Either RuntimeError [Assignment]
forall a b. b -> Either a b
Right [Assignment -> (Bool -> Assignment) -> Maybe Bool -> Assignment
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Assignment
Unknown (Assignment -> Assignment -> Bool -> Assignment
forall a. a -> a -> Bool -> a
bool Assignment
HoldsFalse Assignment
HoldsTrue) (Tagged -> InputMap -> Maybe Bool
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
_,DomId
d) = (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Assignment])
-> M_Subs Assignment
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Assignment])
-> M_Subs Assignment)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Assignment])
-> M_Subs Assignment
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs ->
[Assignment] -> Either RuntimeError [Assignment]
forall a b. b -> Either a b
Right [Assignment -> (Info -> Assignment) -> Maybe Info -> Assignment
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Assignment
Unknown Info -> Assignment
op (Tagged -> Map Tagged Info -> Maybe Info
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Tagged
te (State -> Map Tagged Info
contents State
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 :: (a -> b) -> M_Subs a -> M_Subs b
fmap = (a -> b) -> M_Subs a -> M_Subs b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Applicative M_Subs where
pure :: a -> M_Subs a
pure = a -> M_Subs a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: M_Subs (a -> b) -> M_Subs a -> M_Subs 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 :: a -> M_Subs a
return a
a = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [a] -> Either RuntimeError [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a
a]
>>= :: M_Subs a -> (a -> M_Subs b) -> M_Subs b
(>>=) M_Subs a
m a -> M_Subs b
f = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [b])
-> M_Subs b
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [b])
-> M_Subs b)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [b])
-> M_Subs b
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> do
[a]
as <- M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
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 = ([b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++[b]
res) ([b] -> [b]) -> Either RuntimeError [b] -> Either RuntimeError [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> M_Subs b
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [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
([b] -> a -> Either RuntimeError [b])
-> [b] -> [a] -> Either RuntimeError [b]
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 :: M_Subs a
empty = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [a] -> Either RuntimeError [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
M_Subs a
m1 <|> :: M_Subs a -> M_Subs a -> M_Subs a
<|> M_Subs a
m2 = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a)
-> (Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> do
[a]
xs <- M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
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 <- M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
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
[a] -> Either RuntimeError [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys)
instance MonadPlus M_Subs where
instantiate_domain :: DomId -> Domain -> M_Subs Elem
instantiate_domain :: DomId -> Domain -> M_Subs Elem
instantiate_domain DomId
d Domain
dom = case Domain
dom of
Domain
Time -> M_Subs Int
get_time M_Subs Int -> (Int -> M_Subs Elem) -> M_Subs Elem
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
time -> [Elem] -> M_Subs Elem
forall a. [a] -> M_Subs a
nd [ Int -> Elem
Int Int
i | Int
i <- [Int
0..Int
time]]
Domain
AnyString -> RuntimeError -> M_Subs Elem
forall a. RuntimeError -> M_Subs a
err (InternalError -> RuntimeError
InternalError (InternalError -> RuntimeError) -> InternalError -> RuntimeError
forall a b. (a -> b) -> a -> b
$ DomId -> Domain -> InternalError
EnumerateInfiniteDomain DomId
d Domain
dom)
Domain
AnyInt -> RuntimeError -> M_Subs Elem
forall a. RuntimeError -> M_Subs a
err (InternalError -> RuntimeError
InternalError (InternalError -> RuntimeError) -> InternalError -> RuntimeError
forall a b. (a -> b) -> a -> b
$ DomId -> Domain -> InternalError
EnumerateInfiniteDomain DomId
d Domain
dom)
Strings [DomId]
ss -> [Elem] -> M_Subs Elem
forall a. [a] -> M_Subs a
nd [ DomId -> Elem
String DomId
s | DomId
s <- [DomId]
ss ]
Ints [Int]
is -> [Elem] -> M_Subs Elem
forall a. [a] -> M_Subs a
nd [ Int -> Elem
Int Int
i | Int
i <- [Int]
is ]
Products [Var]
xs -> [Tagged] -> Elem
Product ([Tagged] -> Elem) -> M_Subs [Tagged] -> M_Subs Elem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [M_Subs Tagged] -> M_Subs [Tagged]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Var -> M_Subs Tagged) -> [Var] -> [M_Subs Tagged]
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 Var -> Subs -> Maybe Tagged
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Subs
subs of
Just te :: Tagged
te@(Elem
v,DomId
d') -> Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return (Elem
v, Spec -> Var -> DomId
remove_decoration Spec
spec Var
x)
Maybe Tagged
Nothing -> RuntimeError -> M_Subs Tagged
forall a. RuntimeError -> M_Subs a
err (InternalError -> RuntimeError
InternalError (InternalError -> RuntimeError) -> InternalError -> RuntimeError
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 :: DomId
d = Spec -> Var -> DomId
remove_decoration Spec
spec Var
x
(Domain
dom, Term
_) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
if Spec -> Domain -> Bool
enumerable Spec
spec Domain
dom then DomId -> M_Subs Tagged
generate_instances DomId
d
else Spec -> DomId -> M_Subs Tagged
forall p. p -> DomId -> M_Subs Tagged
every_available_subs Spec
spec DomId
d
where generate_instances :: DomId -> M_Subs Tagged
generate_instances DomId
d = do
(Domain
dom, Term
dom_filter) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
Elem
e <- DomId -> Domain -> M_Subs Elem
instantiate_domain DomId
d Domain
dom
let bindings :: Subs
bindings = case (Domain
dom,Elem
e) of (Products [Var]
xs, Product [Tagged]
args) -> [(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
(Domain, Elem)
_ -> Var -> Tagged -> Subs
forall k a. k -> a -> Map k a
M.singleton (DomId -> Var
no_decoration DomId
d) (Elem
e,DomId
d)
(Subs -> Subs) -> M_Subs () -> M_Subs ()
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))
Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return (Elem
e,DomId
d)
every_available_subs :: p -> DomId -> M_Subs Tagged
every_available_subs p
spec DomId
d = do
State
state <- M_Subs State
get_state
InputMap
inpm <- M_Subs InputMap
get_input
[Tagged] -> M_Subs Tagged
forall a. [a] -> M_Subs a
nd [ Tagged
te | te :: Tagged
te@(Elem
v,DomId
d') <- State -> InputMap -> [Tagged]
state_input_holds State
state InputMap
inpm, DomId
d' DomId -> DomId -> Bool
forall a. Eq a => a -> a -> Bool
== DomId
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
_,DomId
d) = do
Spec
spec <- M_Subs Spec
get_spec
Tagged -> M_Subs Bool
is_valid_instance Tagged
te M_Subs Bool -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
False -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Bool
True -> do
Tagged -> M_Subs Assignment
get_input_assignment Tagged
te M_Subs Assignment -> (Assignment -> M_Subs Bool) -> M_Subs Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Assignment
HoldsTrue -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Assignment
HoldsFalse -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Assignment
Unknown -> do
Tagged -> M_Subs Assignment
get_assignment Tagged
te M_Subs Assignment -> (Assignment -> M_Subs Bool) -> M_Subs Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Assignment
HoldsTrue -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Assignment
HoldsFalse -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Assignment
Unknown -> do
Tagged -> M_Subs Bool
is_derivable Tagged
te M_Subs Bool -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Bool
False -> case Maybe Bool -> Bool
forall a. HasCallStack => Maybe a -> a
fromJust (Spec -> DomId -> Maybe Bool
closed_type Spec
spec DomId
d) of
Bool
True -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Bool
False -> RuntimeError -> M_Subs Bool
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,DomId
d) = do
Spec
spec <- M_Subs Spec
get_spec
Tagged -> M_Subs Bool
is_in_virtual_state Tagged
v M_Subs Bool -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
False -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Bool
True -> Tagged -> M_Subs Bool
sat_conditions Tagged
v M_Subs Bool -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
False -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Bool
True -> case (TypeSpec -> Kind) -> Maybe TypeSpec -> Maybe Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Kind
kind (Spec -> DomId -> Maybe TypeSpec
find_decl Spec
spec DomId
d) of
Just (Act ActSpec
aspec) -> do
(Domain
dom, Term
_) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
let (Product [Tagged]
args, Products [Var]
xs) = (Elem
e, Domain
dom)
(Subs -> Subs) -> M_Subs Bool -> M_Subs Bool
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` ([(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) (M_Subs Bool -> M_Subs Bool) -> M_Subs Bool -> M_Subs Bool
forall a b. (a -> b) -> a -> b
$ do
[TransInfo]
sync_infos <- [[TransInfo]] -> [TransInfo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[TransInfo]] -> [TransInfo])
-> M_Subs [[TransInfo]] -> M_Subs [TransInfo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Sync -> M_Subs [TransInfo]) -> [Sync] -> M_Subs [[TransInfo]]
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)
Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ((TransInfo -> Bool) -> [TransInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (TransInfo -> Bool) -> TransInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransInfo -> Bool
trans_forced) [TransInfo]
sync_infos)
Maybe Kind
_ -> Bool -> M_Subs Bool
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,DomId
d) = do
(Domain
dom, Term
dom_filter) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
let bindings :: Subs
bindings = case (Domain
dom,Elem
e) of (Products [Var]
xs, Product [Tagged]
args) -> [(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
(Domain, Elem)
_ -> Var -> Tagged -> Subs
forall k a. k -> a -> Map k a
M.singleton (DomId -> Var
no_decoration DomId
d) Tagged
te
let check_constraint :: M_Subs Bool
check_constraint = (Subs -> Subs) -> M_Subs Bool -> M_Subs Bool
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) (M_Subs Value -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
dom_filter) Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return)
case (Elem
e, Domain
dom) of
(Int Int
i, Ints [Int]
is) | Int
i Int -> [Int] -> Bool
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 DomId
s, Strings [DomId]
ss) | DomId
s DomId -> [DomId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DomId]
ss -> M_Subs Bool
check_constraint
(String DomId
s, Domain
AnyString) -> M_Subs Bool
check_constraint
(Product [Tagged]
args, Products [Var]
params) | [Tagged] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tagged]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
params ->
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> M_Subs [Bool] -> M_Subs Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Tagged -> M_Subs Bool) -> [Tagged] -> M_Subs [Bool]
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 M_Subs Bool -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
False -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Bool
True -> M_Subs Bool
check_constraint
(Elem, Domain)
_ -> Bool -> M_Subs Bool
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,DomId
d) = Tagged -> M_Subs Bool -> M_Subs Bool
derivation_closure_on Tagged
te (M_Subs Bool -> M_Subs Bool) -> M_Subs Bool -> M_Subs Bool
forall a b. (a -> b) -> a -> b
$ do
Spec
spec <- M_Subs Spec
get_spec
(Domain
dom, Term
_) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
let bindings :: Subs
bindings = case (Domain
dom,Elem
e) of (Products [Var]
xs, Product [Tagged]
args) -> [(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
(Domain, Elem)
_ -> Var -> Tagged -> Subs
forall k a. k -> a -> Map k a
M.singleton (DomId -> Var
no_decoration DomId
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 <- (Subs -> Subs) -> M_Subs [Tagged] -> M_Subs [Tagged]
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings)
([Var] -> M_Subs Tagged -> M_Subs [Tagged]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach ([Var]
xs [Var] -> [Var] -> [Var]
forall a. Eq a => [a] -> [a] -> [a]
\\ Subs -> [Var]
forall k a. Map k a -> [k]
M.keys Subs
bindings) (M_Subs Value -> (Tagged -> M_Subs Tagged) -> M_Subs Tagged
forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
dvt) Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return))
Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged
te Tagged -> [Tagged] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Tagged]
tes)
HoldsWhen Term
t -> (Subs -> Subs) -> M_Subs Bool -> M_Subs Bool
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) (M_Subs Value -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t) Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return )
case (TypeSpec -> [Derivation]) -> Maybe TypeSpec -> Maybe [Derivation]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> [Derivation]
derivation (Spec -> DomId -> Maybe TypeSpec
find_decl Spec
spec DomId
d) of
Maybe [Derivation]
Nothing -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just [Derivation]
dvs -> ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> M_Subs [Bool] -> M_Subs Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Derivation -> M_Subs Bool) -> [Derivation] -> M_Subs [Bool]
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) M_Subs Bool -> (Bool -> M_Subs Bool) -> M_Subs Bool
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 -> Bool -> M_Subs Bool
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 = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [Bool])
-> M_Subs Bool
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [Bool])
-> M_Subs Bool)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Bool])
-> M_Subs Bool
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> case Tagged -> Map Tagged Info -> Maybe Info
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Tagged
te (State -> Map Tagged Info
contents State
state) of
Just Info
info -> [Bool] -> Either RuntimeError [Bool]
forall (m :: * -> *) a. Monad m => a -> m a
return [Info -> Bool
value Info
info]
Maybe Info
Nothing -> M_Subs Bool
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [Bool]
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 = Tagged -> Info -> Map Tagged Info -> Map Tagged Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Tagged
te (Info :: Bool -> Bool -> Info
Info { value :: Bool
value = Bool
False, from_sat :: Bool
from_sat = Bool
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,DomId
d) =
Tagged -> M_Subs Bool
is_valid_instance Tagged
te M_Subs Bool -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
False -> Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Bool
True -> do
TypeSpec
tspec <- DomId -> M_Subs TypeSpec
get_type_spec DomId
d
(Domain
dom, Term
_) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
let bindings :: Subs
bindings = case (Domain
dom,Elem
v) of (Products [Var]
xs, Product [Tagged]
args) -> [(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)
(Domain, Elem)
_ -> Var -> Tagged -> Subs
forall k a. k -> a -> Map k a
M.singleton (DomId -> Var
no_decoration DomId
d) Tagged
te
(Subs -> Subs) -> M_Subs Bool -> M_Subs Bool
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` Subs
bindings) ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> M_Subs [Bool] -> M_Subs Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> M_Subs Bool) -> [Term] -> M_Subs [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((M_Subs Value -> (Bool -> M_Subs Bool) -> M_Subs Bool)
-> (Bool -> M_Subs Bool) -> M_Subs Value -> M_Subs Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip M_Subs Value -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (M_Subs Value -> M_Subs Bool)
-> (Term -> M_Subs Value) -> Term -> M_Subs Bool
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
_,DomId
d) = Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool) -> M_Subs Bool -> M_Subs (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged -> M_Subs Bool
is_in_virtual_state Tagged
te M_Subs (Bool -> Bool) -> M_Subs Bool -> M_Subs Bool
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 -> DomId -> Maybe [Term]
find_violation_cond Spec
spec DomId
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,DomId
d) Maybe [Term]
mconds = do
(Domain
dom, Term
_) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
let Products [Var]
xs = Domain
dom
Product [Tagged]
args = Elem
v
(Subs -> Subs) -> M_Subs Bool -> M_Subs Bool
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` ([(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args)))
(M_Subs Value -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval (Term -> ([Term] -> Term) -> Maybe [Term] -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> Term
BoolLit Bool
False) ((Term -> Term -> Term) -> Term -> [Term] -> Term
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)) Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return)
syncTransInfos :: [TransInfo] -> (Store, Bool )
syncTransInfos :: [TransInfo] -> (Store, Bool)
syncTransInfos = (TransInfo -> (Store, Bool) -> (Store, Bool))
-> (Store, Bool) -> [TransInfo] -> (Store, Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TransInfo -> (Store, Bool) -> (Store, Bool)
op (Store
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 te :: Tagged
te@(Elem
v,DomId
d) = do
TypeSpec
tspec <- DomId -> M_Subs TypeSpec
get_type_spec DomId
d
Bool
is_enabled <- Tagged -> M_Subs Bool
is_enabled Tagged
te
case TypeSpec -> Kind
kind TypeSpec
tspec of
Fact FactSpec
_ -> M_Subs TransInfo
forall (f :: * -> *) a. Alternative f => f a
empty
Duty DutySpec
_ -> M_Subs TransInfo
forall (f :: * -> *) a. Alternative f => f a
empty
Act ActSpec
aspec -> Tagged
-> Maybe Tagged -> Bool -> [Effect] -> [Sync] -> M_Subs TransInfo
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 -> Tagged
-> Maybe Tagged -> Bool -> [Effect] -> [Sync] -> M_Subs TransInfo
forall (t :: * -> *).
Traversable t =>
Tagged
-> Maybe Tagged -> Bool -> [Effect] -> t Sync -> M_Subs TransInfo
do_transition Tagged
te Maybe Tagged
actor Bool
is_enabled (EventSpec -> [Effect]
event_effects EventSpec
espec) []
where do_transition :: Tagged
-> Maybe Tagged -> Bool -> [Effect] -> t Sync -> M_Subs TransInfo
do_transition te :: Tagged
te@(Elem
v,DomId
d) Maybe Tagged
isAction Bool
is_enabled [Effect]
effects t Sync
ss = do
(Domain
dom, Term
_) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
let Products [Var]
xs = Domain
dom
let Product [Tagged]
args = Elem
v
(Subs -> Subs) -> M_Subs TransInfo -> M_Subs TransInfo
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` ([(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) (M_Subs TransInfo -> M_Subs TransInfo)
-> M_Subs TransInfo -> M_Subs TransInfo
forall a b. (a -> b) -> a -> b
$ do
[TransInfo]
sync_infos <- t [TransInfo] -> [TransInfo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (t [TransInfo] -> [TransInfo])
-> M_Subs (t [TransInfo]) -> M_Subs [TransInfo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Sync -> M_Subs [TransInfo]) -> t Sync -> M_Subs (t [TransInfo])
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Sync -> M_Subs [TransInfo]
eval_sync t Sync
ss
let (Store
ss_ass,Bool
any_f) = [TransInfo] -> (Store, Bool)
syncTransInfos [TransInfo]
sync_infos
Store
ass' <- [Store] -> Store
store_unions ([Store] -> Store) -> M_Subs [Store] -> M_Subs Store
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Effect -> M_Subs Store) -> [Effect] -> M_Subs [Store]
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
TransInfo -> M_Subs TransInfo
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
isAction [TransInfo]
sync_infos)
actor :: Maybe Tagged
actor = case Elem
v of Product (Tagged
a:[Tagged]
objs) -> Tagged -> Maybe Tagged
forall a. a -> Maybe a
Just Tagged
a
Elem
_ -> Maybe Tagged
forall a. Maybe a
Nothing
eval_sync :: Sync -> M_Subs [TransInfo]
eval_sync :: Sync -> M_Subs [TransInfo]
eval_sync (Sync [Var]
xs Term
t) = [Var] -> M_Subs TransInfo -> M_Subs [TransInfo]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (M_Subs Value -> (Tagged -> M_Subs TransInfo) -> M_Subs TransInfo
forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) Tagged -> M_Subs TransInfo
instantiate_trans)
eval_effect :: Effect -> M_Subs Store
eval_effect :: Effect -> M_Subs Store
eval_effect (CAll [Var]
xs Term
t) = [(Tagged, Assignment)] -> Store
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Tagged, Assignment)] -> Store)
-> ([Tagged] -> [(Tagged, Assignment)]) -> [Tagged] -> Store
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged -> (Tagged, Assignment))
-> [Tagged] -> [(Tagged, Assignment)]
forall a b. (a -> b) -> [a] -> [b]
map (,Assignment
HoldsTrue) ([Tagged] -> Store) -> M_Subs [Tagged] -> M_Subs Store
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var] -> M_Subs Tagged -> M_Subs [Tagged]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (M_Subs Value -> (Tagged -> M_Subs Tagged) -> M_Subs Tagged
forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return)
eval_effect (TAll [Var]
xs Term
t) = [(Tagged, Assignment)] -> Store
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Tagged, Assignment)] -> Store)
-> ([Tagged] -> [(Tagged, Assignment)]) -> [Tagged] -> Store
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged -> (Tagged, Assignment))
-> [Tagged] -> [(Tagged, Assignment)]
forall a b. (a -> b) -> [a] -> [b]
map (,Assignment
HoldsFalse) ([Tagged] -> Store) -> M_Subs [Tagged] -> M_Subs Store
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var] -> M_Subs Tagged -> M_Subs [Tagged]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (M_Subs Value -> (Tagged -> M_Subs Tagged) -> M_Subs Tagged
forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return)
eval_effect (OAll [Var]
xs Term
t) = [(Tagged, Assignment)] -> Store
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Tagged, Assignment)] -> Store)
-> ([Tagged] -> [(Tagged, Assignment)]) -> [Tagged] -> Store
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged -> (Tagged, Assignment))
-> [Tagged] -> [(Tagged, Assignment)]
forall a b. (a -> b) -> [a] -> [b]
map (,Assignment
Unknown) ([Tagged] -> Store) -> M_Subs [Tagged] -> M_Subs Store
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var] -> M_Subs Tagged -> M_Subs [Tagged]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (M_Subs Value -> (Tagged -> M_Subs Tagged) -> M_Subs Tagged
forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) Tagged -> M_Subs Tagged
forall (m :: * -> *) a. Monad m => a -> m a
return)
get_kind :: DomId -> M_Subs Kind
get_kind :: DomId -> M_Subs Kind
get_kind DomId
d = (Spec -> State -> InputMap -> Subs -> Either RuntimeError [Kind])
-> M_Subs Kind
forall a.
(Spec -> State -> InputMap -> Subs -> Either RuntimeError [a])
-> M_Subs a
M_Subs ((Spec -> State -> InputMap -> Subs -> Either RuntimeError [Kind])
-> M_Subs Kind)
-> (Spec
-> State -> InputMap -> Subs -> Either RuntimeError [Kind])
-> M_Subs Kind
forall a b. (a -> b) -> a -> b
$ \Spec
spec State
state InputMap
inpm Subs
subs -> [Kind] -> Either RuntimeError [Kind]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Kind] -> Either RuntimeError [Kind])
-> [Kind] -> Either RuntimeError [Kind]
forall a b. (a -> b) -> a -> b
$ [Kind] -> (Kind -> [Kind]) -> Maybe Kind -> [Kind]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
:[]) (Spec -> DomId -> Maybe Kind
find_kind Spec
spec DomId
d)
where find_kind :: Spec -> DomId -> Maybe Kind
find_kind :: Spec -> DomId -> Maybe Kind
find_kind Spec
spec DomId
d = (TypeSpec -> Kind) -> Maybe TypeSpec -> Maybe Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Kind
kind (Spec -> DomId -> Maybe TypeSpec
find_decl Spec
spec DomId
d)
whenBool :: M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool :: M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool M_Subs Value
m Bool -> M_Subs a
f = M_Subs Value
m M_Subs Value -> (Value -> M_Subs a) -> M_Subs a
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
_ -> M_Subs a
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 M_Subs Value -> (Value -> M_Subs ()) -> M_Subs ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResBool Bool
True -> () -> M_Subs ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Value
_ -> M_Subs ()
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 M_Subs Value -> (Value -> M_Subs ()) -> M_Subs ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResBool Bool
False -> () -> M_Subs ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Value
_ -> M_Subs ()
forall (f :: * -> *) a. Alternative f => f a
empty
whenInt :: M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt :: M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt M_Subs Value
m Int -> M_Subs a
f = M_Subs Value
m M_Subs Value -> (Value -> M_Subs a) -> M_Subs a
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
_ -> M_Subs a
forall (f :: * -> *) a. Alternative f => f a
empty
whenInts :: M_Subs Value -> ([Int] -> M_Subs a) -> M_Subs a
whenInts :: M_Subs Value -> ([Int] -> M_Subs a) -> M_Subs a
whenInts M_Subs Value
m [Int] -> M_Subs a
f = M_Subs Value -> M_Subs [Value]
forall a. M_Subs a -> M_Subs [a]
results M_Subs Value
m M_Subs [Value] -> ([Value] -> M_Subs [Int]) -> M_Subs [Int]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [M_Subs Int] -> M_Subs [Int]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([M_Subs Int] -> M_Subs [Int])
-> ([Value] -> [M_Subs Int]) -> [Value] -> M_Subs [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> M_Subs Int) -> [Value] -> [M_Subs Int]
forall a b. (a -> b) -> [a] -> [b]
map ((M_Subs Value -> (Int -> M_Subs Int) -> M_Subs Int)
-> (Int -> M_Subs Int) -> M_Subs Value -> M_Subs Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip M_Subs Value -> (Int -> M_Subs Int) -> M_Subs Int
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt Int -> M_Subs Int
forall (m :: * -> *) a. Monad m => a -> m a
return (M_Subs Value -> M_Subs Int)
-> (Value -> M_Subs Value) -> Value -> M_Subs Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return) M_Subs [Int] -> ([Int] -> M_Subs a) -> M_Subs a
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 :: M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged M_Subs Value
m Tagged -> M_Subs a
f = M_Subs Value
m M_Subs Value -> (Value -> M_Subs a) -> M_Subs a
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
_ -> M_Subs a
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 M_Subs Value -> (Value -> M_Subs b) -> M_Subs b
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 M_Subs Bool -> (Bool -> M_Subs b) -> M_Subs b
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 -> M_Subs b
forall (f :: * -> *) a. Alternative f => f a
empty
Value
_ -> M_Subs b
forall (f :: * -> *) a. Alternative f => f a
empty
whenString :: M_Subs Value -> (String -> M_Subs a) -> M_Subs a
whenString :: M_Subs Value -> (DomId -> M_Subs a) -> M_Subs a
whenString M_Subs Value
m DomId -> M_Subs a
f = M_Subs Value
m M_Subs Value -> (Value -> M_Subs a) -> M_Subs a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case ResString DomId
s -> DomId -> M_Subs a
f DomId
s
Value
_ -> M_Subs a
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 (Int -> Value) -> M_Subs Int -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> M_Subs Int
get_time
StringLit DomId
s -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (DomId -> Value
ResString DomId
s)
BoolLit Bool
b -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool Bool
b)
IntLit Int
i -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt Int
i)
Ref Var
x -> Tagged -> Value
ResTagged (Tagged -> Value) -> M_Subs Tagged -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> M_Subs Tagged
substitute_var Var
x
App DomId
d Arguments
params-> do (Domain
dom,Term
dom_filter) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
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 <- ((Var, Term) -> M_Subs (Var, Tagged))
-> [(Var, Term)] -> M_Subs [(Var, Tagged)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Var
x,Term
t) -> M_Subs Value
-> (Tagged -> M_Subs (Var, Tagged)) -> M_Subs (Var, Tagged)
forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) ((Var, Tagged) -> M_Subs (Var, Tagged)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Var, Tagged) -> M_Subs (Var, Tagged))
-> (Tagged -> (Var, Tagged)) -> Tagged -> M_Subs (Var, Tagged)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var
x,))) [(Var, Term)]
replacements
[Tagged]
args <- (Subs -> Subs) -> M_Subs [Tagged] -> M_Subs [Tagged]
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` [(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Var, Tagged)]
tes) ((Var -> M_Subs Tagged) -> [Var] -> M_Subs [Tagged]
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)
(Subs -> Subs) -> M_Subs Value -> M_Subs Value
forall a. (Subs -> Subs) -> M_Subs a -> M_Subs a
modify_subs (Subs -> Subs -> Subs
`subsUnion` ([(Var, Tagged)] -> Subs
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Tagged] -> [(Var, Tagged)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Tagged]
args))) (M_Subs Value -> M_Subs Value) -> M_Subs Value -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ do
M_Subs Value -> M_Subs ()
checkTrue (Term -> M_Subs Value
eval Term
dom_filter)
Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> Value
ResTagged ([Tagged] -> Elem
Product [Tagged]
args, DomId
d))
Domain
_ -> RuntimeError -> M_Subs Value
forall a. RuntimeError -> M_Subs a
err (InternalError -> RuntimeError
InternalError (InternalError -> RuntimeError) -> InternalError -> RuntimeError
forall a b. (a -> b) -> a -> b
$ DomId -> InternalError
PrimitiveApplication DomId
d)
Tag Term
t DomId
d -> Term -> M_Subs Value
eval Term
t M_Subs Value -> (Value -> M_Subs Value) -> M_Subs Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Value -> DomId -> M_Subs Value) -> DomId -> Value -> M_Subs Value
forall a b c. (a -> b -> c) -> b -> a -> c
flip Value -> DomId -> M_Subs Value
tag DomId
d
Untag Term
t -> Term -> M_Subs Value
eval Term
t M_Subs Value -> (Value -> M_Subs Value) -> M_Subs Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> M_Subs Value
untag
Not Term
t -> M_Subs Value -> (Bool -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t) ((Bool -> M_Subs Value) -> M_Subs Value)
-> (Bool -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Bool
b -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Bool -> Bool
not Bool
b))
And Term
t1 Term
t2 -> M_Subs Value -> (Bool -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t1) ((Bool -> M_Subs Value) -> M_Subs Value)
-> (Bool -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \case
Bool
False -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool Bool
False)
Bool
True -> M_Subs Value -> (Bool -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t2) (Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> M_Subs Value) -> (Bool -> Value) -> Bool -> M_Subs Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Value
ResBool)
Or Term
t1 Term
t2 -> M_Subs Value -> (Bool -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t1) ((Bool -> M_Subs Value) -> M_Subs Value)
-> (Bool -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \case
Bool
True -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool Bool
True)
Bool
False -> M_Subs Value -> (Bool -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t2) (Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> M_Subs Value) -> (Bool -> Value) -> Bool -> M_Subs Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Value
ResBool)
Leq Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
v2)))
Le Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
v2)))
Geq Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
v2)))
Ge Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
ResBool (Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
v2)))
Mult Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
v2)))
Mod Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
v2)))
Div Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
v2)))
Sub Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
v2)))
Add Term
t1 Term
t2 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) ((Int -> M_Subs Value) -> M_Subs Value)
-> (Int -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \Int
v1 -> M_Subs Value -> (Int -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t2) (\Int
v2 -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Value
ResInt (Int
v1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
v2)))
Eq Term
t1 Term
t2 -> ((Bool -> Value
ResBool (Bool -> Value) -> (Value -> Bool) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Value -> Bool) -> Value -> Value)
-> (Value -> Value -> Bool) -> Value -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
(==)) (Value -> Value -> Value)
-> M_Subs Value -> M_Subs (Value -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> M_Subs Value
eval Term
t1 M_Subs (Value -> Value) -> M_Subs Value -> M_Subs Value
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 (Bool -> Value) -> (Value -> Bool) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Value -> Bool) -> Value -> Value)
-> (Value -> Value -> Bool) -> Value -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) (Value -> Value -> Value)
-> M_Subs Value -> M_Subs (Value -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> M_Subs Value
eval Term
t1 M_Subs (Value -> Value) -> M_Subs Value -> M_Subs Value
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 (Int -> Value) -> ([Int] -> Int) -> [Int] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Value) -> M_Subs [Int] -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var] -> M_Subs Int -> M_Subs [Int]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (M_Subs Value -> (Int -> M_Subs Int) -> M_Subs Int
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) Int -> M_Subs Int
forall (m :: * -> *) a. Monad m => a -> m a
return)
Count [Var]
xs Term
t1 -> Int -> Value
ResInt (Int -> Value) -> ([Value] -> Int) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Value] -> Value) -> M_Subs [Value] -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var] -> M_Subs Value -> M_Subs [Value]
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 (Int -> Value) -> ([Int] -> Int) -> [Int] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\[Int]
xs -> if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
xs then Int
0 else [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
xs) ([Int] -> Value) -> M_Subs [Int] -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var] -> M_Subs Int -> M_Subs [Int]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (M_Subs Value -> (Int -> M_Subs Int) -> M_Subs Int
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) Int -> M_Subs Int
forall (m :: * -> *) a. Monad m => a -> m a
return)
Min [Var]
xs Term
t1 -> Int -> Value
ResInt (Int -> Value) -> ([Int] -> Int) -> [Int] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\[Int]
xs -> if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
xs then Int
0 else [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Int]
xs) ([Int] -> Value) -> M_Subs [Int] -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var] -> M_Subs Int -> M_Subs [Int]
forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (M_Subs Value -> (Int -> M_Subs Int) -> M_Subs Int
forall a. M_Subs Value -> (Int -> M_Subs a) -> M_Subs a
whenInt (Term -> M_Subs Value
eval Term
t1) Int -> M_Subs Int
forall (m :: * -> *) a. Monad m => a -> m a
return)
When Term
t1 Term
t2 ->
Term -> M_Subs Value
eval Term
t1 M_Subs Value -> (Value -> M_Subs Value) -> M_Subs Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Value
v1 -> M_Subs Value -> (Bool -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t2) (\case Bool
True -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v1
Bool
False -> M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty)
Present Term
t1 -> M_Subs Value -> (Tagged -> M_Subs Value) -> M_Subs Value
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 (Bool -> Value) -> M_Subs Bool -> M_Subs Value
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 -> M_Subs Value -> (Tagged -> M_Subs Value) -> M_Subs Value
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 (Bool -> Value) -> M_Subs Bool -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged -> M_Subs Bool
is_violated Tagged
v)
Enabled Term
t1 -> M_Subs Value -> (Tagged -> M_Subs Value) -> M_Subs Value
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 (Bool -> Value) -> M_Subs Bool -> M_Subs Value
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 (Bool -> Value) -> ([()] -> Bool) -> [()] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([()] -> Value) -> M_Subs [()] -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> M_Subs () -> M_Subs [()]
forall a. M_Subs a -> M_Subs [a]
results ((Var -> M_Subs () -> M_Subs ()) -> M_Subs () -> [Var] -> M_Subs ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> M_Subs () -> M_Subs ()
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 (Bool -> Value) -> ([Bool] -> Bool) -> [Bool] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Value) -> M_Subs [Bool] -> M_Subs Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> M_Subs Bool -> M_Subs [Bool]
forall a. M_Subs a -> M_Subs [a]
results ((Var -> M_Subs Bool -> M_Subs Bool)
-> M_Subs Bool -> [Var] -> M_Subs Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> M_Subs Bool -> M_Subs Bool
forall a. Var -> M_Subs a -> M_Subs a
scope_var (M_Subs Value -> (Bool -> M_Subs Bool) -> M_Subs Bool
forall a. M_Subs Value -> (Bool -> M_Subs a) -> M_Subs a
whenBool (Term -> M_Subs Value
eval Term
t) Bool -> M_Subs Bool
forall (m :: * -> *) a. Monad m => a -> m a
return) [Var]
xs)
Project Term
t Var
x -> M_Subs Value -> (Tagged -> M_Subs Value) -> M_Subs Value
forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval (Term
t)) ((Tagged -> M_Subs Value) -> M_Subs Value)
-> (Tagged -> M_Subs Value) -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ \te :: Tagged
te@(Elem
e,DomId
d) -> case Elem
e of
Product [Tagged]
tes -> do (Domain
dom, Term
_) <- DomId -> M_Subs (Domain, Term)
get_dom DomId
d
case Domain
dom of Products [Var]
rs | [Tagged] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tagged]
tes Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
rs ->
case Var -> [Var] -> Maybe Int
forall a a. (Num a, Enum a, Eq a) => a -> [a] -> Maybe a
elemIndex Var
x [Var]
rs of
Maybe Int
Nothing -> M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty
Just Int
j -> Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> Value
ResTagged ([Tagged]
tes [Tagged] -> Int -> Tagged
forall a. [a] -> Int -> a
!! Int
j))
Domain
_ -> M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty
Elem
_ -> M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty
where elemIndex :: a -> [a] -> Maybe a
elemIndex a
x [a]
rs = [Maybe a] -> Maybe a
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ((a -> a -> Maybe a) -> [a] -> [a] -> [Maybe a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> Maybe a
forall a. a -> a -> Maybe a
op [a
0..] [a]
rs)
where op :: a -> a -> Maybe a
op a
j a
y | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = a -> Maybe a
forall a. a -> Maybe a
Just a
j
| Bool
otherwise = Maybe a
forall a. Maybe a
Nothing
foreach :: [Var] -> M_Subs a -> M_Subs [a]
foreach :: [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs M_Subs a
m = M_Subs a -> M_Subs [a]
forall a. M_Subs a -> M_Subs [a]
results ((Var -> M_Subs a -> M_Subs a) -> M_Subs a -> [Var] -> M_Subs a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> M_Subs a -> M_Subs a
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 -> DomId -> M_Subs Value
tag (ResInt Int
i) DomId
d = Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> M_Subs Value) -> Value -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ Tagged -> Value
ResTagged (Int -> Elem
Int Int
i,DomId
d)
tag (ResString DomId
s) DomId
d = Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> M_Subs Value) -> Value -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ Tagged -> Value
ResTagged (DomId -> Elem
String DomId
s, DomId
d)
tag (ResTagged (Elem
v,DomId
_)) DomId
d = Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> M_Subs Value) -> Value -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ Tagged -> Value
ResTagged (Elem
v,DomId
d)
tag (ResBool Bool
b) DomId
_ = M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty
untag :: Value -> M_Subs Value
untag :: Value -> M_Subs Value
untag (ResTagged (Int Int
i, DomId
d)) = Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> M_Subs Value) -> Value -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ Int -> Value
ResInt Int
i
untag (ResTagged (String DomId
s, DomId
d)) = Value -> M_Subs Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> M_Subs Value) -> Value -> M_Subs Value
forall a b. (a -> b) -> a -> b
$ DomId -> Value
ResString DomId
s
untag (ResTagged (Product [Tagged]
_, DomId
_)) = M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty
untag (ResBool Bool
_) = M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty
untag (ResInt Int
_) = M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty
untag (ResString DomId
_) = M_Subs Value
forall (f :: * -> *) a. Alternative f => f a
empty