{-# LANGUAGE RecordWildCards, LambdaCase, TupleSections #-}
module Language.EFLINT.StaticEval where
import Language.EFLINT.Spec
import Language.EFLINT.Binders
import Control.Monad
import Control.Applicative
import Data.Maybe (isNothing)
import Data.List ((\\))
import qualified Data.Map as M
import qualified Data.Set as S
data M_Stc a = M_Stc {M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic :: Spec -> Either [String] (Spec, a)}
instance Monad M_Stc where
return :: a -> M_Stc a
return a
a = (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, a)) -> M_Stc a)
-> (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a b. (a -> b) -> a -> b
$ \Spec
spec -> (Spec, a) -> Either [String] (Spec, a)
forall a b. b -> Either a b
Right (Spec
spec, a
a)
M_Stc a
m >>= :: M_Stc a -> (a -> M_Stc b) -> M_Stc b
>>= a -> M_Stc b
f = (Spec -> Either [String] (Spec, b)) -> M_Stc b
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, b)) -> M_Stc b)
-> (Spec -> Either [String] (Spec, b)) -> M_Stc b
forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case M_Stc a -> Spec -> Either [String] (Spec, a)
forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
m Spec
spec of
Right (Spec
spec',a
a) -> M_Stc b -> Spec -> Either [String] (Spec, b)
forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic (a -> M_Stc b
f a
a) Spec
spec'
Left [String]
err -> [String] -> Either [String] (Spec, b)
forall a b. a -> Either a b
Left [String]
err
instance Applicative M_Stc where
pure :: a -> M_Stc a
pure = a -> M_Stc a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: M_Stc (a -> b) -> M_Stc a -> M_Stc b
(<*>) = M_Stc (a -> b) -> M_Stc a -> M_Stc b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Functor M_Stc where
fmap :: (a -> b) -> M_Stc a -> M_Stc b
fmap = (a -> b) -> M_Stc a -> M_Stc b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Alternative M_Stc where
empty :: M_Stc a
empty = (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc (Either [String] (Spec, a) -> Spec -> Either [String] (Spec, a)
forall a b. a -> b -> a
const ([String] -> Either [String] (Spec, a)
forall a b. a -> Either a b
Left []))
M_Stc a
p <|> :: M_Stc a -> M_Stc a -> M_Stc a
<|> M_Stc a
q = (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, a)) -> M_Stc a)
-> (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case M_Stc a -> Spec -> Either [String] (Spec, a)
forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
p Spec
spec of
Left [String]
ers1 -> case M_Stc a -> Spec -> Either [String] (Spec, a)
forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
q Spec
spec of
Left [String]
ers2 -> [String] -> Either [String] (Spec, a)
forall a b. a -> Either a b
Left ([String]
ers1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ers2)
Right (Spec, a)
x -> (Spec, a) -> Either [String] (Spec, a)
forall a b. b -> Either a b
Right (Spec, a)
x
Right (Spec, a)
x -> (Spec, a) -> Either [String] (Spec, a)
forall a b. b -> Either a b
Right (Spec, a)
x
err :: String -> M_Stc a
err :: String -> M_Stc a
err String
str = (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, a)) -> M_Stc a)
-> (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a b. (a -> b) -> a -> b
$ \Spec
spec -> [String] -> Either [String] (Spec, a)
forall a b. a -> Either a b
Left [String
str]
get_dom :: DomId -> M_Stc Domain
get_dom :: String -> M_Stc Domain
get_dom String
d = (Spec -> Either [String] (Spec, Domain)) -> M_Stc Domain
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, Domain)) -> M_Stc Domain)
-> (Spec -> Either [String] (Spec, Domain)) -> M_Stc Domain
forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d of
Just TypeSpec
tspec -> (Spec, Domain) -> Either [String] (Spec, Domain)
forall a b. b -> Either a b
Right (Spec
spec, TypeSpec -> Domain
domain TypeSpec
tspec)
Maybe TypeSpec
_ -> [String] -> Either [String] (Spec, Domain)
forall a b. a -> Either a b
Left [String
"undeclared type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d]
get_spec :: M_Stc Spec
get_spec :: M_Stc Spec
get_spec = (Spec -> Either [String] (Spec, Spec)) -> M_Stc Spec
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, Spec)) -> M_Stc Spec)
-> (Spec -> Either [String] (Spec, Spec)) -> M_Stc Spec
forall a b. (a -> b) -> a -> b
$ \Spec
spec -> (Spec, Spec) -> Either [String] (Spec, Spec)
forall a b. b -> Either a b
Right (Spec
spec, Spec
spec)
execute_decl :: Decl -> M_Stc ()
execute_decl :: Decl -> M_Stc ()
execute_decl Decl
decl = (Spec -> Either [String] (Spec, ())) -> M_Stc ()
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, ())) -> M_Stc ())
-> (Spec -> Either [String] (Spec, ())) -> M_Stc ()
forall a b. (a -> b) -> a -> b
$ \Spec
spec ->
let spec' :: Spec
spec' = case Decl
decl of
PlaceholderDecl String
f String
t -> Spec
spec { aliases :: Map String String
aliases = String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
f String
t (Spec -> Map String String
aliases Spec
spec) }
TypeExt String
ty [ModClause]
clauses -> Spec
spec { decls :: Map String TypeSpec
decls = (TypeSpec -> TypeSpec)
-> String -> Map String TypeSpec -> Map String TypeSpec
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust (String -> [ModClause] -> TypeSpec -> TypeSpec
apply_type_ext String
ty [ModClause]
clauses) String
ty (Spec -> Map String TypeSpec
decls Spec
spec) }
TypeDecl String
ty TypeSpec
tspec -> Spec
spec { decls :: Map String TypeSpec
decls = String -> TypeSpec -> Map String TypeSpec -> Map String TypeSpec
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
ty TypeSpec
tspec (Spec -> Map String TypeSpec
decls Spec
spec) }
in (Spec, ()) -> Either [String] (Spec, ())
forall a b. b -> Either a b
Right (Spec
spec', ())
with_spec :: Spec -> M_Stc a -> M_Stc a
with_spec :: Spec -> M_Stc a -> M_Stc a
with_spec Spec
spec' M_Stc a
m = (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, a)) -> M_Stc a)
-> (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case M_Stc a -> Spec -> Either [String] (Spec, a)
forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
m Spec
spec' of
Left [String]
err -> [String] -> Either [String] (Spec, a)
forall a b. a -> Either a b
Left [String]
err
Right (Spec
_,a
a) -> (Spec, a) -> Either [String] (Spec, a)
forall a b. b -> Either a b
Right (Spec
spec, a
a)
with_decl :: DomId -> TypeSpec -> M_Stc a -> M_Stc a
with_decl :: String -> TypeSpec -> M_Stc a -> M_Stc a
with_decl String
ty TypeSpec
tspec M_Stc a
m = (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc ((Spec -> Either [String] (Spec, a)) -> M_Stc a)
-> (Spec -> Either [String] (Spec, a)) -> M_Stc a
forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case M_Stc a -> Spec -> Either [String] (Spec, a)
forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
m (Spec
spec{decls :: Map String TypeSpec
decls=String -> TypeSpec -> Map String TypeSpec -> Map String TypeSpec
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
ty TypeSpec
tspec (Spec -> Map String TypeSpec
decls Spec
spec)}) of
Left [String]
err -> [String] -> Either [String] (Spec, a)
forall a b. a -> Either a b
Left [String]
err
Right (Spec
_,a
a) -> (Spec, a) -> Either [String] (Spec, a)
forall a b. b -> Either a b
Right (Spec
spec, a
a)
free_vars :: Term -> M_Stc (S.Set Var)
free_vars :: Term -> M_Stc (Set Var)
free_vars Term
t = do Spec
spec <- M_Stc Spec
get_spec
let xs :: Set Var
xs = Spec -> Term -> Set Var
forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t
[Var] -> M_Stc ()
check_known_type (Set Var -> [Var]
forall a. Set a -> [a]
S.toList Set Var
xs)
Set Var -> M_Stc (Set Var)
forall (m :: * -> *) a. Monad m => a -> m a
return Set Var
xs
compile_all :: Spec -> Refiner -> Initialiser -> Scenario -> Either [String] (Spec, Refiner, Initialiser, Scenario)
compile_all :: Spec
-> Refiner
-> Initialiser
-> Scenario
-> Either [String] (Spec, Refiner, Initialiser, Scenario)
compile_all Spec
f Refiner
r Initialiser
i Scenario
s = case M_Stc (Spec, Initialiser, Scenario)
-> Spec -> Either [String] (Spec, (Spec, Initialiser, Scenario))
forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc (Spec, Initialiser, Scenario)
compile Spec
f of
Left [String]
errs -> [String] -> Either [String] (Spec, Refiner, Initialiser, Scenario)
forall a b. a -> Either a b
Left [String]
errs
Right (Spec
_,(Spec
spec, Initialiser
init, Scenario
scen)) -> (Spec, Refiner, Initialiser, Scenario)
-> Either [String] (Spec, Refiner, Initialiser, Scenario)
forall a b. b -> Either a b
Right (Spec
spec, Refiner
r, Initialiser
init, Scenario
scen)
where compile :: M_Stc (Spec, Initialiser, Scenario)
compile = do
Spec
f' <- M_Stc Spec
compile_spec
Spec
-> M_Stc (Spec, Initialiser, Scenario)
-> M_Stc (Spec, Initialiser, Scenario)
forall a. Spec -> M_Stc a -> M_Stc a
with_spec Spec
f' (M_Stc (Spec, Initialiser, Scenario)
-> M_Stc (Spec, Initialiser, Scenario))
-> M_Stc (Spec, Initialiser, Scenario)
-> M_Stc (Spec, Initialiser, Scenario)
forall a b. (a -> b) -> a -> b
$ do
Initialiser
i' <- Initialiser -> M_Stc Initialiser
compile_initialiser Initialiser
i
Scenario
s' <- Scenario -> M_Stc Scenario
compile_stmts Scenario
s
(Spec, Initialiser, Scenario)
-> M_Stc (Spec, Initialiser, Scenario)
forall (m :: * -> *) a. Monad m => a -> m a
return (Spec
f',Initialiser
i',Scenario
s')
compile_initialiser :: Initialiser -> M_Stc Initialiser
compile_initialiser :: Initialiser -> M_Stc Initialiser
compile_initialiser = (Effect -> M_Stc Effect) -> Initialiser -> M_Stc Initialiser
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> Effect -> M_Stc Effect
compile_effect [])
compile_stmts :: [Statement] -> M_Stc [Statement]
compile_stmts :: Scenario -> M_Stc Scenario
compile_stmts = (Statement -> M_Stc Statement) -> Scenario -> M_Stc Scenario
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Statement -> M_Stc Statement
compile_stmt
compile_stmt :: Statement -> M_Stc Statement
compile_stmt :: Statement -> M_Stc Statement
compile_stmt (Query Term
t0) = do
Spec
spec <- M_Stc Spec
get_spec
Set Var
fs <- Term -> M_Stc (Set Var)
free_vars Term
t0
let unbounds :: [Var]
unbounds = Set Var -> [Var]
forall a. Set a -> [a]
S.toList Set Var
fs
let t1 :: Term
t1 | [Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
unbounds = Term
t0
| Not Term
inner <- Term
t0 = Term -> Term
Not ([Var] -> Term -> Term
Exists [Var]
unbounds Term
inner)
| Bool
otherwise = [Var] -> Term -> Term
Exists [Var]
unbounds Term
t0
case (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe TypeSpec -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe TypeSpec -> Bool) -> (Var -> Maybe TypeSpec) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> String -> Maybe TypeSpec
find_decl Spec
spec (String -> Maybe TypeSpec)
-> (Var -> String) -> Var -> Maybe TypeSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> Var -> String
remove_decoration Spec
spec) [Var]
unbounds of
[] -> Term -> Statement
Query (Term -> Statement) -> M_Stc Term -> M_Stc Statement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyBool
(Var
t:[Var]
_) -> String -> M_Stc Statement
forall a. String -> M_Stc a
err (String
"undeclared type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Spec -> Var -> String
remove_decoration Spec
spec Var
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in query")
compile_stmt (Trans [Var]
xs TransType
aty (Right (String
d,Arguments
mods))) = [Var] -> TransType -> Term -> Maybe String -> M_Stc Statement
compile_trans_term [Var]
xs TransType
aty (String -> Arguments -> Term
App String
d Arguments
mods) (String -> Maybe String
forall a. a -> Maybe a
Just String
d)
compile_stmt (Trans [Var]
xs TransType
aty (Left Term
t)) = [Var] -> TransType -> Term -> Maybe String -> M_Stc Statement
compile_trans_term [Var]
xs TransType
aty Term
t Maybe String
forall a. Maybe a
Nothing
compile_trans_term :: [Var] -> TransType -> Term -> Maybe String -> M_Stc Statement
compile_trans_term [Var]
xs TransType
aty Term
term Maybe String
md = do
Set Var
fs <- Term -> M_Stc (Set Var)
free_vars Term
term
let unbounds :: [Var]
unbounds = Set Var -> [Var]
forall a. Set a -> [a]
S.toList (Set Var
fs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs)
[Var] -> TransType -> Either Term (String, Arguments) -> Statement
Trans ([Var]
xs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
unbounds) TransType
aty (Either Term (String, Arguments) -> Statement)
-> (Term -> Either Term (String, Arguments)) -> Term -> Statement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Either Term (String, Arguments)
forall a b. a -> Either a b
Left (Term -> Statement) -> M_Stc Term -> M_Stc Statement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> M_Stc Term
converter Term
term
where converter :: Term -> M_Stc Term
converter Term
term = case Maybe String
md of Just d -> Term -> Type -> M_Stc Term
convert_term Term
term (String -> Type
TyTagged String
d)
Maybe String
_ -> (Term, Type) -> Term
forall a b. (a, b) -> a
fst ((Term, Type) -> Term) -> M_Stc (Term, Type) -> M_Stc Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> M_Stc (Term, Type)
compile_term Term
term
compile_phrase :: Phrase -> M_Stc CPhrase
compile_phrase :: Phrase -> M_Stc CPhrase
compile_phrase Phrase
p = case Phrase
p of
Phrase
PSkip -> CPhrase -> M_Stc CPhrase
forall (m :: * -> *) a. Monad m => a -> m a
return CPhrase
CPSkip
PDo Tagged
tv -> CPhrase -> M_Stc CPhrase
forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> CPhrase
CDo Tagged
tv)
PTrigger [Var]
vs Term
t -> (Statement -> CPhrase) -> M_Stc Statement -> M_Stc CPhrase
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Phrase -> Statement -> CPhrase
de_stmt Phrase
p) (Statement -> M_Stc Statement
compile_stmt (Phrase -> Statement
to_stmt Phrase
p))
Create [Var]
vs Term
t -> (Statement -> CPhrase) -> M_Stc Statement -> M_Stc CPhrase
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Phrase -> Statement -> CPhrase
de_stmt Phrase
p) (Statement -> M_Stc Statement
compile_stmt (Phrase -> Statement
to_stmt Phrase
p))
Terminate [Var]
vs Term
t -> (Statement -> CPhrase) -> M_Stc Statement -> M_Stc CPhrase
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Phrase -> Statement -> CPhrase
de_stmt Phrase
p) (Statement -> M_Stc Statement
compile_stmt (Phrase -> Statement
to_stmt Phrase
p))
Obfuscate [Var]
vs Term
t -> (Statement -> CPhrase) -> M_Stc Statement -> M_Stc CPhrase
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Phrase -> Statement -> CPhrase
de_stmt Phrase
p) (Statement -> M_Stc Statement
compile_stmt (Phrase -> Statement
to_stmt Phrase
p))
PQuery Term
t -> (Statement -> CPhrase) -> M_Stc Statement -> M_Stc CPhrase
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Phrase -> Statement -> CPhrase
de_stmt Phrase
p) (Statement -> M_Stc Statement
compile_stmt (Phrase -> Statement
to_stmt Phrase
p))
PDeclBlock [Decl]
ds -> do
[Decl] -> (Decl -> M_Stc ()) -> M_Stc ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((Decl -> Bool) -> [Decl] -> [Decl]
forall a. (a -> Bool) -> [a] -> [a]
filter Decl -> Bool
introducesName [Decl]
ds) Decl -> M_Stc ()
execute_decl
[Decl] -> (Decl -> M_Stc ()) -> M_Stc ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Decl]
ds ((Decl -> M_Stc ()
execute_decl (Decl -> M_Stc ()) -> M_Stc Decl -> M_Stc ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (M_Stc Decl -> M_Stc ())
-> (Decl -> M_Stc Decl) -> Decl -> M_Stc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decl -> M_Stc Decl
compile_decl)
CPhrase -> M_Stc CPhrase
forall (m :: * -> *) a. Monad m => a -> m a
return CPhrase
CPOnlyDecls
where to_stmt :: Phrase -> Statement
to_stmt (PTrigger [Var]
vs Term
t) = [Var] -> TransType -> Either Term (String, Arguments) -> Statement
Trans [Var]
vs TransType
Trigger (Term -> Either Term (String, Arguments)
forall a b. a -> Either a b
Left Term
t)
to_stmt (Create [Var]
vs Term
t) = [Var] -> TransType -> Either Term (String, Arguments) -> Statement
Trans [Var]
vs TransType
AddEvent (Term -> Either Term (String, Arguments)
forall a b. a -> Either a b
Left Term
t)
to_stmt (Terminate [Var]
vs Term
t) = [Var] -> TransType -> Either Term (String, Arguments) -> Statement
Trans [Var]
vs TransType
RemEvent (Term -> Either Term (String, Arguments)
forall a b. a -> Either a b
Left Term
t)
to_stmt (Obfuscate [Var]
vs Term
t) = [Var] -> TransType -> Either Term (String, Arguments) -> Statement
Trans [Var]
vs TransType
ObfEvent (Term -> Either Term (String, Arguments)
forall a b. a -> Either a b
Left Term
t)
to_stmt (PQuery Term
t) = Term -> Statement
Query Term
t
to_stmt Phrase
_ = String -> Statement
forall a. HasCallStack => String -> a
error String
"Explorer.assert 1"
de_stmt :: Phrase -> Statement -> CPhrase
de_stmt (PTrigger [Var]
vs Term
t) (Trans [Var]
vs' TransType
Trigger (Left Term
t')) = [Var] -> Term -> CPhrase
CTrigger [Var]
vs' Term
t'
de_stmt (Create [Var]
vs Term
t) (Trans [Var]
vs' TransType
AddEvent (Left Term
t')) = [Var] -> Term -> CPhrase
CCreate [Var]
vs' Term
t'
de_stmt (Terminate [Var]
vs Term
t) (Trans [Var]
vs' TransType
RemEvent (Left Term
t')) = [Var] -> Term -> CPhrase
CTerminate [Var]
vs' Term
t'
de_stmt (Obfuscate [Var]
vs Term
t) (Trans [Var]
vs' TransType
ObfEvent (Left Term
t')) = [Var] -> Term -> CPhrase
CObfuscate [Var]
vs' Term
t'
de_stmt (PQuery Term
t) (Query Term
t') = Term -> CPhrase
CQuery Term
t'
de_stmt Phrase
_ Statement
_ = String -> CPhrase
forall a. HasCallStack => String -> a
error String
"Explorer.assert 2"
compile_decl :: Decl -> M_Stc Decl
compile_decl :: Decl -> M_Stc Decl
compile_decl d :: Decl
d@(PlaceholderDecl String
x String
y) = [Var] -> M_Stc ()
check_known_type [String -> Var
no_decoration String
y] M_Stc () -> M_Stc Decl -> M_Stc Decl
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Decl -> M_Stc Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
d
compile_decl d :: Decl
d@(TypeExt String
ty [ModClause]
clauses) = String -> [ModClause] -> M_Stc Decl
compile_ext String
ty [ModClause]
clauses
compile_decl d :: Decl
d@(TypeDecl String
ty TypeSpec
tspec) = String -> TypeSpec -> M_Stc Decl
compile_type_spec String
ty TypeSpec
tspec
compile_ext :: DomId -> [ModClause] -> M_Stc Decl
compile_ext :: String -> [ModClause] -> M_Stc Decl
compile_ext String
ty [ModClause]
clauses = do
Spec
spec <- M_Stc Spec
get_spec
case String -> Map String TypeSpec -> Maybe TypeSpec
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
ty (Spec -> Map String TypeSpec
decls Spec
spec) of
Maybe TypeSpec
Nothing -> String -> M_Stc Decl
forall a. String -> M_Stc a
err (String
"cannot find the type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to extend or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" of the wrong kind")
Just TypeSpec
tspec -> String -> [ModClause] -> Decl
TypeExt String
ty ([ModClause] -> Decl) -> M_Stc [ModClause] -> M_Stc Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModClause -> M_Stc ModClause) -> [ModClause] -> M_Stc [ModClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> TypeSpec -> ModClause -> M_Stc ModClause
compile_clause String
ty TypeSpec
tspec) [ModClause]
clauses
where compile_clause :: String -> TypeSpec -> ModClause -> M_Stc ModClause
compile_clause String
ty TypeSpec
tspec ModClause
clause = case ModClause
clause of
ConditionedByCl [Term]
conds -> [Term] -> ModClause
ConditionedByCl ([Term] -> ModClause) -> M_Stc [Term] -> M_Stc ModClause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> M_Stc Term) -> [Term] -> M_Stc [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> TypeSpec -> Term -> M_Stc Term
convert_precon String
ty TypeSpec
tspec) [Term]
conds
DerivationCl [Derivation]
dvs -> [Derivation] -> ModClause
DerivationCl ([Derivation] -> ModClause)
-> M_Stc [Derivation] -> M_Stc ModClause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Derivation -> M_Stc Derivation)
-> [Derivation] -> M_Stc [Derivation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> String -> Derivation -> M_Stc Derivation
compile_derivation [Var]
xs String
ty) [Derivation]
dvs
PostCondCl Initialiser
effs -> Initialiser -> ModClause
PostCondCl (Initialiser -> ModClause) -> M_Stc Initialiser -> M_Stc ModClause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Effect -> M_Stc Effect) -> Initialiser -> M_Stc Initialiser
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> Effect -> M_Stc Effect
compile_effect [Var]
xs) Initialiser
effs
SyncCl [Sync]
ss -> [Sync] -> ModClause
SyncCl ([Sync] -> ModClause) -> M_Stc [Sync] -> M_Stc ModClause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Sync -> M_Stc Sync) -> [Sync] -> M_Stc [Sync]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> Sync -> M_Stc Sync
compile_sync [Var]
xs) [Sync]
ss
ViolationCl [Term]
vts -> [Term] -> ModClause
ViolationCl ([Term] -> ModClause) -> M_Stc [Term] -> M_Stc ModClause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> M_Stc Term) -> [Term] -> M_Stc [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Term -> M_Stc Term
compile_violation_condition String
ty) [Term]
vts
EnforcingActsCl [String]
ds -> ModClause -> M_Stc ModClause
forall (m :: * -> *) a. Monad m => a -> m a
return (ModClause -> M_Stc ModClause) -> ModClause -> M_Stc ModClause
forall a b. (a -> b) -> a -> b
$ [String] -> ModClause
EnforcingActsCl [String]
ds
where xs :: [Var]
xs = case TypeSpec -> Domain
domain TypeSpec
tspec of Products [Var]
xs -> [Var]
xs
Domain
_ -> [String -> Var
no_decoration String
ty]
compile_type_spec :: DomId -> TypeSpec -> M_Stc Decl
compile_type_spec :: String -> TypeSpec -> M_Stc Decl
compile_type_spec String
ty TypeSpec
tspec = do
String -> TypeSpec -> M_Stc Decl -> M_Stc Decl
forall a. String -> TypeSpec -> M_Stc a -> M_Stc a
with_decl String
ty TypeSpec
tspec (M_Stc Decl -> M_Stc Decl) -> M_Stc Decl -> M_Stc Decl
forall a b. (a -> b) -> a -> b
$ do
Domain
dom <- String -> M_Stc Domain
get_dom String
ty
String -> Domain -> M_Stc ()
check_domain String
ty Domain
dom
let xs :: [Var]
xs = case Domain
dom of
Products [Var]
xs -> [Var]
xs
Domain
_ -> [String -> Var
no_decoration String
ty]
[Derivation]
derivation <- (Derivation -> M_Stc Derivation)
-> [Derivation] -> M_Stc [Derivation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> String -> Derivation -> M_Stc Derivation
compile_derivation [Var]
xs String
ty) (TypeSpec -> [Derivation]
derivation TypeSpec
tspec)
Kind
kind <- String -> TypeSpec -> Kind -> M_Stc Kind
compile_kind String
ty TypeSpec
tspec (TypeSpec -> Kind
kind TypeSpec
tspec)
[Term]
conditions <- (Term -> M_Stc Term) -> [Term] -> M_Stc [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> TypeSpec -> Term -> M_Stc Term
convert_precon String
ty TypeSpec
tspec) (TypeSpec -> [Term]
conditions TypeSpec
tspec)
Term
dom_filter <- Term -> Type -> M_Stc Term
convert_term (TypeSpec -> Term
domain_constraint TypeSpec
tspec) Type
TyBool
Set Var
ffs <- Term -> M_Stc (Set Var)
free_vars Term
dom_filter
let domain_constraint :: Term
domain_constraint = case Set Var -> [Var]
forall a. Set a -> [a]
S.toList (Set Var
ffs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs) of
[] -> Term
dom_filter
[Var]
vars -> [Var] -> Term -> Term
Exists [Var]
vars Term
dom_filter
Decl -> M_Stc Decl
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TypeSpec -> Decl
TypeDecl String
ty (TypeSpec :: Kind
-> Domain -> Term -> [Derivation] -> Bool -> [Term] -> TypeSpec
TypeSpec {domain :: Domain
domain = TypeSpec -> Domain
domain TypeSpec
tspec, closed :: Bool
closed = TypeSpec -> Bool
closed TypeSpec
tspec,[Term]
[Derivation]
Term
Kind
domain_constraint :: Term
domain_constraint :: Term
conditions :: [Term]
conditions :: [Term]
kind :: Kind
kind :: Kind
derivation :: [Derivation]
derivation :: [Derivation]
..}))
check_domain :: DomId -> Domain -> M_Stc ()
check_domain :: String -> Domain -> M_Stc ()
check_domain String
dty (Products [Var]
xs) = [Var] -> M_Stc ()
check_known_type [Var]
xs
check_domain String
_ Domain
_ = () -> M_Stc ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check_known_type :: [Var] -> M_Stc ()
check_known_type :: [Var] -> M_Stc ()
check_known_type [Var]
xs = do
Spec
spec <- M_Stc Spec
get_spec
let op :: Var -> M_Stc ()
op var :: Var
var@(Var String
base String
dec) = case Spec -> String -> Maybe TypeSpec
find_decl Spec
spec (Spec -> Var -> String
remove_decoration Spec
spec Var
var) of
Maybe TypeSpec
Nothing -> String -> M_Stc ()
forall a. String -> M_Stc a
err (String
"Undeclared type or placeholder `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
base String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
dec String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"`")
Just TypeSpec
_ -> () -> M_Stc ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(Var -> M_Stc ()) -> [Var] -> M_Stc ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Var -> M_Stc ()
op [Var]
xs
convert_precon :: DomId -> TypeSpec -> Term -> M_Stc Term
convert_precon :: String -> TypeSpec -> Term -> M_Stc Term
convert_precon String
ty TypeSpec
tspec Term
t = do
let xs :: [Var]
xs = case TypeSpec -> Domain
domain TypeSpec
tspec of Products [Var]
xs -> [Var]
xs
Domain
_ -> [String -> Var
no_decoration String
ty]
Term
cond' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
TyBool
Set Var
cond_fs <- Term -> M_Stc (Set Var)
free_vars Term
cond'
let unbounds :: [Var]
unbounds = Set Var -> [Var]
forall a. Set a -> [a]
S.toList (Set Var
cond_fs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs)
Term -> M_Stc Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> M_Stc Term) -> Term -> M_Stc Term
forall a b. (a -> b) -> a -> b
$ if [Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
unbounds then Term
cond' else [Var] -> Term -> Term
Exists [Var]
unbounds Term
cond'
compile_kind :: DomId -> TypeSpec -> Kind -> M_Stc Kind
compile_kind :: String -> TypeSpec -> Kind -> M_Stc Kind
compile_kind String
ty TypeSpec
tspec Kind
k = case Kind
k of
Act ActSpec
aspec -> do
let Products [Var]
xs = TypeSpec -> Domain
domain TypeSpec
tspec
Initialiser
effects' <- [M_Stc Effect] -> M_Stc Initialiser
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Effect -> M_Stc Effect) -> Initialiser -> [M_Stc Effect]
forall a b. (a -> b) -> [a] -> [b]
map ([Var] -> Effect -> M_Stc Effect
compile_effect [Var]
xs) (ActSpec -> Initialiser
effects ActSpec
aspec))
[Sync]
syncs' <- (Sync -> M_Stc Sync) -> [Sync] -> M_Stc [Sync]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> Sync -> M_Stc Sync
compile_sync [Var]
xs) (ActSpec -> [Sync]
syncs ActSpec
aspec)
Kind -> M_Stc Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (ActSpec -> Kind
Act (ActSpec
aspec { effects :: Initialiser
effects = Initialiser
effects', syncs :: [Sync]
syncs = [Sync]
syncs' } ))
Event EventSpec
espec -> do
let Products [Var]
xs = TypeSpec -> Domain
domain TypeSpec
tspec
Initialiser
effects' <- [M_Stc Effect] -> M_Stc Initialiser
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Effect -> M_Stc Effect) -> Initialiser -> [M_Stc Effect]
forall a b. (a -> b) -> [a] -> [b]
map ([Var] -> Effect -> M_Stc Effect
compile_effect [Var]
xs) (EventSpec -> Initialiser
event_effects EventSpec
espec))
Kind -> M_Stc Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (EventSpec -> Kind
Event (EventSpec
espec { event_effects :: Initialiser
event_effects = Initialiser
effects' } ))
Duty DutySpec
dspec -> do
[Term]
e_conds <- [[Term]] -> [Term]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Term]] -> [Term]) -> M_Stc [[Term]] -> M_Stc [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> M_Stc [Term]) -> [String] -> M_Stc [[Term]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> M_Stc [Term]
select_condition (DutySpec -> [String]
enforcing_acts DutySpec
dspec)
[Term]
vconds <- (Term -> M_Stc Term) -> [Term] -> M_Stc [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Term -> M_Stc Term
compile_violation_condition String
ty) ([Term]
e_conds [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ DutySpec -> [Term]
violated_when DutySpec
dspec)
Kind -> M_Stc Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> M_Stc Kind) -> Kind -> M_Stc Kind
forall a b. (a -> b) -> a -> b
$ (DutySpec -> Kind
Duty (DutySpec
dspec { violated_when :: [Term]
violated_when = [Term]
vconds }))
where select_condition :: String -> M_Stc [Term]
select_condition String
a = do
Spec
spec <- M_Stc Spec
get_spec
case String -> Map String TypeSpec -> Maybe TypeSpec
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
a (Spec -> Map String TypeSpec
decls Spec
spec) of
Just TypeSpec
tspec | Act ActSpec
_ <- TypeSpec -> Kind
kind TypeSpec
tspec -> [Term] -> M_Stc [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Term -> Term -> Term
And (Bool -> Term
BoolLit Bool
True) (TypeSpec -> [Term]
conditions TypeSpec
tspec)]
Maybe TypeSpec
_ -> String -> M_Stc [Term]
forall a. String -> M_Stc a
err (String
"duty " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is declared with enforcing act " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" which is not a declared or not declared as an act")
Fact FactSpec
_ -> Kind -> M_Stc Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
compile_violation_condition :: DomId -> Term -> M_Stc Term
compile_violation_condition :: String -> Term -> M_Stc Term
compile_violation_condition String
dty Term
term = do
Domain
domain <- String -> M_Stc Domain
get_dom String
dty
let Products [Var]
xs = Domain
domain
Term
term' <- Term -> Type -> M_Stc Term
convert_term Term
term Type
TyBool
Set Var
fs <- Term -> M_Stc (Set Var)
free_vars Term
term'
let unbounds :: [Var]
unbounds = Set Var -> [Var]
forall a. Set a -> [a]
S.toList (Set Var
fs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` ([Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs))
term'' :: Term
term'' | [Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
unbounds = Term
term'
| Bool
otherwise = [Var] -> Term -> Term
Exists [Var]
unbounds Term
term'
Term -> M_Stc Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
term''
compile_sync :: [Var] -> Sync -> M_Stc Sync
compile_sync :: [Var] -> Sync -> M_Stc Sync
compile_sync [Var]
bound (Sync [Var]
vars Term
t) = do
(Term
t', Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
case Type
tau of
TyTagged String
_ -> do Set Var
frees <- Term -> M_Stc (Set Var)
free_vars Term
t'
let unbounds :: [Var]
unbounds = Set Var -> [Var]
forall a. Set a -> [a]
S.toList (Set Var
frees Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList ([Var]
vars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
bound))
Sync -> M_Stc Sync
forall (m :: * -> *) a. Monad m => a -> m a
return (Sync -> M_Stc Sync) -> Sync -> M_Stc Sync
forall a b. (a -> b) -> a -> b
$ [Var] -> Term -> Sync
Sync ([Var]
vars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
unbounds) Term
t'
Type
_ -> String -> M_Stc Sync
forall a. String -> M_Stc a
err (String
"sync clause is not an instance expression")
compile_spec :: M_Stc Spec
compile_spec :: M_Stc Spec
compile_spec = do
Spec
spec <- M_Stc Spec
get_spec
[Decl]
ds <- [M_Stc Decl] -> M_Stc [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (((String, TypeSpec) -> M_Stc Decl)
-> [(String, TypeSpec)] -> [M_Stc Decl]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> TypeSpec -> M_Stc Decl)
-> (String, TypeSpec) -> M_Stc Decl
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> TypeSpec -> M_Stc Decl
compile_type_spec) (Map String TypeSpec -> [(String, TypeSpec)]
forall k a. Map k a -> [(k, a)]
M.toList (Spec -> Map String TypeSpec
decls Spec
spec)))
let tspecs :: [(String, TypeSpec)]
tspecs = (Decl -> [(String, TypeSpec)]) -> [Decl] -> [(String, TypeSpec)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Decl -> [(String, TypeSpec)]
op [Decl]
ds
where op :: Decl -> [(String, TypeSpec)]
op (TypeDecl String
ty TypeSpec
tspec) = [(String
ty,TypeSpec
tspec)]
op Decl
_ = []
Spec -> M_Stc Spec
forall (m :: * -> *) a. Monad m => a -> m a
return (Spec
spec {decls :: Map String TypeSpec
decls = Map String TypeSpec -> Map String TypeSpec -> Map String TypeSpec
decls_union (Spec -> Map String TypeSpec
decls Spec
spec) ([(String, TypeSpec)] -> Map String TypeSpec
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(String, TypeSpec)]
tspecs) })
compile_derivation :: [Var] -> DomId -> Derivation -> M_Stc Derivation
compile_derivation :: [Var] -> String -> Derivation -> M_Stc Derivation
compile_derivation [Var]
bound String
d (HoldsWhen Term
t) = do
Term
t' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
TyBool
Set Var
fs <- Term -> M_Stc (Set Var)
free_vars Term
t'
let unbounds :: [Var]
unbounds = Set Var -> [Var]
forall a. Set a -> [a]
S.toList (Set Var
fs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` ([Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
bound))
Derivation -> M_Stc Derivation
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Derivation
HoldsWhen (if [Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
unbounds then Term
t' else [Var] -> Term -> Term
Exists [Var]
unbounds Term
t'))
compile_derivation [Var]
bound String
d (Dv [Var]
xs Term
t) = [Var] -> Term -> String -> M_Stc Derivation
compile_derived_from_clause [Var]
xs Term
t String
d
compile_derived_from_clause :: [Var] -> Term -> String -> M_Stc Derivation
compile_derived_from_clause [Var]
xs Term
t String
d = do
Term
t' <- Term -> Type -> M_Stc Term
convert_term Term
t (String -> Type
TyTagged String
d)
Set Var
fs <- Term -> M_Stc (Set Var)
free_vars Term
t'
let unbounds :: [Var]
unbounds = Set Var -> [Var]
forall a. Set a -> [a]
S.toList (Set Var
fs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` ([Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs))
Derivation -> M_Stc Derivation
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Derivation
Dv ([Var]
xs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
unbounds) Term
t')
compile_primitive_application :: DomId -> Arguments -> M_Stc (Term, Type)
compile_primitive_application :: String -> Arguments -> M_Stc (Term, Type)
compile_primitive_application String
d Arguments
params = String -> M_Stc Domain
get_dom String
d M_Stc Domain
-> (Domain -> M_Stc (Term, Type)) -> M_Stc (Term, Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Domain
dom -> case (Domain
dom, Arguments
params) of
(Domain
_, Left [Term]
as) | [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err String
error_string
(Domain
AnyString, Left [Term
a]) -> String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d Term
a (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TyStrings)
(Strings [String
s], Left []) -> String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d (String -> Term
StringLit String
s) (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TyStrings)
(Strings [String
s], Right [])-> String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d (String -> Term
StringLit String
s) (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TyStrings)
(Strings [String]
_, Left [Term
a]) -> String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d Term
a (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TyStrings)
(Domain
AnyInt, Left [Term
a]) -> String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d Term
a (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TyInts)
(Ints [Int
i], Right []) -> String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d (Int -> Term
IntLit Int
i) (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TyInts)
(Ints [Int
i], Left []) -> String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d (Int -> Term
IntLit Int
i) (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TyInts)
(Ints [Int]
_, Left [Term
a]) -> String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d Term
a (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TyInts)
(Domain
_, Right [Modifier]
_) -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err String
error_string
(Domain, Arguments)
_ -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err String
error_string
where error_string :: String
error_string = String
"The constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is primitive, and should receive exactly one argument in functional style"
primitive :: String -> Term -> Maybe Type -> M_Stc (Term, Type)
primitive String
d Term
t Maybe Type
Nothing = do (Term
t', Type
_) <- Term -> M_Stc (Term, Type)
compile_term Term
t
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> String -> Term
Tag Term
t' String
d, String -> Type
TyTagged String
d)
primitive String
d Term
t (Just Type
ty) = do Term
t' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
ty
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> String -> Term
Tag Term
t' String
d, String -> Type
TyTagged String
d)
compile_arguments :: DomId -> Arguments -> M_Stc Arguments
compile_arguments :: String -> Arguments -> M_Stc Arguments
compile_arguments String
_ (Right [Modifier]
ms) = [Modifier] -> Arguments
forall a b. b -> Either a b
Right ([Modifier] -> Arguments) -> M_Stc [Modifier] -> M_Stc Arguments
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Modifier] -> M_Stc [Modifier]
compile_modifiers [Modifier]
ms
compile_arguments String
d (Left [Term]
ts) = do
Spec
spec <- M_Stc Spec
get_spec
Domain
dom <- String -> M_Stc Domain
get_dom String
d
case Domain
dom of Products [Var]
xs
| [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts -> [Modifier] -> Arguments
forall a b. b -> Either a b
Right ([Modifier] -> Arguments) -> M_Stc [Modifier] -> M_Stc Arguments
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Modifier] -> M_Stc [Modifier]
compile_modifiers (((Var, Term) -> Modifier) -> [(Var, Term)] -> [Modifier]
forall a b. (a -> b) -> [a] -> [b]
map ((Var -> Term -> Modifier) -> (Var, Term) -> Modifier
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> Term -> Modifier
Rename) ([Var] -> [Term] -> [(Var, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Term]
ts))
| Bool
otherwise -> String -> M_Stc Arguments
forall a. String -> M_Stc a
err (String
"elements of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" have " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" components, " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" given")
Domain
_ -> String -> M_Stc Arguments
forall a. String -> M_Stc a
err (String
"non-composite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" used in application")
compile_modifiers :: [Modifier] -> M_Stc [Modifier]
compile_modifiers :: [Modifier] -> M_Stc [Modifier]
compile_modifiers [Modifier]
mods = do
Spec
spec <- M_Stc Spec
get_spec
let compile_mod :: Modifier -> M_Stc Modifier
compile_mod (Rename Var
x Term
t) = Var -> Term -> Modifier
Rename Var
x (Term -> Modifier) -> M_Stc Term -> M_Stc Modifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Type -> M_Stc Term
convert_term Term
t (String -> Type
TyTagged (Spec -> Var -> String
remove_decoration Spec
spec Var
x))
[M_Stc Modifier] -> M_Stc [Modifier]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Modifier -> M_Stc Modifier) -> [Modifier] -> [M_Stc Modifier]
forall a b. (a -> b) -> [a] -> [b]
map Modifier -> M_Stc Modifier
compile_mod [Modifier]
mods)
compile_effect :: [Var] -> Effect -> M_Stc Effect
compile_effect :: [Var] -> Effect -> M_Stc Effect
compile_effect [Var]
bound Effect
eff = case Effect
eff of
TAll [Var]
xs Term
t -> ([Var] -> Term -> Effect) -> [Var] -> Term -> M_Stc Effect
forall b. ([Var] -> Term -> b) -> [Var] -> Term -> M_Stc b
compile_effect' [Var] -> Term -> Effect
TAll [Var]
xs Term
t
CAll [Var]
xs Term
t -> ([Var] -> Term -> Effect) -> [Var] -> Term -> M_Stc Effect
forall b. ([Var] -> Term -> b) -> [Var] -> Term -> M_Stc b
compile_effect' [Var] -> Term -> Effect
CAll [Var]
xs Term
t
OAll [Var]
xs Term
t -> ([Var] -> Term -> Effect) -> [Var] -> Term -> M_Stc Effect
forall b. ([Var] -> Term -> b) -> [Var] -> Term -> M_Stc b
compile_effect' [Var] -> Term -> Effect
OAll [Var]
xs Term
t
where compile_effect' :: ([Var] -> Term -> b) -> [Var] -> Term -> M_Stc b
compile_effect' [Var] -> Term -> b
cons [Var]
xs Term
t = do (Term
t',Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
Set Var
fs <- Term -> M_Stc (Set Var)
free_vars Term
t'
let unbounds :: [Var]
unbounds = Set Var -> [Var]
forall a. Set a -> [a]
S.toList (Set Var
fs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList ([Var]
bound [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
xs))
b -> M_Stc b
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> b
cons ([Var]
xs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
unbounds) Term
t')
compile_term :: Term -> M_Stc (Term, Type)
compile_term :: Term -> M_Stc (Term, Type)
compile_term Term
t0 = do
Spec
spec <- M_Stc Spec
get_spec
case Term
t0 of
Term
CurrentTime -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
CurrentTime, Type
TyInts)
StringLit String
s -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t0, Type
TyStrings)
IntLit Int
i -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t0, Type
TyInts)
BoolLit Bool
b -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t0, Type
TyBool)
Ref Var
x -> [Var] -> M_Stc ()
check_known_type [Var
x] M_Stc () -> M_Stc (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t0, String -> Type
TyTagged (Spec -> Var -> String
remove_decoration Spec
spec Var
x))
App String
d Arguments
ms -> do [Var] -> M_Stc ()
check_known_type [String -> Var
no_decoration String
d]
case (TypeSpec -> Domain) -> Maybe TypeSpec -> Maybe Domain
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Domain
domain (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d) of
Just (Products [Var]
_) -> do
Arguments
ms' <- String -> Arguments -> M_Stc Arguments
compile_arguments String
d Arguments
ms
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Arguments -> Term
App String
d Arguments
ms', String -> Type
TyTagged String
d)
Maybe Domain
_ -> String -> Arguments -> M_Stc (Term, Type)
compile_primitive_application String
d Arguments
ms
Tag Term
t String
d -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err String
"tagging is an auxiliary operation"
Untag Term
t -> do (Term
t', Type
ty) <- Term -> M_Stc (Term, Type)
compile_term Term
t
case Type
ty of TyTagged String
d -> case Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d of
Maybe TypeSpec
Nothing -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err String
"untagging is an auxiliary operation"
Just TypeSpec
decl -> case TypeSpec -> Domain
domain TypeSpec
decl of
Strings [String]
_ -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t', Type
TyStrings)
Ints [Int]
_ -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t', Type
TyInts)
Domain
AnyString -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t', Type
TyStrings)
Domain
AnyInt -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t', Type
TyInts)
Domain
_ -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err String
"untagging is an auxiliary operation"
Type
_ -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err String
"untagging is an auxiliary operation"
Not Term
t -> do Term
t' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
TyBool
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Not Term
t', Type
TyBool)
And Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyBool
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyBool
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
And Term
t1' Term
t2', Type
TyBool)
Or Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyBool
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyBool
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Or Term
t1' Term
t2', Type
TyBool)
Geq Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Geq Term
t1' Term
t2', Type
TyBool)
Leq Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Leq Term
t1' Term
t2', Type
TyBool)
Le Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Le Term
t1' Term
t2', Type
TyBool)
Ge Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Ge Term
t1' Term
t2', Type
TyBool)
Mult Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Mult Term
t1' Term
t2', Type
TyInts)
Mod Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Mod Term
t1' Term
t2', Type
TyInts)
Div Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Div Term
t1' Term
t2', Type
TyInts)
Sub Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Sub Term
t1' Term
t2', Type
TyInts)
Add Term
t1 Term
t2 -> do Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
TyInts
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Add Term
t1' Term
t2', Type
TyInts)
Sum [Var]
xs Term
t -> do Term
t' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
TyInts
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Term
Sum [Var]
xs Term
t', Type
TyInts)
Eq Term
t1 Term
t2 -> (do (Term
t1', Type
tau1) <- Term -> M_Stc (Term, Type)
compile_term Term
t1
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
tau1
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Eq Term
t1' Term
t2', Type
TyBool)) M_Stc (Term, Type) -> M_Stc (Term, Type) -> M_Stc (Term, Type)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(do (Term
t2', Type
tau2) <- Term -> M_Stc (Term, Type)
compile_term Term
t2
Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
tau2
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Eq Term
t1' Term
t2', Type
TyBool))
Neq Term
t1 Term
t2 -> (do (Term
t1', Type
tau1) <- Term -> M_Stc (Term, Type)
compile_term Term
t1
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
tau1
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Neq Term
t1' Term
t2', Type
TyBool)) M_Stc (Term, Type) -> M_Stc (Term, Type) -> M_Stc (Term, Type)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(do (Term
t2', Type
tau2) <- Term -> M_Stc (Term, Type)
compile_term Term
t2
Term
t1' <- Term -> Type -> M_Stc Term
convert_term Term
t1 Type
tau2
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Neq Term
t1' Term
t2', Type
TyBool))
Count [Var]
xs Term
t -> do (Term
t', Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Term
Count [Var]
xs Term
t', Type
TyInts)
Max [Var]
xs Term
t -> do (Term
t', Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Term
Max [Var]
xs Term
t', Type
TyInts)
Min [Var]
xs Term
t -> do (Term
t', Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Term
Min [Var]
xs Term
t', Type
TyInts)
When Term
t1 Term
t2 -> do (Term
t1', Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t1
Term
t2' <- Term -> Type -> M_Stc Term
convert_term Term
t2 Type
TyBool
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
When Term
t1' Term
t2', Type
tau)
Present Term
t -> do (Term
t', Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
case Type
tau of TyTagged String
d -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Present Term
t', Type
TyBool)
Type
errt -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err (String
"Holds(t) requires t to evaluate to a an instance, not a literal")
Violated Term
t -> do (Term
t', Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
case Type
tau of TyTagged String
d -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Violated Term
t', Type
TyBool)
Type
errt -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err (String
"Violated(t) requires t to evaluate to an instance, not a literal")
Enabled Term
t -> do (Term
t', Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
case Type
tau of TyTagged String
d -> (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Enabled Term
t', Type
TyBool)
Type
errt -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err (String
"Enabled(t) requires t to evaluate to an instance, not a literal")
Exists [Var]
xs Term
t -> do Term
t' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
TyBool
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Term
Exists [Var]
xs Term
t', Type
TyBool)
Forall [Var]
xs Term
t -> do Term
t' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
TyBool
(Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Term
Forall [Var]
xs Term
t', Type
TyBool)
Project Term
t Var
x -> do (Term
t',Type
tau) <- Term -> M_Stc (Term, Type)
compile_term Term
t
case Type
tau of
TyTagged String
d -> do
Domain
dom <- String -> M_Stc Domain
get_dom String
d
case Domain
dom of
Products [Var]
xs -> if Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
x [Var]
xs
then (Term, Type) -> M_Stc (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Var -> Term
Project Term
t' Var
x, String -> Type
TyTagged (Spec -> Var -> String
remove_decoration Spec
spec Var
x))
else String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err (String
"project(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tString -> String -> String
forall a. [a] -> [a] -> [a]
++ String
","String -> String -> String
forall a. [a] -> [a] -> [a]
++Var -> String
forall a. Show a => a -> String
show Var
xString -> String -> String
forall a. [a] -> [a] -> [a]
++String
") expects t to evaluate to a value of a product-type containing a reference to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Show a => a -> String
show Var
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" instead got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Var] -> String
forall a. Show a => a -> String
show [Var]
xs)
Domain
_ -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err (String
"project(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tString -> String -> String
forall a. [a] -> [a] -> [a]
++ String
","String -> String -> String
forall a. [a] -> [a] -> [a]
++Var -> String
forall a. Show a => a -> String
show Var
xString -> String -> String
forall a. [a] -> [a] -> [a]
++String
") expects t to evaluate to a value of a product-type, instead got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Domain -> String
forall a. Show a => a -> String
show Domain
dom)
Type
_ -> String -> M_Stc (Term, Type)
forall a. String -> M_Stc a
err (String
"project(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tString -> String -> String
forall a. [a] -> [a] -> [a]
++ String
","String -> String -> String
forall a. [a] -> [a] -> [a]
++Var -> String
forall a. Show a => a -> String
show Var
xString -> String -> String
forall a. [a] -> [a] -> [a]
++String
") expects t to evaluate to a tagged-element, instead got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tau)
convert_term :: Term -> Type -> M_Stc Term
convert_term :: Term -> Type -> M_Stc Term
convert_term Term
t Type
ty = do
(Term
t', Type
ty') <- Term -> M_Stc (Term, Type)
compile_term Term
t
if Type
ty' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty then Term -> M_Stc Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t'
else case Type
ty of
Type
TyStrings -> case Type
ty' of TyTagged String
d -> (Domain -> Domain -> Bool) -> Domain -> Domain -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Domain -> Domain -> Bool
match_domain Domain
AnyString (Domain -> Bool) -> M_Stc Domain -> M_Stc Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> M_Stc Domain
get_dom String
d M_Stc Bool -> (Bool -> M_Stc Term) -> M_Stc Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> Term -> M_Stc Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t')
Bool
False -> Type -> Type -> M_Stc Term
forall a a a. (Show a, Show a) => a -> a -> M_Stc a
conv_err Type
ty' Type
ty
Type
_ -> Type -> Type -> M_Stc Term
forall a a a. (Show a, Show a) => a -> a -> M_Stc a
conv_err Type
ty' Type
ty
Type
TyInts -> case Type
ty' of TyTagged String
d -> (Domain -> Domain -> Bool) -> Domain -> Domain -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Domain -> Domain -> Bool
match_domain Domain
AnyInt (Domain -> Bool) -> M_Stc Domain -> M_Stc Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> M_Stc Domain
get_dom String
d M_Stc Bool -> (Bool -> M_Stc Term) -> M_Stc Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> Term -> M_Stc Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t')
Bool
False -> Type -> Type -> M_Stc Term
forall a a a. (Show a, Show a) => a -> a -> M_Stc a
conv_err Type
ty' Type
ty
Type
_ -> Type -> Type -> M_Stc Term
forall a a a. (Show a, Show a) => a -> a -> M_Stc a
conv_err Type
ty' Type
ty
Type
TyBool -> case Type
ty' of Type
TyInts -> Term -> M_Stc Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> M_Stc Term) -> Term -> M_Stc Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Geq Term
t' (Int -> Term
IntLit Int
1)
TyTagged String
_ -> Term -> M_Stc Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> M_Stc Term) -> Term -> M_Stc Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
Present Term
t'
Type
_ -> Type -> Type -> M_Stc Term
forall a a a. (Show a, Show a) => a -> a -> M_Stc a
conv_err Type
ty' Type
ty
TyTagged String
d -> String -> M_Stc Domain
get_dom String
d M_Stc Domain -> (Domain -> M_Stc Bool) -> M_Stc Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Domain -> M_Stc Bool
match_type Type
ty' M_Stc Bool -> (Bool -> M_Stc Term) -> M_Stc Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case Bool
True -> Term -> M_Stc Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> String -> Term
Tag Term
t' String
d)
Bool
False -> Type -> Type -> M_Stc Term
forall a a a. (Show a, Show a) => a -> a -> M_Stc a
conv_err Type
ty' Type
ty
where conv_err :: a -> a -> M_Stc a
conv_err a
source a
target = String -> M_Stc a
forall a. String -> M_Stc a
err (String
"cannot convert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
source String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
target)
match_type :: Type -> Domain -> M_Stc Bool
match_type :: Type -> Domain -> M_Stc Bool
match_type (TyTagged String
d) Domain
dom = String -> M_Stc Domain
get_dom String
d M_Stc Domain -> (Domain -> M_Stc Bool) -> M_Stc Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> M_Stc Bool) -> (Domain -> Bool) -> Domain -> M_Stc Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Domain -> Domain -> Bool) -> Domain -> Domain -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Domain -> Domain -> Bool
match_domain Domain
dom
match_type Type
TyInts Domain
dom = case Domain
dom of
Domain
AnyInt -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Ints [Int]
_ -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Domain
Time -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Strings [String]
_ -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Domain
AnyString -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Products [Var]
_ -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
match_type Type
TyStrings Domain
dom = case Domain
dom of
Domain
AnyString -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Strings [String]
_ -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Domain
AnyInt -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Ints [Int]
_ -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Products [Var]
_ -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Domain
Time -> Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
match_type Type
_ Domain
_ = Bool -> M_Stc Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
match_domain :: Domain -> Domain -> Bool
match_domain :: Domain -> Domain -> Bool
match_domain Domain
dom Domain
dom' = case (Domain
dom, Domain
dom') of
(Domain
AnyString, Domain
AnyString) -> Bool
True
(Strings [String]
_, Domain
AnyString) -> Bool
True
(Domain
AnyString, Strings [String]
_) -> Bool
False
(Strings [String]
s1, Strings [String]
s2) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String]
s1 [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String]
s2)
(Domain
AnyString, Domain
_) -> Bool
False
(Strings [String]
_, Domain
_) -> Bool
False
(Domain
AnyInt, Domain
AnyInt) -> Bool
True
(Ints [Int]
_, Domain
AnyInt) -> Bool
True
(Domain
AnyInt, Ints [Int]
_) -> Bool
True
(Ints [Int]
i1, Ints [Int]
i2) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Int]
i1 [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int]
i2)
(Domain
AnyInt, Domain
AnyString) -> Bool
False
(Domain
AnyInt, Strings [String]
_) -> Bool
False
(Domain
AnyInt, Products [Var]
_) -> Bool
False
(Ints [Int]
_, Domain
AnyString) -> Bool
False
(Ints [Int]
_, Strings [String]
_) -> Bool
False
(Ints [Int]
_, Products [Var]
_) -> Bool
False
(Domain
AnyInt, Domain
Time) -> Bool
False
(Ints [Int]
_, Domain
Time) -> Bool
False
(Domain
Time, Domain
Time) -> Bool
True
(Domain
Time, Domain
AnyInt) -> Bool
True
(Domain
Time, Ints [Int]
_) -> Bool
False
(Domain
Time, Domain
AnyString) -> Bool
False
(Domain
Time, Strings [String]
_) -> Bool
False
(Domain
Time, Products [Var]
_) -> Bool
False
(Products [Var]
r, Products [Var]
r') -> [Var]
r [Var] -> [Var] -> Bool
forall a. Eq a => a -> a -> Bool
== [Var]
r'
(Products [Var]
_, Domain
_) -> Bool
False