{-# LANGUAGE CPP #-}
module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where

-- The code here is based on the paper:
-- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich.
-- Practical type inference for arbitrary-rank types.
-- 14 September 2011

import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.Lockfield
import GF.Compile.Compute.Concrete
import GF.Compile.Compute.Predef(predef,predefName)
import GF.Infra.CheckM
import GF.Data.Operations
import Control.Applicative(Applicative(..))
import Control.Monad(ap,liftM,mplus)
import GF.Text.Pretty
import Data.List (nub, (\\), tails)
import qualified Data.IntMap as IntMap
import Data.Maybe(fromMaybe,isNothing)
import qualified Control.Monad.Fail as Fail

checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type)
checkLType :: GlobalEnv -> Term -> Term -> Check (Term, Term)
checkLType GlobalEnv
ge Term
t Term
ty = TcM (Term, Term) -> Check (Term, Term)
forall a. TcM a -> Check a
runTcM (TcM (Term, Term) -> Check (Term, Term))
-> TcM (Term, Term) -> Check (Term, Term)
forall a b. (a -> b) -> a -> b
$ do
  Value
vty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge [] Term
ty)
  (Term
t,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge [] Term
t (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vty)
  Term
t <- Term -> TcM Term
zonkTerm Term
t
  (Term, Term) -> TcM (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t,Term
ty)

inferLType :: GlobalEnv -> Term -> Check (Term, Type)
inferLType :: GlobalEnv -> Term -> Check (Term, Term)
inferLType GlobalEnv
ge Term
t = TcM (Term, Term) -> Check (Term, Term)
forall a. TcM a -> Check a
runTcM (TcM (Term, Term) -> Check (Term, Term))
-> TcM (Term, Term) -> Check (Term, Term)
forall a b. (a -> b) -> a -> b
$ do
  (Term
t,Value
ty) <- GlobalEnv -> Env -> Term -> TcM (Term, Value)
inferSigma GlobalEnv
ge [] Term
t
  Term
t  <- Term -> TcM Term
zonkTerm Term
t
  Term
ty <- Term -> TcM Term
zonkTerm (Term -> TcM Term) -> TcM Term -> TcM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) [] Value
ty
  (Term, Term) -> TcM (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t,Term
ty)

inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma)
inferSigma :: GlobalEnv -> Env -> Term -> TcM (Term, Value)
inferSigma GlobalEnv
ge Env
scope Term
t = do                                      -- GEN1
  (Term
t,Value
ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t Maybe Value
forall a. Maybe a
Nothing
  [MetaId]
env_tvs <- GLocation -> [(Env, Value)] -> TcM [MetaId]
getMetaVars (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [(Env, Value)]
forall a b. [(a, b)] -> [([(a, b)], b)]
scopeTypes Env
scope)
  [MetaId]
res_tvs <- GLocation -> [(Env, Value)] -> TcM [MetaId]
getMetaVars (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) [(Env
scope,Value
ty)]
  let forall_tvs :: [MetaId]
forall_tvs = [MetaId]
res_tvs [MetaId] -> [MetaId] -> [MetaId]
forall a. Eq a => [a] -> [a] -> [a]
\\ [MetaId]
env_tvs
  GlobalEnv -> Env -> Term -> [MetaId] -> Value -> TcM (Term, Value)
quantify GlobalEnv
ge Env
scope Term
t [MetaId]
forall_tvs Value
ty

Just Value
vtypeInt   = (Predefined -> Value) -> Maybe Predefined -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Predefined -> [Value] -> Value) -> [Value] -> Predefined -> Value
forall a b c. (a -> b -> c) -> b -> a -> c
flip Predefined -> [Value] -> Value
VApp []) (Ident -> Maybe Predefined
forall (m :: * -> *). MonadFail m => Ident -> m Predefined
predef Ident
cInt)
Just Value
vtypeFloat = (Predefined -> Value) -> Maybe Predefined -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Predefined -> [Value] -> Value) -> [Value] -> Predefined -> Value
forall a b c. (a -> b -> c) -> b -> a -> c
flip Predefined -> [Value] -> Value
VApp []) (Ident -> Maybe Predefined
forall (m :: * -> *). MonadFail m => Ident -> m Predefined
predef Ident
cFloat)
Just MetaId -> Value
vtypeInts  = (Predefined -> MetaId -> Value)
-> Maybe Predefined -> Maybe (MetaId -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Predefined
p MetaId
i -> Predefined -> [Value] -> Value
VApp Predefined
p [MetaId -> Value
VInt MetaId
i]) (Ident -> Maybe Predefined
forall (m :: * -> *). MonadFail m => Ident -> m Predefined
predef Ident
cInts)
vtypeStr :: Value
vtypeStr   = Ident -> Value
VSort Ident
cStr
vtypeStrs :: Value
vtypeStrs  = Ident -> Value
VSort Ident
cStrs
vtypeType :: Value
vtypeType  = Ident -> Value
VSort Ident
cType
vtypePType :: Value
vtypePType = Ident -> Value
VSort Ident
cPType

tcRho :: GlobalEnv -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho)
tcRho :: GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope t :: Term
t@(EInt MetaId
i)   Maybe Value
mb_ty = GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t (MetaId -> Value
vtypeInts MetaId
i) Maybe Value
mb_ty -- INT
tcRho GlobalEnv
ge Env
scope t :: Term
t@(EFloat Double
_) Maybe Value
mb_ty = GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
vtypeFloat Maybe Value
mb_ty    -- FLOAT
tcRho GlobalEnv
ge Env
scope t :: Term
t@(K String
_)      Maybe Value
mb_ty = GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
vtypeStr   Maybe Value
mb_ty    -- STR
tcRho GlobalEnv
ge Env
scope t :: Term
t@(Term
Empty)    Maybe Value
mb_ty = GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
vtypeStr   Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope t :: Term
t@(Vr Ident
v)     Maybe Value
mb_ty = do                          -- VAR
  case Ident -> Env -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
v Env
scope of
    Just Value
v_sigma -> GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
v_sigma Maybe Value
mb_ty
    Maybe Value
Nothing      -> Message -> TcM (Term, Value)
forall a. Message -> TcM a
tcError (String
"Unknown variable" String -> Ident -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> Ident
v)
tcRho GlobalEnv
ge Env
scope t :: Term
t@(Q QIdent
id)     Maybe Value
mb_ty =
  ([(Term, Term)] -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value) -> TcM (Term, Value)
forall x a. ([x] -> TcM a) -> TcA x a -> TcM a
runTcA (Term -> [(Term, Term)] -> TcM (Term, Value)
forall a a a. Pretty a => a -> [(a, Term)] -> TcM a
tcOverloadFailed Term
t) (TcA (Term, Term) (Term, Value) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value) -> TcM (Term, Value)
forall a b. (a -> b) -> a -> b
$
    GlobalEnv -> Env -> Term -> TcA (Term, Term) (Term, Value)
tcApp GlobalEnv
ge Env
scope Term
t TcA (Term, Term) (Term, Value)
-> ((Term, Value) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value)
forall x a b. TcA x a -> (a -> TcM b) -> TcA x b
`bindTcA` \(Term
t,Value
ty) ->
      GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
ty Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope t :: Term
t@(QC QIdent
id)    Maybe Value
mb_ty =
  ([(Term, Term)] -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value) -> TcM (Term, Value)
forall x a. ([x] -> TcM a) -> TcA x a -> TcM a
runTcA (Term -> [(Term, Term)] -> TcM (Term, Value)
forall a a a. Pretty a => a -> [(a, Term)] -> TcM a
tcOverloadFailed Term
t) (TcA (Term, Term) (Term, Value) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value) -> TcM (Term, Value)
forall a b. (a -> b) -> a -> b
$
    GlobalEnv -> Env -> Term -> TcA (Term, Term) (Term, Value)
tcApp GlobalEnv
ge Env
scope Term
t TcA (Term, Term) (Term, Value)
-> ((Term, Value) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value)
forall x a b. TcA x a -> (a -> TcM b) -> TcA x b
`bindTcA` \(Term
t,Value
ty) ->
      GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
ty Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope t :: Term
t@(App Term
fun Term
arg) Maybe Value
mb_ty = do
  ([(Term, Term)] -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value) -> TcM (Term, Value)
forall x a. ([x] -> TcM a) -> TcA x a -> TcM a
runTcA (Term -> [(Term, Term)] -> TcM (Term, Value)
forall a a a. Pretty a => a -> [(a, Term)] -> TcM a
tcOverloadFailed Term
t) (TcA (Term, Term) (Term, Value) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value) -> TcM (Term, Value)
forall a b. (a -> b) -> a -> b
$
    GlobalEnv -> Env -> Term -> TcA (Term, Term) (Term, Value)
tcApp GlobalEnv
ge Env
scope Term
t TcA (Term, Term) (Term, Value)
-> ((Term, Value) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value)
forall x a b. TcA x a -> (a -> TcM b) -> TcA x b
`bindTcA` \(Term
t,Value
ty) ->
      GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
ty Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (Abs BindType
bt Ident
var Term
body) Maybe Value
Nothing = do                   -- ABS1
  MetaId
i <- Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
  let arg_ty :: Value
arg_ty = MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) []
  (Term
body,Value
body_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge ((Ident
var,Value
arg_ty)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) Term
body Maybe Value
forall a. Maybe a
Nothing
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType -> Ident -> Term -> Term
Abs BindType
bt Ident
var Term
body, (BindType -> Value -> Ident -> Binding -> Value
VProd BindType
bt Value
arg_ty Ident
identW ((Value -> Value) -> Binding
forall a. (a -> Value) -> Bind a
Bind (Value -> Value -> Value
forall a b. a -> b -> a
const Value
body_ty))))
tcRho GlobalEnv
ge Env
scope t :: Term
t@(Abs BindType
Implicit Ident
var Term
body) (Just Value
ty) = do         -- ABS2
  (BindType
bt, Value
var_ty, Value -> Value
body_ty) <- GlobalEnv -> Env -> Value -> TcM (BindType, Value, Value -> Value)
unifyFun GlobalEnv
ge Env
scope Value
ty
  if BindType
bt BindType -> BindType -> Bool
forall a. Eq a => a -> a -> Bool
== BindType
Implicit
    then () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else Message -> TcM ()
