GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-23 11:42:49 -06:00
Code Issues Packages Projects Releases Wiki Activity

more stuff in the new type checker

Browse Source
This commit is contained in:
kr.angelov
2011-11-30 14:55:52 +00:00
parent f9af731c9c
commit 7863b21c1a
5 changed files with 328 additions and 199 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
src/compiler/GF/Compile/CheckGrammar.hs
View File

@@ -28,6 +28,7 @@ import GF.Infra.Option
import GF.Compile.TypeCheck.Abstract import GF.Compile.TypeCheck.Abstract
import GF.Compile.TypeCheck.Concrete import GF.Compile.TypeCheck.Concrete
import qualified GF.Compile.TypeCheck.ConcreteNew as CN import qualified GF.Compile.TypeCheck.ConcreteNew as CN
import qualified GF.Compile.Compute.ConcreteNew as CN
import GF.Grammar import GF.Grammar
import GF.Grammar.Lexer import GF.Grammar.Lexer
@@ -211,7 +212,9 @@ checkInfo opts ms (m,mo) c info = do
(pty', pde') <- case (pty,pde) of (pty', pde') <- case (pty,pde) of
(Just (L loct ty), Just (L locd de)) -> do (Just (L loct ty), Just (L locd de)) -> do
ty' <- chIn loct "operation" $ 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" $ (de',_) <- chIn locd "operation" $
(if flag optNewComp opts (if flag optNewComp opts
then CN.checkLType gr de ty' then CN.checkLType gr de ty'

58
src/compiler/GF/Compile/Compute/ConcreteNew.hs
View File

@@ -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 data Value
= VApp QIdent [Value] = VApp QIdent [Value]
@@ -8,29 +14,37 @@ data Value
| VMeta MetaId Env [Value] | VMeta MetaId Env [Value]
| VClosure Env Term | VClosure Env Term
| VSort Ident | VSort Ident
| VTblType Value Value
| VRecType [(Label,Value)]
deriving Show deriving Show
type Env = [(Ident,Value)] type Env = [(Ident,Value)]
eval :: Env -> Term -> Value eval :: SourceGrammar -> Env -> Term -> Value
eval env (Vr x) = case lookup x env of eval gr env (Vr x) = case lookup x env of
Just v -> v Just v -> v
Nothing -> error ("Unknown variable "++showIdent x) Nothing -> error ("Unknown variable "++showIdent x)
eval env (Q x) = VApp x [] eval gr env (Q x) = VApp x []
eval env (Meta i) = VMeta i env [] eval gr env (QC x) = VApp x []
eval env t@(Prod _ _ _ _) = VClosure env t eval gr env (Meta i) = VMeta i env []
eval env t@(Abs _ _ _) = VClosure env t eval gr env t@(Prod _ _ _ _) = VClosure env t
eval env (Sort s) = VSort s eval gr env t@(Abs _ _ _) = VClosure env t
eval env t = error (show 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 :: SourceGrammar -> [Ident] -> Value -> Term
value2term xs (VApp f vs) = foldl App (Q f) (map (value2term xs) vs) value2term gr xs (VApp f vs) = foldl App (Q f) (map (value2term gr xs) vs)
value2term xs (VGen j vs) = foldl App (Vr (reverse xs !! j)) (map (value2term xs) vs) value2term gr xs (VGen j vs) = foldl App (Vr (reverse xs !! j)) (map (value2term gr xs) vs)
value2term xs (VMeta j env vs) = foldl App (Meta j) (map (value2term xs) vs) value2term gr xs (VMeta j env vs) = foldl App (Meta j) (map (value2term gr xs) vs)
value2term xs (VClosure env (Prod bt x t1 t2)) = Prod bt x (value2term xs (eval env t1)) value2term gr xs (VClosure env (Prod bt x t1 t2)) = Prod bt x (value2term gr xs (eval gr env t1))
(value2term (x:xs) (eval ((x,VGen (length xs) []) : env) t2)) (value2term gr (x:xs) (eval gr ((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 gr xs (VClosure env (Abs bt x t)) = Abs bt x (value2term gr (x:xs) (eval gr ((x,VGen (length xs) []) : env) t))
value2term xs (VSort s) = Sort s value2term gr xs (VSort s) = Sort s
value2term xs v = error (show 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 v = error ("value2term "++show v)

460
src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
View File

@@ -1,14 +1,16 @@
module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where 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.Lookup
import GF.Grammar.Predef
import GF.Compile.Compute.ConcreteNew import GF.Compile.Compute.ConcreteNew
import GF.Compile.Compute.AppPredefined
import GF.Infra.CheckM import GF.Infra.CheckM
import GF.Infra.UseIO import GF.Infra.UseIO
import GF.Data.Operations import GF.Data.Operations
import Text.PrettyPrint import Text.PrettyPrint
import Data.List (nub, (\\)) import Data.List (nub, (\\), tails)
import qualified Data.IntMap as IntMap import qualified Data.IntMap as IntMap
import qualified Data.ByteString.Char8 as BS import qualified Data.ByteString.Char8 as BS
@@ -18,7 +20,7 @@ import Debug.Trace
checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type) checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
checkLType gr t ty = runTcM $ do checkLType gr t ty = runTcM $ do
t <- checkSigma gr [] t (eval [] ty) t <- checkSigma gr [] t (eval gr [] ty)
t <- zonkTerm t t <- zonkTerm t
return (t,ty) return (t,ty)
@@ -26,66 +28,72 @@ inferLType :: SourceGrammar -> Term -> Check (Term, Type)
inferLType gr t = runTcM $ do inferLType gr t = runTcM $ do
(t,ty) <- inferSigma gr [] t (t,ty) <- inferSigma gr [] t
t <- zonkTerm t t <- zonkTerm t
ty <- zonkTerm (value2term [] ty) ty <- zonkTerm (value2term gr [] ty)
return (t,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 :: SourceGrammar -> Scope -> Term -> Sigma -> TcM Term
checkSigma gr scope t sigma = do checkSigma gr scope t sigma = do -- GEN2
(skol_tvs, rho) <- skolemise scope sigma (abs, scope, t, rho) <- skolemise id gr scope t sigma
let skol_tvs = []
(t,rho) <- tcRho gr scope t (Just rho) (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 let bad_tvs = filter (`elem` esc_tvs) skol_tvs
if null bad_tvs if null bad_tvs
then return t then return (abs t)
else tcError (text "Type not polymorphic enough") 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 :: 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@(EInt _) mb_ty = instSigma gr scope t (eval gr [] typeInt) mb_ty
tcRho gr scope t@(EFloat _) mb_ty = instSigma scope t (eval [] typeFloat) 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 scope t (eval [] typeString) 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 scope t (eval [] typeString) 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 tcRho gr scope t@(Vr v) mb_ty = do -- VAR
case lookup v scope of 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) Nothing -> tcError (text "Unknown variable" <+> ppIdent v)
tcRho gr scope t@(Q id) mb_ty = do tcRho gr scope t@(Q id) mb_ty
case lookupResType gr id of | elem (fst id) [cPredef,cPredefAbs] =
Ok ty -> instSigma scope t (eval [] ty) mb_ty case typPredefined (snd id) of
Bad err -> tcError (text err) 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 tcRho gr scope t@(QC id) mb_ty = do
case lookupResType gr id of 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) 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 (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 arg <- checkSigma gr scope arg arg_ty
instSigma scope (App fun arg) res_ty mb_ty instSigma gr scope (App fun arg) res_ty mb_ty
tcRho gr scope (Abs bt var body) (Just ty) = do tcRho gr scope (Abs bt var body) Nothing = do -- ABS1
trace (show ty) $ return () i <- newMeta (eval gr [] typeType)
(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)
(body,body_ty) <- tcRho gr ((var,VMeta i (scopeEnv scope) []):scope) body Nothing (body,body_ty) <- tcRho gr ((var,VMeta i (scopeEnv scope) []):scope) body Nothing
return (Abs bt var body, (VClosure (scopeEnv scope) return (Abs bt var body, (VClosure (scopeEnv scope)
(Prod bt identW (Meta i) (value2term (scopeVars scope) body_ty)))) (Prod bt identW (Meta i) (value2term gr (scopeVars scope) body_ty))))
tcRho gr scope (Typed body ann_ty) mb_ty = do tcRho gr scope (Abs bt var body) (Just ty) = do -- ABS2
body <- checkSigma gr scope body (eval (scopeEnv scope) ann_ty) (var_ty, body_ty) <- unifyFun gr scope (VGen (length scope) []) ty
instSigma scope (Typed body ann_ty) (eval (scopeEnv scope) ann_ty) mb_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 tcRho gr scope (FV ts) mb_ty = do
case ts of case ts of
[] -> do i <- newMeta (eval [] typeType) [] -> do i <- newMeta (eval gr [] typeType)
instSigma scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty instSigma gr scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty
(t:ts) -> do (t,ty) <- tcRho gr scope t mb_ty (t:ts) -> do (t,ty) <- tcRho gr scope t mb_ty
let go [] ty = return ([],ty) let go [] ty = return ([],ty)
@@ -95,93 +103,202 @@ tcRho gr scope (FV ts) mb_ty = do
(ts,ty) <- go ts ty (ts,ty) <- go ts ty
return (FV (t: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) 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), -- | Invariant: if the third argument is (Just rho),
-- then rho is in weak-prenex form -- then rho is in weak-prenex form
instSigma :: Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho) instSigma :: SourceGrammar -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
instSigma scope t ty1 (Just ty2) = do t <- subsCheckRho scope t ty1 ty2 instSigma gr scope t ty1 Nothing = instantiate gr t ty1 -- INST1
return (t,ty2) instSigma gr scope t ty1 (Just ty2) = do -- INST2
instSigma scope t ty1 Nothing = instantiate t ty1 t <- subsCheckRho gr scope t ty1 ty2
return (t,ty2)
-- | (subsCheck scope args off exp) checks that -- | (subsCheck scope args off exp) checks that
-- 'off' is at least as polymorphic as 'args -> exp' -- 'off' is at least as polymorphic as 'args -> exp'
subsCheck :: Scope -> Term -> Sigma -> Sigma -> TcM Term subsCheck :: SourceGrammar -> Scope -> Term -> Sigma -> Sigma -> TcM Term
subsCheck scope t sigma1 sigma2 = do -- Rule DEEP-SKOL subsCheck gr scope t sigma1 sigma2 = do -- DEEP-SKOL
(skol_tvs, rho2) <- skolemise scope sigma2 (abs, scope, t, rho2) <- skolemise id gr scope t sigma2
t <- subsCheckRho scope t sigma1 rho2 let skol_tvs = []
esc_tvs <- getFreeTyVars [sigma1,sigma2] t <- subsCheckRho gr scope t sigma1 rho2
esc_tvs <- getFreeVars gr [(scope,sigma1),(scope,sigma2)]
let bad_tvs = filter (`elem` esc_tvs) skol_tvs let bad_tvs = filter (`elem` esc_tvs) skol_tvs
if null bad_tvs if null bad_tvs
then return () then return (abs t)
else tcError (vcat [text "Subsumption check failed:", 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", text "is not as polymorphic as",
nest 2 (ppTerm Unqualified 0 (value2term [] sigma2))]) nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) sigma2))])
return t
-- | Invariant: the second argument is in weak-prenex form -- | Invariant: the second argument is in weak-prenex form
subsCheckRho :: Scope -> Term -> Sigma -> Rho -> TcM Term subsCheckRho :: SourceGrammar -> Scope -> Term -> Sigma -> Rho -> TcM Term
subsCheckRho scope t sigma1@(VClosure env (Prod Implicit _ _ _)) rho2 = do -- Rule SPEC subsCheckRho gr scope t sigma1@(VClosure env (Prod Implicit _ _ _)) rho2 = do -- Rule SPEC
(t,rho1) <- instantiate t sigma1 (t,rho1) <- instantiate gr t sigma1
subsCheckRho scope t rho1 rho2 subsCheckRho gr scope t rho1 rho2
subsCheckRho scope t rho1 (VClosure env (Prod Explicit _ a2 r2)) = do -- Rule FUN subsCheckRho gr scope t rho1 (VClosure env (Prod Explicit _ a2 r2)) = do -- Rule FUN
(a1,r1) <- unifyFun scope rho1 (a1,r1) <- unifyFun gr scope (VGen (length scope) []) rho1
subsCheckFun scope t a1 r1 (eval env a2) (eval env r2) subsCheckFun gr scope t a1 r1 (eval gr env a2) (eval gr env r2)
subsCheckRho scope t (VClosure env (Prod Explicit _ a1 r1)) rho2 = do -- Rule FUN subsCheckRho gr scope t (VClosure env (Prod Explicit _ a1 r1)) rho2 = do -- Rule FUN
(a2,r2) <- unifyFun scope rho2 (a2,r2) <- unifyFun gr scope (VGen (length scope) []) rho2
subsCheckFun scope t (eval env a1) (eval env r1) a2 r2 subsCheckFun gr scope t (eval gr env a1) (eval gr env r1) a2 r2
subsCheckRho scope t tau1 tau2 = do -- Rule MONO subsCheckRho gr scope t (VSort s1) (VSort s2)
unify scope tau1 tau2 -- Revert to ordinary unification | 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 return t
subsCheckFun :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term subsCheckFun :: SourceGrammar -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
subsCheckFun scope t a1 r1 a2 r2 = do subsCheckFun gr scope t a1 r1 a2 r2 = do
let v = newVar scope let v = newVar scope
vt <- subsCheck scope (Vr v) a2 a1 vt <- subsCheck gr scope (Vr v) a2 a1
t <- subsCheckRho ((v,eval [] typeType):scope) (App t vt) r1 r2 ; t <- subsCheckRho gr ((v,eval gr [] typeType):scope) (App t vt) r1 r2 ;
return (Abs Implicit v t) return (Abs Explicit v t)
----------------------------------------------------------------------- -----------------------------------------------------------------------
-- Unification -- Unification
----------------------------------------------------------------------- -----------------------------------------------------------------------
unifyFun :: Scope -> Rho -> TcM (Sigma, Rho) unifyFun :: SourceGrammar -> Scope -> Value -> Rho -> TcM (Sigma, Rho)
unifyFun scope (VClosure env (Prod Explicit x arg res)) unifyFun gr scope arg_v (VClosure env (Prod Explicit x arg res))
| x /= identW = return (eval env arg,eval ((x,VGen (length scope) []):env) res) | x /= identW = return (eval gr env arg,eval gr ((x,arg_v):env) res)
| otherwise = return (eval env arg,eval env res) | otherwise = return (eval gr env arg,eval gr env res)
unifyFun scope tau = do unifyFun gr scope arg_v tau = do
arg_ty <- newMeta (eval [] typeType) arg_ty <- newMeta (eval gr [] typeType)
res_ty <- newMeta (eval [] typeType) res_ty <- newMeta (eval gr [] typeType)
unify scope tau (VClosure [] (Prod Explicit identW (Meta arg_ty) (Meta res_ty))) unify gr scope tau (VClosure [] (Prod Explicit identW (Meta arg_ty) (Meta res_ty)))
return (VMeta arg_ty [] [], VMeta res_ty [] []) return (VMeta arg_ty [] [], VMeta res_ty [] [])
unify scope (VApp f1 vs1) (VApp f2 vs2) unify gr scope (VApp f1 vs1) (VApp f2 vs2)
| f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2) | f1 == f2 = sequence_ (zipWith (unify gr scope) vs1 vs2)
unify scope (VMeta i env1 vs1) (VMeta j env2 vs2) unify gr scope (VSort s1) (VSort s2)
| i == j = sequence_ (zipWith (unify scope) vs1 vs2) | 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 | otherwise = do mv <- getMeta j
case mv of 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)) Unbound _ -> setMeta i (Bound (Meta j))
unify scope (VMeta i env vs) v = unifyVar scope i env vs v unify gr scope (VMeta i env vs) v = unifyVar gr scope i env vs v
unify scope v (VMeta i env vs) = unifyVar scope i env vs v unify gr scope v (VMeta i env vs) = unifyVar gr scope i env vs v
unify scope v1 v2 = do unify gr scope (VTblType p1 res1) (VTblType p2 res2) = do
v1 <- zonkTerm (value2term (scopeVars scope) v1) unify gr scope p1 p2
v2 <- zonkTerm (value2term (scopeVars scope) v2) 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 $$ tcError (text "Cannot unify types:" <+> (ppTerm Unqualified 0 v1 $$
ppTerm Unqualified 0 v2)) ppTerm Unqualified 0 v2))
-- | Invariant: tv1 is a flexible type variable -- | Invariant: tv1 is a flexible type variable
unifyVar :: Scope -> MetaId -> Env -> [Value] -> Tau -> TcM () unifyVar :: SourceGrammar -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
unifyVar scope i env vs ty2 = do -- Check whether i is bound unifyVar gr scope i env vs ty2 = do -- Check whether i is bound
mv <- getMeta i mv <- getMeta i
case mv of case mv of
Bound ty1 -> unify scope (apply env ty1 vs) ty2 Bound ty1 -> unify gr scope (apply gr env ty1 vs) ty2
Unbound _ -> do let ty2' = value2term [] ty2 Unbound _ -> do let ty2' = value2term gr (scopeVars scope) ty2
ms2 <- getMetaVars [ty2] ms2 <- getMetaVars gr [(scope,ty2)]
if i `elem` ms2 if i `elem` ms2
then tcError (text "Occurs check for" <+> ppMeta i <+> text "in:" $$ then tcError (text "Occurs check for" <+> ppMeta i <+> text "in:" $$
nest 2 (ppTerm Unqualified 0 ty2')) 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 -- | Instantiate the topmost for-alls of the argument type
-- with metavariables -- with metavariables
instantiate :: Term -> Sigma -> TcM (Term,Rho) instantiate :: SourceGrammar -> Term -> Sigma -> TcM (Term,Rho)
instantiate t (VClosure env (Prod Implicit x ty1 ty2)) = do instantiate gr t (VClosure env (Prod Implicit x ty1 ty2)) = do
i <- newMeta (eval env ty1) i <- newMeta (eval gr env ty1)
instantiate (App t (ImplArg (Meta i))) (eval ((x,VMeta i [] []):env) ty2) instantiate gr (App t (ImplArg (Meta i))) (eval gr ((x,VMeta i [] []):env) ty2)
instantiate t ty = do instantiate gr t ty = do
return (t,ty) return (t,ty)
skolemise scope (VClosure env (Prod Implicit x arg_ty res_ty)) = do -- Rule PRPOLY skolemise f gr scope t (VClosure env (Prod Implicit x arg_ty res_ty)) -- Rule PRPOLY
sk <- newSkolemTyVar arg_ty | x /= identW =
(sks, res_ty) <- skolemise scope (eval ((x,undefined):env) res_ty) let (y,body) = case t of
return (sk : sks, res_ty) Abs Implicit y body -> (y, body)
skolemise scope (VClosure env (Prod Explicit x arg_ty res_ty)) = do -- Rule PRFUN body -> (newVar scope, body)
(sks, res_ty) <- if x /= identW in skolemise (f . Abs Implicit y)
then skolemise scope (eval ((x,VGen (length scope) []):env) res_ty) gr
else skolemise scope (eval env res_ty) ((y,eval gr env arg_ty):scope) body
return (sks, VClosure env (Prod Explicit x arg_ty (value2term [] res_ty))) (eval gr ((x,VGen (length scope) []):env) res_ty)
skolemise scope ty -- Rule PRMONO skolemise f gr scope t (VClosure env (Prod Explicit x arg_ty res_ty)) -- Rule PRFUN
= return ([], ty) | 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)
newSkolemTyVar _ = undefined
-- Quantify over the specified type variables (all flexible) -- | Quantify over the specified type variables (all flexible)
quantify :: Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma) quantify :: SourceGrammar -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
quantify scope t tvs ty0 = do quantify gr scope t tvs ty0 = do
mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
ty <- zonkTerm ty -- of doing the substitution ty <- zonkTerm ty -- of doing the substitution
return (foldr (Abs Implicit) t new_bndrs 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 where
ty = value2term (scopeVars scope) ty0 ty = value2term gr (scopeVars scope) ty0
used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
new_bndrs = take (length tvs) (allBinders \\ used_bndrs) new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
@@ -253,37 +379,46 @@ data MetaValue
| Bound Term | Bound Term
type MetaStore = IntMap.IntMap MetaValue type MetaStore = IntMap.IntMap MetaValue
data TcResult a data TcResult a
= TcOk MetaStore a = TcOk a MetaStore [Message]
| TcFail Doc | TcFail [Message]
newtype TcM a = TcM {unTcM :: MetaStore -> TcResult a} newtype TcM a = TcM {unTcM :: MetaStore -> [Message] -> TcResult a}
instance Monad TcM where instance Monad TcM where
return x = TcM (\ms -> TcOk ms x) return x = TcM (\ms msgs -> TcOk x ms msgs)
f >>= g = TcM (\ms -> case unTcM f ms of f >>= g = TcM (\ms msgs -> case unTcM f ms msgs of
TcOk ms x -> unTcM (g x) ms TcOk x ms msgs -> unTcM (g x) ms msgs
TcFail msg -> TcFail msg) TcFail msgs -> TcFail msgs)
fail = tcError . text 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 :: 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 :: TcM a -> Check a
runTcM f = case unTcM f IntMap.empty of runTcM f = Check (\ctxt msgs -> case unTcM f IntMap.empty msgs of
TcOk _ x -> return x TcOk x _ msgs -> Success x msgs
TcFail s -> checkError s TcFail msgs -> Fail msgs)
newMeta :: Sigma -> TcM MetaId newMeta :: Sigma -> TcM MetaId
newMeta ty = TcM (\ms -> let i = IntMap.size ms newMeta ty = TcM (\ms msgs ->
in TcOk (IntMap.insert i (Unbound ty) ms) i) let i = IntMap.size ms
in TcOk i (IntMap.insert i (Unbound ty) ms) msgs)
getMeta :: MetaId -> TcM MetaValue getMeta :: MetaId -> TcM MetaValue
getMeta i = TcM (\ms -> getMeta i = TcM (\ms msgs ->
case IntMap.lookup i ms of case IntMap.lookup i ms of
Just mv -> TcOk ms mv Just mv -> TcOk mv ms msgs
Nothing -> TcFail (text "Unknown metavariable" <+> ppMeta i)) Nothing -> TcFail ((text "Unknown metavariable" <+> ppMeta i) : msgs))
setMeta :: MetaId -> MetaValue -> TcM () 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 -> Ident
newVar scope = head [x | i <- [1..], newVar scope = head [x | i <- [1..],
@@ -293,14 +428,15 @@ newVar scope = head [x | i <- [1..],
isFree [] x = True isFree [] x = True
isFree ((y,_):scope) x = x /= y && isFree scope x isFree ((y,_):scope) x = x /= y && isFree scope x
scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..] scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..]
scopeVars scope = map fst scope 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 -- | This function takes account of zonking, and returns a set
-- (no duplicates) of unbound meta-type variables -- (no duplicates) of unbound meta-type variables
getMetaVars :: [Sigma] -> TcM [MetaId] getMetaVars :: SourceGrammar -> [(Scope,Sigma)] -> TcM [MetaId]
getMetaVars tys = do getMetaVars gr sc_tys = do
tys <- mapM (zonkTerm . value2term []) tys tys <- mapM (\(scope,ty) -> zonkTerm (value2term gr (scopeVars scope) ty)) sc_tys
return (foldr go [] tys) return (foldr go [] tys)
where where
-- Get the MetaIds from a term; no duplicates in result -- Get the MetaIds from a term; no duplicates in result
@@ -312,15 +448,17 @@ getMetaVars tys = do
go (QC _) acc = acc go (QC _) acc = acc
go (Sort _) acc = acc go (Sort _) acc = acc
go (Prod _ _ arg res) acc = go arg (go res 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) go t acc = error ("go "++show t)
-- | This function takes account of zonking, and returns a set -- | This function takes account of zonking, and returns a set
-- (no duplicates) of free type variables -- (no duplicates) of free type variables
getFreeTyVars :: [Sigma] -> TcM [Ident] getFreeVars :: SourceGrammar -> [(Scope,Sigma)] -> TcM [Ident]
getFreeTyVars tys = do getFreeVars gr sc_tys = do
tys <- mapM (zonkTerm . value2term []) tys tys <- mapM (\(scope,ty) -> zonkTerm (value2term gr (scopeVars scope) ty)) sc_tys
return (foldr (go []) [] tys) return (foldr (go []) [] tys)
where where
go bound (Vr tv) acc go bound (Vr tv) acc
| tv `elem` bound = acc | tv `elem` bound = acc
| tv `elem` acc = acc | tv `elem` acc = acc
@@ -329,32 +467,11 @@ getFreeTyVars tys = do
go bound (Q _) acc = acc go bound (Q _) acc = acc
go bound (QC _) acc = acc go bound (QC _) acc = acc
go bound (Prod _ x arg res) acc = go bound arg (go (x : bound) res 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 -- | Eliminate any substitutions in a term
zonkTerm :: Term -> TcM 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 zonkTerm (Meta i) = do
mv <- getMeta i mv <- getMeta i
case mv of case mv of
@@ -362,10 +479,5 @@ zonkTerm (Meta i) = do
Bound t -> do t <- zonkTerm t Bound t -> do t <- zonkTerm t
setMeta i (Bound t) -- "Short out" multiple hops setMeta i (Bound t) -- "Short out" multiple hops
return t return t
zonkTerm (ImplArg t) = do zonkTerm t = composOp zonkTerm t
t <- zonkTerm t
return (ImplArg t)
zonkTerm (FV ts) = do
ts <- mapM zonkTerm ts
return (FV ts)
zonkTerm t = error ("zonkTerm "++show t)

2
src/compiler/GF/Grammar/Grammar.hs
View File

@@ -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 Context = [Hypo] -- (x:A)(y:B) (x,y:A) (_,_:A)
type Equation = ([Patt],Term) type Equation = ([Patt],Term)
type Labelling = (Label, Term) type Labelling = (Label, Type)
type Assign = (Label, (Maybe Type, Term)) type Assign = (Label, (Maybe Type, Term))
type Case = (Patt, Term) type Case = (Patt, Term)
type Cases = ([Patt], Term) type Cases = ([Patt], Term)

2
src/compiler/GF/Infra/CheckM.hs
View File

@@ -13,7 +13,7 @@
----------------------------------------------------------------------------- -----------------------------------------------------------------------------
module GF.Infra.CheckM module GF.Infra.CheckM
(Check, Message, runCheck, (Check(..), CheckResult(..), Message, runCheck,
checkError, checkCond, checkWarn, checkError, checkCond, checkWarn,
checkErr, checkIn, checkMap checkErr, checkIn, checkMap
) where ) where