{-# 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
    -- introduce new types first
    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)
    -- then process other type declarations
    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 -- 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 <- 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
    -- convert post-conditions
    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))
    -- convert syncs
    [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)
    -- build new act
    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))
    -- convert syncs
    [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
--  (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 (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 -- simplification, assuming no conversion to tagged-elems yet
                    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 -- simplification, as above
                    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 -- simplification, as above
                    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) 

-- 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' forall a. Eq a => a -> a -> Bool
== Type
ty then 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 -> 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) -- rule INT -> BOOL
                          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

-- | 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)  -> 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