From b8776e6e289a9f73989a3e396ae33e776ad2ae4f Mon Sep 17 00:00:00 2001 From: krasimir Date: Fri, 19 Jun 2009 12:03:18 +0000 Subject: [PATCH] fix the current PGF typechecker --- src/PGF/Expr.hs | 20 +++++++++++++------- src/PGF/TypeCheck.hs | 10 +++++++--- 2 files changed, 20 insertions(+), 10 deletions(-) diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs index 90b1af64a..1edba0e54 100644 --- a/src/PGF/Expr.hs +++ b/src/PGF/Expr.hs @@ -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 (EMeta n) = ppMeta n 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 (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 (EMeta k) = VMeta k [] 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 e [] = eval funs env e @@ -338,14 +340,18 @@ match eqs as = -- Equality checking ----------------------------------------------------- -eqValue :: Int -> Value -> Value -> [(Value,Value)] -eqValue k v1 v2 = - case (v1,v2) of - (VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue k) vs1 vs2) +eqValue :: Funs -> Int -> Value -> Value -> [(Value,Value)] +eqValue funs k v1 v2 = + case (whnf v1,whnf v2) of + (VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue funs k) vs1 vs2) (VLit l1, VLit l2 ) | l1 == l2 -> [] - (VMeta i vs1, VMeta j vs2) | i == j -> concat (zipWith (eqValue k) vs1 vs2) - (VGen i vs1, VGen 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 funs k) vs1 vs2) (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) -> 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)] + where + whnf (VClosure env e) = eval funs env e -- should be removed when the typechecker is improved + whnf v = v + diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs index 833a531dd..4ab6d58c1 100644 --- a/src/PGF/TypeCheck.hs +++ b/src/PGF/TypeCheck.hs @@ -53,7 +53,7 @@ infer pgf tenv@(k,rho,gamma) e = case e of case typ of VClosure env (EPi x a b) -> do (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) _ -> Bad ("function type expected for function " ++ show f) _ -> 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,[]) EAbs x t -> case typ of 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 (VClosure (eins y v env) b) return (EAbs x t', cs) _ -> Bad ("function type expected for " ++ show e) _ -> 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 tenv@(k,_,_) e typ = do (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) lookupEVar :: PGF -> TCEnv -> CId -> Err Value