forall a. Message -> TcM a
tcError (TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
t Message -> String -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> String
"is an implicit function, but no implicit function is expected")
  (Term
body, Value
body_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge ((Ident
var,Value
var_ty)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) Term
body (Value -> Maybe Value
forall a. a -> Maybe a
Just (Value -> Value
body_ty (MetaId -> [Value] -> Value
VGen (Env -> MetaId
forall (t :: * -> *) a. Foldable t => t a -> MetaId
length Env
scope) [])))
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType -> Ident -> Term -> Term
Abs BindType
Implicit Ident
var Term
body,Value
ty)
tcRho GlobalEnv
ge Env
scope (Abs BindType
Explicit Ident
var Term
body) (Just Value
ty) = do           -- ABS3
  (Env
scope,Term -> Term
f,Value
ty') <- GlobalEnv -> Env -> Value -> TcM (Env, Term -> Term, Value)
skolemise GlobalEnv
ge Env
scope Value
ty
  (BindType
_,Value
var_ty,Value -> Value
body_ty) <- GlobalEnv -> Env -> Value -> TcM (BindType, Value, Value -> Value)
unifyFun GlobalEnv
ge Env
scope Value
ty'
  (Term
body, Value
body_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge ((Ident
var,Value
var_ty)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) Term
body (Value -> Maybe Value
forall a. a -> Maybe a
Just (Value -> Value
body_ty (MetaId -> [Value] -> Value
VGen (Env -> MetaId
forall (t :: * -> *) a. Foldable t => t a -> MetaId
length Env
scope) [])))
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
f (BindType -> Ident -> Term -> Term
Abs BindType
Explicit Ident
var Term
body),Value
ty)
tcRho GlobalEnv
ge Env
scope (Let (Ident
var, (Maybe Term
mb_ann_ty, Term
rhs)) Term
body) Maybe Value
mb_ty = do    -- LET
  (Term
rhs,Value
var_ty) <- case Maybe Term
mb_ann_ty of
                    Maybe Term
Nothing     -> GlobalEnv -> Env -> Term -> TcM (Term, Value)
inferSigma GlobalEnv
ge Env
scope Term
rhs
                    Just Term
ann_ty -> do (Term
ann_ty, Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
ann_ty (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
                                      Value
v_ann_ty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) Term
ann_ty)
                                      (Term
rhs,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
rhs (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
v_ann_ty)
                                      (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
rhs, Value
v_ann_ty)
  (Term
body, Value
body_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge ((Ident
var,Value
var_ty)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) Term
body Maybe Value
mb_ty
  Term
var_ty <- GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
var_ty
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ident, (Maybe Term, Term)) -> Term -> Term
Let (Ident
var, (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
var_ty, Term
rhs)) Term
body, Value
body_ty)
tcRho GlobalEnv
ge Env
scope (Typed Term
body Term
ann_ty) Maybe Value
mb_ty = do                   -- ANNOT
  (Term
ann_ty, Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
ann_ty (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
  Value
v_ann_ty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) Term
ann_ty)
  (Term
body,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
body (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
v_ann_ty)
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (Term -> Term -> Term
Typed Term
body Term
ann_ty) Value
v_ann_ty Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (FV [Term]
ts) Maybe Value
mb_ty = do
  case [Term]
ts of
    []     -> do MetaId
i <- Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
                 GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope ([Term] -> Term
FV []) (MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) []) Maybe Value
mb_ty
    (Term
t:[Term]
ts) -> do (Term
t,Value
ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t Maybe Value
mb_ty

                 let go :: [Term] -> Value -> TcM ([Term], Value)
go []     Value
ty = ([Term], Value) -> TcM ([Term], Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ([],Value
ty)
                     go (Term
t:[Term]
ts) Value
ty = do (Term
t, Value
ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
ty)
                                       ([Term]
ts,Value
ty) <- [Term] -> Value -> TcM ([Term], Value)
go [Term]
ts Value
ty
                                       ([Term], Value) -> TcM ([Term], Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
ts,Value
ty)

                 ([Term]
ts,Value
ty) <- [Term] -> Value -> TcM ([Term], Value)
go [Term]
ts Value
ty
                 (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> Term
FV (Term
tTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
ts), Value
ty)
tcRho GlobalEnv
ge Env
scope t :: Term
t@(Sort Ident
s) Maybe Value
mb_ty = do
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
vtypeType Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope t :: Term
t@(RecType [Labelling]
rs) Maybe Value
Nothing   = do
  ([Labelling]
rs,Maybe Value
mb_ty) <- GlobalEnv
-> Env
-> [Labelling]
-> Maybe Value
-> TcM ([Labelling], Maybe Value)
forall a.
Pretty a =>
GlobalEnv
-> Env
-> [(a, Term)]
-> Maybe Value
-> TcM ([(a, Term)], Maybe Value)
tcRecTypeFields GlobalEnv
ge Env
scope [Labelling]
rs Maybe Value
forall a. Maybe a
Nothing
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Labelling] -> Term
RecType [Labelling]
rs,Value -> Maybe Value -> Value
forall a. a -> Maybe a -> a
fromMaybe Value
vtypePType Maybe Value
mb_ty)
tcRho GlobalEnv
ge Env
scope t :: Term
t@(RecType [Labelling]
rs) (Just Value
ty) = do
  (Env
scope,Term -> Term
f,Value
ty') <- GlobalEnv -> Env -> Value -> TcM (Env, Term -> Term, Value)
skolemise GlobalEnv
ge Env
scope Value
ty
  case Value
ty' of
    VSort Ident
s
      | Ident
s Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cType  -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Ident
s Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cPType -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    VMeta MetaId
i Env
env [Value]
vs  -> case [Labelling]
rs of
                         [] -> GlobalEnv -> Env -> MetaId -> Env -> [Value] -> Value -> TcM ()
unifyVar GlobalEnv
ge Env
scope MetaId
i Env
env [Value]
vs Value
vtypePType
                         [Labelling]
_  -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Value
ty              -> do Term
ty <- Term -> TcM Term
zonkTerm (Term -> TcM Term) -> TcM Term -> TcM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
ty
                          Message -> TcM ()
forall a. Message -> TcM a
tcError (String
"The record type" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
t Message -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
$$
                                   String
"cannot be of type" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
ty)
  ([Labelling]
rs,Maybe Value
mb_ty) <- GlobalEnv
-> Env
-> [Labelling]
-> Maybe Value
-> TcM ([Labelling], Maybe Value)
forall a.
Pretty a =>
GlobalEnv
-> Env
-> [(a, Term)]
-> Maybe Value
-> TcM ([(a, Term)], Maybe Value)
tcRecTypeFields GlobalEnv
ge Env
scope [Labelling]
rs (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
ty')
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
f ([Labelling] -> Term
RecType [Labelling]
rs),Value
ty)
tcRho GlobalEnv
ge Env
scope t :: Term
t@(Table Term
p Term
res) Maybe Value
mb_ty = do
  (Term
p,  Value
p_ty)   <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
p   (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypePType)
  (Term
res,Value
res_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
res (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (Term -> Term -> Term
Table Term
p Term
res) Value
vtypeType Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (Prod BindType
bt Ident
x Term
ty1 Term
ty2) Maybe Value
mb_ty = do
  (Term
ty1,Value
ty1_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
ty1 (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
  Value
vty1 <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) Term
ty1)
  (Term
ty2,Value
ty2_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge ((Ident
x,Value
vty1)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) Term
ty2 (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (BindType -> Ident -> Term -> Term -> Term
Prod BindType
bt Ident
x Term
ty1 Term
ty2) Value
vtypeType Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (S Term
t Term
p) Maybe Value
mb_ty = do
  Value
p_ty   <- (MetaId -> Value) -> TcM MetaId -> TcM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\MetaId
i -> MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) []) (TcM MetaId -> TcM Value) -> TcM MetaId -> TcM Value
forall a b. (a -> b) -> a -> b
$ Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypePType
  Value
res_ty <- case Maybe Value
mb_ty of
              Maybe Value
Nothing -> (MetaId -> Value) -> TcM MetaId -> TcM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\MetaId
i -> MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) []) (TcM MetaId -> TcM Value) -> TcM MetaId -> TcM Value
forall a b. (a -> b) -> a -> b
$ Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
              Just Value
ty -> Value -> TcM Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
ty
  let t_ty :: Value
t_ty = Value -> Value -> Value
VTblType Value
p_ty Value
res_ty
  (Term
t,Value
t_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
t_ty)
  (Term
p,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
p (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
p_ty)
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
S Term
t Term
p, Value
res_ty)
tcRho GlobalEnv
ge Env
scope (T TInfo
tt [Case]
ps) Maybe Value
Nothing = do                           -- ABS1/AABS1 for tables
  Value
p_ty   <- case TInfo
tt of
              TInfo
TRaw      -> (MetaId -> Value) -> TcM MetaId -> TcM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\MetaId
i -> MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) []) (TcM MetaId -> TcM Value) -> TcM MetaId -> TcM Value
forall a b. (a -> b) -> a -> b
$ Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypePType
              TTyped Term
ty -> do (Term
ty, Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
ty (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
                              Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) Term
ty)
  ([Case]
ps,Maybe Value
mb_res_ty) <- GlobalEnv
-> Env
-> [Case]
-> Value
-> Maybe Value
-> TcM ([Case], Maybe Value)
tcCases GlobalEnv
ge Env
scope [Case]
ps Value
p_ty Maybe Value
forall a. Maybe a
Nothing
  Value
res_ty <- case Maybe Value
mb_res_ty of
              Just Value
res_ty -> Value -> TcM Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
res_ty
              Maybe Value
Nothing     -> (MetaId -> Value) -> TcM MetaId -> TcM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\MetaId
i -> MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) []) (TcM MetaId -> TcM Value) -> TcM MetaId -> TcM Value
forall a b. (a -> b) -> a -> b
$ Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
  Term
p_ty_t <- GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) [] Value
p_ty
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (TInfo -> [Case] -> Term
T (Term -> TInfo
TTyped Term
p_ty_t) [Case]
ps, Value -> Value -> Value
VTblType Value
p_ty Value
res_ty)
tcRho GlobalEnv
ge Env
scope (T TInfo
tt [Case]
ps) (Just Value
ty) = do                         -- ABS2/AABS2 for tables
  (Env
scope,Term -> Term
f,Value
ty') <- GlobalEnv -> Env -> Value -> TcM (Env, Term -> Term, Value)
skolemise GlobalEnv
ge Env
scope Value
ty
  (Value
p_ty, Value
res_ty) <- GlobalEnv -> Env -> Value -> TcM (Value, Value)
unifyTbl GlobalEnv
ge Env
scope Value
ty'
  case TInfo
tt of
    TInfo
TRaw      -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    TTyped Term
ty -> do (Term
ty, Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
ty (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
                    () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()--subsCheckRho ge scope -> Term ty res_ty
  ([Case]
ps,Just Value
res_ty) <- GlobalEnv
-> Env
-> [Case]
-> Value
-> Maybe Value
-> TcM ([Case], Maybe Value)
tcCases GlobalEnv
ge Env
scope [Case]
ps Value
p_ty (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
res_ty)
  Term
p_ty_t <- GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) [] Value
p_ty
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
f (TInfo -> [Case] -> Term
T (Term -> TInfo
TTyped Term
p_ty_t) [Case]
ps), Value -> Value -> Value
VTblType Value
p_ty Value
res_ty)
tcRho GlobalEnv
ge Env
scope (R [Assign]
rs) Maybe Value
Nothing = do
  [(Label, Term, Value)]
lttys <- GlobalEnv -> Env -> [Assign] -> TcM [(Label, Term, Value)]
forall (t :: * -> *) a.
Traversable t =>
GlobalEnv
-> Env -> t (a, (Maybe Term, Term)) -> TcM (t (a, Term, Value))
inferRecFields GlobalEnv
ge Env
scope [Assign]
rs
  [Assign]
rs <- ((Label, Term, Value) -> TcM Assign)
-> [(Label, Term, Value)] -> TcM [Assign]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Label
l,Term
t,Value
ty) -> GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
ty TcM Term -> (Term -> TcM Assign) -> TcM Assign
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Term
ty -> Assign -> TcM Assign
forall (m :: * -> *) a. Monad m => a -> m a
return (Label
l, (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
ty, Term
t))) [(Label, Term, Value)]
lttys
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Assign] -> Term
R        [Assign]
rs,
          [(Label, Value)] -> Value
VRecType [(Label
l, Value
ty) | (Label
l,Term
t,Value
ty) <- [(Label, Term, Value)]
lttys]
         )
tcRho GlobalEnv
ge Env
scope (R [Assign]
rs) (Just Value
ty) = do
  (Env
scope,Term -> Term
f,Value
ty') <- GlobalEnv -> Env -> Value -> TcM (Env, Term -> Term, Value)
skolemise GlobalEnv
ge Env
scope Value
ty
  case Value
ty' of
    (VRecType [(Label, Value)]
ltys) -> do [(Label, Term, Value)]
lttys <- GlobalEnv
-> Env
-> [Assign]
-> [(Label, Value)]
-> TcM [(Label, Term, Value)]
forall a.
(Pretty a, Eq a) =>
GlobalEnv
-> Env
-> [(a, (Maybe Term, Term))]
-> [(a, Value)]
-> TcM [(a, Term, Value)]
checkRecFields GlobalEnv
ge Env
scope [Assign]
rs [(Label, Value)]
ltys
                          [Assign]
rs <- ((Label, Term, Value) -> TcM Assign)
-> [(Label, Term, Value)] -> TcM [Assign]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Label
l,Term
t,Value
ty) -> GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
ty TcM Term -> (Term -> TcM Assign) -> TcM Assign
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Term
ty -> Assign -> TcM Assign
forall (m :: * -> *) a. Monad m => a -> m a
return (Label
l, (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
ty, Term
t))) [(Label, Term, Value)]
lttys
                          (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> Term
f (Term -> Term) -> ([Assign] -> Term) -> [Assign] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Assign] -> Term
R)  [Assign]
rs,
                                  [(Label, Value)] -> Value
VRecType [(Label
l, Value
ty) | (Label
l,Term
t,Value
ty) <- [(Label, Term, Value)]
lttys]
                                 )
    Value
ty              -> do [(Label, Term, Value)]
lttys <- GlobalEnv -> Env -> [Assign] -> TcM [(Label, Term, Value)]
forall (t :: * -> *) a.
Traversable t =>
GlobalEnv
-> Env -> t (a, (Maybe Term, Term)) -> TcM (t (a, Term, Value))
inferRecFields GlobalEnv
ge Env
scope [Assign]
rs
                          Term
t <- ([Assign] -> Term) -> TcM [Assign] -> TcM Term
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Term -> Term
f (Term -> Term) -> ([Assign] -> Term) -> [Assign] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Assign] -> Term
R) (((Label, Term, Value) -> TcM Assign)
-> [(Label, Term, Value)] -> TcM [Assign]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Label
l,Term
t,Value
ty) -> GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
ty TcM Term -> (Term -> TcM Assign) -> TcM Assign
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Term
ty -> Assign -> TcM Assign
forall (m :: * -> *) a. Monad m => a -> m a
return (Label
l, (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
ty, Term
t))) [(Label, Term, Value)]
lttys)
                          let ty' :: Value
ty' = [(Label, Value)] -> Value
VRecType [(Label
l, Value
ty) | (Label
l,Term
t,Value
ty) <- [(Label, Term, Value)]
lttys]
                          Term
