diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs index 1e43c68bd..5c1743b74 100644 --- a/src/compiler/GF/Compile/CheckGrammar.hs +++ b/src/compiler/GF/Compile/CheckGrammar.hs @@ -177,7 +177,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do mty <- case mty of Just (L loc typ) -> chIn loc "linearization type of" $ (if False --flag optNewComp opts - then do (typ,_) <- CN.checkLType gr typ typeType + then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType typ <- computeLType gr [] typ return (Just (L loc typ)) else do (typ,_) <- checkLType gr [] typ typeType @@ -224,17 +224,17 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do (Just (L loct ty), Just (L locd de)) -> do ty' <- chIn loct "operation" $ (if False --flag optNewComp opts - then CN.checkLType gr ty typeType >>= return . CN.normalForm (CN.resourceValues opts gr) (L loct c) . fst -- !! + then CN.checkLType (CN.resourceValues opts gr) ty typeType >>= return . CN.normalForm (CN.resourceValues opts gr) (L loct c) . fst -- !! else checkLType gr [] ty typeType >>= computeLType gr [] . fst) (de',_) <- chIn locd "operation" $ (if False -- flag optNewComp opts - then CN.checkLType gr de ty' + then CN.checkLType (CN.resourceValues opts gr) de ty' else checkLType gr [] de ty') return (Just (L loct ty'), Just (L locd de')) (Nothing , Just (L locd de)) -> do (de',ty') <- chIn locd "operation" $ (if False -- flag optNewComp opts - then CN.inferLType gr de + then CN.inferLType (CN.resourceValues opts gr) de else inferLType gr [] de) return (Just (L locd ty'), Just (L locd de')) (Just (L loct ty), Nothing) -> do diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs index e368d9d77..f8517c07e 100644 --- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs +++ b/src/compiler/GF/Compile/Compute/ConcreteNew.hs @@ -1,8 +1,9 @@ -- | Functions for computing the values of terms in the concrete syntax, in -- | preparation for PMCFG generation. module GF.Compile.Compute.ConcreteNew - (GlobalEnv, resourceValues, normalForm, - --, Value(..), Env, value2term, eval, apply + (GlobalEnv(..), GLocation, resourceValues, normalForm, + Value(..), Bind(..), Env, value2term, + eval, value, toplevel ) where import GF.Grammar hiding (Env, VGen, VApp, VRecType) diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew1.hs b/src/compiler/GF/Compile/Compute/ConcreteNew1.hs deleted file mode 100644 index eba1db57b..000000000 --- a/src/compiler/GF/Compile/Compute/ConcreteNew1.hs +++ /dev/null @@ -1,107 +0,0 @@ -module GF.Compile.Compute.ConcreteNew1 - ( normalForm - , Value(..), Env, eval, apply, value2term - ) where - -import GF.Grammar hiding (Env, VGen, VApp, VRecType) -import GF.Grammar.Lookup -import GF.Grammar.Predef -import GF.Data.Operations -import Data.List (intersect) -import GF.Text.Pretty - -normalForm :: SourceGrammar -> Term -> Term -normalForm gr t = value2term gr [] (eval gr [] t) - -data Value - = VApp QIdent [Value] - | VGen Int [Value] - | VMeta MetaId Env [Value] - | VClosure Env Term - | VInt Int - | VFloat Double - | VString String - | VSort Ident - | VImplArg Value - | VTblType Value Value - | VRecType [(Label,Value)] - | VRec [(Label,Value)] - | VTbl Type [Value] --- | VC Value Value - | VPatt Patt - | VPattType Value - | VFV [Value] - | VAlts Value [(Value, Value)] - | VError String - deriving Show - -type Env = [(Ident,Value)] - -eval :: SourceGrammar -> Env -> Term -> Value -eval gr env (Vr x) = case lookup x env of - Just v -> v - Nothing -> error ("Unknown variable "++showIdent x) -eval gr env (Q x) - | x == (cPredef,cErrorType) -- to be removed - = let varP = identS "P" - in eval gr [] (mkProd [(Implicit,varP,typeType)] (Vr varP) []) - | fst x == cPredef = VApp x [] - | otherwise = case lookupResDef gr x of - Ok t -> eval gr [] t - Bad err -> error err -eval gr env (QC x) = VApp x [] -eval gr env (App e1 e2) = apply gr env e1 [eval gr env e2] -eval gr env (Meta i) = VMeta i env [] -eval gr env t@(Prod _ _ _ _) = VClosure env t -eval gr env t@(Abs _ _ _) = VClosure env t -eval gr env (EInt n) = VInt n -eval gr env (EFloat f) = VFloat f -eval gr env (K s) = VString s -eval gr env Empty = VString "" -eval gr env (Sort s) - | s == cTok = VSort cStr -- to be removed - | otherwise = VSort s -eval gr env (ImplArg t) = VImplArg (eval gr env t) -eval gr env (Table p res) = VTblType (eval gr env p) (eval gr env res) -eval gr env (RecType rs) = VRecType [(l,eval gr env ty) | (l,ty) <- rs] -eval gr env t@(ExtR t1 t2) = - let error = VError (show ("The term" <+> ppTerm Unqualified 0 t <+> "is not reducible")) - in case (eval gr env t1, eval gr env t2) of - (VRecType rs1, VRecType rs2) -> case intersect (map fst rs1) (map fst rs2) of - [] -> VRecType (rs1 ++ rs2) - _ -> error - (VRec rs1, VRec rs2) -> case intersect (map fst rs1) (map fst rs2) of - [] -> VRec (rs1 ++ rs2) - _ -> error - _ -> error -eval gr env (FV ts) = VFV (map (eval gr env) ts) -eval gr env t = error ("unimplemented: eval "++show t) - -apply gr env t [] = eval gr env t -apply gr env (Q x) vs - | fst x == cPredef = VApp x vs -- hmm - | otherwise = case lookupResDef gr x of - Ok t -> apply gr [] t vs - Bad err -> error err -apply gr env (App t1 t2) vs = apply gr env t1 (eval gr env t2 : vs) -apply gr env (Abs b x t) (v:vs) = case (b,v) of - (Implicit,VImplArg v) -> apply gr ((x,v):env) t vs - (Explicit, v) -> apply gr ((x,v):env) t vs -apply gr env t vs = error ("apply "++show t) - -value2term :: SourceGrammar -> [Ident] -> Value -> Term -value2term gr xs (VApp f vs) = foldl App (Q f) (map (value2term gr xs) vs) -value2term gr xs (VGen j vs) = foldl App (Vr (reverse xs !! j)) (map (value2term gr xs) vs) -value2term gr xs (VMeta j env vs) = foldl App (Meta j) (map (value2term gr xs) vs) -value2term gr xs (VClosure env (Prod bt x t1 t2)) = Prod bt x (value2term gr xs (eval gr env t1)) - (value2term gr (x:xs) (eval gr ((x,VGen (length xs) []) : env) t2)) -value2term gr xs (VClosure env (Abs bt x t)) = Abs bt x (value2term gr (x:xs) (eval gr ((x,VGen (length xs) []) : env) t)) -value2term gr xs (VInt n) = EInt n -value2term gr xs (VFloat f) = EFloat f -value2term gr xs (VString s) = if null s then Empty else K s -value2term gr xs (VSort s) = Sort s -value2term gr xs (VImplArg v) = ImplArg (value2term gr xs v) -value2term gr xs (VTblType p res) = Table (value2term gr xs p) (value2term gr xs res) -value2term gr xs (VRecType rs) = RecType [(l,value2term gr xs v) | (l,v) <- rs] -value2term gr xs (VFV vs) = FV (map (value2term gr xs) vs) -value2term gr xs v = error ("unimplemented: value2term "++show v) diff --git a/src/compiler/GF/Compile/Compute/Predef.hs b/src/compiler/GF/Compile/Compute/Predef.hs index 0e02402f7..0acf85720 100644 --- a/src/compiler/GF/Compile/Compute/Predef.hs +++ b/src/compiler/GF/Compile/Compute/Predef.hs @@ -2,7 +2,6 @@ {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} module GF.Compile.Compute.Predef(predef,predefName,delta) where ---import GF.Text.Pretty(render,hang) import qualified Data.Map as Map import Data.Array(array,(!)) import Data.List (isInfixOf) @@ -15,7 +14,6 @@ import GF.Compile.Compute.Value import GF.Infra.Ident (Ident,showIdent) --,varX import GF.Data.Operations(Err) -- ,err import GF.Grammar.Predef ---import PGF.Data(BindType(..)) -------------------------------------------------------------------------------- class Predef a where @@ -166,4 +164,4 @@ swap (x,y) = (y,x) bug msg = ppbug msg ppbug doc = error $ render $ hang "Internal error in Compute.Predef:" 4 doc --} \ No newline at end of file +-} diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index 0701b23f4..eadbff56f 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -1,10 +1,16 @@ 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.ConcreteNew1 +import GF.Compile.Compute.ConcreteNew +import GF.Compile.Compute.Predef(predef) import GF.Compile.TypeCheck.Primitives import GF.Infra.CheckM --import GF.Infra.UseIO @@ -16,253 +22,275 @@ import GF.Text.Pretty import Data.List (nub, (\\), tails) import qualified Data.IntMap as IntMap ---import GF.Grammar.Parser ---import System.IO ---import Debug.Trace - -checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type) -checkLType gr t ty = runTcM $ do - t <- checkSigma gr [] t (eval gr [] ty) +checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type) +checkLType ge t ty = runTcM $ do + vty <- runErr (eval ge ty) + t <- checkSigma ge [] t vty t <- zonkTerm t return (t,ty) -inferLType :: SourceGrammar -> Term -> Check (Term, Type) -inferLType gr t = runTcM $ do - (t,ty) <- inferSigma gr [] t +inferLType :: GlobalEnv -> Term -> Check (Term, Type) +inferLType ge@(GE _ _ _ gloc) t = runTcM $ do + (t,ty) <- inferSigma ge [] t t <- zonkTerm t - ty <- zonkTerm (value2term gr [] ty) + ty <- zonkTerm (value2term gloc [] ty) return (t,ty) -inferSigma :: SourceGrammar -> Scope -> Term -> TcM (Term,Sigma) -inferSigma gr scope t = do -- GEN1 - (t,ty) <- tcRho gr scope t Nothing - env_tvs <- getMetaVars gr (scopeTypes scope) - res_tvs <- getMetaVars gr [(scope,ty)] +inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma) +inferSigma ge scope t = do -- GEN1 + (t,ty) <- tcRho ge scope t Nothing + let GE _ _ _ loc = ge + env_tvs <- getMetaVars loc (scopeTypes scope) + res_tvs <- getMetaVars loc [(scope,ty)] let forall_tvs = res_tvs \\ env_tvs - quantify gr scope t forall_tvs ty + quantify ge scope t forall_tvs ty -checkSigma :: SourceGrammar -> Scope -> Term -> Sigma -> TcM Term -checkSigma gr scope t sigma = do -- GEN2 - (abs, scope, t, rho) <- skolemise id gr scope t sigma +checkSigma :: GlobalEnv -> Scope -> Term -> Sigma -> TcM Term +checkSigma ge scope t sigma = do -- GEN2 + (abs, scope, t, rho) <- skolemise id scope t sigma let skol_tvs = [] - (t,rho) <- tcRho gr scope t (Just rho) - esc_tvs <- getFreeVars gr ((scope,sigma) : scopeTypes scope) + (t,rho) <- tcRho ge scope t (Just rho) + let GE _ _ _ loc = ge + esc_tvs <- getFreeVars loc ((scope,sigma) : scopeTypes scope) let bad_tvs = filter (`elem` esc_tvs) skol_tvs if null bad_tvs then return (abs t) else tcError (pp "Type not polymorphic enough") -tcRho :: SourceGrammar -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho) -tcRho gr scope t@(EInt _) mb_ty = instSigma gr scope t (eval gr [] typeInt) mb_ty -tcRho gr scope t@(EFloat _) mb_ty = instSigma gr scope t (eval gr [] typeFloat) mb_ty -tcRho gr scope t@(K _) mb_ty = instSigma gr scope t (eval gr [] typeStr) mb_ty -tcRho gr scope t@(Empty) mb_ty = instSigma gr scope t (eval gr [] typeStr) mb_ty -tcRho gr scope t@(Vr v) mb_ty = do -- VAR +Just vtypeInt = fmap (flip VApp []) (predef cInt) +Just vtypeFloat = fmap (flip VApp []) (predef cFloat) +vtypeStr = VSort cStr +vtypeStrs = VSort cStrs +vtypeType = VSort cType +vtypePType = VSort cPType + +tcRho :: GlobalEnv -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho) +tcRho ge scope t@(EInt _) mb_ty = instSigma ge scope t vtypeInt mb_ty +tcRho ge scope t@(EFloat _) mb_ty = instSigma ge scope t vtypeFloat mb_ty +tcRho ge scope t@(K _) mb_ty = instSigma ge scope t vtypeStr mb_ty +tcRho ge scope t@(Empty) mb_ty = instSigma ge scope t vtypeStr mb_ty +tcRho ge scope t@(Vr v) mb_ty = do -- VAR case lookup v scope of - Just v_sigma -> instSigma gr scope t v_sigma mb_ty + Just v_sigma -> instSigma ge scope t v_sigma mb_ty Nothing -> tcError ("Unknown variable" <+> v) -tcRho gr scope t@(Q id) mb_ty - | elem (fst id) [cPredef,cPredefAbs] = - case typPredefined (snd id) of - Just ty -> instSigma gr scope t (eval gr [] ty) mb_ty - Nothing -> tcError (pp "unknown in Predef:" <+> ppQIdent Qualified id) - | otherwise = do - case lookupResType gr id of - Ok ty -> instSigma gr scope t (eval gr [] ty) mb_ty - Bad err -> tcError (pp err) -tcRho gr scope t@(QC id) mb_ty = do - case lookupResType gr id of - Ok ty -> instSigma gr scope t (eval gr [] ty) mb_ty - Bad err -> tcError (pp err) -tcRho gr scope (App fun arg) mb_ty = do -- APP - (fun,fun_ty) <- tcRho gr scope fun Nothing - (arg_ty, res_ty) <- unifyFun gr scope (eval gr (scopeEnv scope) arg) fun_ty - arg <- checkSigma gr scope arg arg_ty - instSigma gr scope (App fun arg) res_ty mb_ty +tcRho ge scope t@(Q id) mb_ty = + let GE gr _ _ _ = ge + in case lookupResType gr id of + Ok ty -> do vty <- runErr (eval ge ty) + instSigma ge scope t vty mb_ty + Bad err -> tcError (pp err) +tcRho ge scope t@(QC id) mb_ty = + let GE gr _ _ _ = ge + in case lookupResType gr id of + Ok ty -> do vty <- runErr (eval ge ty) + instSigma ge scope t vty mb_ty + Bad err -> tcError (pp err) +tcRho ge scope (App fun arg) mb_ty = do -- APP + (fun,fun_ty) <- tcRho ge scope fun Nothing + varg <- runErr (value (toplevel ge) arg) + let GE _ _ _ loc = ge + (arg_ty, res_ty) <- unifyFun loc scope (varg (scopeStack scope)) fun_ty + arg <- checkSigma ge scope arg arg_ty + instSigma ge scope (App fun arg) res_ty mb_ty tcRho gr scope (Abs bt var body) Nothing = do -- ABS1 - i <- newMeta (eval gr [] typeType) - (body,body_ty) <- tcRho gr ((var,VMeta i (scopeEnv scope) []):scope) body Nothing - return (Abs bt var body, (VClosure (scopeEnv scope) - (Prod bt identW (Meta i) (value2term gr (scopeVars scope) body_ty)))) -tcRho gr scope (Abs bt var body) (Just ty) = do -- ABS2 - (var_ty, body_ty) <- unifyFun gr scope (VGen (length scope) []) ty - (body, body_ty) <- tcRho gr ((var,var_ty):scope) body (Just body_ty) + i <- newMeta vtypeType + let arg_ty = VMeta i (scopeEnv scope) [] + (body,body_ty) <- tcRho gr ((var,arg_ty):scope) body Nothing + return (Abs bt var body, (VProd bt arg_ty identW (Bind (const body_ty)))) +tcRho ge scope (Abs bt var body) (Just ty) = do -- ABS2 + let GE _ _ _ loc = ge + (var_ty, body_ty) <- unifyFun loc scope (VGen (length scope) []) ty + (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just body_ty) return (Abs bt var body,ty) -tcRho gr scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET +tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET (rhs,var_ty) <- case mb_ann_ty of - Nothing -> inferSigma gr scope rhs - Just ann_ty -> do (ann_ty, _) <- tcRho gr scope ann_ty (Just (eval gr [] typeType)) - let v_ann_ty = eval gr (scopeEnv scope) ann_ty - rhs <- checkSigma gr scope rhs v_ann_ty + Nothing -> inferSigma ge scope rhs + Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) + ov_ann_ty <- runErr (value (toplevel ge) ann_ty) + let v_ann_ty = ov_ann_ty (scopeStack scope) + rhs <- checkSigma ge scope rhs v_ann_ty return (rhs, v_ann_ty) - (body, body_ty) <- tcRho gr ((var,var_ty):scope) body mb_ty - return (Let (var, (Just (value2term gr (scopeVars scope) var_ty), rhs)) body, body_ty) -tcRho gr scope (Typed body ann_ty) mb_ty = do -- ANNOT - (ann_ty, _) <- tcRho gr scope ann_ty (Just (eval gr [] typeType)) - let v_ann_ty = eval gr (scopeEnv scope) ann_ty - body <- checkSigma gr scope body v_ann_ty - instSigma gr scope (Typed body ann_ty) v_ann_ty mb_ty -tcRho gr scope (FV ts) mb_ty = do + (body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty + let GE _ _ _ loc = ge + return (Let (var, (Just (value2term loc (scopeVars scope) var_ty), rhs)) body, body_ty) +tcRho ge scope (Typed body ann_ty) mb_ty = do -- ANNOT + (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) + ov_ann_ty <- runErr (value (toplevel ge) ann_ty) + let v_ann_ty = ov_ann_ty (scopeStack scope) + body <- checkSigma ge scope body v_ann_ty + instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty +tcRho ge scope (FV ts) mb_ty = do case ts of - [] -> do i <- newMeta (eval gr [] typeType) - instSigma gr scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty - (t:ts) -> do (t,ty) <- tcRho gr scope t mb_ty + [] -> do i <- newMeta vtypeType + instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty + (t:ts) -> do (t,ty) <- tcRho ge scope t mb_ty let go [] ty = return ([],ty) - go (t:ts) ty = do (t, ty) <- tcRho gr scope t (Just ty) + go (t:ts) ty = do (t, ty) <- tcRho ge scope t (Just ty) (ts,ty) <- go ts ty return (t:ts,ty) - + (ts,ty) <- go ts ty return (FV (t:ts), ty) -tcRho gr scope t@(Sort s) mb_ty = do - instSigma gr scope t (eval gr [] typeType) mb_ty -tcRho gr scope t@(RecType rs) mb_ty = do - mapM_ (\(l,ty) -> tcRho gr scope ty (Just (eval gr [] typeType))) rs - instSigma gr scope t (eval gr [] typeType) mb_ty -tcRho gr scope t@(Table p res) mb_ty = do - (p, p_ty) <- tcRho gr scope p (Just (eval gr [] typePType)) - (res,res_ty) <- tcRho gr scope res Nothing - subsCheckRho gr scope t res_ty (eval gr [] typeType) - instSigma gr scope (Table p res) res_ty mb_ty -tcRho gr scope (Prod bt x ty1 ty2) mb_ty = do - (ty1,ty1_ty) <- tcRho gr scope ty1 (Just (eval gr [] typeType)) - (ty2,ty2_ty) <- tcRho gr ((x,eval gr (scopeEnv scope) ty1):scope) ty2 (Just (eval gr [] typeType)) - instSigma gr scope (Prod bt x ty1 ty2) (eval gr [] typeType) mb_ty -tcRho gr scope (S t p) mb_ty = do - p_ty <- fmap Meta $ newMeta (eval gr [] typePType) - res_ty <- fmap Meta $ newMeta (eval gr [] typeType) - let t_ty = eval gr (scopeEnv scope) (Table p_ty res_ty) - (t,t_ty) <- tcRho gr scope t (Just t_ty) - p <- checkSigma gr scope p (eval gr (scopeEnv scope) p_ty) - instSigma gr scope (S t p) (eval gr (scopeEnv scope) res_ty) mb_ty -tcRho gr scope (T tt ps) mb_ty = do +tcRho ge scope t@(Sort s) mb_ty = do + instSigma ge scope t vtypeType mb_ty +tcRho ge scope t@(RecType rs) mb_ty = do + mapM_ (\(l,ty) -> tcRho ge scope ty (Just vtypeType)) rs + instSigma ge scope t vtypeType mb_ty +tcRho ge scope t@(Table p res) mb_ty = do + (p, p_ty) <- tcRho ge scope p (Just vtypePType) + (res,res_ty) <- tcRho ge scope res Nothing + let GE _ _ _ loc = ge + subsCheckRho loc scope t res_ty vtypeType + instSigma ge scope (Table p res) res_ty mb_ty +tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do + (ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType) + ov_ty1 <- runErr (value (toplevel ge) ty1) + let vty1 = ov_ty1 (scopeStack scope) + (ty2,ty2_ty) <- tcRho ge ((x,vty1):scope) ty2 (Just vtypeType) + instSigma ge scope (Prod bt x ty1 ty2) vtypeType mb_ty +tcRho ge scope (S t p) mb_ty = do + p_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType + res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType + let t_ty = VTblType p_ty res_ty + (t,t_ty) <- tcRho ge scope t (Just t_ty) + p <- checkSigma ge scope p p_ty + instSigma ge scope (S t p) res_ty mb_ty +tcRho ge scope (T tt ps) mb_ty = do p_ty <- case tt of - TRaw -> fmap Meta $ newMeta (eval gr [] typePType) - TTyped ty -> do (ty, _) <- tcRho gr scope ty (Just (eval gr [] typeType)) - return ty - res_ty <- fmap Meta $ newMeta (eval gr [] typeType) - ps <- mapM (tcCase gr scope (eval gr (scopeEnv scope) p_ty) (eval gr (scopeEnv scope) res_ty)) ps - instSigma gr scope (T (TTyped p_ty) ps) (eval gr (scopeEnv scope) (Table p_ty res_ty)) mb_ty -tcRho gr scope t@(R rs) mb_ty = do + TRaw -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType + TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType) + ov_arg <- runErr (value (toplevel ge) ty) + return (ov_arg (scopeStack scope)) + res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType + ps <- mapM (tcCase ge scope p_ty res_ty) ps + let GE _ _ _ loc = ge + instSigma ge scope (T (TTyped (value2term loc [] p_ty)) ps) (VTblType p_ty res_ty) mb_ty +tcRho ge scope t@(R rs) mb_ty = do + let GE _ _ _ loc = ge lttys <- case mb_ty of - Nothing -> inferRecFields gr scope rs + Nothing -> inferRecFields ge scope rs Just ty -> case ty of - VRecType ltys -> checkRecFields gr scope rs ltys - VMeta _ _ _ -> inferRecFields gr scope rs + VRecType ltys -> checkRecFields ge scope rs ltys + VMeta _ _ _ -> inferRecFields ge scope rs _ -> tcError ("Record type is inferred but:" $$ - nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) ty)) $$ + nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) ty)) $$ "is expected in the expresion:" $$ nest 2 (ppTerm Unqualified 0 t)) - return (R [(l, (Just (value2term gr (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], - VRecType [(l, ty) | (l,t,ty) <- lttys] + return (R [(l, (Just (value2term loc (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], + VRecType [(l, ty) | (l,t,ty) <- lttys] ) -tcRho gr scope (P t l) mb_ty = do +tcRho ge scope (P t l) mb_ty = do x_ty <- case mb_ty of Just ty -> return ty - Nothing -> do i <- newMeta (eval gr [] typeType) + Nothing -> do i <- newMeta vtypeType return (VMeta i (scopeEnv scope) []) - (t,t_ty) <- tcRho gr scope t (Just (VRecType [(l,x_ty)])) + (t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,x_ty)])) return (P t l,x_ty) -tcRho gr scope (C t1 t2) mb_ty = do - (t1,t1_ty) <- tcRho gr scope t1 (Just (eval gr [] typeStr)) - (t2,t2_ty) <- tcRho gr scope t2 (Just (eval gr [] typeStr)) - instSigma gr scope (C t1 t2) (eval gr [] typeStr) mb_ty -tcRho gr scope (Glue t1 t2) mb_ty = do - (t1,t1_ty) <- tcRho gr scope t1 (Just (eval gr [] typeStr)) - (t2,t2_ty) <- tcRho gr scope t2 (Just (eval gr [] typeStr)) - instSigma gr scope (Glue t1 t2) (eval gr [] typeStr) mb_ty -tcRho gr scope t@(ExtR t1 t2) mb_ty = do - (t1,t1_ty) <- tcRho gr scope t1 Nothing - (t2,t2_ty) <- tcRho gr scope t2 Nothing +tcRho ge scope (C t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr) + instSigma ge scope (C t1 t2) vtypeStr mb_ty +tcRho ge scope (Glue t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr) + instSigma ge scope (Glue t1 t2) vtypeStr mb_ty +tcRho ge scope t@(ExtR t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho ge scope t1 Nothing + (t2,t2_ty) <- tcRho ge scope t2 Nothing case (t1_ty,t2_ty) of (VSort s1,VSort s2) - | s1 == cType && s2 == cType -> instSigma gr scope (ExtR t1 t2) (VSort cType) mb_ty + | s1 == cType && s2 == cType -> instSigma ge scope (ExtR t1 t2) (VSort cType) mb_ty (VRecType rs1, VRecType rs2) | otherwise -> do tcWarn (pp "bbbb") - instSigma gr scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty + instSigma ge scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty _ -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t) -tcRho gr scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser - tcRho gr scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty -tcRho gr scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser - tcRho gr scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty -tcRho gr scope (Alts t ss) mb_ty = do - (t,_) <- tcRho gr scope t (Just (eval gr [] typeStr)) +tcRho ge scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho ge scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty +tcRho ge scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho ge scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty +tcRho ge scope (Alts t ss) mb_ty = do + (t,_) <- tcRho ge scope t (Just vtypeStr) ss <- flip mapM ss $ \(t1,t2) -> do - (t1,_) <- tcRho gr scope t1 (Just (eval gr [] typeStr)) - (t2,_) <- tcRho gr scope t2 (Just (eval gr [] typeStrs)) + (t1,_) <- tcRho ge scope t1 (Just vtypeStr) + (t2,_) <- tcRho ge scope t2 (Just vtypeStrs) return (t1,t2) - instSigma gr scope (Alts t ss) (eval gr [] typeStr) mb_ty -tcRho gr scope (Strs ss) mb_ty = do + instSigma ge scope (Alts t ss) vtypeStr mb_ty +tcRho ge scope (Strs ss) mb_ty = do ss <- flip mapM ss $ \t -> do - (t,_) <- tcRho gr scope t (Just (eval gr [] typeStr)) + (t,_) <- tcRho ge scope t (Just vtypeStr) return t - instSigma gr scope (Strs ss) (eval gr [] typeStrs) mb_ty + instSigma ge scope (Strs ss) vtypeStrs mb_ty tcRho gr scope t _ = error ("tcRho "++show t) -tcCase gr scope p_ty res_ty (p,t) = do - scope <- tcPatt gr scope p p_ty - (t,res_ty) <- tcRho gr scope t (Just res_ty) +tcCase ge scope p_ty res_ty (p,t) = do + scope <- tcPatt ge scope p p_ty + (t,res_ty) <- tcRho ge scope t (Just res_ty) return (p,t) -tcPatt gr scope PW ty0 = +tcPatt ge scope PW ty0 = return scope -tcPatt gr scope (PV x) ty0 = +tcPatt ge scope (PV x) ty0 = return ((x,ty0):scope) -tcPatt gr scope (PP c ps) ty0 = - case lookupResType gr c of - Ok ty -> do let go scope ty [] = return (scope,ty) - go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun gr scope (VGen (length scope) []) ty - scope <- tcPatt gr scope p arg_ty - go scope res_ty ps - (scope,ty) <- go scope (eval gr [] ty) ps - unify gr scope ty0 ty - return scope - Bad err -> tcError (pp err) -tcPatt gr scope (PString s) ty0 = do - unify gr scope ty0 (eval gr [] typeStr) +tcPatt ge scope (PP c ps) ty0 = + let GE gr _ _ loc = ge + in case lookupResType gr c of + Ok ty -> do let go scope ty [] = return (scope,ty) + go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun loc scope (VGen (length scope) []) ty + scope <- tcPatt ge scope p arg_ty + go scope res_ty ps + vty <- runErr (eval ge ty) + (scope,ty) <- go scope vty ps + unify loc scope ty0 ty + return scope + Bad err -> tcError (pp err) +tcPatt ge scope (PString s) ty0 = do + let GE _ _ _ loc = ge + unify loc scope ty0 vtypeStr return scope -tcPatt gr scope PChar ty0 = do - unify gr scope ty0 (eval gr [] typeStr) +tcPatt ge scope PChar ty0 = do + let GE _ _ _ loc = ge + unify loc scope ty0 vtypeStr return scope -tcPatt gr scope (PSeq p1 p2) ty0 = do - unify gr scope ty0 (eval gr [] typeStr) - scope <- tcPatt gr scope p1 (eval gr [] typeStr) - scope <- tcPatt gr scope p2 (eval gr [] typeStr) +tcPatt ge scope (PSeq p1 p2) ty0 = do + let GE _ _ _ loc = ge + unify loc scope ty0 vtypeStr + scope <- tcPatt ge scope p1 vtypeStr + scope <- tcPatt ge scope p2 vtypeStr return scope -tcPatt gr scope (PAs x p) ty0 = do - tcPatt gr ((x,ty0):scope) p ty0 -tcPatt gr scope (PR rs) ty0 = do +tcPatt ge scope (PAs x p) ty0 = do + tcPatt ge ((x,ty0):scope) p ty0 +tcPatt ge scope (PR rs) ty0 = do let go scope [] = return (scope,[]) - go scope ((l,p):rs) = do i <- newMeta (eval gr [] typePType) + go scope ((l,p):rs) = do i <- newMeta vtypePType let ty = VMeta i (scopeEnv scope) [] - scope <- tcPatt gr scope p ty + scope <- tcPatt ge scope p ty (scope,rs) <- go scope rs return (scope,(l,ty) : rs) (scope',rs) <- go scope rs - unify gr scope ty0 (VRecType rs) + let GE _ _ _ loc = ge + unify loc scope ty0 (VRecType rs) return scope' tcPatt gr scope (PAlt p1 p2) ty0 = do tcPatt gr scope p1 ty0 tcPatt gr scope p2 ty0 return scope -tcPatt gr scope p ty = unimplemented ("tcPatt "++show p) +tcPatt ge scope p ty = unimplemented ("tcPatt "++show p) +inferRecFields ge scope rs = + mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs -inferRecFields gr scope rs = - mapM (\(l,r) -> tcRecField gr scope l r Nothing) rs - -checkRecFields gr scope [] ltys +checkRecFields ge scope [] ltys | null ltys = return [] | otherwise = tcError ("Missing fields:" <+> hsep (map fst ltys)) -checkRecFields gr scope ((l,t):lts) ltys = +checkRecFields ge scope ((l,t):lts) ltys = case takeIt l ltys of - (Just ty,ltys) -> do ltty <- tcRecField gr scope l t (Just ty) - lttys <- checkRecFields gr scope lts ltys + (Just ty,ltys) -> do ltty <- tcRecField ge scope l t (Just ty) + lttys <- checkRecFields ge scope lts ltys return (ltty : lttys) (Nothing,ltys) -> do tcWarn ("Discarded field:" <+> l) - ltty <- tcRecField gr scope l t Nothing - lttys <- checkRecFields gr scope lts ltys + ltty <- tcRecField ge scope l t Nothing + lttys <- checkRecFields ge scope lts ltys return lttys -- ignore the field where takeIt l1 [] = (Nothing, []) @@ -271,63 +299,64 @@ checkRecFields gr scope ((l,t):lts) ltys = | otherwise = let (mb_ty,ltys') = takeIt l1 ltys in (mb_ty,lty:ltys') -tcRecField gr scope l (mb_ann_ty,t) mb_ty = do +tcRecField ge scope l (mb_ann_ty,t) mb_ty = do (t,ty) <- case mb_ann_ty of - Just ann_ty -> do (ann_ty, _) <- tcRho gr scope ann_ty (Just (eval gr [] typeType)) - let v_ann_ty = eval gr (scopeEnv scope) ann_ty - t <- checkSigma gr scope t v_ann_ty - instSigma gr scope t v_ann_ty mb_ty - Nothing -> tcRho gr scope t mb_ty + Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) + ov_ann_ty <- runErr (value (toplevel ge) ann_ty) + let v_ann_ty = ov_ann_ty (scopeStack scope) + t <- checkSigma ge scope t v_ann_ty + instSigma ge scope t v_ann_ty mb_ty + Nothing -> tcRho ge scope t mb_ty return (l,t,ty) -- | Invariant: if the third argument is (Just rho), -- then rho is in weak-prenex form -instSigma :: SourceGrammar -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho) -instSigma gr scope t ty1 Nothing = instantiate gr t ty1 -- INST1 -instSigma gr scope t ty1 (Just ty2) = do -- INST2 - t <- subsCheckRho gr scope t ty1 ty2 +instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho) +instSigma ge scope t ty1 Nothing = instantiate t ty1 -- INST1 +instSigma ge scope t ty1 (Just ty2) = do -- INST2 + let GE _ _ _ loc = ge + t <- subsCheckRho loc scope t ty1 ty2 return (t,ty2) -- | (subsCheck scope args off exp) checks that -- 'off' is at least as polymorphic as 'args -> exp' -subsCheck :: SourceGrammar -> Scope -> Term -> Sigma -> Sigma -> TcM Term -subsCheck gr scope t sigma1 sigma2 = do -- DEEP-SKOL - (abs, scope, t, rho2) <- skolemise id gr scope t sigma2 +subsCheck :: GLocation -> Scope -> Term -> Sigma -> Sigma -> TcM Term +subsCheck loc scope t sigma1 sigma2 = do -- DEEP-SKOL + (abs, scope, t, rho2) <- skolemise id scope t sigma2 let skol_tvs = [] - t <- subsCheckRho gr scope t sigma1 rho2 - esc_tvs <- getFreeVars gr [(scope,sigma1),(scope,sigma2)] + t <- subsCheckRho loc scope t sigma1 rho2 + esc_tvs <- getFreeVars loc [(scope,sigma1),(scope,sigma2)] let bad_tvs = filter (`elem` esc_tvs) skol_tvs if null bad_tvs then return (abs t) else tcError (vcat [pp "Subsumption check failed:", - nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) sigma1)), + nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) sigma1)), pp "is not as polymorphic as", - nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) sigma2))]) - + nest 2 (ppTerm Unqualified 0 (value2term loc (scopeVars scope) sigma2))]) -- | Invariant: the second argument is in weak-prenex form -subsCheckRho :: SourceGrammar -> Scope -> Term -> Sigma -> Rho -> TcM Term -subsCheckRho gr scope t sigma1@(VClosure env (Prod Implicit _ _ _)) rho2 = do -- Rule SPEC - (t,rho1) <- instantiate gr t sigma1 - subsCheckRho gr scope t rho1 rho2 -subsCheckRho gr scope t rho1 (VClosure env (Prod Explicit _ a2 r2)) = do -- Rule FUN - (a1,r1) <- unifyFun gr scope (VGen (length scope) []) rho1 - subsCheckFun gr scope t a1 r1 (eval gr env a2) (eval gr env r2) -subsCheckRho gr scope t (VClosure env (Prod Explicit _ a1 r1)) rho2 = do -- Rule FUN - (a2,r2) <- unifyFun gr scope (VGen (length scope) []) rho2 - subsCheckFun gr scope t (eval gr env a1) (eval gr env r1) a2 r2 -subsCheckRho gr scope t (VSort s1) (VSort s2) +subsCheckRho :: GLocation -> Scope -> Term -> Sigma -> Rho -> TcM Term +subsCheckRho loc scope t sigma1@(VProd Implicit _ _ _) rho2 = do -- Rule SPEC + (t,rho1) <- instantiate t sigma1 + subsCheckRho loc scope t rho1 rho2 +subsCheckRho loc scope t rho1 (VProd Explicit a2 _ (Bind r2)) = do -- Rule FUN + (a1,r1) <- unifyFun loc scope (VGen (length scope) []) rho1 + subsCheckFun loc scope t a1 r1 a2 (r2 (VGen (length scope) [])) +subsCheckRho loc scope t (VProd Explicit a1 _ (Bind r1)) rho2 = do -- Rule FUN + (a2,r2) <- unifyFun loc scope (VGen (length scope) []) rho2 + subsCheckFun loc scope t a1 (r1 (VGen (length scope) [])) a2 r2 +subsCheckRho loc scope t (VSort s1) (VSort s2) | s1 == cPType && s2 == cType = return t -subsCheckRho gr scope t tau1 tau2 = do -- Rule MONO - unify gr scope tau1 tau2 -- Revert to ordinary unification +subsCheckRho loc scope t tau1 tau2 = do -- Rule MONO + unify loc scope tau1 tau2 -- Revert to ordinary unification return t -subsCheckFun :: SourceGrammar -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term -subsCheckFun gr scope t a1 r1 a2 r2 = do +subsCheckFun :: GLocation -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term +subsCheckFun loc scope t a1 r1 a2 r2 = do let v = newVar scope - vt <- subsCheck gr scope (Vr v) a2 a1 - t <- subsCheckRho gr ((v,eval gr [] typeType):scope) (App t vt) r1 r2 ; + vt <- subsCheck loc scope (Vr v) a2 a1 + t <- subsCheckRho loc ((v,vtypeType):scope) (App t vt) r1 r2 ; return (Abs Explicit v t) @@ -335,102 +364,97 @@ subsCheckFun gr scope t a1 r1 a2 r2 = do -- Unification ----------------------------------------------------------------------- -unifyFun :: SourceGrammar -> Scope -> Value -> Rho -> TcM (Sigma, Rho) -unifyFun gr scope arg_v (VClosure env (Prod Explicit x arg res)) - | x /= identW = return (eval gr env arg,eval gr ((x,arg_v):env) res) - | otherwise = return (eval gr env arg,eval gr env res) -unifyFun gr scope arg_v tau = do - arg_ty <- newMeta (eval gr [] typeType) - res_ty <- newMeta (eval gr [] typeType) - unify gr scope tau (VClosure [] (Prod Explicit identW (Meta arg_ty) (Meta res_ty))) +unifyFun :: GLocation -> Scope -> Value -> Rho -> TcM (Sigma, Rho) +unifyFun loc scope arg_v (VProd Explicit arg x (Bind res)) = + return (arg,res arg_v) +unifyFun loc scope arg_v tau = do + arg_ty <- newMeta vtypeType + res_ty <- newMeta vtypeType + unify loc scope tau (VProd Explicit (VMeta arg_ty [] []) identW (Bind (const (VMeta arg_ty [] [])))) return (VMeta arg_ty [] [], VMeta res_ty [] []) -unify gr scope (VApp f1 vs1) (VApp f2 vs2) - | f1 == f2 = sequence_ (zipWith (unify gr scope) vs1 vs2) -unify gr scope (VSort s1) (VSort s2) +unify loc scope (VApp f1 vs1) (VApp f2 vs2) + | f1 == f2 = sequence_ (zipWith (unify loc scope) vs1 vs2) +unify loc scope (VSort s1) (VSort s2) | s1 == s2 = return () -unify gr scope (VGen i vs1) (VGen j vs2) - | i == j = sequence_ (zipWith (unify gr scope) vs1 vs2) -unify gr scope (VMeta i env1 vs1) (VMeta j env2 vs2) - | i == j = sequence_ (zipWith (unify gr scope) vs1 vs2) +unify loc scope (VGen i vs1) (VGen j vs2) + | i == j = sequence_ (zipWith (unify loc scope) vs1 vs2) +unify loc scope (VMeta i env1 vs1) (VMeta j env2 vs2) + | i == j = sequence_ (zipWith (unify loc scope) vs1 vs2) | otherwise = do mv <- getMeta j case mv of - Bound t2 -> unify gr scope (VMeta i env1 vs1) (apply gr env2 t2 vs2) + --Bound t2 -> unify gr scope (VMeta i env1 vs1) (apply gr env2 t2 vs2) Unbound _ -> setMeta i (Bound (Meta j)) -unify gr scope (VMeta i env vs) v = unifyVar gr scope i env vs v -unify gr scope v (VMeta i env vs) = unifyVar gr scope i env vs v -unify gr scope (VTblType p1 res1) (VTblType p2 res2) = do - unify gr scope p1 p2 - unify gr scope res1 res2 -unify gr scope (VRecType rs1) (VRecType rs2) = do - sequence_ [unify gr scope ty1 ty2 | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]] -unify gr scope v1 v2 = do - t1 <- zonkTerm (value2term gr (scopeVars scope) v1) - t2 <- zonkTerm (value2term gr (scopeVars scope) v2) +unify loc scope (VMeta i env vs) v = unifyVar loc scope i env vs v +unify loc scope v (VMeta i env vs) = unifyVar loc scope i env vs v +unify loc scope (VTblType p1 res1) (VTblType p2 res2) = do + unify loc scope p1 p2 + unify loc scope res1 res2 +unify loc scope (VRecType rs1) (VRecType rs2) = do + sequence_ [unify loc scope ty1 ty2 | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]] +unify loc scope v1 v2 = do + t1 <- zonkTerm (value2term loc (scopeVars scope) v1) + t2 <- zonkTerm (value2term loc (scopeVars scope) v2) tcError ("Cannot unify types:" <+> (ppTerm Unqualified 0 t1 $$ ppTerm Unqualified 0 t2)) -- | Invariant: tv1 is a flexible type variable -unifyVar :: SourceGrammar -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM () -unifyVar gr scope i env vs ty2 = do -- Check whether i is bound +unifyVar :: GLocation -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM () +unifyVar loc scope i env vs ty2 = do -- Check whether i is bound mv <- getMeta i case mv of - Bound ty1 -> unify gr scope (apply gr env ty1 vs) ty2 - Unbound _ -> do let ty2' = value2term gr (scopeVars scope) ty2 - ms2 <- getMetaVars gr [(scope,ty2)] +-- Bound ty1 -> unify gr scope (apply gr env ty1 vs) ty2 + Unbound _ -> do let ty2' = value2term loc (scopeVars scope) ty2 + ms2 <- getMetaVars loc [(scope,ty2)] if i `elem` ms2 then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$ nest 2 (ppTerm Unqualified 0 ty2')) else setMeta i (Bound ty2') - ----------------------------------------------------------------------- -- Instantiation and quantification ----------------------------------------------------------------------- -- | Instantiate the topmost for-alls of the argument type -- with metavariables -instantiate :: SourceGrammar -> Term -> Sigma -> TcM (Term,Rho) -instantiate gr t (VClosure env (Prod Implicit x ty1 ty2)) = do - i <- newMeta (eval gr env ty1) - instantiate gr (App t (ImplArg (Meta i))) (eval gr ((x,VMeta i [] []):env) ty2) -instantiate gr t ty = do +instantiate :: Term -> Sigma -> TcM (Term,Rho) +instantiate t (VProd Implicit ty1 x (Bind ty2)) = do + i <- newMeta ty1 + instantiate (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) +instantiate t ty = do return (t,ty) -skolemise f gr scope t (VClosure env (Prod Implicit x arg_ty res_ty)) -- Rule PRPOLY +skolemise f scope t (VProd Implicit arg_ty x (Bind res_ty)) -- Rule PRPOLY | x /= identW = let (y,body) = case t of Abs Implicit y body -> (y, body) body -> (newVar scope, body) in skolemise (f . Abs Implicit y) - gr - ((y,eval gr env arg_ty):scope) body - (eval gr ((x,VGen (length scope) []):env) res_ty) -skolemise f gr scope t (VClosure env (Prod Explicit x arg_ty res_ty)) -- Rule PRFUN - | x /= identW = + ((y,arg_ty):scope) body + (res_ty (VGen (length scope) [])) +skolemise f scope t (VProd Explicit arg_ty x (Bind res_ty)) -- Rule PRFUN + | x /= identW = let (y,body) = case t of Abs Explicit y body -> (y, body) body -> let y = newVar scope in (y, App body (Vr y)) in skolemise (f . Abs Explicit y) - gr - ((y,eval gr env arg_ty):scope) body - (eval gr ((x,VGen (length scope) []):env) res_ty) -skolemise f gr scope t ty -- Rule PRMONO + ((y,arg_ty):scope) body + (res_ty (VGen (length scope) [])) +skolemise f scope t ty -- Rule PRMONO = return (f, scope, t, ty) - -- | Quantify over the specified type variables (all flexible) -quantify :: SourceGrammar -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma) -quantify gr scope t tvs ty0 = do +quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma) +quantify ge scope t tvs ty0 = do mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way ty <- zonkTerm ty -- of doing the substitution - return (foldr (Abs Implicit) t new_bndrs - ,eval gr [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs) - ) + vty <- runErr (eval ge (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs)) + return (foldr (Abs Implicit) t new_bndrs,vty) where - ty = value2term gr (scopeVars scope) ty0 - + GE _ _ _ loc = ge + ty = value2term loc (scopeVars scope) ty0 + used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use new_bndrs = take (length tvs) (allBinders \\ used_bndrs) bind (i, name) = setMeta i (Bound (Vr name)) @@ -491,6 +515,10 @@ runTcM f = case unTcM f IntMap.empty [] of TcOk x _ msgs -> do checkWarnings msgs; return x TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg +runErr :: Err a -> TcM a +runErr (Bad msg) = TcM (\ms msgs -> TcFail (pp msg:msgs)) +runErr (Ok x) = TcM (\ms msgs -> TcOk x ms msgs) + newMeta :: Sigma -> TcM MetaId newMeta ty = TcM (\ms msgs -> let i = IntMap.size ms @@ -514,14 +542,15 @@ newVar scope = head [x | i <- [1..], isFree ((y,_):scope) x = x /= y && isFree scope x scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..] +scopeStack scope = zipWith (\(x,ty) i -> VGen i []) (reverse scope) [0..] scopeVars scope = map fst scope scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) -- | This function takes account of zonking, and returns a set -- (no duplicates) of unbound meta-type variables -getMetaVars :: SourceGrammar -> [(Scope,Sigma)] -> TcM [MetaId] -getMetaVars gr sc_tys = do - tys <- mapM (\(scope,ty) -> zonkTerm (value2term gr (scopeVars scope) ty)) sc_tys +getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId] +getMetaVars loc sc_tys = do + tys <- mapM (\(scope,ty) -> zonkTerm (value2term loc (scopeVars scope) ty)) sc_tys return (foldr go [] tys) where -- Get the MetaIds from a term; no duplicates in result @@ -539,9 +568,9 @@ getMetaVars gr sc_tys = do -- | This function takes account of zonking, and returns a set -- (no duplicates) of free type variables -getFreeVars :: SourceGrammar -> [(Scope,Sigma)] -> TcM [Ident] -getFreeVars gr sc_tys = do - tys <- mapM (\(scope,ty) -> zonkTerm (value2term gr (scopeVars scope) ty)) sc_tys +getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident] +getFreeVars loc sc_tys = do + tys <- mapM (\(scope,ty) -> zonkTerm (value2term loc (scopeVars scope) ty)) sc_tys return (foldr (go []) [] tys) where go bound (Vr tv) acc @@ -566,3 +595,4 @@ zonkTerm (Meta i) = do return t zonkTerm t = composOp zonkTerm t +