From: Simon Huber <hubsim@gmail.com>
Date: Thu, 19 Mar 2015 13:11:31 +0000 (+0100)
Subject: the endpoints of a path should match the Id arguments; inferType
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=02343c62f620981615a40a82a96983d982b5ba34;p=cubicaltt.git

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

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