t <- GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
ty' Value
ty
                          (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t, Value
ty')
tcRho GlobalEnv
ge Env
scope (P Term
t Label
l) Maybe Value
mb_ty = do
  Value
l_ty   <- case Maybe Value
mb_ty of
              Just Value
ty -> Value -> TcM Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
ty
              Maybe Value
Nothing -> do MetaId
i <- Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
                            Value -> TcM Value
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) [])
  (Term
t,Value
t_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t (Value -> Maybe Value
forall a. a -> Maybe a
Just ([(Label, Value)] -> Value
VRecType [(Label
l,Value
l_ty)]))
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Label -> Term
P Term
t Label
l,Value
l_ty)
tcRho GlobalEnv
ge Env
scope (C Term
t1 Term
t2) Maybe Value
mb_ty = do
  (Term
t1,Value
t1_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t1 (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeStr)
  (Term
t2,Value
t2_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t2 (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeStr)
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (Term -> Term -> Term
C Term
t1 Term
t2) Value
vtypeStr Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (Glue Term
t1 Term
t2) Maybe Value
mb_ty = do
  (Term
t1,Value
t1_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t1 (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeStr)
  (Term
t2,Value
t2_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t2 (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeStr)
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (Term -> Term -> Term
Glue Term
t1 Term
t2) Value
vtypeStr Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope t :: Term
t@(ExtR Term
t1 Term
t2) Maybe Value
mb_ty = do
  (Term
t1,Value
t1_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t1 Maybe Value
forall a. Maybe a
Nothing
  (Term
t2,Value
t2_ty) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t2 Maybe Value
forall a. Maybe a
Nothing
  case (Value
t1_ty,Value
t2_ty) of
    (VSort Ident
s1,VSort Ident
s2)
       | (Ident
s1 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cType Bool -> Bool -> Bool
|| Ident
s1 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cPType) Bool -> Bool -> Bool
&&
         (Ident
s2 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cType Bool -> Bool -> Bool
|| Ident
s2 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cPType) -> let sort :: Ident
sort | Ident
s1 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cPType Bool -> Bool -> Bool
&& Ident
s2 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cPType = Ident
cPType
                                                   | Bool
otherwise                    = Ident
cType
                                          in GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (Term -> Term -> Term
ExtR Term
t1 Term
t2) (Ident -> Value
VSort Ident
sort) Maybe Value
mb_ty
    (VRecType [(Label, Value)]
rs1, VRecType [(Label, Value)]
rs2)       -> GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (Term -> Term -> Term
ExtR Term
t1 Term
t2) ([(Label, Value)] -> Value
VRecType ([(Label, Value)]
rs2[(Label, Value)] -> [(Label, Value)] -> [(Label, Value)]
forall a. [a] -> [a] -> [a]
++[(Label, Value)]
rs1)) Maybe Value
mb_ty
    (Value, Value)
_                                  -> Message -> TcM (Term, Value)
forall a. Message -> TcM a
tcError (String
"Cannot type check" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
t)
tcRho GlobalEnv
ge Env
scope (ELin Ident
cat Term
t) Maybe Value
mb_ty = do  -- this could be done earlier, i.e. in the parser
  GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope (Term -> Term -> Term
ExtR Term
t ([Assign] -> Term
R [(Ident -> Label
lockLabel Ident
cat,(Term -> Maybe Term
forall a. a -> Maybe a
Just ([Labelling] -> Term
RecType []),[Assign] -> Term
R []))])) Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (ELincat Ident
cat Term
t) Maybe Value
mb_ty = do  -- this could be done earlier, i.e. in the parser
  GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope (Term -> Term -> Term
ExtR Term
t ([Labelling] -> Term
RecType [(Ident -> Label
lockLabel Ident
cat,[Labelling] -> Term
RecType [])])) Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (Alts Term
t [(Term, Term)]
ss) Maybe Value
mb_ty = do
  (Term
t,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeStr)
  [(Term, Term)]
ss    <- (((Term, Term) -> TcM (Term, Term))
 -> [(Term, Term)] -> TcM [(Term, Term)])
-> [(Term, Term)]
-> ((Term, Term) -> TcM (Term, Term))
-> TcM [(Term, Term)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Term, Term) -> TcM (Term, Term))
-> [(Term, Term)] -> TcM [(Term, Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [(Term, Term)]
ss (((Term, Term) -> TcM (Term, Term)) -> TcM [(Term, Term)])
-> ((Term, Term) -> TcM (Term, Term)) -> TcM [(Term, Term)]
forall a b. (a -> b) -> a -> b
$ \(Term
t1,Term
t2) -> do
              (Term
t1,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t1 (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeStr)
              (Term
t2,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t2 (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeStrs)
              (Term, Term) -> TcM (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t1,Term
t2)
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (Term -> [(Term, Term)] -> Term
Alts Term
t [(Term, Term)]
ss) Value
vtypeStr Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (Strs [Term]
ss) Maybe Value
mb_ty = do
  [Term]
ss <- ((Term -> TcM Term) -> [Term] -> TcM [Term])
-> [Term] -> (Term -> TcM Term) -> TcM [Term]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Term -> TcM Term) -> [Term] -> TcM [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [Term]
ss ((Term -> TcM Term) -> TcM [Term])
-> (Term -> TcM Term) -> TcM [Term]
forall a b. (a -> b) -> a -> b
$ \Term
t -> do
           (Term
t,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeStr)
           Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope ([Term] -> Term
Strs [Term]
ss) Value
vtypeStrs Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope (EPattType Term
ty) Maybe Value
mb_ty = do
  (Term
ty, Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
ty (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
  GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope (Term -> Term
EPattType Term
ty) Value
vtypeType Maybe Value
mb_ty
tcRho GlobalEnv
ge Env
scope t :: Term
t@(EPatt Patt
p) Maybe Value
mb_ty = do
  (Env
scope,Term -> Term
f,Value
ty) <- case Maybe Value
mb_ty of
                    Maybe Value
Nothing -> do MetaId
i <- Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
                                  (Env, Term -> Term, Value) -> TcM (Env, Term -> Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope,Term -> Term
forall a. a -> a
id,MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) [])
                    Just Value
ty -> do (Env
scope,Term -> Term
f,Value
ty) <- GlobalEnv -> Env -> Value -> TcM (Env, Term -> Term, Value)
skolemise GlobalEnv
ge Env
scope Value
ty
                                  case Value
ty of
                                    VPattType Value
ty -> (Env, Term -> Term, Value) -> TcM (Env, Term -> Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope,Term -> Term
f,Value
ty)
                                    Value
_            -> Message -> TcM (Env, Term -> Term, Value)
forall a. Message -> TcM a
tcError (TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
t Message -> String -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> String
"must be of pattern type but" Message -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
t Message -> String -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> String
"is expected")
  GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
p Value
ty
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
f (Patt -> Term
EPatt Patt
p), Value
ty)
tcRho GlobalEnv
gr Env
scope Term
t Maybe Value
_ = String -> TcM (Term, Value)
forall (m :: * -> *) a. MonadFail m => String -> m a
unimplemented (String
"tcRho "String -> String -> String
forall a. [a] -> [a] -> [a]
++Term -> String
forall a. Show a => a -> String
show Term
t)

tcCases :: GlobalEnv
-> Env
-> [Case]
-> Value
-> Maybe Value
-> TcM ([Case], Maybe Value)
tcCases GlobalEnv
ge Env
scope []         Value
p_ty Maybe Value
mb_res_ty = ([Case], Maybe Value) -> TcM ([Case], Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ([],Maybe Value
mb_res_ty)
tcCases GlobalEnv
ge Env
scope ((Patt
p,Term
t):[Case]
cs) Value
p_ty Maybe Value
mb_res_ty = do
  Env
scope' <- GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
p Value
p_ty
  (Term
t,Value
res_ty)     <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope' Term
t Maybe Value
mb_res_ty
  ([Case]
cs,Maybe Value
mb_res_ty) <- GlobalEnv
-> Env
-> [Case]
-> Value
-> Maybe Value
-> TcM ([Case], Maybe Value)
tcCases GlobalEnv
ge Env
scope [Case]
cs Value
p_ty (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
res_ty)
  ([Case], Maybe Value) -> TcM ([Case], Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Patt
p,Term
t)Case -> [Case] -> [Case]
forall a. a -> [a] -> [a]
:[Case]
cs,Maybe Value
mb_res_ty)


tcApp :: GlobalEnv -> Env -> Term -> TcA (Term, Term) (Term, Value)
tcApp GlobalEnv
ge Env
scope t :: Term
t@(App Term
fun (ImplArg Term
arg)) = do                   -- APP1
  GlobalEnv -> Env -> Term -> TcA (Term, Term) (Term, Value)
tcApp GlobalEnv
ge Env
scope Term
fun TcA (Term, Term) (Term, Value)
-> ((Term, Value) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value)
forall x a b. TcA x a -> (a -> TcM b) -> TcA x b
`bindTcA` \(Term
fun,Value
fun_ty) ->
     do (BindType
bt, Value
arg_ty, Value -> Value
res_ty) <- GlobalEnv -> Env -> Value -> TcM (BindType, Value, Value -> Value)
unifyFun GlobalEnv
ge Env
scope Value
fun_ty
        if (BindType
bt BindType -> BindType -> Bool
forall a. Eq a => a -> a -> Bool
== BindType
Implicit)
          then () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          else Message -> TcM ()
forall a. Message -> TcM a
tcError (TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
t Message -> String -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> String
"is an implicit argument application, but no implicit argument is expected")
        (Term
arg,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
arg (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
arg_ty)
        Value
varg <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) Term
arg)
        (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
App Term
fun (Term -> Term
ImplArg Term
arg), Value -> Value
res_ty Value
varg)
tcApp GlobalEnv
ge Env
scope (App Term
fun Term
arg) =                                  -- APP2
  GlobalEnv -> Env -> Term -> TcA (Term, Term) (Term, Value)
tcApp GlobalEnv
ge Env
scope Term
fun TcA (Term, Term) (Term, Value)
-> ((Term, Value) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value)
forall x a b. TcA x a -> (a -> TcM b) -> TcA x b
`bindTcA` \(Term
fun,Value
fun_ty) ->
     do (Term
fun,Value
fun_ty) <- Env -> Term -> Value -> TcM (Term, Value)
instantiate Env
scope Term
fun Value
fun_ty
        (BindType
_, Value
arg_ty, Value -> Value
res_ty) <- GlobalEnv -> Env -> Value -> TcM (BindType, Value, Value -> Value)
unifyFun GlobalEnv
ge Env
scope Value
fun_ty
        (Term
arg,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
arg (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
arg_ty)
        Value
varg <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) Term
arg)
        (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Term
App Term
fun Term
arg, Value -> Value
res_ty Value
varg)
tcApp GlobalEnv
ge Env
scope (Q QIdent
id) =                                          -- VAR (global)
  Err [(Term, Term)] -> TcA (Term, Term) (Term, Term)
forall a. Err [a] -> TcA a a
mkTcA (Grammar -> QIdent -> Err [(Term, Term)]
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m [(Term, Term)]
lookupOverloadTypes (GlobalEnv -> Grammar
geGrammar GlobalEnv
ge) QIdent
id) TcA (Term, Term) (Term, Term)
-> ((Term, Term) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value)
forall x a b. TcA x a -> (a -> TcM b) -> TcA x b
`bindTcA` \(Term
t,Term
ty) ->
     do Value
ty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge [] Term
ty)
        (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t,Value
ty)
tcApp GlobalEnv
ge Env
scope (QC QIdent
id) =                                         -- VAR (global)
  Err [(Term, Term)] -> TcA (Term, Term) (Term, Term)
forall a. Err [a] -> TcA a a
mkTcA (Grammar -> QIdent -> Err [(Term, Term)]
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m [(Term, Term)]
lookupOverloadTypes (GlobalEnv -> Grammar
geGrammar GlobalEnv
ge) QIdent
id) TcA (Term, Term) (Term, Term)
-> ((Term, Term) -> TcM (Term, Value))
-> TcA (Term, Term) (Term, Value)
forall x a b. TcA x a -> (a -> TcM b) -> TcA x b
`bindTcA` \(Term
t,Term
ty) ->
     do Value
ty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge [] Term
ty)
        (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t,Value
ty)
tcApp GlobalEnv
ge Env
scope Term
t =
  TcM (Term, Value) -> TcA (Term, Term) (Term, Value)
forall a x. TcM a -> TcA x a
singleTcA (GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t Maybe Value
forall a. Maybe a
Nothing)


tcOverloadFailed :: a -> [(a, Term)] -> TcM a
tcOverloadFailed a
t [(a, Term)]
ttys =
  Message -> TcM a
forall a. Message -> TcM a
tcError (String
"Overload resolution failed" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
$$
           String
"of term   " String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> a -> Message
forall a. Pretty a => a -> Message
pp a
t Message -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
$$
           String
"with types" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> [Message] -> Message
forall a. Pretty a => [a] -> Message
vcat [TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Terse Integer
0 Term
ty | (a
_,Term
ty) <- [(a, Term)]
ttys])


tcPatt :: GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
PW        Value
ty0 =
  Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
tcPatt GlobalEnv
ge Env
scope (PV Ident
x)    Value
ty0 =
  Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ident
x,Value
ty0)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope)
tcPatt GlobalEnv
ge Env
scope (PP QIdent
c [Patt]
ps) Value
ty0 =
  case Grammar -> QIdent -> Err Term
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Term
lookupResType (GlobalEnv -> Grammar
geGrammar GlobalEnv
ge) QIdent
c of
    Ok Term
ty  -> do let go :: Env -> Value -> [Patt] -> TcM (Env, Value)
go Env
scope Value
ty []     = (Env, Value) -> TcM (Env, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope,Value
ty)
                     go Env
scope Value
ty (Patt
p:[Patt]
ps) = do (BindType
_,Value
arg_ty,Value -> Value
res_ty) <- GlobalEnv -> Env -> Value -> TcM (BindType, Value, Value -> Value)
unifyFun GlobalEnv
ge Env
scope Value
ty
                                             Env
scope <- GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
p Value
arg_ty
                                             Env -> Value -> [Patt] -> TcM (Env, Value)
go Env
scope (Value -> Value
res_ty (MetaId -> [Value] -> Value
VGen (Env -> MetaId
forall (t :: * -> *) a. Foldable t => t a -> MetaId
length Env
scope) [])) [Patt]
ps
                 Value
vty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge [] Term
ty)
                 (Env
scope,Value
ty) <- Env -> Value -> [Patt] -> TcM (Env, Value)
go Env
scope Value
vty [Patt]
ps
                 GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
ty0 Value
ty
                 Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
    Bad String
err -> Message -> TcM Env
forall a. Message -> TcM a
tcError (String -> Message
forall a. Pretty a => a -> Message
pp String
err)
tcPatt GlobalEnv
ge Env
scope (PInt MetaId
i) Value
ty0 = do
  GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope (MetaId -> Term
EInt MetaId
i) (MetaId -> Value
vtypeInts MetaId
i) Value
ty0
  Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
tcPatt GlobalEnv
ge Env
scope (PString String
s) Value
ty0 = do
  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
ty0 Value
vtypeStr
  Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
tcPatt GlobalEnv
ge Env
scope Patt
PChar Value
ty0 = do
  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
ty0 Value
vtypeStr
  Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
tcPatt GlobalEnv
ge Env
scope (PSeq Patt
p1 Patt
p2) Value
ty0 = do
  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
ty0 Value
vtypeStr
  Env
scope <- GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
p1 Value
vtypeStr
  Env
scope <- GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
p2 Value
vtypeStr
  Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
tcPatt GlobalEnv
ge Env
scope (PAs Ident
x Patt
p) Value
ty0 = do
  GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge ((Ident
x,Value
ty0)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) Patt
p Value
ty0
tcPatt GlobalEnv
ge Env
scope (PR [(Label, Patt)]
rs) Value
ty0 = do
  let mk_ltys :: [(a, b)] -> TcM [(a, b, Value)]
mk_ltys  []            = [(a, b, Value)] -> TcM [(a, b, Value)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      mk_ltys  ((a
l,b
p):[(a, b)]
rs)    = do MetaId
i <- Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypePType
                                  [(a, b, Value)]
ltys <- [(a, b)] -> TcM [(a, b, Value)]
mk_ltys [(a, b)]
rs
                                  [(a, b, Value)] -> TcM [(a, b, Value)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
l,b
p,MetaId -> Env -> [Value] -> Value
VMeta MetaId
i (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) []) (a, b, Value) -> [(a, b, Value)] -> [(a, b, Value)]
forall a. a -> [a] -> [a]
: [(a, b, Value)]
ltys)
      go :: Env -> [(a, Patt, Value)] -> TcM Env
go Env
scope []            = Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
      go Env
scope ((a
l,Patt
p,Value
ty):[(a, Patt, Value)]
rs) = do Env
scope <- GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
p Value
ty
                                  Env -> [(a, Patt, Value)] -> TcM Env
go Env
scope [(a, Patt, Value)]
rs
  [(Label, Patt, Value)]
ltys <- [(Label, Patt)] -> TcM [(Label, Patt, Value)]
forall a b. [(a, b)] -> TcM [(a, b, Value)]
mk_ltys [(Label, Patt)]
rs
  GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope (Patt -> Term
EPatt ([(Label, Patt)] -> Patt
PR [(Label, Patt)]
rs)) ([(Label, Value)] -> Value
VRecType [(Label
l,Value
ty) | (Label
l,Patt
p,Value
ty) <- [(Label, Patt, Value)]
ltys]) Value
ty0
  Env -> [(Label, Patt, Value)] -> TcM Env
forall a. Env -> [(a, Patt, Value)] -> TcM Env
go Env
scope [(Label, Patt, Value)]
ltys
tcPatt GlobalEnv
ge Env
scope (PAlt Patt
p1 Patt
p2) Value
ty0 = do
  GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
p1 Value
ty0
  GlobalEnv -> Env -> Patt -> Value -> TcM Env
tcPatt GlobalEnv
ge Env
scope Patt
p2 Value
ty0
  Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
tcPatt GlobalEnv
ge Env
scope (PM QIdent
q) Value
ty0 = do
  case Grammar -> QIdent -> Err Term
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Term
lookupResType (GlobalEnv -> Grammar
geGrammar GlobalEnv
ge) QIdent
q of
    Ok (EPattType Term
ty)
            -> do Value
vty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge [] Term
ty)
                  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
