fix the current PGF typechecker

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