From: Anders <mortberg@chalmers.se>
Date: Wed, 15 Apr 2015 09:46:54 +0000 (+0200)
Subject: Fix undefined
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=b6db2f91011bde17b4f96263c1d129a0d6c7b955;p=cubicaltt.git

Fix undefined
---

diff --git a/CTT.hs b/CTT.hs
index 176651c..ee1f020 100644
--- a/CTT.hs
+++ b/CTT.hs
@@ -167,6 +167,7 @@ data Val = VU
 
 isNeutral :: Val -> Bool
 isNeutral v = case v of
+  Ter Undef{} _     -> True
   VVar _ _          -> True
   VFst v            -> isNeutral v
   VSnd v            -> isNeutral v
diff --git a/TypeChecker.hs b/TypeChecker.hs
index 39e920b..407f7af 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -143,6 +143,7 @@ evalTyping t = eval <$> asks env <*> pure t
 -- Check that t has type a
 check :: Val -> Ter -> Typing ()
 check a t = case (a,t) of
+  (_,Undef{}) -> return ()
   (_,Con c es) -> do
     (bs,nu) <- getLblType c a
     checks (bs,nu) es
@@ -359,7 +360,7 @@ infer :: Ter -> Typing Val
 infer e = case e of
   U         -> return VU  -- U : U
   Var n     -> lookType n <$> asks env
-  Undef _ t -> evalTyping t
+--  Undef _ t -> evalTyping t
   App t u -> do
     c <- infer t
     case c of