ty0 Value
vty
                  Env -> TcM Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
scope
    Ok Term
ty   -> Message -> TcM Env
forall a. Message -> TcM a
tcError (String
"Pattern type expected but " String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> Term -> Message
forall a. Pretty a => a -> Message
pp Term
ty Message -> String -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> String
" found.")
    Bad String
err -> Message -> TcM Env
forall a. Message -> TcM a
tcError (String -> Message
forall a. Pretty a => a -> Message
pp String
err)
tcPatt GlobalEnv
ge Env
scope Patt
p Value
ty = String -> TcM Env
forall (m :: * -> *) a. MonadFail m => String -> m a
unimplemented (String
"tcPatt "String -> String -> String
forall a. [a] -> [a] -> [a]
++Patt -> String
forall a. Show a => a -> String
show Patt
p)

inferRecFields :: GlobalEnv
-> Env -> t (a, (Maybe Term, Term)) -> TcM (t (a, Term, Value))
inferRecFields GlobalEnv
ge Env
scope t (a, (Maybe Term, Term))
rs =
  ((a, (Maybe Term, Term)) -> TcM (a, Term, Value))
-> t (a, (Maybe Term, Term)) -> TcM (t (a, Term, Value))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(a
l,(Maybe Term, Term)
r) -> GlobalEnv
-> Env
-> a
-> (Maybe Term, Term)
-> Maybe Value
-> TcM (a, Term, Value)
forall a.
GlobalEnv
-> Env
-> a
-> (Maybe Term, Term)
-> Maybe Value
-> TcM (a, Term, Value)
tcRecField GlobalEnv
ge Env
scope a
l (Maybe Term, Term)
r Maybe Value
forall a. Maybe a
Nothing) t (a, (Maybe Term, Term))
rs

checkRecFields :: GlobalEnv
-> Env
-> [(a, (Maybe Term, Term))]
-> [(a, Value)]
-> TcM [(a, Term, Value)]
checkRecFields GlobalEnv
ge Env
scope []          [(a, Value)]
ltys
  | [(a, Value)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(a, Value)]
ltys                            = [(a, Term, Value)] -> TcM [(a, Term, Value)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  | Bool
otherwise                            = Message -> TcM [(a, Term, Value)]
forall a. Message -> TcM a
tcError (String
"Missing fields:" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> [a] -> Message
forall a. Pretty a => [a] -> Message
hsep (((a, Value) -> a) -> [(a, Value)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Value) -> a
forall a b. (a, b) -> a
fst [(a, Value)]
ltys))
checkRecFields GlobalEnv
ge Env
scope ((a
l,(Maybe Term, Term)
t):[(a, (Maybe Term, Term))]
lts) [(a, Value)]
ltys =
  case a -> [(a, Value)] -> (Maybe Value, [(a, Value)])
forall a a. Eq a => a -> [(a, a)] -> (Maybe a, [(a, a)])
takeIt a
l [(a, Value)]
ltys of
    (Just Value
ty,[(a, Value)]
ltys) -> do (a, Term, Value)
ltty  <- GlobalEnv
-> Env
-> a
-> (Maybe Term, Term)
-> Maybe Value
-> TcM (a, Term, Value)
forall a.
GlobalEnv
-> Env
-> a
-> (Maybe Term, Term)
-> Maybe Value
-> TcM (a, Term, Value)
tcRecField GlobalEnv
ge Env
scope a
l (Maybe Term, Term)
t (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
ty)
                         [(a, Term, Value)]
lttys <- GlobalEnv
-> Env
-> [(a, (Maybe Term, Term))]
-> [(a, Value)]
-> TcM [(a, Term, Value)]
checkRecFields GlobalEnv
ge Env
scope [(a, (Maybe Term, Term))]
lts [(a, Value)]
ltys
                         [(a, Term, Value)] -> TcM [(a, Term, Value)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, Term, Value)
ltty (a, Term, Value) -> [(a, Term, Value)] -> [(a, Term, Value)]
forall a. a -> [a] -> [a]
: [(a, Term, Value)]
lttys)
    (Maybe Value
Nothing,[(a, Value)]
ltys) -> do Message -> TcM ()
tcWarn (String
"Discarded field:" String -> a -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> a
l)
                         (a, Term, Value)
ltty  <- GlobalEnv
-> Env
-> a
-> (Maybe Term, Term)
-> Maybe Value
-> TcM (a, Term, Value)
forall a.
GlobalEnv
-> Env
-> a
-> (Maybe Term, Term)
-> Maybe Value
-> TcM (a, Term, Value)
tcRecField GlobalEnv
ge Env
scope a
l (Maybe Term, Term)
t Maybe Value
forall a. Maybe a
Nothing
                         [(a, Term, Value)]
lttys <- GlobalEnv
-> Env
-> [(a, (Maybe Term, Term))]
-> [(a, Value)]
-> TcM [(a, Term, Value)]
checkRecFields GlobalEnv
ge Env
scope [(a, (Maybe Term, Term))]
lts [(a, Value)]
ltys
                         [(a, Term, Value)] -> TcM [(a, Term, Value)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(a, Term, Value)]
lttys     -- ignore the field
  where
    takeIt :: a -> [(a, a)] -> (Maybe a, [(a, a)])
takeIt a
l1 []  = (Maybe a
forall a. Maybe a
Nothing, [])
    takeIt a
l1 (lty :: (a, a)
lty@(a
l2,a
ty):[(a, a)]
ltys)
      | a
l1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
l2  = (a -> Maybe a
forall a. a -> Maybe a
Just a
ty,[(a, a)]
ltys)
      | Bool
otherwise = let (Maybe a
mb_ty,[(a, a)]
ltys') = a -> [(a, a)] -> (Maybe a, [(a, a)])
takeIt a
l1 [(a, a)]
ltys
                    in (Maybe a
mb_ty,(a, a)
lty(a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
:[(a, a)]
ltys')

tcRecField :: GlobalEnv
-> Env
-> a
-> (Maybe Term, Term)
-> Maybe Value
-> TcM (a, Term, Value)
tcRecField GlobalEnv
ge Env
scope a
l (Maybe Term
mb_ann_ty,Term
t) Maybe Value
mb_ty = do
  (Term
t,Value
ty) <- case Maybe Term
mb_ann_ty of
              Just Term
ann_ty -> do (Term
ann_ty, Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
ann_ty (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
vtypeType)
                                Value
v_ann_ty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) Term
ann_ty)
                                (Term
t,Value
_) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
v_ann_ty)
                                GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
v_ann_ty Maybe Value
mb_ty
              Maybe Term
Nothing     -> GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
t Maybe Value
mb_ty
  (a, Term, Value) -> TcM (a, Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
l,Term
t,Value
ty)

tcRecTypeFields :: GlobalEnv
-> Env
-> [(a, Term)]
-> Maybe Value
-> TcM ([(a, Term)], Maybe Value)
tcRecTypeFields GlobalEnv
ge Env
scope []          Maybe Value
mb_ty = ([(a, Term)], Maybe Value) -> TcM ([(a, Term)], Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ([],Maybe Value
mb_ty)
tcRecTypeFields GlobalEnv
ge Env
scope ((a
l,Term
ty):[(a, Term)]
rs) Maybe Value
mb_ty = do
  (Term
ty,Value
sort) <- GlobalEnv -> Env -> Term -> Maybe Value -> TcM (Term, Value)
tcRho GlobalEnv
ge Env
scope Term
ty Maybe Value
mb_ty
  Maybe Value
mb_ty <- case Value
sort of
             VSort Ident
s
               | Ident
s Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cType  -> Maybe Value -> TcM (Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
sort)
               | Ident
s Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cPType -> Maybe Value -> TcM (Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
mb_ty
             VMeta MetaId
_ Env
_ [Value]
_     -> Maybe Value -> TcM (Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
mb_ty
             Value
_               -> do Term
sort <- Term -> TcM Term
zonkTerm (Term -> TcM Term) -> TcM Term -> TcM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
sort
                                   Message -> TcM (Maybe Value)
forall a. Message -> TcM a
tcError (String
"The record type field" String -> a -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> a
l Message -> Char -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> Char
':' Message -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
ty Message -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
$$
                                            String
"cannot be of type" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
sort)
  ([(a, Term)]
rs,Maybe Value
mb_ty) <- GlobalEnv
-> Env
-> [(a, Term)]
-> Maybe Value
-> TcM ([(a, Term)], Maybe Value)
tcRecTypeFields GlobalEnv
ge Env
scope [(a, Term)]
rs Maybe Value
mb_ty
  ([(a, Term)], Maybe Value) -> TcM ([(a, Term)], Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
l,Term
ty)(a, Term) -> [(a, Term)] -> [(a, Term)]
forall a. a -> [a] -> [a]
:[(a, Term)]
rs,Maybe Value
mb_ty)

-- | Invariant: if the third argument is (Just rho),
--              then rho is in weak-prenex form
instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
instSigma :: GlobalEnv
-> Env -> Term -> Value -> Maybe Value -> TcM (Term, Value)
instSigma GlobalEnv
ge Env
scope Term
t Value
ty1 Maybe Value
Nothing    = (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t,Value
ty1)           -- INST1
instSigma GlobalEnv
ge Env
scope Term
t Value
ty1 (Just Value
ty2) = do                       -- INST2
  Term
t <- GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
ty1 Value
ty2
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t,Value
ty2)

-- | Invariant: the second argument is in weak-prenex form
subsCheckRho :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> TcM Term
subsCheckRho :: GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope Term
t ty1 :: Value
ty1@(VMeta MetaId
i Env
env [Value]
vs) Value
ty2 = do
  MetaValue
mv <- MetaId -> TcM MetaValue
getMeta MetaId
i
  case MetaValue
mv of
    Unbound Env
_ Value
_ -> do GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
ty1 Value
ty2
                      Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
    Bound Term
ty1   -> do Value
vty1 <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge Env
env Term
ty1)
                      GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope Term
t (GLocation -> Value -> [Value] -> Value
vapply (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) Value
vty1 [Value]
vs) Value
ty2
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
ty1 ty2 :: Value
ty2@(VMeta MetaId
i Env
env [Value]
vs) = do
  MetaValue
mv <- MetaId -> TcM MetaValue
getMeta MetaId
i
  case MetaValue
mv of
    Unbound Env
_ Value
_ -> do GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
ty1 Value
ty2
                      Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
    Bound Term
ty2   -> do Value
vty2 <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge Env
env Term
ty2)
                      GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
