{-# 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 ((\\), partition)
import qualified Data.Map as M
import qualified Data.Set as S
data M_Stc a = M_Stc {forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic :: Spec -> Either [String] (Spec, a)}
instance Monad M_Stc where
return :: forall a. a -> M_Stc a
return a
a = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> forall a b. b -> Either a b
Right (Spec
spec, a
a)
M_Stc a
m >>= :: forall a b. M_Stc a -> (a -> M_Stc b) -> M_Stc b
>>= a -> M_Stc b
f = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
m Spec
spec of
Right (Spec
spec',a
a) -> forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic (a -> M_Stc b
f a
a) Spec
spec'
Left [String]
err -> forall a b. a -> Either a b
Left [String]
err
instance Applicative M_Stc where
pure :: forall a. a -> M_Stc a
pure = forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: forall a 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 :: forall a b. (a -> b) -> M_Stc a -> M_Stc b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Alternative M_Stc where
empty :: forall a. M_Stc a
empty = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc (forall a b. a -> b -> a
const (forall a b. a -> Either a b
Left []))
M_Stc a
p <|> :: forall a. M_Stc a -> M_Stc a -> M_Stc a
<|> M_Stc a
q = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
p Spec
spec of
Left [String]
ers1 -> case forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
q Spec
spec of
Left [String]
ers2 -> forall a b. a -> Either a b
Left ([String]
ers1 forall a. [a] -> [a] -> [a]
++ [String]
ers2)
Right (Spec, a)
x -> forall a b. b -> Either a b
Right (Spec, a)
x
Right (Spec, a)
x -> forall a b. b -> Either a b
Right (Spec, a)
x
err :: String -> M_Stc a
err :: forall a. String -> M_Stc a
err String
str = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> 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 = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d of
Just TypeSpec
tspec -> forall a b. b -> Either a b
Right (Spec
spec, TypeSpec -> Domain
domain TypeSpec
tspec)
Maybe TypeSpec
_ -> forall a b. a -> Either a b
Left [String
"undeclared type: " forall a. [a] -> [a] -> [a]
++ String
d]
get_spec :: M_Stc Spec
get_spec :: M_Stc Spec
get_spec = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> forall a b. b -> Either a b
Right (Spec
spec, Spec
spec)
insert_typespec :: DomId -> TypeSpec -> M_Stc ()
insert_typespec :: String -> TypeSpec -> M_Stc ()
insert_typespec String
ty TypeSpec
tspec = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> forall a b. b -> Either a b
Right (Spec
spec { decls :: Map String TypeSpec
decls = 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) }, ())
execute_decl :: CDecl -> M_Stc ()
execute_decl :: CDecl -> M_Stc ()
execute_decl CDecl
decl = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec ->
let spec' :: Spec
spec' = case CDecl
decl of
CPlaceholderDecl String
f String
t -> Spec
spec { aliases :: Map String String
aliases = 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) }
CTypeExt String
ty [CModClause]
clauses -> Spec
spec { decls :: Map String TypeSpec
decls = forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust (String -> [CModClause] -> TypeSpec -> TypeSpec
apply_type_ext String
ty [CModClause]
clauses) String
ty (Spec -> Map String TypeSpec
decls Spec
spec) }
CTypeDecl String
ty TypeSpec
tspec -> Spec
spec { decls :: Map String TypeSpec
decls = 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 forall a b. b -> Either a b
Right (Spec
spec', ())
with_spec :: Spec -> M_Stc a -> M_Stc a
with_spec :: forall a. Spec -> M_Stc a -> M_Stc a
with_spec Spec
spec' M_Stc a
m = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
m Spec
spec' of
Left [String]
err -> forall a b. a -> Either a b
Left [String]
err
Right (Spec
_,a
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 :: forall a. String -> TypeSpec -> M_Stc a -> M_Stc a
with_decl String
ty TypeSpec
tspec M_Stc a
m = forall a. (Spec -> Either [String] (Spec, a)) -> M_Stc a
M_Stc forall a b. (a -> b) -> a -> b
$ \Spec
spec -> case forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc a
m (Spec
spec{decls :: Map String TypeSpec
decls=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 -> forall a b. a -> Either a b
Left [String]
err
Right (Spec
_,a
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 = forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t
[Var] -> M_Stc ()
check_known_type (forall a. Set a -> [a]
S.toList Set Var
xs)
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 forall a. M_Stc a -> Spec -> Either [String] (Spec, a)
runStatic M_Stc (Spec, Initialiser, Scenario)
compile Spec
f of
Left [String]
errs -> forall a b. a -> Either a b
Left [String]
errs
Right (Spec
_,(Spec
spec, Initialiser
init, Scenario
scen)) -> 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
forall a. Spec -> M_Stc a -> M_Stc a
with_spec Spec
f' 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
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 = 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 = 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 = forall a. Set a -> [a]
S.toList Set Var
fs
let t1 :: Term
t1 | 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 forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> String -> Maybe TypeSpec
find_decl Spec
spec forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> Var -> String
remove_decoration Spec
spec) [Var]
unbounds of
[] -> Term -> Statement
Query 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]
_) -> forall a. String -> M_Stc a
err (String
"undeclared type " forall a. [a] -> [a] -> [a]
++ Spec -> Var -> String
remove_decoration Spec
spec Var
t 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) (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 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 = forall a. Set a -> [a]
S.toList (Set Var
fs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs)
[Var] -> TransType -> Either Term (String, Arguments) -> Statement
Trans ([Var]
xs forall a. [a] -> [a] -> [a]
++ [Var]
unbounds) TransType
aty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left 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 String
d -> Term -> Type -> M_Stc Term
convert_term Term
term (String -> Type
TyTagged String
d)
Maybe String
_ -> forall a b. (a, b) -> a
fst 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return CPhrase
CPSkip
PDo Tagged
tv -> forall (m :: * -> *) a. Monad m => a -> m a
return (Tagged -> CPhrase
CDo Tagged
tv)
PTrigger [Var]
vs Term
t -> 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 -> 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 -> 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 -> 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 -> 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))
PInstQuery Bool
b [Var]
vs Term
t -> do
Set Var
fs <- Term -> M_Stc (Set Var)
free_vars Term
t
let unbounds :: [Var]
unbounds = forall a. Set a -> [a]
S.toList (Set Var
fs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
vs)
Bool -> [Var] -> Term -> CPhrase
CInstQuery Bool
b ([Var]
vs forall a. [a] -> [a] -> [a]
++ [Var]
unbounds) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> M_Stc (Term, Type)
compile_term Term
t
PDeclBlock [Decl]
ds -> do
let ([Decl]
type_decls, [Decl]
others) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Decl -> Bool
isInitialTypeDecl [Decl]
ds
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Decl]
type_decls (\(TypeDecl String
d TypeSpec
tspec) -> String -> TypeSpec -> M_Stc ()
insert_typespec String
d TypeSpec
tspec)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Decl]
others forall a b. (a -> b) -> a -> b
$ \Decl
decl -> do
[CDecl]
decls <- Decl -> M_Stc [CDecl]
compile_decl Decl
decl
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [CDecl]
decls CDecl -> M_Stc ()
execute_decl
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 (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 (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 (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 (forall a b. a -> Either a b
Left Term
t)
to_stmt (PQuery Term
t) = Term -> Statement
Query Term
t
to_stmt Phrase
_ = 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
_ = forall a. HasCallStack => String -> a
error String
"Explorer.assert 2"
compile_decl :: Decl -> M_Stc [CDecl]
compile_decl :: Decl -> M_Stc [CDecl]
compile_decl d :: Decl
d@(PlaceholderDecl String
x String
y) = [Var] -> M_Stc ()
check_known_type [String -> Var
no_decoration String
y]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return [String -> String -> CDecl
CPlaceholderDecl String
x String
y]
compile_decl d :: Decl
d@(TypeExt String
ty [ModClause]
clauses) = String -> [ModClause] -> M_Stc [CDecl]
compile_ext String
ty [ModClause]
clauses
compile_decl d :: Decl
d@(TypeDecl String
ty TypeSpec
tspec) = (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TypeSpec -> M_Stc CDecl
compile_type_spec String
ty TypeSpec
tspec
compile_ext :: DomId -> [ModClause] -> M_Stc [CDecl]
compile_ext :: String -> [ModClause] -> M_Stc [CDecl]
compile_ext String
ty [ModClause]
clauses = do
Spec
spec <- M_Stc Spec
get_spec
case 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 -> forall a. String -> M_Stc a
err (String
"cannot find the type " forall a. [a] -> [a] -> [a]
++ String
ty forall a. [a] -> [a] -> [a]
++ String
" to extend or " forall a. [a] -> [a] -> [a]
++ String
ty forall a. [a] -> [a] -> [a]
++ String
" of the wrong kind")
Just TypeSpec
tspec -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> TypeSpec -> ModClause -> M_Stc [CDecl]
compile_clause String
ty TypeSpec
tspec) [ModClause]
clauses
where compile_clause :: String -> TypeSpec -> ModClause -> M_Stc [CDecl]
compile_clause String
ty TypeSpec
tspec ModClause
clause = case ModClause
clause of
ConditionedByCl [Term]
conds -> String -> CModClause -> [CDecl]
to_ext String
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> CModClause
CConditionedByCl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> TypeSpec -> Term -> M_Stc Term
convert_precon String
ty TypeSpec
tspec) [Term]
conds
DerivationCl [Derivation]
dvs -> String -> CModClause -> [CDecl]
to_ext String
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Derivation] -> CModClause
CDerivationCl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> String -> Derivation -> M_Stc Derivation
compile_derivation [Var]
xs String
ty) [Derivation]
dvs
PostCondCl Initialiser
effs -> String -> CModClause -> [CDecl]
to_ext String
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Initialiser -> CModClause
CPostCondCl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> Effect -> M_Stc Effect
compile_effect [Var]
xs) Initialiser
effs
SyncCl [Sync]
ss -> String -> CModClause -> [CDecl]
to_ext String
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sync] -> CModClause
CSyncCl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Var] -> Sync -> M_Stc Sync
compile_sync [Var]
xs) [Sync]
ss
ViolationCl [Term]
vts -> String -> CModClause -> [CDecl]
to_ext String
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> CModClause
CViolationCl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Term -> M_Stc Term
compile_violation_condition String
ty) [Term]
vts
EnforcingActsCl [String]
as -> do [CDecl]
viols <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> M_Stc CDecl
compile_enf [String]
as
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> [CModClause] -> CDecl
CTypeExt String
ty [[String] -> CModClause
CEnforcingActsCl [String]
as] forall a. a -> [a] -> [a]
: [CDecl]
viols
where compile_enf :: String -> M_Stc CDecl
compile_enf String
a = String -> [CModClause] -> CDecl
CTypeExt String
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> CModClause
CViolationCl forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> M_Stc (Term, Type)
compile_term (String -> Term
enforcing_act_condition String
a)
TerminatedByCl [String]
as -> do [CDecl]
posts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> M_Stc CDecl
compile_termby [String]
as
[CDecl]
holds <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> M_Stc CDecl
compile_holdsby [String]
as
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String -> [CModClause] -> CDecl
CTypeExt String
ty [[String] -> CModClause
CTerminatedByCl [String]
as]] forall a. [a] -> [a] -> [a]
++ [CDecl]
posts forall a. [a] -> [a] -> [a]
++ [CDecl]
holds
where compile_termby :: String -> M_Stc CDecl
compile_termby String
a = String -> [CModClause] -> CDecl
CTypeExt String
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Initialiser -> CModClause
CPostCondCl forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Var] -> Term -> Effect) -> [Var] -> [Var] -> Term -> M_Stc Effect
compile_effect' [Var] -> Term -> Effect
TAll [Var]
xs [] (String -> String -> Term
terminated_by_condition String
ty String
a)
compile_holdsby :: String -> M_Stc CDecl
compile_holdsby String
a = String -> [CModClause] -> CDecl
CTypeExt String
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Derivation] -> CModClause
CDerivationCl forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var] -> String -> Derivation -> M_Stc Derivation
compile_derivation [Var]
xs String
a (Term -> Derivation
HoldsWhen (String -> String -> Term
terminated_by_precondition String
ty String
a))
CreatedByCl [String]
as -> do [CDecl]
posts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> M_Stc CDecl
compile_createdby [String]
as
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String -> [CModClause] -> CDecl
CTypeExt String
ty [[String] -> CModClause
CCreatedByCl [String]
as]] forall a. [a] -> [a] -> [a]
++ [CDecl]
posts
where compile_createdby :: String -> M_Stc CDecl
compile_createdby String
a = String -> [CModClause] -> CDecl
CTypeExt String
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Initialiser -> CModClause
CPostCondCl forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Var] -> Term -> Effect) -> [Var] -> [Var] -> Term -> M_Stc Effect
compile_effect' [Var] -> Term -> Effect
CAll [Var]
xs [] (String -> String -> Term
created_by_condition String
ty String
a)
where xs :: [Var]
xs = case TypeSpec -> Domain
domain TypeSpec
tspec of Products [Var]
xs -> [Var]
xs
Domain
_ -> [String -> Var
no_decoration String
ty]
to_ext :: String -> CModClause -> [CDecl]
to_ext String
ty CModClause
clause = [String -> [CModClause] -> CDecl
CTypeExt String
ty [CModClause
clause]]
compile_type_spec :: DomId -> TypeSpec -> M_Stc CDecl
compile_type_spec :: String -> TypeSpec -> M_Stc CDecl
compile_type_spec String
ty TypeSpec
tspec = do
forall a. String -> TypeSpec -> M_Stc a -> M_Stc a
with_decl String
ty TypeSpec
tspec 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 <- 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 <- 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 forall a. Set a -> [a]
S.toList (Set Var
ffs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` 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
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TypeSpec -> CDecl
CTypeDecl String
ty (TypeSpec {domain :: Domain
domain = TypeSpec -> Domain
domain TypeSpec
tspec, closed :: Bool
closed = TypeSpec -> Bool
closed TypeSpec
tspec
,restriction :: Maybe Restriction
restriction = TypeSpec -> Maybe Restriction
restriction 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
_ = 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 -> forall a. String -> M_Stc a
err (String
"Undeclared type or placeholder `" forall a. [a] -> [a] -> [a]
++ String
base forall a. [a] -> [a] -> [a]
++ String
dec forall a. [a] -> [a] -> [a]
++ String
"`")
Just TypeSpec
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
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 = forall a. Set a -> [a]
S.toList (Set Var
cond_fs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if 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' <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map ([Var] -> Effect -> M_Stc Effect
compile_effect [Var]
xs) (ActSpec -> Initialiser
effects ActSpec
aspec))
[Sync]
syncs' <- 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)
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' <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map ([Var] -> Effect -> M_Stc Effect
compile_effect [Var]
xs) (EventSpec -> Initialiser
event_effects EventSpec
espec))
[Sync]
syncs' <- 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) (EventSpec -> [Sync]
event_syncs EventSpec
espec)
forall (m :: * -> *) a. Monad m => a -> m a
return (EventSpec -> Kind
Event (EventSpec
espec { event_effects :: Initialiser
event_effects = Initialiser
effects', event_syncs :: [Sync]
event_syncs = [Sync]
syncs' } ))
Duty DutySpec
dspec -> do [Term]
vconds <- 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) (DutySpec -> [Term]
violated_when DutySpec
dspec)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (DutySpec -> Kind
Duty (DutySpec
dspec { violated_when :: [Term]
violated_when = [Term]
vconds }))
Fact FactSpec
_ -> 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 = forall a. Set a -> [a]
S.toList (Set Var
fs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` (forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs))
term'' :: Term
term'' | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
unbounds = Term
term'
| Bool
otherwise = [Var] -> Term -> Term
Exists [Var]
unbounds Term
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 = forall a. Set a -> [a]
S.toList (Set Var
frees forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList ([Var]
vars forall a. [a] -> [a] -> [a]
++ [Var]
bound))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Var] -> Term -> Sync
Sync ([Var]
vars forall a. [a] -> [a] -> [a]
++ [Var]
unbounds) Term
t'
Type
_ -> 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
[CDecl]
ds <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> TypeSpec -> M_Stc CDecl
compile_type_spec) (forall k a. Map k a -> [(k, a)]
M.toList (Spec -> Map String TypeSpec
decls Spec
spec)))
let tspecs :: [(String, TypeSpec)]
tspecs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CDecl -> [(String, TypeSpec)]
op [CDecl]
ds
where op :: CDecl -> [(String, TypeSpec)]
op (CTypeDecl String
ty TypeSpec
tspec) = [(String
ty,TypeSpec
tspec)]
op CDecl
_ = []
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) (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 = forall a. Set a -> [a]
S.toList (Set Var
fs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` (forall a. Ord a => [a] -> Set a
S.fromList [Var]
bound))
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Derivation
HoldsWhen (if 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 = forall a. Set a -> [a]
S.toList (Set Var
fs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` (forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Derivation
Dv ([Var]
xs 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 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) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
as forall a. Ord a => a -> a -> Bool
> Int
1 -> 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 (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) (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) (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 (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 (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) (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) (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 (forall a. a -> Maybe a
Just Type
TyInts)
(Domain
_, Right [Modifier]
_) -> forall a. String -> M_Stc a
err String
error_string
(Domain, Arguments)
_ -> forall a. String -> M_Stc a
err String
error_string
where error_string :: String
error_string = String
"The constructor " forall a. [a] -> [a] -> [a]
++ String
d 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
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
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) = forall a b. b -> Either a b
Right 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
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Modifier] -> M_Stc [Modifier]
compile_modifiers (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> Term -> Modifier
Rename) (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Term]
ts))
| Bool
otherwise -> forall a. String -> M_Stc a
err (String
"elements of " forall a. [a] -> [a] -> [a]
++ String
d forall a. [a] -> [a] -> [a]
++ String
" have " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs) forall a. [a] -> [a] -> [a]
++ String
" components, " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts) forall a. [a] -> [a] -> [a]
++ String
" given")
Domain
_ -> forall a. String -> M_Stc a
err (String
"non-composite " forall a. [a] -> [a] -> [a]
++ String
d 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 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))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (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] -> [Var] -> Term -> M_Stc Effect
compile_effect' [Var] -> Term -> Effect
TAll [Var]
bound [Var]
xs Term
t
CAll [Var]
xs Term
t -> ([Var] -> Term -> Effect) -> [Var] -> [Var] -> Term -> M_Stc Effect
compile_effect' [Var] -> Term -> Effect
CAll [Var]
bound [Var]
xs Term
t
OAll [Var]
xs Term
t -> ([Var] -> Term -> Effect) -> [Var] -> [Var] -> Term -> M_Stc Effect
compile_effect' [Var] -> Term -> Effect
OAll [Var]
bound [Var]
xs Term
t
compile_effect' :: ([Var] -> Term -> Effect) -> [Var] -> [Var] -> Term -> M_Stc Effect
compile_effect' :: ([Var] -> Term -> Effect) -> [Var] -> [Var] -> Term -> M_Stc Effect
compile_effect' [Var] -> Term -> Effect
cons [Var]
bound [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 = forall a. Set a -> [a]
S.toList (Set Var
fs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList ([Var]
bound forall a. [a] -> [a] -> [a]
++ [Var]
xs))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> Term -> Effect
cons ([Var]
xs 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term
CurrentTime, Type
TyInts)
StringLit String
s -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t0, Type
TyStrings)
IntLit Int
i -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t0, Type
TyInts)
BoolLit Bool
b -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t0, Type
TyBool)
Ref Var
x -> [Var] -> M_Stc ()
check_known_type [Var
x] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 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
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 -> 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 -> 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]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t', Type
TyStrings)
Ints [Int]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t', Type
TyInts)
Domain
AnyString -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t', Type
TyStrings)
Domain
AnyInt -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t', Type
TyInts)
Domain
_ -> forall a. String -> M_Stc a
err String
"untagging is an auxiliary operation"
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
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
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
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
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
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
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
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
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
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
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
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
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
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
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Eq Term
t1' Term
t2', Type
TyBool)) 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
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
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
Neq Term
t1' Term
t2', Type
TyBool)) 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
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
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' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
TyInts
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' <- Term -> Type -> M_Stc Term
convert_term Term
t Type
TyInts
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
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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Present Term
t', Type
TyBool)
Type
errt -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Violated Term
t', Type
TyBool)
Type
errt -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Enabled Term
t', Type
TyBool)
Type
errt -> 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
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
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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
x [Var]
xs
then 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 forall a. String -> M_Stc a
err (String
"project(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tforall a. [a] -> [a] -> [a]
++ String
","forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> String
show Var
xforall a. [a] -> [a] -> [a]
++String
") expects t to evaluate to a value of a product-type containing a reference to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var
x forall a. [a] -> [a] -> [a]
++ String
" instead got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Var]
xs)
Domain
_ -> forall a. String -> M_Stc a
err (String
"project(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tforall a. [a] -> [a] -> [a]
++ String
","forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> String
show Var
xforall a. [a] -> [a] -> [a]
++String
") expects t to evaluate to a value of a product-type, instead got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Domain
dom)
Type
_ -> forall a. String -> M_Stc a
err (String
"project(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tforall a. [a] -> [a] -> [a]
++ String
","forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> String
show Var
xforall a. [a] -> [a] -> [a]
++String
") expects t to evaluate to a tagged-element, instead got: " forall a. [a] -> [a] -> [a]
++ 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' forall a. Eq a => a -> a -> Bool
== Type
ty then 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 -> forall a b c. (a -> b -> c) -> b -> a -> c
flip Domain -> Domain -> Bool
match_domain Domain
AnyString forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> M_Stc Domain
get_dom String
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t')
Bool
False -> forall {a} {a} {a}. (Show a, Show a) => a -> a -> M_Stc a
conv_err Type
ty' Type
ty
Type
_ -> 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 -> forall a b c. (a -> b -> c) -> b -> a -> c
flip Domain -> Domain -> Bool
match_domain Domain
AnyInt forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> M_Stc Domain
get_dom String
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
Untag Term
t')
Bool
False -> forall {a} {a} {a}. (Show a, Show a) => a -> a -> M_Stc a
conv_err Type
ty' Type
ty
Type
_ -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Geq Term
t' (Int -> Term
IntLit Int
1)
TyTagged String
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term -> Term
Present Term
t'
Type
_ -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Domain -> M_Stc Bool
match_type Type
ty' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> String -> Term
Tag Term
t' String
d)
Bool
False -> 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 = forall a. String -> M_Stc a
err (String
"cannot convert " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
source forall a. [a] -> [a] -> [a]
++ String
" to " forall a. [a] -> [a] -> [a]
++ 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Ints [Int]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Domain
Time -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Strings [String]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Domain
AnyString -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Products [Var]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
match_type Type
TyStrings Domain
dom = case Domain
dom of
Domain
AnyString -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Strings [String]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Domain
AnyInt -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Ints [Int]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Products [Var]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Domain
Time -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
match_type Type
_ Domain
_ = 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) -> forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String]
s1 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) -> forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Int]
i1 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 forall a. Eq a => a -> a -> Bool
== [Var]
r'
(Products [Var]
_, Domain
_) -> Bool
False