diff options
Diffstat (limited to 'src/compiler')
| -rw-r--r-- | src/compiler/GF/Compile/CheckGrammar.hs | 5 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/Compute/ConcreteNew.hs | 58 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs | 464 | ||||
| -rw-r--r-- | src/compiler/GF/Grammar/Grammar.hs | 2 | ||||
| -rw-r--r-- | src/compiler/GF/Infra/CheckM.hs | 2 |
5 files changed, 330 insertions, 201 deletions
diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs index 9a566ad8d..b5d288cc8 100644 --- a/src/compiler/GF/Compile/CheckGrammar.hs +++ b/src/compiler/GF/Compile/CheckGrammar.hs @@ -28,6 +28,7 @@ import GF.Infra.Option import GF.Compile.TypeCheck.Abstract import GF.Compile.TypeCheck.Concrete import qualified GF.Compile.TypeCheck.ConcreteNew as CN +import qualified GF.Compile.Compute.ConcreteNew as CN import GF.Grammar import GF.Grammar.Lexer @@ -211,7 +212,9 @@ checkInfo opts ms (m,mo) c info = do (pty', pde') <- case (pty,pde) of (Just (L loct ty), Just (L locd de)) -> do ty' <- chIn loct "operation" $ - checkLType gr [] ty typeType >>= computeLType gr [] . fst + (if flag optNewComp opts + then CN.checkLType gr ty typeType >>= return . CN.normalForm gr . fst + else checkLType gr [] ty typeType >>= computeLType gr [] . fst) (de',_) <- chIn locd "operation" $ (if flag optNewComp opts then CN.checkLType gr de ty' diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs index 1172ece42..8ca08e348 100644 --- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs +++ b/src/compiler/GF/Compile/Compute/ConcreteNew.hs @@ -1,6 +1,12 @@ -module GF.Compile.Compute.ConcreteNew ( Value(..), Env, eval, apply, value2term ) where +module GF.Compile.Compute.ConcreteNew + ( normalForm + , Value(..), Env, eval, apply, value2term + ) where -import GF.Grammar hiding (Env, VGen, VApp) +import GF.Grammar hiding (Env, VGen, VApp, VRecType) + +normalForm :: SourceGrammar -> Term -> Term +normalForm gr t = value2term gr [] (eval gr [] t) data Value = VApp QIdent [Value] @@ -8,29 +14,37 @@ data Value | VMeta MetaId Env [Value] | VClosure Env Term | VSort Ident + | VTblType Value Value + | VRecType [(Label,Value)] deriving Show type Env = [(Ident,Value)] -eval :: Env -> Term -> Value -eval env (Vr x) = case lookup x env of - Just v -> v - Nothing -> error ("Unknown variable "++showIdent x) -eval env (Q x) = VApp x [] -eval env (Meta i) = VMeta i env [] -eval env t@(Prod _ _ _ _) = VClosure env t -eval env t@(Abs _ _ _) = VClosure env t -eval env (Sort s) = VSort s -eval env t = error (show t) +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) = VApp x [] +eval gr env (QC x) = VApp x [] +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 (Sort s) = VSort s +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 = error ("eval "++show t) -apply env t vs = undefined +apply gr env t [] = eval gr env t +apply gr env t vs = error ("apply "++show t) -value2term :: [Ident] -> Value -> Term -value2term xs (VApp f vs) = foldl App (Q f) (map (value2term xs) vs) -value2term xs (VGen j vs) = foldl App (Vr (reverse xs !! j)) (map (value2term xs) vs) -value2term xs (VMeta j env vs) = foldl App (Meta j) (map (value2term xs) vs) -value2term xs (VClosure env (Prod bt x t1 t2)) = Prod bt x (value2term xs (eval env t1)) - (value2term (x:xs) (eval ((x,VGen (length xs) []) : env) t2)) -value2term xs (VClosure env (Abs bt x t)) = Abs bt x (value2term (x:xs) (eval ((x,VGen (length xs) []) : env) t)) -value2term xs (VSort s) = Sort s -value2term xs v = error (show v) +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 (VSort s) = Sort s +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 v = error ("value2term "++show v) diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index 265563611..ffc09eec3 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -1,14 +1,16 @@ module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where -import GF.Grammar hiding (Env, VGen, VApp) +import GF.Grammar hiding (Env, VGen, VApp, VRecType) import GF.Grammar.Lookup +import GF.Grammar.Predef import GF.Compile.Compute.ConcreteNew +import GF.Compile.Compute.AppPredefined import GF.Infra.CheckM import GF.Infra.UseIO import GF.Data.Operations import Text.PrettyPrint -import Data.List (nub, (\\)) +import Data.List (nub, (\\), tails) import qualified Data.IntMap as IntMap import qualified Data.ByteString.Char8 as BS @@ -18,7 +20,7 @@ import Debug.Trace checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type) checkLType gr t ty = runTcM $ do - t <- checkSigma gr [] t (eval [] ty) + t <- checkSigma gr [] t (eval gr [] ty) t <- zonkTerm t return (t,ty) @@ -26,66 +28,72 @@ inferLType :: SourceGrammar -> Term -> Check (Term, Type) inferLType gr t = runTcM $ do (t,ty) <- inferSigma gr [] t t <- zonkTerm t - ty <- zonkTerm (value2term [] ty) + ty <- zonkTerm (value2term gr [] 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)] + let forall_tvs = res_tvs \\ env_tvs + quantify gr scope t forall_tvs ty + checkSigma :: SourceGrammar -> Scope -> Term -> Sigma -> TcM Term -checkSigma gr scope t sigma = do - (skol_tvs, rho) <- skolemise scope sigma +checkSigma gr scope t sigma = do -- GEN2 + (abs, scope, t, rho) <- skolemise id gr scope t sigma + let skol_tvs = [] (t,rho) <- tcRho gr scope t (Just rho) - esc_tvs <- getFreeTyVars (sigma : map snd scope) + esc_tvs <- getFreeVars gr ((scope,sigma) : scopeTypes scope) let bad_tvs = filter (`elem` esc_tvs) skol_tvs if null bad_tvs - then return t + then return (abs t) else tcError (text "Type not polymorphic enough") -inferSigma :: SourceGrammar -> Scope -> Term -> TcM (Term,Sigma) -inferSigma gr scope t = do - (t,ty) <- tcRho gr scope t Nothing - env_tvs <- getMetaVars [ty | (_,ty) <- scope] - res_tvs <- getMetaVars [ty] - let forall_tvs = res_tvs \\ env_tvs - quantify scope t forall_tvs ty - tcRho :: SourceGrammar -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho) -tcRho gr scope t@(EInt _) mb_ty = instSigma scope t (eval [] typeInt) mb_ty -tcRho gr scope t@(EFloat _) mb_ty = instSigma scope t (eval [] typeFloat) mb_ty -tcRho gr scope t@(K _) mb_ty = instSigma scope t (eval [] typeString) mb_ty -tcRho gr scope t@(Empty) mb_ty = instSigma scope t (eval [] typeString) mb_ty -tcRho gr scope t@(Vr v) mb_ty = do +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 case lookup v scope of - Just v_sigma -> instSigma scope t v_sigma mb_ty + Just v_sigma -> instSigma gr scope t v_sigma mb_ty Nothing -> tcError (text "Unknown variable" <+> ppIdent v) -tcRho gr scope t@(Q id) mb_ty = do - case lookupResType gr id of - Ok ty -> instSigma scope t (eval [] ty) mb_ty - Bad err -> tcError (text err) +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 (text "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 (text err) tcRho gr scope t@(QC id) mb_ty = do case lookupResType gr id of - Ok ty -> instSigma scope t (eval [] ty) mb_ty + Ok ty -> instSigma gr scope t (eval gr [] ty) mb_ty Bad err -> tcError (text err) -tcRho gr scope (App fun arg) mb_ty = do +tcRho gr scope (App fun arg) mb_ty = do -- APP (fun,fun_ty) <- tcRho gr scope fun Nothing - (arg_ty, res_ty) <- unifyFun scope fun_ty + (arg_ty, res_ty) <- unifyFun gr scope (eval gr (scopeEnv scope) arg) fun_ty arg <- checkSigma gr scope arg arg_ty - instSigma scope (App fun arg) res_ty mb_ty -tcRho gr scope (Abs bt var body) (Just ty) = do - trace (show ty) $ return () - (var_ty, body_ty) <- unifyFun scope ty - (body, body_ty) <- tcRho gr ((var,var_ty):scope) body (Just body_ty) - return (Abs bt var body,ty) -tcRho gr scope (Abs bt var body) Nothing = do - i <- newMeta (eval [] typeType) + instSigma gr 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 (scopeVars scope) body_ty)))) -tcRho gr scope (Typed body ann_ty) mb_ty = do - body <- checkSigma gr scope body (eval (scopeEnv scope) ann_ty) - instSigma scope (Typed body ann_ty) (eval (scopeEnv scope) ann_ty) mb_ty + (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) + return (Abs bt var body,ty) +tcRho gr scope (Typed body ann_ty) mb_ty = do -- ANNOT + 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 case ts of - [] -> do i <- newMeta (eval [] typeType) - instSigma scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty + [] -> 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 let go [] ty = return ([],ty) @@ -95,93 +103,202 @@ tcRho gr scope (FV ts) mb_ty = do (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 + p_ty <- case tt of + TRaw -> fmap Meta $ newMeta (eval gr [] typePType) + TTyped ty -> 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 (R rs) mb_ty = do + lttys <- case mb_ty of + Nothing -> inferRecFields gr scope rs + Just ty -> case ty of + VRecType ltys -> checkRecFields gr scope rs ltys + _ -> tcError (text "Record expected") + return (R [(l, (Just (value2term gr (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], + VRecType [(l, ty) | (l,t,ty) <- lttys] + ) +tcRho gr scope (P t l) mb_ty = do + x_ty <- case mb_ty of + Just ty -> return ty + Nothing -> do i <- newMeta (eval gr [] typeType) + return (VMeta i (scopeEnv scope) []) + (t,t_ty) <- tcRho gr 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 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) + return (p,t) + +tcPatt gr scope PW ty0 = + return scope +tcPatt gr scope (PV x) ty0 = + return ((x,ty0):scope) +tcPatt gr scope (PP c ps) ty0 = + case lookupResType gr c of + Ok ty -> do unify gr scope ty0 (eval gr [] ty) + return scope + Bad err -> tcError (text err) +tcPatt gr scope p ty = error ("tcPatt "++show p) + + +inferRecFields gr scope rs = + mapM (\(l,r) -> tcRecField gr scope l r Nothing) rs + +checkRecFields gr scope [] ltys + | null ltys = return [] + | otherwise = tcError (hsep (map (ppLabel . fst) ltys)) +checkRecFields gr 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 + return (ltty : lttys) + (Nothing,ltys) -> do tcWarn (ppLabel l) + ltty <- tcRecField gr scope l t Nothing + lttys <- checkRecFields gr scope lts ltys + return lttys -- ignore the field + where + takeIt l1 [] = (Nothing, []) + takeIt l1 (lty@(l2,ty):ltys) + | l1 == l2 = (Just ty,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 + (t,ty) <- case mb_ann_ty of + Just ann_ty -> do 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 + return (l,t,ty) + + -- | Invariant: if the third argument is (Just rho), -- then rho is in weak-prenex form -instSigma :: Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho) -instSigma scope t ty1 (Just ty2) = do t <- subsCheckRho scope t ty1 ty2 - return (t,ty2) -instSigma scope t ty1 Nothing = instantiate t ty1 +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 + return (t,ty2) -- | (subsCheck scope args off exp) checks that -- 'off' is at least as polymorphic as 'args -> exp' -subsCheck :: Scope -> Term -> Sigma -> Sigma -> TcM Term -subsCheck scope t sigma1 sigma2 = do -- Rule DEEP-SKOL - (skol_tvs, rho2) <- skolemise scope sigma2 - t <- subsCheckRho scope t sigma1 rho2 - esc_tvs <- getFreeTyVars [sigma1,sigma2] +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 + let skol_tvs = [] + t <- subsCheckRho gr scope t sigma1 rho2 + esc_tvs <- getFreeVars gr [(scope,sigma1),(scope,sigma2)] let bad_tvs = filter (`elem` esc_tvs) skol_tvs if null bad_tvs - then return () + then return (abs t) else tcError (vcat [text "Subsumption check failed:", - nest 2 (ppTerm Unqualified 0 (value2term [] sigma1)), + nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) sigma1)), text "is not as polymorphic as", - nest 2 (ppTerm Unqualified 0 (value2term [] sigma2))]) - return t + nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) sigma2))]) -- | Invariant: the second argument is in weak-prenex form -subsCheckRho :: Scope -> Term -> Sigma -> Rho -> TcM Term -subsCheckRho scope t sigma1@(VClosure env (Prod Implicit _ _ _)) rho2 = do -- Rule SPEC - (t,rho1) <- instantiate t sigma1 - subsCheckRho scope t rho1 rho2 -subsCheckRho scope t rho1 (VClosure env (Prod Explicit _ a2 r2)) = do -- Rule FUN - (a1,r1) <- unifyFun scope rho1 - subsCheckFun scope t a1 r1 (eval env a2) (eval env r2) -subsCheckRho scope t (VClosure env (Prod Explicit _ a1 r1)) rho2 = do -- Rule FUN - (a2,r2) <- unifyFun scope rho2 - subsCheckFun scope t (eval env a1) (eval env r1) a2 r2 -subsCheckRho scope t tau1 tau2 = do -- Rule MONO - unify scope tau1 tau2 -- Revert to ordinary unification +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) + | s1 == cPType && s2 == cType = return t + | s1 == cTok && s2 == cStr = return t +subsCheckRho gr scope t tau1 tau2 = do -- Rule MONO + unify gr scope tau1 tau2 -- Revert to ordinary unification return t -subsCheckFun :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term -subsCheckFun scope t a1 r1 a2 r2 = do +subsCheckFun :: SourceGrammar -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term +subsCheckFun gr scope t a1 r1 a2 r2 = do let v = newVar scope - vt <- subsCheck scope (Vr v) a2 a1 - t <- subsCheckRho ((v,eval [] typeType):scope) (App t vt) r1 r2 ; - return (Abs Implicit v t) + vt <- subsCheck gr scope (Vr v) a2 a1 + t <- subsCheckRho gr ((v,eval gr [] typeType):scope) (App t vt) r1 r2 ; + return (Abs Explicit v t) ----------------------------------------------------------------------- -- Unification ----------------------------------------------------------------------- -unifyFun :: Scope -> Rho -> TcM (Sigma, Rho) -unifyFun scope (VClosure env (Prod Explicit x arg res)) - | x /= identW = return (eval env arg,eval ((x,VGen (length scope) []):env) res) - | otherwise = return (eval env arg,eval env res) -unifyFun scope tau = do - arg_ty <- newMeta (eval [] typeType) - res_ty <- newMeta (eval [] typeType) - unify scope tau (VClosure [] (Prod Explicit identW (Meta arg_ty) (Meta res_ty))) +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))) return (VMeta arg_ty [] [], VMeta res_ty [] []) -unify scope (VApp f1 vs1) (VApp f2 vs2) - | f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2) -unify scope (VMeta i env1 vs1) (VMeta j env2 vs2) - | i == j = sequence_ (zipWith (unify scope) vs1 vs2) +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) + | 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) | otherwise = do mv <- getMeta j case mv of - Bound t2 -> unify scope (VMeta i env1 vs1) (apply env2 t2 vs2) + Bound t2 -> unify gr scope (VMeta i env1 vs1) (apply gr env2 t2 vs2) Unbound _ -> setMeta i (Bound (Meta j)) -unify scope (VMeta i env vs) v = unifyVar scope i env vs v -unify scope v (VMeta i env vs) = unifyVar scope i env vs v -unify scope v1 v2 = do - v1 <- zonkTerm (value2term (scopeVars scope) v1) - v2 <- zonkTerm (value2term (scopeVars scope) v2) +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 + tcWarn (text "aaaa") +unify gr scope v1 v2 = do + v1 <- zonkTerm (value2term gr (scopeVars scope) v1) + v2 <- zonkTerm (value2term gr (scopeVars scope) v2) tcError (text "Cannot unify types:" <+> (ppTerm Unqualified 0 v1 $$ ppTerm Unqualified 0 v2)) -- | Invariant: tv1 is a flexible type variable -unifyVar :: Scope -> MetaId -> Env -> [Value] -> Tau -> TcM () -unifyVar scope i env vs ty2 = do -- Check whether i is bound +unifyVar :: SourceGrammar -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM () +unifyVar gr scope i env vs ty2 = do -- Check whether i is bound mv <- getMeta i case mv of - Bound ty1 -> unify scope (apply env ty1 vs) ty2 - Unbound _ -> do let ty2' = value2term [] ty2 - ms2 <- getMetaVars [ty2] + 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)] if i `elem` ms2 then tcError (text "Occurs check for" <+> ppMeta i <+> text "in:" $$ nest 2 (ppTerm Unqualified 0 ty2')) @@ -194,37 +311,46 @@ unifyVar scope i env vs ty2 = do -- Check whether i is bound -- | Instantiate the topmost for-alls of the argument type -- with metavariables -instantiate :: Term -> Sigma -> TcM (Term,Rho) -instantiate t (VClosure env (Prod Implicit x ty1 ty2)) = do - i <- newMeta (eval env ty1) - instantiate (App t (ImplArg (Meta i))) (eval ((x,VMeta i [] []):env) ty2) -instantiate t ty = do +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 return (t,ty) -skolemise scope (VClosure env (Prod Implicit x arg_ty res_ty)) = do -- Rule PRPOLY - sk <- newSkolemTyVar arg_ty - (sks, res_ty) <- skolemise scope (eval ((x,undefined):env) res_ty) - return (sk : sks, res_ty) -skolemise scope (VClosure env (Prod Explicit x arg_ty res_ty)) = do -- Rule PRFUN - (sks, res_ty) <- if x /= identW - then skolemise scope (eval ((x,VGen (length scope) []):env) res_ty) - else skolemise scope (eval env res_ty) - return (sks, VClosure env (Prod Explicit x arg_ty (value2term [] res_ty))) -skolemise scope ty -- Rule PRMONO - = return ([], ty) - -newSkolemTyVar _ = undefined - --- Quantify over the specified type variables (all flexible) -quantify :: Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma) -quantify scope t tvs ty0 = do +skolemise f gr scope t (VClosure env (Prod Implicit x arg_ty 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 = + 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 + = 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 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 [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs) + ,eval gr [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs) ) where - ty = value2term (scopeVars scope) ty0 + ty = value2term gr (scopeVars scope) ty0 used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use new_bndrs = take (length tvs) (allBinders \\ used_bndrs) @@ -253,37 +379,46 @@ data MetaValue | Bound Term type MetaStore = IntMap.IntMap MetaValue data TcResult a - = TcOk MetaStore a - | TcFail Doc -newtype TcM a = TcM {unTcM :: MetaStore -> TcResult a} + = TcOk a MetaStore [Message] + | TcFail [Message] +newtype TcM a = TcM {unTcM :: MetaStore -> [Message] -> TcResult a} instance Monad TcM where - return x = TcM (\ms -> TcOk ms x) - f >>= g = TcM (\ms -> case unTcM f ms of - TcOk ms x -> unTcM (g x) ms - TcFail msg -> TcFail msg) + return x = TcM (\ms msgs -> TcOk x ms msgs) + f >>= g = TcM (\ms msgs -> case unTcM f ms msgs of + TcOk x ms msgs -> unTcM (g x) ms msgs + TcFail msgs -> TcFail msgs) fail = tcError . text +instance Functor TcM where + fmap f g = TcM (\ms msgs -> case unTcM g ms msgs of + TcOk x ms msgs -> TcOk (f x) ms msgs + TcFail msgs -> TcFail msgs) + tcError :: Message -> TcM a -tcError msg = TcM (\ms -> TcFail msg) +tcError msg = TcM (\ms msgs -> TcFail (msg : msgs)) + +tcWarn :: Message -> TcM () +tcWarn msg = TcM (\ms msgs -> TcOk () ms ((text "Warning:" <+> msg) : msgs)) runTcM :: TcM a -> Check a -runTcM f = case unTcM f IntMap.empty of - TcOk _ x -> return x - TcFail s -> checkError s +runTcM f = Check (\ctxt msgs -> case unTcM f IntMap.empty msgs of + TcOk x _ msgs -> Success x msgs + TcFail msgs -> Fail msgs) newMeta :: Sigma -> TcM MetaId -newMeta ty = TcM (\ms -> let i = IntMap.size ms - in TcOk (IntMap.insert i (Unbound ty) ms) i) +newMeta ty = TcM (\ms msgs -> + let i = IntMap.size ms + in TcOk i (IntMap.insert i (Unbound ty) ms) msgs) getMeta :: MetaId -> TcM MetaValue -getMeta i = TcM (\ms -> +getMeta i = TcM (\ms msgs -> case IntMap.lookup i ms of - Just mv -> TcOk ms mv - Nothing -> TcFail (text "Unknown metavariable" <+> ppMeta i)) + Just mv -> TcOk mv ms msgs + Nothing -> TcFail ((text "Unknown metavariable" <+> ppMeta i) : msgs)) setMeta :: MetaId -> MetaValue -> TcM () -setMeta i mv = TcM (\ms -> TcOk (IntMap.insert i mv ms) ()) +setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs) newVar :: Scope -> Ident newVar scope = head [x | i <- [1..], @@ -293,14 +428,15 @@ newVar scope = head [x | i <- [1..], isFree [] x = True isFree ((y,_):scope) x = x /= y && isFree scope x -scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..] -scopeVars scope = map fst scope +scopeEnv scope = zipWith (\(x,ty) i -> (x,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 :: [Sigma] -> TcM [MetaId] -getMetaVars tys = do - tys <- mapM (zonkTerm . value2term []) tys +getMetaVars :: SourceGrammar -> [(Scope,Sigma)] -> TcM [MetaId] +getMetaVars gr sc_tys = do + tys <- mapM (\(scope,ty) -> zonkTerm (value2term gr (scopeVars scope) ty)) sc_tys return (foldr go [] tys) where -- Get the MetaIds from a term; no duplicates in result @@ -312,15 +448,17 @@ getMetaVars tys = do go (QC _) acc = acc go (Sort _) acc = acc go (Prod _ _ arg res) acc = go arg (go res acc) + go (Table p t) acc = go p (go t acc) + go (RecType rs) acc = foldl (\acc (l,ty) -> go ty acc) acc rs go t acc = error ("go "++show t) -- | This function takes account of zonking, and returns a set -- (no duplicates) of free type variables -getFreeTyVars :: [Sigma] -> TcM [Ident] -getFreeTyVars tys = do - tys <- mapM (zonkTerm . value2term []) tys +getFreeVars :: SourceGrammar -> [(Scope,Sigma)] -> TcM [Ident] +getFreeVars gr sc_tys = do + tys <- mapM (\(scope,ty) -> zonkTerm (value2term gr (scopeVars scope) ty)) sc_tys return (foldr (go []) [] tys) - where + where go bound (Vr tv) acc | tv `elem` bound = acc | tv `elem` acc = acc @@ -329,32 +467,11 @@ getFreeTyVars tys = do go bound (Q _) acc = acc go bound (QC _) acc = acc 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 Term -zonkTerm (Prod bt x t1 t2) = do - t1 <- zonkTerm t1 - t2 <- zonkTerm t2 - return (Prod bt x t1 t2) -zonkTerm (Q n) = return (Q n) -zonkTerm (QC n) = return (QC n) -zonkTerm (EInt n) = return (EInt n) -zonkTerm (EFloat f) = return (EFloat f) -zonkTerm (K s) = return (K s) -zonkTerm (Empty) = return (Empty) -zonkTerm (Sort s) = return (Sort s) -zonkTerm (App arg res) = do - arg <- zonkTerm arg - res <- zonkTerm res - return (App arg res) -zonkTerm (Abs bt x body) = do - body <- zonkTerm body - return (Abs bt x body) -zonkTerm (Typed body ty) = do - body <- zonkTerm body - ty <- zonkTerm ty - return (Typed body ty) -zonkTerm (Vr x) = return (Vr x) zonkTerm (Meta i) = do mv <- getMeta i case mv of @@ -362,10 +479,5 @@ zonkTerm (Meta i) = do Bound t -> do t <- zonkTerm t setMeta i (Bound t) -- "Short out" multiple hops return t -zonkTerm (ImplArg t) = do - t <- zonkTerm t - return (ImplArg t) -zonkTerm (FV ts) = do - ts <- mapM zonkTerm ts - return (FV ts) -zonkTerm t = error ("zonkTerm "++show t) +zonkTerm t = composOp zonkTerm t + diff --git a/src/compiler/GF/Grammar/Grammar.hs b/src/compiler/GF/Grammar/Grammar.hs index 5174b1695..01d9cc9ec 100644 --- a/src/compiler/GF/Grammar/Grammar.hs +++ b/src/compiler/GF/Grammar/Grammar.hs @@ -476,7 +476,7 @@ type Hypo = (BindType,Ident,Term) -- (x:A) (_:A) A ({x}:A) type Context = [Hypo] -- (x:A)(y:B) (x,y:A) (_,_:A) type Equation = ([Patt],Term) -type Labelling = (Label, Term) +type Labelling = (Label, Type) type Assign = (Label, (Maybe Type, Term)) type Case = (Patt, Term) type Cases = ([Patt], Term) diff --git a/src/compiler/GF/Infra/CheckM.hs b/src/compiler/GF/Infra/CheckM.hs index 8a1b42cdf..7a5ac2d45 100644 --- a/src/compiler/GF/Infra/CheckM.hs +++ b/src/compiler/GF/Infra/CheckM.hs @@ -13,7 +13,7 @@ ----------------------------------------------------------------------------- module GF.Infra.CheckM - (Check, Message, runCheck, + (Check(..), CheckResult(..), Message, runCheck, checkError, checkCond, checkWarn, checkErr, checkIn, checkMap ) where |