ty1 (GLocation -> Value -> [Value] -> Value
vapply (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) Value
vty2 [Value]
vs)
subsCheckRho GlobalEnv
ge Env
scope Term
t (VProd BindType
Implicit Value
ty1 Ident
x (Bind Value -> Value
ty2)) Value
rho2 = do     -- Rule SPEC
  MetaId
i <- Env -> Value -> TcM MetaId
newMeta Env
scope Value
ty1
  GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope (Term -> Term -> Term
App Term
t (Term -> Term
ImplArg (MetaId -> Term
Meta MetaId
i))) (Value -> Value
ty2 (MetaId -> Env -> [Value] -> Value
VMeta MetaId
i [] [])) Value
rho2
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
rho1 (VProd BindType
Implicit Value
ty1 Ident
x (Bind Value -> Value
ty2)) = do     -- Rule SKOL
  let v :: Ident
v = Env -> Ident
newVar Env
scope
  Term
t <- GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge ((Ident
v,Value
ty1)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) Term
t Value
rho1 (Value -> Value
ty2 (MetaId -> [Value] -> Value
VGen (Env -> MetaId
forall (t :: * -> *) a. Foldable t => t a -> MetaId
length Env
scope) []))
  Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType -> Ident -> Term -> Term
Abs BindType
Implicit Ident
v Term
t)
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
rho1 (VProd BindType
Explicit Value
a2 Ident
_ (Bind Value -> Value
r2)) = do       -- Rule FUN
  (BindType
_,Value
a1,Value -> Value
r1) <- GlobalEnv -> Env -> Value -> TcM (BindType, Value, Value -> Value)
unifyFun GlobalEnv
ge Env
scope Value
rho1
  GlobalEnv
-> Env
-> Term
-> Value
-> (Value -> Value)
-> Value
-> (Value -> Value)
-> TcM Term
subsCheckFun GlobalEnv
ge Env
scope Term
t Value
a1 Value -> Value
r1 Value
a2 Value -> Value
r2
subsCheckRho GlobalEnv
ge Env
scope Term
t (VProd BindType
Explicit Value
a1 Ident
_ (Bind Value -> Value
r1)) Value
rho2 = do       -- Rule FUN
  (BindType
bt,Value
a2,Value -> Value
r2) <- GlobalEnv -> Env -> Value -> TcM (BindType, Value, Value -> Value)
unifyFun GlobalEnv
ge Env
scope Value
rho2
  GlobalEnv
-> Env
-> Term
-> Value
-> (Value -> Value)
-> Value
-> (Value -> Value)
-> TcM Term
subsCheckFun GlobalEnv
ge Env
scope Term
t Value
a1 Value -> Value
r1 Value
a2 Value -> Value
r2
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
rho1 (VTblType Value
p2 Value
r2) = do                      -- Rule TABLE
  (Value
p1,Value
r1) <- GlobalEnv -> Env -> Value -> TcM (Value, Value)
unifyTbl GlobalEnv
ge Env
scope Value
rho1
  GlobalEnv
-> Env -> Term -> Value -> Value -> Value -> Value -> TcM Term
subsCheckTbl GlobalEnv
ge Env
scope Term
t Value
p1 Value
r1 Value
p2 Value
r2
subsCheckRho GlobalEnv
ge Env
scope Term
t (VTblType Value
p1 Value
r1) Value
rho2 = do                      -- Rule TABLE
  (Value
p2,Value
r2) <- GlobalEnv -> Env -> Value -> TcM (Value, Value)
unifyTbl GlobalEnv
ge Env
scope Value
rho2
  GlobalEnv
-> Env -> Term -> Value -> Value -> Value -> Value -> TcM Term
subsCheckTbl GlobalEnv
ge Env
scope Term
t Value
p1 Value
r1 Value
p2 Value
r2
subsCheckRho GlobalEnv
ge Env
scope Term
t (VSort Ident
s1) (VSort Ident
s2)                           -- Rule PTYPE
  | Ident
s1 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cPType Bool -> Bool -> Bool
&& Ident
s2 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cType = Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
subsCheckRho GlobalEnv
ge Env
scope Term
t (VApp Predefined
p1 [Value]
_) (VApp Predefined
p2 [Value]
_)                         -- Rule INT1
  | Predefined -> Ident
predefName Predefined
p1 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cInts Bool -> Bool -> Bool
&& Predefined -> Ident
predefName Predefined
p2 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cInt = Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
subsCheckRho GlobalEnv
ge Env
scope Term
t (VApp Predefined
p1 [VInt MetaId
i]) (VApp Predefined
p2 [VInt MetaId
j])           -- Rule INT2
  | Predefined -> Ident
predefName Predefined
p1 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cInts Bool -> Bool -> Bool
&& Predefined -> Ident
predefName Predefined
p2 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cInts =
      if MetaId
i MetaId -> MetaId -> Bool
forall a. Ord a => a -> a -> Bool
<= MetaId
j
        then Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
        else Message -> TcM Term
forall a. Message -> TcM a
tcError (String
"Ints" String -> MetaId -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> MetaId
i Message -> String -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> String
"is not a subtype of" Message -> String -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> String
"Ints" Message -> MetaId -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> MetaId
j)
subsCheckRho GlobalEnv
ge Env
scope Term
t ty1 :: Value
ty1@(VRecType [(Label, Value)]
rs1) ty2 :: Value
ty2@(VRecType [(Label, Value)]
rs2) = do      -- Rule REC
  let mkAccess :: Env
