From bd9bd8b32f61f010a2cb0d38146d0671c7b985eb Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Fri, 24 Nov 2023 08:35:11 +0100 Subject: [PATCH] the experimental typechecker is almost converted to the new evaluator --- src/compiler/GF/Compile/Compute/Concrete.hs | 50 +- .../GF/Compile/TypeCheck/ConcreteNew.hs | 598 +++++++++--------- 2 files changed, 331 insertions(+), 317 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 6b19a15e6..7844fcf93 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -4,20 +4,22 @@ -- | preparation for PMCFG generation. module GF.Compile.Compute.Concrete ( normalForm - , Value(..), Thunk, ThunkState(..), Env, showValue + , Value(..), Thunk, ThunkState(..), Env, Scope, showValue , MetaThunks , EvalM(..), runEvalM, evalError , eval, apply, force, value2term, patternMatch , newThunk, newEvaluatedThunk , newResiduation, newNarrowing, getVariables - , getRef - , getResDef, getInfo, getAllParamValues + , getRef, setRef + , getResDef, getInfo, getResType, getAllParamValues ) where import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint import GF.Grammar hiding (Env, VGen, VApp, VRecType) -import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo,allParamValues) +import GF.Grammar.Lookup(lookupResDef,lookupResType, + lookupOrigInfo,lookupOverloadTypes, + allParamValues) import GF.Grammar.Predef import GF.Grammar.Lockfield(lockLabel) import GF.Grammar.Printer @@ -45,14 +47,18 @@ normalForm gr t = mkFV [t] = t mkFV ts = FV ts +type Sigma s = Value s + data ThunkState s = Unevaluated (Env s) Term | Evaluated {-# UNPACK #-} !Int (Value s) - | Residuation {-# UNPACK #-} !MetaId + | Hole {-# UNPACK #-} !MetaId + | Residuation {-# UNPACK #-} !MetaId (Scope s) (Value s) | Narrowing {-# UNPACK #-} !MetaId Type type Thunk s = STRef s (ThunkState s) type Env s = [(Ident,Thunk s)] +type Scope s = [(Ident,Value s)] data Value s = VApp QIdent [Thunk s] @@ -131,7 +137,7 @@ eval env (App t1 t2) vs = do tnk <- newThunk env t2 eval env t1 (tnk : vs) eval env (Abs b x t) [] = return (VClosure env (Abs b x t)) eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs -eval env (Meta i) vs = do tnk <- newResiduation i +eval env (Meta i) vs = do tnk <- newHole i return (VMeta tnk env vs) eval env (ImplArg t) [] = eval env t [] eval env (Prod b x t1 t2)[] = do v1 <- eval env t1 [] @@ -733,6 +739,12 @@ getInfo q = EvalM $ \gr k mt d r -> do Ok res -> k res mt d r Bad msg -> return (Fail (pp msg)) +getResType :: QIdent -> EvalM s Type +getResType q = EvalM $ \gr k mt d r -> do + case lookupResType gr q of + Ok t -> k t mt d r + Bad msg -> return (Fail (pp msg)) + getAllParamValues :: Type -> EvalM s [Term] getAllParamValues ty = EvalM $ \gr k mt d r -> case allParamValues gr ty of @@ -747,15 +759,19 @@ newEvaluatedThunk v = EvalM $ \gr k mt d r -> do tnk <- newSTRef (Evaluated maxBound v) k tnk mt d r -newResiduation i = EvalM $ \gr k mt d r -> +newHole i = EvalM $ \gr k mt d r -> if i == 0 - then do tnk <- newSTRef (Residuation i) + then do tnk <- newSTRef (Hole i) k tnk mt d r else case Map.lookup i mt of Just tnk -> k tnk mt d r - Nothing -> do tnk <- newSTRef (Residuation i) + Nothing -> do tnk <- newSTRef (Hole i) k tnk (Map.insert i tnk mt) d r +newResiduation scope ty = EvalM $ \gr k mt d r -> do + tnk <- newSTRef (Residuation 0 scope ty) + k tnk mt d r + newNarrowing i ty = EvalM $ \gr k mt d r -> if i == 0 then do tnk <- newSTRef (Narrowing i ty) @@ -788,6 +804,7 @@ getVariables = EvalM $ \gr k mt d r -> do _ -> metas2params gr tnks getRef tnk = EvalM $ \gr k mt d r -> readSTRef tnk >>= \st -> k st mt d r +setRef tnk st = EvalM $ \gr k mt d r -> writeSTRef tnk st >>= \st -> k () mt d r force tnk = EvalM $ \gr k mt d r -> do s <- readSTRef tnk @@ -799,7 +816,8 @@ force tnk = EvalM $ \gr k mt d r -> do writeSTRef tnk s return r) mt d r Evaluated d v -> k v mt d r - Residuation _ -> k (VMeta tnk [] []) mt d r + Hole _ -> k (VMeta tnk [] []) mt d r + Residuation _ _ _ -> k (VMeta tnk [] []) mt d r Narrowing _ _ -> k (VMeta tnk [] []) mt d r tnk2term xs tnk = EvalM $ \gr k mt d r -> @@ -835,13 +853,15 @@ tnk2term xs tnk = EvalM $ \gr k mt d r -> Fail msg -> return (Fail msg) Success (r,0,xs) -> k (FV []) mt d r Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r - Residuation i -> k (Meta i) mt d r + Hole i -> k (Meta i) mt d r + Residuation i _ _ -> k (Meta i) mt d r Narrowing i _ -> k (Meta i) mt d r zonk tnk vs = EvalM $ \gr k mt d r -> do s <- readSTRef tnk case s of - Evaluated _ v -> case apply v vs of - EvalM f -> f gr (k . Left) mt d r - Residuation i -> k (Right i) mt d r - Narrowing i _ -> k (Right i) mt d r + Evaluated _ v -> case apply v vs of + EvalM f -> f gr (k . Left) mt d r + Hole i -> k (Right i) mt d r + Residuation i _ _ -> k (Right i) mt d r + Narrowing i _ -> k (Right i) mt d r diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index e71858975..6eab451ab 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -14,7 +14,7 @@ import GF.Compile.Compute.Concrete import GF.Infra.CheckM import GF.Data.Operations import Control.Applicative(Applicative(..)) -import Control.Monad(ap,liftM,mplus,foldM) +import Control.Monad(ap,liftM,mplus,foldM,zipWithM) import Control.Monad.ST import GF.Text.Pretty import Data.List (nub, (\\), tails) @@ -62,308 +62,319 @@ tcRho scope t@(Vr v) mb_ty = do -- VAR Just v_sigma -> instSigma scope t v_sigma mb_ty Nothing -> tcError ("Unknown variable" <+> v) tcRho scope t@(Q id) mb_ty = - runTcA (tcOverloadFailed t) $ - tcApp scope t `bindTcA` \(t,ty) -> + runTcA (tcOverloadFailed t) $ \gr -> + tcApp gr scope t `bindTcA` \(t,ty) -> instSigma scope t ty mb_ty tcRho scope t@(QC id) mb_ty = - runTcA (tcOverloadFailed t) $ - tcApp scope t `bindTcA` \(t,ty) -> + runTcA (tcOverloadFailed t) $ \gr -> + tcApp gr scope t `bindTcA` \(t,ty) -> instSigma scope t ty mb_ty tcRho scope t@(App fun arg) mb_ty = do - runTcA (tcOverloadFailed t) $ - tcApp scope t `bindTcA` \(t,ty) -> + runTcA (tcOverloadFailed t) $ \gr -> + tcApp gr scope t `bindTcA` \(t,ty) -> instSigma scope t ty mb_ty -{-tcRho scope (Abs bt var body) Nothing = do -- ABS1 - i <- newMeta scope vtypeType - let arg_ty = VMeta i (scopeEnv scope) [] +tcRho scope (Abs bt var body) Nothing = do -- ABS1 + tnk <- liftEvalM (newResiduation scope vtypeType) + env <- scopeEnv scope + let arg_ty = VMeta tnk env [] (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing - return (Abs bt var body, (VProd bt arg_ty identW body_ty)) -tcRho ge scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 - (bt, var_ty, body_ty) <- unifyFun ge scope ty + return (Abs bt var body, (VProd bt identW arg_ty body_ty)) +tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2 + (bt, var_ty, body_ty) <- unifyFun scope ty if bt == Implicit then return () else tcError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") - (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) []))) + (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (Abs Implicit var body,ty) -tcRho ge scope (Abs Explicit var body) (Just ty) = do -- ABS3 - (scope,f,ty') <- skolemise ge scope ty - (_,var_ty,body_ty) <- unifyFun ge scope ty' - (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) []))) +tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3 + (scope,f,ty') <- skolemise scope ty + (_,var_ty,body_ty) <- unifyFun scope ty' + (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty) return (f (Abs Explicit var body),ty) -tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET +tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET (rhs,var_ty) <- case mb_ann_ty of - Nothing -> inferSigma ge scope rhs - Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) - v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty) - (rhs,_) <- tcRho ge scope rhs (Just v_ann_ty) + Nothing -> inferSigma scope rhs + Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) + env <- scopeEnv scope + v_ann_ty <- liftEvalM (eval env ann_ty []) + (rhs,_) <- tcRho scope rhs (Just v_ann_ty) return (rhs, v_ann_ty) - (body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty - var_ty <- tc_value2term (geLoc ge) (scopeVars scope) var_ty + (body, body_ty) <- tcRho ((var,var_ty):scope) body mb_ty + var_ty <- liftEvalM (value2term (scopeVars scope) var_ty) return (Let (var, (Just 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) - v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty) - (body,_) <- tcRho ge scope body (Just v_ann_ty) - instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty -tcRho ge scope (FV ts) mb_ty = do +tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT + (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) + env <- scopeEnv scope + v_ann_ty <- liftEvalM (eval env ann_ty []) + (body,_) <- tcRho scope body (Just v_ann_ty) + instSigma scope (Typed body ann_ty) v_ann_ty mb_ty +tcRho scope (FV ts) mb_ty = do case ts of - [] -> do i <- newMeta scope vtypeType - instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty - (t:ts) -> do (t,ty) <- tcRho ge scope t mb_ty + [] -> do i <- liftEvalM (newResiduation scope vtypeType) + env <- scopeEnv scope + instSigma scope (FV []) (VMeta i env []) mb_ty + (t:ts) -> do (t,ty) <- tcRho scope t mb_ty let go [] ty = return ([],ty) - go (t:ts) ty = do (t, ty) <- tcRho ge scope t (Just ty) + go (t:ts) ty = do (t, ty) <- tcRho scope t (Just ty) (ts,ty) <- go ts ty return (t:ts,ty) (ts,ty) <- go ts ty return (FV (t:ts), ty) -tcRho ge scope t@(Sort s) mb_ty = do - instSigma ge scope t vtypeType mb_ty -tcRho ge scope t@(RecType rs) Nothing = do - (rs,mb_ty) <- tcRecTypeFields ge scope rs Nothing +tcRho scope t@(Sort s) mb_ty = do + instSigma scope t vtypeType mb_ty +tcRho scope t@(RecType rs) Nothing = do + (rs,mb_ty) <- tcRecTypeFields scope rs Nothing return (RecType rs,fromMaybe vtypePType mb_ty) -tcRho ge scope t@(RecType rs) (Just ty) = do - (scope,f,ty') <- skolemise ge scope ty +tcRho scope t@(RecType rs) (Just ty) = do + (scope,f,ty') <- skolemise scope ty case ty' of VSort s | s == cType -> return () | s == cPType -> return () VMeta i env vs -> case rs of - [] -> unifyVar ge scope i env vs vtypePType + [] -> unifyVar scope i env vs vtypePType _ -> return () - ty -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty + ty -> do ty <- zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty) tcError ("The record type" <+> ppTerm Unqualified 0 t $$ "cannot be of type" <+> ppTerm Unqualified 0 ty) - (rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty') + (rs,mb_ty) <- tcRecTypeFields scope rs (Just ty') return (f (RecType rs),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 (Just vtypeType) - instSigma ge scope (Table p res) vtypeType mb_ty -tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do - (ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType) - vty1 <- liftErr (eval ge (scopeEnv scope) ty1) - (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 scope vtypePType +tcRho scope t@(Table p res) mb_ty = do + (p, p_ty) <- tcRho scope p (Just vtypePType) + (res,res_ty) <- tcRho scope res (Just vtypeType) + instSigma scope (Table p res) vtypeType mb_ty +tcRho scope (Prod bt x ty1 ty2) mb_ty = do + (ty1,ty1_ty) <- tcRho scope ty1 (Just vtypeType) + env <- scopeEnv scope + vty1 <- liftEvalM (eval env ty1 []) + (ty2,ty2_ty) <- tcRho ((x,vty1):scope) ty2 (Just vtypeType) + instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty +tcRho scope (S t p) mb_ty = do + env <- scopeEnv scope + p_ty <- fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType) res_ty <- case mb_ty of - Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType + Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType) Just ty -> return ty - let t_ty = VTblType p_ty res_ty - (t,t_ty) <- tcRho ge scope t (Just t_ty) - (p,_) <- tcRho ge scope p (Just p_ty) + let t_ty = VTable p_ty res_ty + (t,t_ty) <- tcRho scope t (Just t_ty) + (p,_) <- tcRho scope p (Just p_ty) return (S t p, res_ty) -tcRho ge scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables +tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables + env <- scopeEnv scope p_ty <- case tt of - TRaw -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType - TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType) - liftErr (eval ge (scopeEnv scope) ty) - (ps,mb_res_ty) <- tcCases ge scope ps p_ty Nothing + TRaw -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType) + TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) + liftEvalM (eval env ty []) + (ps,mb_res_ty) <- tcCases scope ps p_ty Nothing res_ty <- case mb_res_ty of Just res_ty -> return res_ty - Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType - p_ty_t <- tc_value2term (geLoc ge) [] p_ty - return (T (TTyped p_ty_t) ps, VTblType p_ty res_ty) -tcRho ge scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables - (scope,f,ty') <- skolemise ge scope ty - (p_ty, res_ty) <- unifyTbl ge scope ty' + Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType) + p_ty_t <- liftEvalM (value2term [] p_ty) + return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) +tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables + (scope,f,ty') <- skolemise scope ty + (p_ty, res_ty) <- unifyTbl scope ty' case tt of TRaw -> return () - TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType) + TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType) return ()--subsCheckRho ge scope -> Term ty res_ty - (ps,Just res_ty) <- tcCases ge scope ps p_ty (Just res_ty) - p_ty_t <- tc_value2term (geLoc ge) [] p_ty - return (f (T (TTyped p_ty_t) ps), VTblType p_ty res_ty) -tcRho ge scope (R rs) Nothing = do - lttys <- inferRecFields ge scope rs - rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys + (ps,Just res_ty) <- tcCases scope ps p_ty (Just res_ty) + p_ty_t <- liftEvalM (value2term [] p_ty) + return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) +tcRho scope (R rs) Nothing = do + lttys <- inferRecFields scope rs + rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) return (R rs, VRecType [(l, ty) | (l,t,ty) <- lttys] ) -tcRho ge scope (R rs) (Just ty) = do - (scope,f,ty') <- skolemise ge scope ty +tcRho scope (R rs) (Just ty) = do + (scope,f,ty') <- skolemise scope ty case ty' of - (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys - rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys + (VRecType ltys) -> do lttys <- checkRecFields scope rs ltys + rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) return ((f . R) rs, VRecType [(l, ty) | (l,t,ty) <- lttys] ) - ty -> do lttys <- inferRecFields ge scope rs - t <- liftM (f . R) (mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) + ty -> do lttys <- inferRecFields scope rs + t <- liftEvalM (liftM (f . R) (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)) let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys] - t <- subsCheckRho ge scope t ty' ty + t <- subsCheckRho scope t ty' ty return (t, ty') -tcRho ge scope (P t l) mb_ty = do +tcRho scope (P t l) mb_ty = do l_ty <- case mb_ty of Just ty -> return ty - Nothing -> do i <- newMeta scope vtypeType - return (VMeta i (scopeEnv scope) []) - (t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,l_ty)])) + Nothing -> do env <- scopeEnv scope + i <- liftEvalM (newEvaluatedThunk vtypeType) + return (VMeta i env []) + (t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)])) return (P t l,l_ty) -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 +tcRho scope (C t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho scope t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho scope t2 (Just vtypeStr) + instSigma scope (C t1 t2) vtypeStr mb_ty +tcRho scope (Glue t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho scope t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho scope t2 (Just vtypeStr) + instSigma scope (Glue t1 t2) vtypeStr mb_ty +tcRho scope t@(ExtR t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho scope t1 Nothing + (t2,t2_ty) <- tcRho scope t2 Nothing case (t1_ty,t2_ty) of (VSort s1,VSort s2) | (s1 == cType || s1 == cPType) && (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType | otherwise = cType - in instSigma ge scope (ExtR t1 t2) (VSort sort) mb_ty - (VRecType rs1, VRecType rs2) -> instSigma ge scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty + in instSigma scope (ExtR t1 t2) (VSort sort) mb_ty + (VRecType rs1, VRecType rs2) -> instSigma scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty _ -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t) -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) +tcRho scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty +tcRho scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty +tcRho scope (Alts t ss) mb_ty = do + (t,_) <- tcRho scope t (Just vtypeStr) ss <- flip mapM ss $ \(t1,t2) -> do - (t1,_) <- tcRho ge scope t1 (Just vtypeStr) - (t2,_) <- tcRho ge scope t2 (Just vtypeStrs) + (t1,_) <- tcRho scope t1 (Just vtypeStr) + (t2,_) <- tcRho scope t2 (Just vtypeStrs) return (t1,t2) - instSigma ge scope (Alts t ss) vtypeStr mb_ty -tcRho ge scope (Strs ss) mb_ty = do + instSigma scope (Alts t ss) vtypeStr mb_ty +tcRho scope (Strs ss) mb_ty = do ss <- flip mapM ss $ \t -> do - (t,_) <- tcRho ge scope t (Just vtypeStr) + (t,_) <- tcRho scope t (Just vtypeStr) return t - instSigma ge scope (Strs ss) vtypeStrs mb_ty -tcRho ge scope (EPattType ty) mb_ty = do - (ty, _) <- tcRho ge scope ty (Just vtypeType) - instSigma ge scope (EPattType ty) vtypeType mb_ty -tcRho ge scope t@(EPatt p) mb_ty = do + instSigma scope (Strs ss) vtypeStrs mb_ty +tcRho scope (EPattType ty) mb_ty = do + (ty, _) <- tcRho scope ty (Just vtypeType) + instSigma scope (EPattType ty) vtypeType mb_ty +tcRho scope t@(EPatt min max p) mb_ty = do (scope,f,ty) <- case mb_ty of - Nothing -> do i <- newMeta scope vtypeType - return (scope,id,VMeta i (scopeEnv scope) []) - Just ty -> do (scope,f,ty) <- skolemise ge scope ty + Nothing -> do env <- scopeEnv scope + i <- liftEvalM (newEvaluatedThunk vtypeType) + return (scope,id,VMeta i env []) + Just ty -> do (scope,f,ty) <- skolemise scope ty case ty of VPattType ty -> return (scope,f,ty) _ -> tcError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") - tcPatt ge scope p ty - return (f (EPatt p), ty) -tcRho gr scope t _ = unimplemented ("tcRho "++show t) - -tcCases ge scope [] p_ty mb_res_ty = return ([],mb_res_ty) -tcCases ge scope ((p,t):cs) p_ty mb_res_ty = do - scope' <- tcPatt ge scope p p_ty - (t,res_ty) <- tcRho ge scope' t mb_res_ty - (cs,mb_res_ty) <- tcCases ge scope cs p_ty (Just res_ty) + tcPatt scope p ty + return (f (EPatt min max p), ty) +tcRho scope t _ = unimplemented ("tcRho "++show t) + +tcCases scope [] p_ty mb_res_ty = return ([],mb_res_ty) +tcCases scope ((p,t):cs) p_ty mb_res_ty = do + scope' <- tcPatt scope p p_ty + (t,res_ty) <- tcRho scope' t mb_res_ty + (cs,mb_res_ty) <- tcCases scope cs p_ty (Just res_ty) return ((p,t):cs,mb_res_ty) --} -tcApp scope t@(App fun (ImplArg arg)) = undefined {- do -- APP1 - tcApp ge scope fun `bindTcA` \(fun,fun_ty) -> - do (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty +tcApp gr scope t@(App fun (ImplArg arg)) = do -- APP1 + tcApp gr scope fun `bindTcA` \(fun,fun_ty) -> + do (bt, arg_ty, res_ty) <- unifyFun scope fun_ty if (bt == Implicit) then return () else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") - (arg,_) <- tcRho ge scope arg (Just arg_ty) - varg <- liftErr (eval ge (scopeEnv scope) arg) - return (App fun (ImplArg arg), res_ty varg) -tcApp ge scope (App fun arg) = -- APP2 - tcApp ge scope fun `bindTcA` \(fun,fun_ty) -> + (arg,_) <- tcRho scope arg (Just arg_ty) + env <- scopeEnv scope + varg <- liftEvalM (eval env arg []) + return (App fun (ImplArg arg), res_ty) +tcApp gr scope (App fun arg) = -- APP2 + tcApp gr scope fun `bindTcA` \(fun,fun_ty) -> do (fun,fun_ty) <- instantiate scope fun fun_ty - (_, arg_ty, res_ty) <- unifyFun ge scope fun_ty - (arg,_) <- tcRho ge scope arg (Just arg_ty) - varg <- liftErr (eval ge (scopeEnv scope) arg) - return (App fun arg, res_ty varg) -tcApp ge scope (Q id) = -- VAR (global) - mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> - do ty <- liftErr (eval ge [] ty) + (_, arg_ty, res_ty) <- unifyFun scope fun_ty + (arg,_) <- tcRho scope arg (Just arg_ty) + env <- scopeEnv scope + varg <- liftEvalM (eval env arg []) + return (App fun arg, res_ty) +tcApp gr scope (Q id) = do -- VAR (global) + mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) -> + do ty <- liftEvalM (eval [] ty []) return (t,ty) -tcApp ge scope (QC id) = -- VAR (global) - mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> - do ty <- liftErr (eval ge [] ty) +tcApp gr scope (QC id) = -- VAR (global) + mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) -> + do ty <- liftEvalM (eval [] ty []) return (t,ty) -tcApp ge scope t = - singleTcA (tcRho ge scope t Nothing) +tcApp gr scope t = + singleTcA (tcRho scope t Nothing) + --} tcOverloadFailed t ttys = tcError ("Overload resolution failed" $$ "of term " <+> pp t $$ "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]) -{- -tcPatt ge scope PW ty0 = + +tcPatt scope PW ty0 = return scope -tcPatt ge scope (PV x) ty0 = +tcPatt scope (PV x) ty0 = return ((x,ty0):scope) -tcPatt ge scope (PP c ps) ty0 = - case lookupResType (geGrammar ge) c of - Ok ty -> do let go scope ty [] = return (scope,ty) - go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun ge scope ty - scope <- tcPatt ge scope p arg_ty - go scope (res_ty (VGen (length scope) [])) ps - vty <- liftErr (eval ge [] ty) - (scope,ty) <- go scope vty ps - unify ge scope ty0 ty - return scope - Bad err -> tcError (pp err) -tcPatt ge scope (PInt i) ty0 = do - subsCheckRho ge scope (EInt i) (vtypeInts i) ty0 +tcPatt scope (PP c ps) ty0 = do + ty <- liftEvalM (getResType c) + let go scope ty [] = return (scope,ty) + go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun scope ty + scope <- tcPatt scope p arg_ty + go scope res_ty ps + vty <- liftEvalM (eval [] ty []) + (scope,ty) <- go scope vty ps + unify scope ty0 ty return scope -tcPatt ge scope (PString s) ty0 = do - unify ge scope ty0 vtypeStr +tcPatt scope (PInt i) ty0 = do + ty <- vtypeInts i + subsCheckRho scope (EInt i) ty ty0 return scope -tcPatt ge scope PChar ty0 = do - unify ge scope ty0 vtypeStr +tcPatt scope (PString s) ty0 = do + unify scope ty0 vtypeStr return scope -tcPatt ge scope (PSeq _ _ p1 _ _ p2) ty0 = do - unify ge scope ty0 vtypeStr - scope <- tcPatt ge scope p1 vtypeStr - scope <- tcPatt ge scope p2 vtypeStr +tcPatt scope PChar ty0 = do + unify scope ty0 vtypeStr return scope -tcPatt ge scope (PAs x p) ty0 = do - tcPatt ge ((x,ty0):scope) p ty0 -tcPatt ge scope (PR rs) ty0 = do +tcPatt scope (PSeq _ _ p1 _ _ p2) ty0 = do + unify scope ty0 vtypeStr + scope <- tcPatt scope p1 vtypeStr + scope <- tcPatt scope p2 vtypeStr + return scope +tcPatt scope (PAs x p) ty0 = do + tcPatt ((x,ty0):scope) p ty0 +tcPatt scope (PR rs) ty0 = do let mk_ltys [] = return [] - mk_ltys ((l,p):rs) = do i <- newMeta scope vtypePType + mk_ltys ((l,p):rs) = do i <- liftEvalM (newEvaluatedThunk vtypePType) ltys <- mk_ltys rs - return ((l,p,VMeta i (scopeEnv scope) []) : ltys) + env <- scopeEnv scope + return ((l,p,VMeta i env []) : ltys) go scope [] = return scope - go scope ((l,p,ty):rs) = do scope <- tcPatt ge scope p ty + go scope ((l,p,ty):rs) = do scope <- tcPatt scope p ty go scope rs ltys <- mk_ltys rs - subsCheckRho ge scope (EPatt (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0 + subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0 go scope ltys -tcPatt ge scope (PAlt p1 p2) ty0 = do - tcPatt ge scope p1 ty0 - tcPatt ge scope p2 ty0 +tcPatt scope (PAlt p1 p2) ty0 = do + tcPatt scope p1 ty0 + tcPatt scope p2 ty0 return scope -tcPatt ge scope (PM q) ty0 = do - case lookupResType (geGrammar ge) q of - Ok (EPattType ty) - -> do vty <- liftErr (eval ge [] ty) - unify ge scope ty0 vty +tcPatt scope (PM q) ty0 = do + ty <- liftEvalM (getResType q) + case ty of + EPattType ty + -> do vty <- liftEvalM (eval [] ty []) + unify scope ty0 vty return scope - Ok ty -> tcError ("Pattern type expected but " <+> pp ty <+> " found.") - Bad err -> tcError (pp err) -tcPatt ge scope p ty = unimplemented ("tcPatt "++show p) + ty -> tcError ("Pattern type expected but " <+> pp ty <+> " found.") +tcPatt scope p ty = unimplemented ("tcPatt "++show p) -inferRecFields ge scope rs = - mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs +inferRecFields scope rs = + mapM (\(l,r) -> tcRecField scope l r Nothing) rs -checkRecFields ge scope [] ltys +checkRecFields scope [] ltys | null ltys = return [] | otherwise = tcError ("Missing fields:" <+> hsep (map fst ltys)) -checkRecFields ge scope ((l,t):lts) ltys = +checkRecFields scope ((l,t):lts) ltys = case takeIt l ltys of - (Just ty,ltys) -> do ltty <- tcRecField ge scope l t (Just ty) - lttys <- checkRecFields ge scope lts ltys + (Just ty,ltys) -> do ltty <- tcRecField scope l t (Just ty) + lttys <- checkRecFields scope lts ltys return (ltty : lttys) (Nothing,ltys) -> do tcWarn ("Discarded field:" <+> l) - ltty <- tcRecField ge scope l t Nothing - lttys <- checkRecFields ge scope lts ltys + ltty <- tcRecField scope l t Nothing + lttys <- checkRecFields scope lts ltys return lttys -- ignore the field where takeIt l1 [] = (Nothing, []) @@ -372,29 +383,30 @@ checkRecFields ge scope ((l,t):lts) ltys = | otherwise = let (mb_ty,ltys') = takeIt l1 ltys in (mb_ty,lty:ltys') -tcRecField ge scope l (mb_ann_ty,t) mb_ty = do +tcRecField scope l (mb_ann_ty,t) mb_ty = do (t,ty) <- case mb_ann_ty of - Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType) - v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty) - (t,_) <- tcRho ge scope t (Just v_ann_ty) - instSigma ge scope t v_ann_ty mb_ty - Nothing -> tcRho ge scope t mb_ty + Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType) + env <- scopeEnv scope + v_ann_ty <- liftEvalM (eval env ann_ty []) + (t,_) <- tcRho scope t (Just v_ann_ty) + instSigma scope t v_ann_ty mb_ty + Nothing -> tcRho scope t mb_ty return (l,t,ty) -tcRecTypeFields ge scope [] mb_ty = return ([],mb_ty) -tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do - (ty,sort) <- tcRho ge scope ty mb_ty +tcRecTypeFields scope [] mb_ty = return ([],mb_ty) +tcRecTypeFields scope ((l,ty):rs) mb_ty = do + (ty,sort) <- tcRho scope ty mb_ty mb_ty <- case sort of VSort s | s == cType -> return (Just sort) | s == cPType -> return mb_ty VMeta _ _ _ -> return mb_ty - _ -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort + _ -> do sort <- zonkTerm =<< liftEvalM (value2term (scopeVars scope) sort) tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ "cannot be of type" <+> ppTerm Unqualified 0 sort) - (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty + (rs,mb_ty) <- tcRecTypeFields scope rs mb_ty return ((l,ty):rs,mb_ty) --} + -- | Invariant: if the third argument is (Just rho), -- then rho is in weak-prenex form instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> TcM s (Term, Rho s) @@ -405,21 +417,21 @@ instSigma scope t ty1 (Just ty2) = do -- INST2 -- | Invariant: the second argument is in weak-prenex form subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> TcM s Term -subsCheckRho scope t ty1@(VMeta i env vs) ty2 = undefined {- do - mv <- getMeta i +subsCheckRho scope t ty1@(VMeta i env vs) ty2 = do + mv <- liftEvalM (getRef i) case mv of - Unbound _ _ -> do unify ge scope ty1 ty2 - return t - Bound ty1 -> do vty1 <- liftErr (eval ge env ty1) - subsCheckRho ge scope t (vapply (geLoc ge) vty1 vs) ty2 -subsCheckRho ge scope t ty1 ty2@(VMeta i env vs) = do - mv <- getMeta i + Residuation _ _ _ -> do unify scope ty1 ty2 + return t + Evaluated _ vty1 -> do vty1 <- liftEvalM (apply vty1 vs) + subsCheckRho scope t vty1 ty2 +subsCheckRho scope t ty1 ty2@(VMeta i env vs) = do + mv <- liftEvalM (getRef i) case mv of - Unbound _ _ -> do unify ge scope ty1 ty2 - return t - Bound ty2 -> do vty2 <- liftErr (eval ge env ty2) - subsCheckRho ge scope t ty1 (vapply (geLoc ge) vty2 vs) -subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC + Residuation _ _ _ -> do unify scope ty1 ty2 + return t + Evaluated _ vty2 -> do vty2 <- liftEvalM (apply vty2 vs) + subsCheckRho scope t ty1 vty2 +{-subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC i <- newMeta scope ty1 subsCheckRho ge scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) rho2 subsCheckRho ge scope t rho1 (VProd Implicit ty1 x (Bind ty2)) = do -- Rule SKOL @@ -506,34 +518,35 @@ subsCheckTbl ge scope t p1 r1 p2 r2 = do t <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ; p2 <- tc_value2term (geLoc ge) (scopeVars scope) p2 return (T (TTyped p2) [(PV x,t)]) - +-} ----------------------------------------------------------------------- -- Unification ----------------------------------------------------------------------- -unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (BindType, Sigma, Value -> Rho) -unifyFun ge scope (VProd bt arg x (Bind res)) = +unifyFun :: Scope s -> Rho s -> TcM s (BindType, Sigma s, Rho s) +unifyFun scope (VProd bt x arg res) = return (bt,arg,res) -unifyFun ge scope tau = do +unifyFun scope tau = do let mk_val ty = VMeta ty [] [] - arg <- fmap mk_val $ newMeta scope vtypeType - res <- fmap mk_val $ newMeta scope vtypeType + arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) + res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) let bt = Explicit - unify ge scope tau (VProd bt arg identW (Bind (const res))) - return (bt,arg,const res) + unify scope tau (VProd bt identW arg res) + return (bt,arg,res) -unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho) -unifyTbl ge scope (VTblType arg res) = +unifyTbl :: Scope s -> Rho s -> TcM s (Sigma s, Rho s) +unifyTbl scope (VTable arg res) = return (arg,res) -unifyTbl ge scope tau = do - let mk_val ty = VMeta ty (scopeEnv scope) [] - arg <- fmap mk_val $ newMeta scope vtypePType - res <- fmap mk_val $ newMeta scope vtypeType - unify ge scope tau (VTblType arg res) +unifyTbl scope tau = do + env <- scopeEnv scope + let mk_val ty = VMeta ty env [] + arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypePType) + res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType) + unify scope tau (VTable arg res) return (arg,res) -unify ge scope (VApp f1 vs1) (VApp f2 vs2) - | f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2) +unify scope (VApp f1 vs1) (VApp f2 vs2) + | f1 == f2 = undefined {- sequence_ (zipWith (unify ge scope) vs1 vs2) unify ge scope (VCApp f1 vs1) (VCApp f2 vs2) | f1 == f2 = sequence_ (zipWith (unify ge scope) vs1 vs2) unify ge scope (VSort s1) (VSort s2) @@ -559,50 +572,48 @@ unify ge scope v1 v2 = do t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2 tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ ppTerm Unqualified 0 t2)) - +-} -- | Invariant: tv1 is a flexible type variable -unifyVar :: GlobalEnv -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM () -unifyVar ge scope i env vs ty2 = do -- Check whether i is bound - mv <- getMeta i +unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> TcM s () +unifyVar scope tnk env vs ty2 = do -- Check whether i is bound + mv <- liftEvalM (getRef tnk) case mv of - Bound ty1 -> do v <- liftErr (eval ge env ty1) - unify ge scope (vapply (geLoc ge) v vs) ty2 - Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of - -- Left i -> let (v,_) = reverse scope !! i - -- in tcError ("Variable" <+> pp v <+> "has escaped") - ty2' -> do ms2 <- getMetaVars (geLoc ge) [(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') + Unevaluated _ ty1 -> do v <- liftEvalM (eval env ty1 [] >>= \v -> apply v vs) + unify scope v ty2 + Residuation i scope' _ -> do ty2' <- liftEvalM (value2term (scopeVars scope') ty2) + ms2 <- getMetaVars [(scope,ty2)] + if i `elem` ms2 + then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$ + nest 2 (ppTerm Unqualified 0 ty2')) + else liftEvalM (setRef tnk (Unevaluated env ty2')) ----------------------------------------------------------------------- -- Instantiation and quantification ----------------------------------------------------------------------- -- | Instantiate the topmost implicit arguments with metavariables -instantiate :: Scope -> Term -> Sigma -> TcM (Term,Rho) -instantiate scope t (VProd Implicit ty1 x (Bind ty2)) = do +instantiate :: Scope s -> Term -> Sigma s -> TcM s (Term,Rho s) +instantiate scope t (VProd Implicit x ty1 ty2) = undefined {- do i <- newMeta scope ty1 - instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) + instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) -} instantiate scope t ty = do return (t,ty) -- | Build fresh lambda abstractions for the topmost implicit arguments -skolemise :: GlobalEnv -> Scope -> Sigma -> TcM (Scope, Term->Term, Rho) -skolemise ge scope ty@(VMeta i env vs) = do - mv <- getMeta i +skolemise :: Scope s -> Sigma s -> TcM s (Scope s, Term->Term, Rho s) +skolemise scope ty@(VMeta i env vs) = undefined {-do + mv <- getRef i case mv of - Unbound _ _ -> return (scope,id,ty) -- guarded constant? - Bound ty -> do vty <- liftErr (eval ge env ty) - skolemise ge scope (vapply (geLoc ge) vty vs) -skolemise ge scope (VProd Implicit ty1 x (Bind ty2)) = do + Residuation _ _ _ -> return (scope,id,ty) -- guarded constant? + Evaluated _ vty -> do vty <- liftEvalM (apply vty vs) + skolemise scope vty +skolemise scope (VProd Implicit ty1 x ty2) = do let v = newVar scope - (scope,f,ty2) <- skolemise ge ((v,ty1):scope) (ty2 (VGen (length scope) [])) - return (scope,Abs Implicit v . f,ty2) -skolemise ge scope ty = do - return (scope,id,ty) --} + (scope,f,ty2) <- skolemise ((v,ty1):scope) (ty2 (VGen (length scope) [])) + return (scope,undefined {-Abs Implicit v . f-},ty2) +skolemise scope ty = do + return (scope,undefined,ty)-} + -- | Quantify over the specified type variables (all flexible) quantify :: Scope s -> Term -> [MetaId] -> Rho s -> TcM s (Term,Sigma s) quantify scope t tvs ty0 = undefined {- do @@ -618,17 +629,16 @@ quantify scope t tvs ty0 = undefined {- do bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2 bndrs _ = [] - +-} allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']] --} + ----------------------------------------------------------------------- -- The Monad ----------------------------------------------------------------------- -type Scope s = [(Ident,Value s)] type Sigma s = Value s type Rho s = Value s -- No top-level ForAll type Tau s = Value s -- No ForAlls anywhere @@ -697,39 +707,23 @@ liftEvalM (EvalM f) = TcM $ \gr ms msgs -> do Success (x,ms) -> return (TcOk x ms []) Fail msg -> return (TcFail [msg]) - - -newMeta :: Scope s -> Sigma s -> TcM s MetaId -newMeta scope ty = undefined {- TcM (\ms msgs -> - let i = IntMap.size ms - in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs) - -getMeta :: MetaId -> TcM MetaValue -getMeta i = TcM (\ms msgs -> - case IntMap.lookup i ms of - Just mv -> TcOk mv ms msgs - Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs)) - -setMeta :: MetaId -> MetaValue -> TcM () -setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs) - -newVar :: Scope -> Ident +newVar :: Scope s -> Ident newVar scope = head [x | i <- [1..], let x = identS ('v':show i), isFree scope x] where isFree [] x = True isFree ((y,_):scope) x = x /= y && isFree scope x --} -scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..] + +scopeEnv scope = zipWithM (\(x,ty) i -> liftEvalM (newEvaluatedThunk (VGen i [])) >>= \tnk -> return (x,tnk)) (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 :: [(Scope s,Sigma s)] -> TcM s [MetaId] -getMetaVars sc_tys = undefined {- do - tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys +getMetaVars sc_tys = do + tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys return (foldr go [] tys) where -- Get the MetaIds from a term; no duplicates in result @@ -748,9 +742,9 @@ getMetaVars sc_tys = undefined {- do -- | This function takes account of zonking, and returns a set -- (no duplicates) of free type variables -getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident] -getFreeVars loc sc_tys = do - tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys +getFreeVars :: [(Scope s,Sigma s)] -> TcM s [Ident] +getFreeVars sc_tys = do + tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys return (foldr (go []) [] tys) where go bound (Vr tv) acc @@ -764,7 +758,7 @@ getFreeVars loc sc_tys = do go bound (Prod _ x arg res) acc = go bound arg (go (x : bound) res acc) go bound (RecType rs) acc = foldl (\acc (l,ty) -> go bound ty acc) acc rs go bound (Table p t) acc = go bound p (go bound t acc) --} + -- | Eliminate any substitutions in a term zonkTerm :: Term -> TcM s Term zonkTerm (Meta i) = undefined {- do @@ -802,8 +796,8 @@ bindTcA f g = case f of TcFail _ -> return rs TcOk y ms msgs -> return ((y,ms,msgs):rs) -runTcA :: ([x] -> TcM s a) -> TcA s x a -> TcM s a -runTcA g f = TcM (\gr ms msgs -> case f of +runTcA :: ([x] -> TcM s a) -> (SourceGrammar -> TcA s x a) -> TcM s a +runTcA g f = TcM (\gr ms msgs -> case f gr of TcMany xs f -> do rs <- f gr ms msgs case rs of [(x,ms,msgs)] -> return (TcOk x ms msgs)