the endpoints of a path should match the Id arguments; inferType

diff --git a/Eval.hs b/Eval.hs
index 8910371a028dd04c94e080cc9d67e472f7f50604..6a4bc389c01d6271096fa689664b79d2d34505e9 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -167,11 +167,21 @@ sndVal u | isNeutral u = VSnd u
 inferType :: Val -> Val
 inferType v = case v of
   VVar _ t -> t
-  VFst t -> undefined
-  VSnd t -> undefined
-  VSplit t0 t1 -> undefined
-  VApp t0 t1 -> undefined
-  VAppFormula t phi -> undefined
+  VFst t -> case inferType t of
+    VSigma a _ -> a
+    _       -> error $ "inferType: not neutral " ++ show v
+  VSnd t -> case inferType t of
+    VSigma _ f -> app f (VFst t)
+    _       -> error $ "inferType: not neutral " ++ show v
+  VSplit t0 t1 -> case inferType t0 of
+    VPi _ f -> app f t1
+    _       -> error $ "inferType: not neutral " ++ show v
+  VApp t0 t1 -> case inferType t0 of
+    VPi _ f -> app f t1
+    _       -> error $ "inferType: not neutral " ++ show v
+  VAppFormula t phi -> case inferType t of
+    VIdP a _ _ -> a @@ phi
+    _          -> error $ "inferType: not neutral " ++ show v
 
 (@@) :: ToFormula a => Val -> a -> Val
 (VPath i u) @@ phi = u `act` (i,toFormula phi)

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 7c781965821020c64af7fc915462eec3b4db2180..c2edbcdcff8306a34e8006bc4a7692bd6f141dea 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -165,11 +165,16 @@ check a t = case (a,t) of
           check b0 e0\r
           check b1 e1\r
         _ -> throwError ("IdP expects a path but got " ++ show a)\r
-  (VIdP p a b,Path i e) -> do\r
+  (VIdP p a0 a1,Path i e) -> do\r
     rho <- asks env\r
+    k   <- asks index\r
     when (i `elem` support rho)\r
       (throwError (show i ++ " is already declared"))\r
     local (addSub (i,Atom i)) $ check (p @@ i) e\r
+    let u0 = eval (Sub rho (i,Dir 0)) e\r
+        u1 = eval (Sub rho (i,Dir 1)) e\r
+    unless (conv k a0 u0 && conv k a1 u1) $\r
+      throwError $ "path endpoints don't match " ++ show e\r
   _ -> do\r
     v <- infer t\r
     k <- index <$> ask\r