-> Term
-> TcM (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
mkAccess Env
scope Term
t =
        case Term
t of
          ExtR Term
t1 Term
t2 -> do (Env
scope,Label -> Maybe (Maybe Term, Term)
mkProj1,Term -> Term
mkWrap1) <- Env
-> Term
-> TcM (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
mkAccess Env
scope Term
t1
                           (Env
scope,Label -> Maybe (Maybe Term, Term)
mkProj2,Term -> Term
mkWrap2) <- Env
-> Term
-> TcM (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
mkAccess Env
scope Term
t2
                           (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
-> TcM (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope
                                  ,\Label
l -> Label -> Maybe (Maybe Term, Term)
mkProj2 Label
l Maybe (Maybe Term, Term)
-> Maybe (Maybe Term, Term) -> Maybe (Maybe Term, Term)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Label -> Maybe (Maybe Term, Term)
mkProj1 Label
l
                                  ,Term -> Term
mkWrap1 (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
mkWrap2
                                  )
          R [Assign]
rs -> do [TcM ()] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [Message -> TcM ()
tcWarn (String
"Discarded field:" String -> Label -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> Label
l) | (Label
l,(Maybe Term, Term)
_) <- [Assign]
rs, Maybe Value -> Bool
forall a. Maybe a -> Bool
isNothing (Label -> [(Label, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [(Label, Value)]
rs2)]
                     (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
-> TcM (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope
                            ,\Label
l -> Label -> [Assign] -> Maybe (Maybe Term, Term)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [Assign]
rs
                            ,Term -> Term
forall a. a -> a
id
                            )
          Vr Ident
x -> do (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
-> TcM (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope
                            ,\Label
l -> do VRecType [(Label, Value)]
rs <- Ident -> Env -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
x Env
scope
                                      Value
ty <- Label -> [(Label, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [(Label, Value)]
rs
                                      (Maybe Term, Term) -> Maybe (Maybe Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term
forall a. Maybe a
Nothing,Term -> Label -> Term
P Term
t Label
l)
                            ,Term -> Term
forall a. a -> a
id
                            )
          Term
t    -> let x :: Ident
x = Env -> Ident
newVar Env
scope
                  in (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
-> TcM (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (((Ident
x,Value
ty1)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope)
                            ,\Label
l  -> (Maybe Term, Term) -> Maybe (Maybe Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term
forall a. Maybe a
Nothing,Term -> Label -> Term
P (Ident -> Term
Vr Ident
x) Label
l)
                            ,(Ident, (Maybe Term, Term)) -> Term -> Term
Let (Ident
x, (Maybe Term
forall a. Maybe a
Nothing, Term
t))
                            )

      mkField :: Env -> a -> (a, Term) -> Value -> Value -> TcM (a, (a, Term))
mkField Env
scope a
l (a
mb_ty,Term
t) Value
ty1 Value
ty2 = do
        Term
t <- GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
ty1 Value
ty2
        (a, (a, Term)) -> TcM (a, (a, Term))
forall (m :: * -> *) a. Monad m => a -> m a
return (a
l, (a
mb_ty,Term
t))

  (Env
scope,Label -> Maybe (Maybe Term, Term)
mkProj,Term -> Term
mkWrap) <- Env
-> Term
-> TcM (Env, Label -> Maybe (Maybe Term, Term), Term -> Term)
mkAccess Env
scope Term
t

  let fields :: [(Label, Value, Maybe Value)]
fields = [(Label
l,Value
ty2,Label -> [(Label, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [(Label, Value)]
rs1) | (Label
l,Value
ty2) <- [(Label, Value)]
rs2]
  case [Label
l | (Label
l,Value
_,Maybe Value
Nothing) <- [(Label, Value, Maybe Value)]
fields] of
    []      -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [Label]
missing -> Message -> TcM ()
forall a. Message -> TcM a
tcError (String
"In the term" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> Term -> Message
forall a. Pretty a => a -> Message
pp Term
t Message -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
$$
                        String
"there are no values for fields:" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> [Label] -> Message
forall a. Pretty a => [a] -> Message
hsep [Label]
missing)
  [Assign]
rs <- [TcM Assign] -> TcM [Assign]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Env -> Label -> (Maybe Term, Term) -> Value -> Value -> TcM Assign
forall a a.
Env -> a -> (a, Term) -> Value -> Value -> TcM (a, (a, Term))
mkField Env
scope Label
l (Maybe Term, Term)
t Value
ty1 Value
ty2 | (Label
l,Value
ty2,Just Value
ty1) <- [(Label, Value, Maybe Value)]
fields, Just (Maybe Term, Term)
t <- [Label -> Maybe (Maybe Term, Term)
mkProj Label
l]]
  Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term
mkWrap ([Assign] -> Term
R [Assign]
rs))
subsCheckRho GlobalEnv
ge Env
scope Term
t Value
tau1 Value
tau2 = do                                  -- Rule EQ
  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
tau1 Value
tau2                                 -- Revert to ordinary unification
  Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> TcM Term
subsCheckFun :: GlobalEnv
-> Env
-> Term
-> Value
-> (Value -> Value)
-> Value
-> (Value -> Value)
-> TcM Term
subsCheckFun GlobalEnv
ge Env
scope Term
t Value
a1 Value -> Value
r1 Value
a2 Value -> Value
r2 = do
  let v :: Ident
v   = Env -> Ident
newVar Env
scope
  Term
vt <- GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge ((Ident
v,Value
a2)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) (Ident -> Term
Vr Ident
v) Value
a2 Value
a1
  Value
val1 <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv ((Ident
v,Value
vtypeType)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope)) Term
vt)
  Value
val2 <- Value -> TcM Value
forall (m :: * -> *) a. Monad m => a -> m a
return  (MetaId -> [Value] -> Value
VGen (Env -> MetaId
forall (t :: * -> *) a. Foldable t => t a -> MetaId
length Env
scope) [])
  Term
t  <- GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge ((Ident
v,Value
vtypeType)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) (Term -> Term -> Term
App Term
t Term
vt) (Value -> Value
r1 Value
val1) (Value -> Value
r2 Value
val2)
  Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType -> Ident -> Term -> Term
Abs BindType
Explicit Ident
v Term
t)

subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
subsCheckTbl :: GlobalEnv
-> Env -> Term -> Value -> Value -> Value -> Value -> TcM Term
subsCheckTbl GlobalEnv
ge Env
scope Term
t Value
p1 Value
r1 Value
p2 Value
r2 = do
  let x :: Ident
x = Env -> Ident
newVar Env
scope
  Term
xt <- GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge Env
scope (Ident -> Term
Vr Ident
x) Value
p2 Value
p1
  Term
t  <- GlobalEnv -> Env -> Term -> Value -> Value -> TcM Term
subsCheckRho GlobalEnv
ge ((Ident
x,Value
vtypePType)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) (Term -> Term -> Term
S Term
t Term
xt) Value
r1 Value
r2 ;
  Term
p2 <- GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
p2
  Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (TInfo -> [Case] -> Term
T (Term -> TInfo
TTyped Term
p2) [(Ident -> Patt
PV Ident
x,Term
t)])

-----------------------------------------------------------------------
-- Unification
-----------------------------------------------------------------------

unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (BindType, Sigma, Value -> Rho)
unifyFun :: GlobalEnv -> Env -> Value -> TcM (BindType, Value, Value -> Value)
unifyFun GlobalEnv
ge Env
scope (VProd BindType
bt Value
arg Ident
x (Bind Value -> Value
res)) =
  (BindType, Value, Value -> Value)
-> TcM (BindType, Value, Value -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType
bt,Value
arg,Value -> Value
res)
unifyFun GlobalEnv
ge Env
scope Value
tau = do
  let mk_val :: MetaId -> Value
mk_val MetaId
ty = MetaId -> Env -> [Value] -> Value
VMeta MetaId
ty [] []
  Value
arg <- (MetaId -> Value) -> TcM MetaId -> TcM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MetaId -> Value
mk_val (TcM MetaId -> TcM Value) -> TcM MetaId -> TcM Value
forall a b. (a -> b) -> a -> b
$ Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
  Value
res <- (MetaId -> Value) -> TcM MetaId -> TcM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MetaId -> Value
mk_val (TcM MetaId -> TcM Value) -> TcM MetaId -> TcM Value
forall a b. (a -> b) -> a -> b
$ Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
  let bt :: BindType
bt = BindType
Explicit
  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
tau (BindType -> Value -> Ident -> Binding -> Value
VProd BindType
bt Value
arg Ident
identW ((Value -> Value) -> Binding
forall a. (a -> Value) -> Bind a
Bind (Value -> Value -> Value
forall a b. a -> b -> a
const Value
res)))
  (BindType, Value, Value -> Value)
-> TcM (BindType, Value, Value -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType
bt,Value
arg,Value -> Value -> Value
forall a b. a -> b -> a
const Value
res)

unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho)
unifyTbl :: GlobalEnv -> Env -> Value -> TcM (Value, Value)
unifyTbl GlobalEnv
ge Env
scope (VTblType Value
arg Value
res) =
  (Value, Value) -> TcM (Value, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Value
arg,Value
res)
unifyTbl GlobalEnv
ge Env
scope Value
tau = do
  let mk_val :: MetaId -> Value
mk_val MetaId
ty = MetaId -> Env -> [Value] -> Value
VMeta MetaId
ty (Env -> Env
forall a b. [(a, b)] -> [(a, Value)]
scopeEnv Env
scope) []
  Value
arg <- (MetaId -> Value) -> TcM MetaId -> TcM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MetaId -> Value
mk_val (TcM MetaId -> TcM Value) -> TcM MetaId -> TcM Value
forall a b. (a -> b) -> a -> b
$ Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypePType
  Value
res <- (MetaId -> Value) -> TcM MetaId -> TcM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MetaId -> Value
mk_val (TcM MetaId -> TcM Value) -> TcM MetaId -> TcM Value
forall a b. (a -> b) -> a -> b
$ Env -> Value -> TcM MetaId
newMeta Env
scope Value
vtypeType
  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
tau (Value -> Value -> Value
VTblType Value
arg Value
res)
  (Value, Value) -> TcM (Value, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Value
arg,Value
res)

unify :: GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope (VApp Predefined
f1 [Value]
vs1)      (VApp Predefined
f2 [Value]
vs2)
  | Predefined
f1 Predefined -> Predefined -> Bool
forall a. Eq a => a -> a -> Bool
== Predefined
f2                   = [TcM ()] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ((Value -> Value -> TcM ()) -> [Value] -> [Value] -> [TcM ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope) [Value]
vs1 [Value]
vs2)
unify GlobalEnv
ge Env
scope (VCApp QIdent
f1 [Value]
vs1)     (VCApp QIdent
f2 [Value]
vs2)
  | QIdent
f1 QIdent -> QIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QIdent
f2                   = [TcM ()] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ((Value -> Value -> TcM ()) -> [Value] -> [Value] -> [TcM ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope) [Value]
vs1 [Value]
vs2)
unify GlobalEnv
ge Env
scope (VSort Ident
s1)         (VSort Ident
s2)
  | Ident
s1 Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
s2                   = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unify GlobalEnv
ge Env
scope (VGen MetaId
i [Value]
vs1)       (VGen MetaId
j [Value]
vs2)
  | MetaId
i MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
j                     = [TcM ()] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ((Value -> Value -> TcM ()) -> [Value] -> [Value] -> [TcM ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope) [Value]
vs1 [Value]
vs2)
unify GlobalEnv
ge Env
scope (VTblType Value
p1 Value
res1) (VTblType Value
p2 Value
res2) = do
  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
p1   Value
p2
  GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope Value
res1 Value
res2
unify GlobalEnv
ge Env
scope (VMeta MetaId
i Env
env1 [Value]
vs1) (VMeta MetaId
j Env
env2 [Value]
vs2)
  | MetaId
i  MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
j                    = [TcM ()] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ((Value -> Value -> TcM ()) -> [Value] -> [Value] -> [TcM ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope) [Value]
vs1 [Value]
vs2)
  | Bool
otherwise                  = do MetaValue
mv <- MetaId -> TcM MetaValue
getMeta MetaId
j
                                    case MetaValue
mv of
                                      Bound Term
t2    -> do Value
v2 <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge Env
env2 Term
t2)
                                                        GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope (MetaId -> Env -> [Value] -> Value
VMeta MetaId
i Env
env1 [Value]
vs1) (GLocation -> Value -> [Value] -> Value
vapply (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) Value
v2 [Value]
vs2)
                                      Unbound Env
_ Value
_ -> MetaId -> MetaValue -> TcM ()
setMeta MetaId
i (Term -> MetaValue
Bound (MetaId -> Term
Meta MetaId
j))
unify GlobalEnv
ge Env
scope (VInt MetaId
i)       (VInt MetaId
j)
  | MetaId
i MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
j                     = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unify GlobalEnv
ge Env
scope (VMeta MetaId
i Env
env [Value]
vs) Value
v = GlobalEnv -> Env -> MetaId -> Env -> [Value] -> Value -> TcM ()
unifyVar GlobalEnv
ge Env
scope MetaId
i Env
env [Value]
vs Value
v
unify GlobalEnv
ge Env
scope Value
v (VMeta MetaId
i Env
env [Value]
vs) = GlobalEnv -> Env -> MetaId -> Env -> [Value] -> Value -> TcM ()
unifyVar GlobalEnv
ge Env
scope MetaId
i Env
env [Value]
vs Value
v
unify GlobalEnv
ge Env
scope Value
v1 Value
v2 = do
  Term
t1 <- Term -> TcM Term
zonkTerm (Term -> TcM Term) -> TcM Term -> TcM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
v1
  Term
t2 <- Term -> TcM Term
zonkTerm (Term -> TcM Term) -> TcM Term -> TcM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
v2
  Message -> TcM ()
forall a. Message -> TcM a
tcError (String
"Cannot unify terms:" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> (TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
t1 Message -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
$$
                                      TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
t2))

-- | Invariant: tv1 is a flexible type variable
unifyVar :: GlobalEnv -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
unifyVar :: GlobalEnv -> Env -> MetaId -> Env -> [Value] -> Value -> TcM ()
unifyVar GlobalEnv
ge Env
scope MetaId
i Env
env [Value]
vs Value
ty2 = do            -- Check whether i is bound
  MetaValue
mv <- MetaId -> TcM MetaValue
getMeta MetaId
i
  case MetaValue
mv of
    Bound Term
ty1       -> do Value
v <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge Env
env Term
ty1)
                          GlobalEnv -> Env -> Value -> Value -> TcM ()
unify GlobalEnv
ge Env
scope (GLocation -> Value -> [Value] -> Value
vapply (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) Value
v [Value]
vs) Value
ty2
    Unbound Env
scope' Value
_ -> case GLocation -> [Ident] -> Value -> Term
value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope') Value
ty2 of
                          -- Left i     -> let (v,_) = reverse scope !! i
                          --               in tcError ("Variable" <+> pp v <+> "has escaped")
                                Term
ty2' -> do [MetaId]
ms2 <- GLocation -> [(Env, Value)] -> TcM [MetaId]
getMetaVars (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) [(Env
scope,Value
ty2)]
                                           if MetaId
i MetaId -> [MetaId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaId]
ms2
                                             then Message -> TcM ()
forall a. Message -> TcM a
tcError (String
"Occurs check for" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> MetaId -> Message
ppMeta MetaId
i Message -> String -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> String
"in:" Message -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
$$
                                                           MetaId -> Message -> Message
forall a. Pretty a => MetaId -> a -> Message
nest MetaId
2 (TermPrintQual -> Integer -> Term -> Message
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Message
ppTerm TermPrintQual
Unqualified Integer
0 Term
ty2'))
                                             else MetaId -> MetaValue -> TcM ()
setMeta MetaId
i (Term -> MetaValue
Bound Term
ty2')

-----------------------------------------------------------------------
-- Instantiation and quantification
-----------------------------------------------------------------------

-- | Instantiate the topmost implicit arguments with metavariables
instantiate :: Scope -> Term -> Sigma -> TcM (Term,Rho)
instantiate :: Env -> Term -> Value -> TcM (Term, Value)
instantiate Env
scope Term
t (VProd BindType
Implicit Value
ty1 Ident
x (Bind Value -> Value
ty2)) = do
  MetaId
i <- Env -> Value -> TcM MetaId
newMeta Env
scope Value
ty1
  Env -> Term -> Value -> TcM (Term, Value)
instantiate Env
scope (Term -> Term -> Term
App Term
t (Term -> Term
ImplArg (MetaId -> Term
Meta MetaId
i))) (Value -> Value
ty2 (MetaId -> Env -> [Value] -> Value
VMeta MetaId
i [] []))
instantiate Env
scope Term
t Value
ty = do
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t,Value
ty)

-- | Build fresh lambda abstractions for the topmost implicit arguments
skolemise :: GlobalEnv -> Scope -> Sigma -> TcM (Scope, Term->Term, Rho)
skolemise :: GlobalEnv -> Env -> Value -> TcM (Env, Term -> Term, Value)
skolemise GlobalEnv
ge Env
scope ty :: Value
ty@(VMeta MetaId
i Env
env [Value]
vs) = do
  MetaValue
mv <- MetaId -> TcM MetaValue
getMeta MetaId
i
  case MetaValue
mv of
    Unbound Env
_ Value
_ -> (Env, Term -> Term, Value) -> TcM (Env, Term -> Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope,Term -> Term
forall a. a -> a
id,Value
ty)                   -- guarded constant?
    Bound Term
ty    -> do Value
vty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge Env
env Term
ty)
                      GlobalEnv -> Env -> Value -> TcM (Env, Term -> Term, Value)
skolemise GlobalEnv
ge Env
scope (GLocation -> Value -> [Value] -> Value
vapply (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) Value
vty [Value]
vs)
skolemise GlobalEnv
ge Env
scope (VProd BindType
Implicit Value
ty1 Ident
x (Bind Value -> Value
ty2)) = do
  let v :: Ident
v = Env -> Ident
newVar Env
scope
  (Env
scope,Term -> Term
f,Value
ty2) <- GlobalEnv -> Env -> Value -> TcM (Env, Term -> Term, Value)
skolemise GlobalEnv
ge ((Ident
v,Value
ty1)(Ident, Value) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
scope) (Value -> Value
ty2 (MetaId -> [Value] -> Value
VGen (Env -> MetaId
forall (t :: * -> *) a. Foldable t => t a -> MetaId
length Env
scope) []))
  (Env, Term -> Term, Value) -> TcM (Env, Term -> Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope,BindType -> Ident -> Term -> Term
Abs BindType
Implicit Ident
v (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
f,Value
ty2)
skolemise GlobalEnv
ge Env
scope Value
ty = do
  (Env, Term -> Term, Value) -> TcM (Env, Term -> Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
scope,Term -> Term
forall a. a -> a
id,Value
ty)

-- | Quantify over the specified type variables (all flexible)
quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
quantify :: GlobalEnv -> Env -> Term -> [MetaId] -> Value -> TcM (Term, Value)
quantify GlobalEnv
ge Env
scope Term
t [MetaId]
tvs Value
ty0 = do
  Term
ty <- GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term (GlobalEnv -> GLocation
geLoc GlobalEnv
ge) (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
ty0
  let used_bndrs :: [Ident]
used_bndrs = [Ident] -> [Ident]
forall a. Eq a => [a] -> [a]
nub (Term -> [Ident]
bndrs Term
ty)  -- Avoid quantified type variables in use
      new_bndrs :: [Ident]
new_bndrs  = MetaId -> [Ident] -> [Ident]
forall a. MetaId -> [a] -> [a]
take ([MetaId] -> MetaId
forall (t :: * -> *) a. Foldable t => t a -> MetaId
length [MetaId]
tvs) ([Ident]
allBinders [Ident] -> [Ident] -> [Ident]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Ident]
used_bndrs)
  ((MetaId, Ident) -> TcM ()) -> [(MetaId, Ident)] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (MetaId, Ident) -> TcM ()
bind ([MetaId]
tvs [MetaId] -> [Ident] -> [(MetaId, Ident)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Ident]
new_bndrs)   -- 'bind' is just a cunning way
  Term
ty <- Term -> TcM Term
zonkTerm Term
ty                  -- of doing the substitution
  Value
vty <- Err Value -> TcM Value
forall (m :: * -> *) a. ErrorMonad m => Err a -> m a
liftErr (GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
ge [] ((Ident -> Term -> Term) -> Term -> [Ident] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Ident
v Term
ty -> BindType -> Ident -> Term -> Term -> Term
Prod BindType
Implicit Ident
v Term
typeType Term
ty) Term
ty [Ident]
new_bndrs))
  (Term, Value) -> TcM (Term, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ident -> Term -> Term) -> Term -> [Ident] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (BindType -> Ident -> Term -> Term
Abs BindType
Implicit) Term
t [Ident]
new_bndrs,Value
vty)
  where
    bind :: (MetaId, Ident) -> TcM ()
bind (MetaId
i, Ident
name) = MetaId -> MetaValue -> TcM ()
setMeta MetaId
i (Term -> MetaValue
Bound (Ident -> Term
Vr Ident
name))

    bndrs :: Term -> [Ident]
bndrs (Prod BindType
_ Ident
x Term
t1 Term
t2) = [Ident
x] [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ Term -> [Ident]
bndrs Term
t1  [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ Term -> [Ident]
bndrs Term
t2
    bndrs Term
_                = []

allBinders :: [Ident]    -- a,b,..z, a1, b1,... z1, a2, b2,...
allBinders :: [Ident]
allBinders = [ String -> Ident
identS [Char
x]          | Char
x <- [Char
'a'..Char
'z'] ] [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++
             [ String -> Ident
identS (Char
x Char -> String -> String
forall a. a -> [a] -> [a]
: Integer -> String
forall a. Show a => a -> String
show Integer
i) | Integer
i <- [Integer
1 :: Integer ..], Char
x <- [Char
'a'..Char
'z']]


-----------------------------------------------------------------------
-- The Monad
-----------------------------------------------------------------------

type Scope = [(Ident,Value)]

type Sigma = Value
type Rho   = Value -- No top-level ForAll
type Tau   = Value -- No ForAlls anywhere

data MetaValue
  = Unbound Scope Sigma
  | Bound   Term
type MetaStore = IntMap.IntMap MetaValue
data TcResult a
  = TcOk   a MetaStore [Message]
  | TcFail             [Message] -- First msg is error, the rest are warnings?
newtype TcM a = TcM {TcM a -> MetaStore -> [Message] -> TcResult a
unTcM :: MetaStore -> [Message] -> TcResult a}

instance Monad TcM where
  return :: a -> TcM a
return a
x = (MetaStore -> [Message] -> TcResult a) -> TcM a
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs -> a -> MetaStore -> [Message] -> TcResult a
forall a. a -> MetaStore -> [Message] -> TcResult a
TcOk a
x MetaStore
ms [Message]
msgs)
  TcM a
f >>= :: TcM a -> (a -> TcM b) -> TcM b
>>= a -> TcM b
g  = (MetaStore -> [Message] -> TcResult b) -> TcM b
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs -> case TcM a -> MetaStore -> [Message] -> TcResult a
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM TcM a
f MetaStore
ms [Message]
msgs of
                                TcOk a
x MetaStore
ms [Message]
msgs -> TcM b -> MetaStore -> [Message] -> TcResult b
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM (a -> TcM b
g a
x) MetaStore
ms [Message]
msgs
                                TcFail    [Message]
msgs -> [Message] -> TcResult b
forall a. [Message] -> TcResult a
TcFail [Message]
msgs)

#if !(MIN_VERSION_base(4,13,0))
  -- Monad(fail) will be removed in GHC 8.8+
  fail = Fail.fail
#endif

instance Fail.MonadFail TcM where
  fail :: String -> TcM a
fail     = Message -> TcM a
forall a. Message -> TcM a
tcError (Message -> TcM a) -> (String -> Message) -> String -> TcM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Message
forall a. Pretty a => a -> Message
pp


instance Applicative TcM where
  pure :: a -> TcM a
pure = a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: TcM (a -> b) -> TcM a -> TcM b
(<*>) = TcM (a -> b) -> TcM a -> TcM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Functor TcM where
  fmap :: (a -> b) -> TcM a -> TcM b
fmap a -> b
f TcM a
g = (MetaStore -> [Message] -> TcResult b) -> TcM b
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs -> case TcM a -> MetaStore -> [Message] -> TcResult a
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM TcM a
g MetaStore
ms [Message]
msgs of
                           TcOk a
x MetaStore
ms [Message]
msgs -> b -> MetaStore -> [Message] -> TcResult b
forall a. a -> MetaStore -> [Message] -> TcResult a
TcOk (a -> b
f a
x) MetaStore
ms [Message]
msgs
                           TcFail [Message]
msgs    -> [Message] -> TcResult b
forall a. [Message] -> TcResult a
TcFail [Message]
msgs)

instance ErrorMonad TcM where
  raise :: String -> TcM a
raise  = Message -> TcM a
forall a. Message -> TcM a
tcError (Message -> TcM a) -> (String -> Message) -> String -> TcM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Message
forall a. Pretty a => a -> Message
pp
  handle :: TcM a -> (String -> TcM a) -> TcM a
handle TcM a
f String -> TcM a
g = (MetaStore -> [Message] -> TcResult a) -> TcM a
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs -> case TcM a -> MetaStore -> [Message] -> TcResult a
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM TcM a
f MetaStore
ms [Message]
msgs of
                                  TcFail (Message
msg:[Message]
msgs) -> TcM a -> MetaStore -> [Message] -> TcResult a
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM (String -> TcM a
g (Message -> String
forall a. Pretty a => a -> String
render Message
msg)) MetaStore
ms [Message]
msgs
                                  TcResult a
r                 -> TcResult a
r)

tcError :: Message -> TcM a
tcError :: Message -> TcM a
tcError Message
msg = (MetaStore -> [Message] -> TcResult a) -> TcM a
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs -> [Message] -> TcResult a
forall a. [Message] -> TcResult a
TcFail (Message
msg Message -> [Message] -> [Message]
forall a. a -> [a] -> [a]
: [Message]
msgs))

tcWarn :: Message -> TcM ()
tcWarn :: Message -> TcM ()
tcWarn Message
msg = (MetaStore -> [Message] -> TcResult ()) -> TcM ()
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs -> () -> MetaStore -> [Message] -> TcResult ()
forall a. a -> MetaStore -> [Message] -> TcResult a
TcOk () MetaStore
ms (Message
msg Message -> [Message] -> [Message]
forall a. a -> [a] -> [a]
: [Message]
msgs))

unimplemented :: String -> m a
unimplemented String
str = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unimplemented: "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
str)


runTcM :: TcM a -> Check a
runTcM :: TcM a -> Check a
runTcM TcM a
f = case TcM a -> MetaStore -> [Message] -> TcResult a
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM TcM a
f MetaStore
forall a. IntMap a
IntMap.empty [] of
             TcOk a
x MetaStore
_ [Message]
msgs -> do [Message] -> Check ()
forall (t :: * -> *). Foldable t => t Message -> Check ()
checkWarnings [Message]
msgs; a -> Check a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
             TcFail (Message
msg:[Message]
msgs) -> do [Message] -> Check ()
forall (t :: * -> *). Foldable t => t Message -> Check ()
checkWarnings [Message]
msgs; Message -> Check a
forall a. Message -> Check a
checkError Message
msg

newMeta :: Scope -> Sigma -> TcM MetaId
newMeta :: Env -> Value -> TcM MetaId
newMeta Env
scope Value
ty = (MetaStore -> [Message] -> TcResult MetaId) -> TcM MetaId
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs ->
  let i :: MetaId
i = MetaStore -> MetaId
forall a. IntMap a -> MetaId
IntMap.size MetaStore
ms
  in MetaId -> MetaStore -> [Message] -> TcResult MetaId
forall a. a -> MetaStore -> [Message] -> TcResult a
TcOk MetaId
i (MetaId -> MetaValue -> MetaStore -> MetaStore
forall a. MetaId -> a -> IntMap a -> IntMap a
IntMap.insert MetaId
i (Env -> Value -> MetaValue
Unbound Env
scope Value
ty) MetaStore
ms) [Message]
msgs)

getMeta :: MetaId -> TcM MetaValue
getMeta :: MetaId -> TcM MetaValue
getMeta MetaId
i = (MetaStore -> [Message] -> TcResult MetaValue) -> TcM MetaValue
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs ->
  case MetaId -> MetaStore -> Maybe MetaValue
forall a. MetaId -> IntMap a -> Maybe a
IntMap.lookup MetaId
i MetaStore
ms of
    Just MetaValue
mv -> MetaValue -> MetaStore -> [Message] -> TcResult MetaValue
forall a. a -> MetaStore -> [Message] -> TcResult a
TcOk MetaValue
mv MetaStore
ms [Message]
msgs
    Maybe MetaValue
Nothing -> [Message] -> TcResult MetaValue
forall a. [Message] -> TcResult a
TcFail ((String
"Unknown metavariable" String -> Message -> Message
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Message
<+> MetaId -> Message
ppMeta MetaId
i) Message -> [Message] -> [Message]
forall a. a -> [a] -> [a]
: [Message]
msgs))

setMeta :: MetaId -> MetaValue -> TcM ()
setMeta :: MetaId -> MetaValue -> TcM ()
setMeta MetaId
i MetaValue
mv = (MetaStore -> [Message] -> TcResult ()) -> TcM ()
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs -> () -> MetaStore -> [Message] -> TcResult ()
forall a. a -> MetaStore -> [Message] -> TcResult a
TcOk () (MetaId -> MetaValue -> MetaStore -> MetaStore
forall a. MetaId -> a -> IntMap a -> IntMap a
IntMap.insert MetaId
i MetaValue
mv MetaStore
ms) [Message]
msgs)

