msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

fix the current PGF typechecker

Browse Source
This commit is contained in:
krasimir
2009-06-19 12:03:18 +00:00
parent 46439cdab9
commit ec4b9c18af
2 changed files with 20 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
src/PGF/Expr.hs
View File

@@ -180,6 +180,7 @@ ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2))
ppExpr d (ELit l) = ppLit l ppExpr d (ELit l) = ppLit l
ppExpr d (EMeta n) = ppMeta n ppExpr d (EMeta n) = ppMeta n
ppExpr d (EVar f) = PP.text (prCId f) ppExpr d (EVar f) = PP.text (prCId f)
ppExpr d (EPi x e1 e2)= PP.parens (PP.text (prCId x) PP.<+> PP.colon PP.<+> ppExpr 0 e1) PP.<+> PP.text "->" PP.<+> ppExpr 0 e2
ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps)) ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps))
ppPatt d (PLit l) = ppLit l ppPatt d (PLit l) = ppLit l
@@ -278,6 +279,7 @@ eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
eval funs env (EAbs x e) = VClosure env (EAbs x e) eval funs env (EAbs x e) = VClosure env (EAbs x e)
eval funs env (EMeta k) = VMeta k [] eval funs env (EMeta k) = VMeta k []
eval funs env (ELit l) = VLit l eval funs env (ELit l) = VLit l
eval funs env (EPi x e1 e2)= VClosure env (EPi x e1 e2)
apply :: Funs -> Env -> Expr -> [Value] -> Value apply :: Funs -> Env -> Expr -> [Value] -> Value
apply funs env e [] = eval funs env e apply funs env e [] = eval funs env e
@@ -338,14 +340,18 @@ match eqs as =
-- Equality checking -- Equality checking
----------------------------------------------------- -----------------------------------------------------
eqValue :: Int -> Value -> Value -> [(Value,Value)] eqValue :: Funs -> Int -> Value -> Value -> [(Value,Value)]
eqValue k v1 v2 = eqValue funs k v1 v2 =
case (v1,v2) of case (whnf v1,whnf v2) of
(VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue k) vs1 vs2) (VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue funs k) vs1 vs2)
(VLit l1, VLit l2 ) | l1 == l2 -> [] (VLit l1, VLit l2 ) | l1 == l2 -> []
(VMeta i vs1, VMeta j vs2) | i == j -> concat (zipWith (eqValue k) vs1 vs2) (VMeta i vs1, VMeta j vs2) | i == j -> concat (zipWith (eqValue funs k) vs1 vs2)
(VGen i vs1, VGen j vs2) | i == j -> concat (zipWith (eqValue k) vs1 vs2) (VGen i vs1, VGen j vs2) | i == j -> concat (zipWith (eqValue funs k) vs1 vs2)
(VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) -> (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
let v = VGen k [] let v = VGen k []
in eqValue (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2) in eqValue funs (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2)
_ -> [(v1,v2)] _ -> [(v1,v2)]
where
whnf (VClosure env e) = eval funs env e -- should be removed when the typechecker is improved
whnf v = v

10
src/PGF/TypeCheck.hs
View File

@@ -53,7 +53,7 @@ infer pgf tenv@(k,rho,gamma) e = case e of
case typ of case typ of
VClosure env (EPi x a b) -> do VClosure env (EPi x a b) -> do
(a',csa) <- checkExp pgf tenv t (VClosure env a) (a',csa) <- checkExp pgf tenv t (VClosure env a)
let b' = eval (funs (abstract pgf)) (eins x (VClosure rho t) env) b let b' = eval (getFunEnv (abstract pgf)) (eins x (VClosure rho t) env) b
return $ (EApp f' a', b', csf ++ csa) return $ (EApp f' a', b', csf ++ csa)
_ -> Bad ("function type expected for function " ++ show f) _ -> Bad ("function type expected for function " ++ show f)
_ -> Bad ("cannot infer type of expression" ++ show e) _ -> Bad ("cannot infer type of expression" ++ show e)
@@ -66,17 +66,21 @@ checkExp pgf tenv@(k,rho,gamma) e typ = do
EMeta m -> return $ (e,[]) EMeta m -> return $ (e,[])
EAbs x t -> case typ of EAbs x t -> case typ of
VClosure env (EPi y a b) -> do VClosure env (EPi y a b) -> do
let a' = eval (funs (abstract pgf)) env a let a' = eval (getFunEnv (abstract pgf)) env a
(t',cs) <- checkExp pgf (k+1,eins x v rho, eins x a' gamma) t (t',cs) <- checkExp pgf (k+1,eins x v rho, eins x a' gamma) t
(VClosure (eins y v env) b) (VClosure (eins y v env) b)
return (EAbs x t', cs) return (EAbs x t', cs)
_ -> Bad ("function type expected for " ++ show e) _ -> Bad ("function type expected for " ++ show e)
_ -> checkInferExp pgf tenv e typ _ -> checkInferExp pgf tenv e typ
getFunEnv abs = Map.union (funs abs) (Map.map (\hypos -> (DTyp hypos cidType [],0,[])) (cats abs))
where
cidType = mkCId "Type"
checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)]) checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
checkInferExp pgf tenv@(k,_,_) e typ = do checkInferExp pgf tenv@(k,_,_) e typ = do
(e',w,cs1) <- infer pgf tenv e (e',w,cs1) <- infer pgf tenv e
let cs2 = eqValue k w typ let cs2 = eqValue (getFunEnv (abstract pgf)) k w typ
return (e',cs1 ++ cs2) return (e',cs1 ++ cs2)
lookupEVar :: PGF -> TCEnv -> CId -> Err Value lookupEVar :: PGF -> TCEnv -> CId -> Err Value