{-# 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 -- ensure the declaration is active during its compilation 
    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
    -- convert post-conditions
    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))
    -- convert syncs
    [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)
    -- build new act
    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 -- TODO, should be dealt with by outer -> inner translation
                 [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
--  (AnyString, Left [])   -> primitive d (StringLit "()") (Just TyStrings)
--  (AnyString, Right [])  -> primitive d (StringLit "()") (Just TyStrings)
  (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 -- simplification, assuming no conversion to tagged-elems yet
                    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 -- simplification, as above
                    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 -- simplification, as above
                    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) 

-- term => term : type
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'   -- rule id
               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) -- rule INT -> BOOL
                          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

-- | second domain is the conversion target
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