newVar :: Scope -> Ident
newVar :: Env -> Ident
newVar Env
scope = [Ident] -> Ident
forall a. [a] -> a
head [Ident
x | Integer
i <- [Integer
1..],
                         let x :: Ident
x = String -> Ident
identS (Char
'v'Char -> String -> String
forall a. a -> [a] -> [a]
:Integer -> String
forall a. Show a => a -> String
show Integer
i),
                         Env -> Ident -> Bool
forall t b. Eq t => [(t, b)] -> t -> Bool
isFree Env
scope Ident
x]
  where
    isFree :: [(t, b)] -> t -> Bool
isFree []            t
x = Bool
True
    isFree ((t
y,b
_):[(t, b)]
scope) t
x = t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
/= t
y Bool -> Bool -> Bool
&& [(t, b)] -> t -> Bool
isFree [(t, b)]
scope t
x

scopeEnv :: [(a, b)] -> [(a, Value)]
scopeEnv   [(a, b)]
scope = ((a, b) -> MetaId -> (a, Value))
-> [(a, b)] -> [MetaId] -> [(a, Value)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(a
x,b
ty) MetaId
i -> (a
x,MetaId -> [Value] -> Value
VGen MetaId
i [])) ([(a, b)] -> [(a, b)]
forall a. [a] -> [a]
reverse [(a, b)]
scope) [MetaId
0..]
scopeVars :: [(b, b)] -> [b]
scopeVars  [(b, b)]
scope = ((b, b) -> b) -> [(b, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (b, b) -> b
forall a b. (a, b) -> a
fst [(b, b)]
scope
scopeTypes :: [(a, b)] -> [([(a, b)], b)]
scopeTypes [(a, b)]
scope = ((a, b) -> [(a, b)] -> ([(a, b)], b))
-> [(a, b)] -> [[(a, b)]] -> [([(a, b)], b)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(a
_,b
ty) [(a, b)]
scope -> ([(a, b)]
scope,b
ty)) [(a, b)]
scope ([(a, b)] -> [[(a, b)]]
forall a. [a] -> [[a]]
tails [(a, b)]
scope)

-- | This function takes account of zonking, and returns a set
-- (no duplicates) of unbound meta-type variables
getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId]
getMetaVars :: GLocation -> [(Env, Value)] -> TcM [MetaId]
getMetaVars GLocation
loc [(Env, Value)]
sc_tys = do
  [Term]
tys <- ((Env, Value) -> TcM Term) -> [(Env, Value)] -> TcM [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Env
scope,Value
ty) -> Term -> TcM Term
zonkTerm (Term -> TcM Term) -> TcM Term -> TcM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term GLocation
loc (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
ty) [(Env, Value)]
sc_tys
  [MetaId] -> TcM [MetaId]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> [MetaId] -> [MetaId]) -> [MetaId] -> [Term] -> [MetaId]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Term -> [MetaId] -> [MetaId]
go [] [Term]
tys)
  where
    -- Get the MetaIds from a term; no duplicates in result
    go :: Term -> [MetaId] -> [MetaId]
go (Vr Ident
tv)    [MetaId]
acc = [MetaId]
acc
    go (App Term
x Term
y)  [MetaId]
acc = Term -> [MetaId] -> [MetaId]
go Term
x (Term -> [MetaId] -> [MetaId]
go Term
y [MetaId]
acc)
    go (Meta MetaId
i)   [MetaId]
acc
      | MetaId
i MetaId -> [MetaId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaId]
acc  = [MetaId]
acc
      | Bool
otherwise     = MetaId
i MetaId -> [MetaId] -> [MetaId]
forall a. a -> [a] -> [a]
: [MetaId]
acc
    go (Q QIdent
_)      [MetaId]
acc = [MetaId]
acc
    go (QC QIdent
_)     [MetaId]
acc = [MetaId]
acc
    go (Sort Ident
_)   [MetaId]
acc = [MetaId]
acc
    go (Prod BindType
_ Ident
_ Term
arg Term
res) [MetaId]
acc = Term -> [MetaId] -> [MetaId]
go Term
arg (Term -> [MetaId] -> [MetaId]
go Term
res [MetaId]
acc)
    go (Table Term
p Term
t) [MetaId]
acc = Term -> [MetaId] -> [MetaId]
go Term
p (Term -> [MetaId] -> [MetaId]
go Term
t [MetaId]
acc)
    go (RecType [Labelling]
rs) [MetaId]
acc = ([MetaId] -> Labelling -> [MetaId])
-> [MetaId] -> [Labelling] -> [MetaId]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\[MetaId]
acc (Label
l,Term
ty) -> Term -> [MetaId] -> [MetaId]
go Term
ty [MetaId]
acc) [MetaId]
acc [Labelling]
rs
    go Term
t [MetaId]
acc = String -> [MetaId]
forall (m :: * -> *) a. MonadFail m => String -> m a
unimplemented (String
"go "String -> String -> String
forall a. [a] -> [a] -> [a]
++Term -> String
forall a. Show a => a -> String
show Term
t)

-- | This function takes account of zonking, and returns a set
-- (no duplicates) of free type variables
getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident]
getFreeVars :: GLocation -> [(Env, Value)] -> TcM [Ident]
getFreeVars GLocation
loc [(Env, Value)]
sc_tys = do
  [Term]
tys <- ((Env, Value) -> TcM Term) -> [(Env, Value)] -> TcM [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Env
scope,Value
ty) -> Term -> TcM Term
zonkTerm (Term -> TcM Term) -> TcM Term -> TcM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GLocation -> [Ident] -> Value -> TcM Term
forall (m :: * -> *).
Monad m =>
GLocation -> [Ident] -> Value -> m Term
tc_value2term GLocation
loc (Env -> [Ident]
forall b b. [(b, b)] -> [b]
scopeVars Env
scope) Value
ty) [(Env, Value)]
sc_tys
  [Ident] -> TcM [Ident]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> [Ident] -> [Ident]) -> [Ident] -> [Term] -> [Ident]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Ident] -> Term -> [Ident] -> [Ident]
go []) [] [Term]
tys)
  where
    go :: [Ident] -> Term -> [Ident] -> [Ident]
go [Ident]
bound (Vr Ident
tv)            [Ident]
acc
      | Ident
tv Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ident]
bound             = [Ident]
acc
      | Ident
tv Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ident]
acc               = [Ident]
acc
      | Bool
otherwise                   = Ident
tv Ident -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
: [Ident]
acc
    go [Ident]
bound (App Term
x Term
y)          [Ident]
acc = [Ident] -> Term -> [Ident] -> [Ident]
go [Ident]
bound Term
x ([Ident] -> Term -> [Ident] -> [Ident]
go [Ident]
bound Term
y [Ident]
acc)
    go [Ident]
bound (Meta MetaId
_)           [Ident]
acc = [Ident]
acc
    go [Ident]
bound (Q QIdent
_)              [Ident]
acc = [Ident]
acc
    go [Ident]
bound (QC QIdent
_)             [Ident]
acc = [Ident]
acc
    go [Ident]
bound (Prod BindType
_ Ident
x Term
arg Term
res) [Ident]
acc = [Ident] -> Term -> [Ident] -> [Ident]
go [Ident]
bound Term
arg ([Ident] -> Term -> [Ident] -> [Ident]
go (Ident
x Ident -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
: [Ident]
bound) Term
res [Ident]
acc)
    go [Ident]
bound (RecType [Labelling]
rs) [Ident]
acc = ([Ident] -> Labelling -> [Ident])
-> [Ident] -> [Labelling] -> [Ident]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\[Ident]
acc (Label
l,Term
ty) -> [Ident] -> Term -> [Ident] -> [Ident]
go [Ident]
bound Term
ty [Ident]
acc) [Ident]
acc [Labelling]
rs
    go [Ident]
bound (Table Term
p Term
t)        [Ident]
acc = [Ident] -> Term -> [Ident] -> [Ident]
go [Ident]
bound Term
p ([Ident] -> Term -> [Ident] -> [Ident]
go [Ident]
bound Term
t [Ident]
acc)

-- | Eliminate any substitutions in a term
zonkTerm :: Term -> TcM Term
zonkTerm :: Term -> TcM Term
zonkTerm (Meta MetaId
i) = do
  MetaValue
mv <- MetaId -> TcM MetaValue
getMeta MetaId
i
  case MetaValue
mv of
    Unbound Env
_ Value
_ -> Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId -> Term
Meta MetaId
i)
    Bound Term
t     -> do Term
t <- Term -> TcM Term
zonkTerm Term
t
                      MetaId -> MetaValue -> TcM ()
setMeta MetaId
i (Term -> MetaValue
Bound Term
t)       -- "Short out" multiple hops
                      Term -> TcM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
zonkTerm Term
t = (Term -> TcM Term) -> Term -> TcM Term
forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
composOp Term -> TcM Term
zonkTerm Term
t

tc_value2term :: GLocation -> [Ident] -> Value -> m Term
tc_value2term GLocation
loc [Ident]
xs Value
v =
  Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ GLocation -> [Ident] -> Value -> Term
value2term GLocation
loc [Ident]
xs Value
v
    -- Old value2term error message:
    -- Left i  -> tcError ("Variable #" <+> pp i <+> "has escaped")



data TcA x a
  = TcSingle   (MetaStore -> [Message] -> TcResult a)
  | TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])])

mkTcA :: Err [a] -> TcA a a
mkTcA :: Err [a] -> TcA a a
mkTcA Err [a]
f = case Err [a]
f of
            Bad String
msg -> (MetaStore -> [Message] -> TcResult a) -> TcA a a
forall x a. (MetaStore -> [Message] -> TcResult a) -> TcA x a
TcSingle  (\MetaStore
ms [Message]
msgs -> [Message] -> TcResult a
forall a. [Message] -> TcResult a
TcFail (String -> Message
forall a. Pretty a => a -> Message
pp String
msg Message -> [Message] -> [Message]
forall a. a -> [a] -> [a]
: [Message]
msgs))
            Ok  [a
x] -> (MetaStore -> [Message] -> TcResult a) -> TcA a a
forall x a. (MetaStore -> [Message] -> TcResult a) -> TcA x a
TcSingle  (\MetaStore
ms [Message]
msgs -> a -> MetaStore -> [Message] -> TcResult a
forall a. a -> MetaStore -> [Message] -> TcResult a
TcOk a
x MetaStore
ms [Message]
msgs)
            Ok  [a]
xs  -> [a]
-> (MetaStore -> [Message] -> [(a, MetaStore, [Message])])
-> TcA a a
forall x a.
[x]
-> (MetaStore -> [Message] -> [(a, MetaStore, [Message])])
-> TcA x a
TcMany [a]
xs (\MetaStore
ms [Message]
msgs -> [(a
x,MetaStore
ms,[Message]
msgs) | a
x <- [a]
xs])

singleTcA :: TcM a -> TcA x a
singleTcA :: TcM a -> TcA x a
singleTcA = (MetaStore -> [Message] -> TcResult a) -> TcA x a
forall x a. (MetaStore -> [Message] -> TcResult a) -> TcA x a
TcSingle ((MetaStore -> [Message] -> TcResult a) -> TcA x a)
-> (TcM a -> MetaStore -> [Message] -> TcResult a)
-> TcM a
-> TcA x a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcM a -> MetaStore -> [Message] -> TcResult a
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM

bindTcA :: TcA x a -> (a -> TcM b) -> TcA x b
bindTcA :: TcA x a -> (a -> TcM b) -> TcA x b
bindTcA TcA x a
f a -> TcM b
g = case TcA x a
f of
                TcSingle  MetaStore -> [Message] -> TcResult a
f -> (MetaStore -> [Message] -> TcResult b) -> TcA x b
forall x a. (MetaStore -> [Message] -> TcResult a) -> TcA x a
TcSingle (TcM b -> MetaStore -> [Message] -> TcResult b
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM ((MetaStore -> [Message] -> TcResult a) -> TcM a
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM MetaStore -> [Message] -> TcResult a
f TcM a -> (a -> TcM b) -> TcM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> TcM b
g))
                TcMany [x]
xs MetaStore -> [Message] -> [(a, MetaStore, [Message])]
f -> [x]
-> (MetaStore -> [Message] -> [(b, MetaStore, [Message])])
-> TcA x b
forall x a.
[x]
-> (MetaStore -> [Message] -> [(a, MetaStore, [Message])])
-> TcA x a
TcMany [x]
xs (\MetaStore
ms [Message]
msgs -> ((a, MetaStore, [Message])
 -> [(b, MetaStore, [Message])] -> [(b, MetaStore, [Message])])
-> [(b, MetaStore, [Message])]
-> [(a, MetaStore, [Message])]
-> [(b, MetaStore, [Message])]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a, MetaStore, [Message])
-> [(b, MetaStore, [Message])] -> [(b, MetaStore, [Message])]
add [] (MetaStore -> [Message] -> [(a, MetaStore, [Message])]
f MetaStore
ms [Message]
msgs))
  where
    add :: (a, MetaStore, [Message])
-> [(b, MetaStore, [Message])] -> [(b, MetaStore, [Message])]
add (a
y,MetaStore
ms,[Message]
msgs) [(b, MetaStore, [Message])]
rs =
      case TcM b -> MetaStore -> [Message] -> TcResult b
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM (a -> TcM b
g a
y) MetaStore
ms [Message]
msgs of
        TcFail [Message]
_       -> [(b, MetaStore, [Message])]
rs
        TcOk b
y MetaStore
ms [Message]
msgs -> (b
y,MetaStore
ms,[Message]
msgs)(b, MetaStore, [Message])
-> [(b, MetaStore, [Message])] -> [(b, MetaStore, [Message])]
forall a. a -> [a] -> [a]
:[(b, MetaStore, [Message])]
rs

runTcA :: ([x] -> TcM a) -> TcA x a -> TcM a
runTcA :: ([x] -> TcM a) -> TcA x a -> TcM a
runTcA [x] -> TcM a
g TcA x a
f = (MetaStore -> [Message] -> TcResult a) -> TcM a
forall a. (MetaStore -> [Message] -> TcResult a) -> TcM a
TcM (\MetaStore
ms [Message]
msgs -> case TcA x a
f of
                                TcMany [x]
xs MetaStore -> [Message] -> [(a, MetaStore, [Message])]
f -> case MetaStore -> [Message] -> [(a, MetaStore, [Message])]
f MetaStore
ms [Message]
msgs of
                                                 [(a
x,MetaStore
ms,[Message]
msgs)] -> a -> MetaStore -> [Message] -> TcResult a
forall a. a -> MetaStore -> [Message] -> TcResult a
TcOk a
x MetaStore
ms [Message]
msgs
                                                 [(a, MetaStore, [Message])]
rs            -> TcM a -> MetaStore -> [Message] -> TcResult a
forall a. TcM a -> MetaStore -> [Message] -> TcResult a
unTcM ([x] -> TcM a
g [x]
xs) MetaStore
ms [Message]
msgs
                                TcSingle MetaStore -> [Message] -> TcResult a
f                     -> MetaStore -> [Message] -> TcResult a
f MetaStore
ms [Message]
msgs)