Remove VUndef

diff --git a/CTT.hs b/CTT.hs
index b8c462e9656ce31e160b33594abb2a34561e4175..176651c6acb34ea0a6b127e0d5ff50f858f2bd6e 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -157,7 +157,6 @@ data Val = VU
 
            -- Neutral values:
          | VVar Ident Val
-         | VUndef Loc Val
          | VFst Val
          | VSnd Val
          | VSplit Val Val
@@ -168,7 +167,6 @@ data Val = VU
 
 isNeutral :: Val -> Bool
 isNeutral v = case v of
-  VUndef _ _        -> True
   VVar _ _          -> True
   VFst v            -> isNeutral v
   VSnd v            -> isNeutral v
@@ -365,7 +363,6 @@ showVal v = case v of
                          text "->" <+> showVal e
   VSplit u v        -> showVal u <+> showVal1 v
   VVar x t          -> text x
-  VUndef _ _        -> text "undefined"
   VFst u            -> showVal1 u <> text ".1"
   VSnd u            -> showVal1 u <> text ".2"
   VIdP v0 v1 v2     -> text "IdP" <+> showVals [v0,v1,v2]
@@ -385,7 +382,6 @@ showVal1 v = case v of
   VU              -> char 'U'
   VCon c []       -> text c
   VVar{}          -> showVal v
-  VUndef{}        -> showVal v
   Ter t@Sum{} rho -> showTer t <+> showEnv rho
   _               -> parens (showVal v)
 

diff --git a/Eval.hs b/Eval.hs
index 3118272595779f13243f2effcffb9b88b99946c9..b3306ea56d71584349e5fddeb98467615cbb7441 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -59,7 +59,6 @@ instance Nominal Val where
   support (VCon _ vs)           = support vs
   support (VPCon _ a vs phi)    = support (a,vs,phi)
   support (VVar _ v)            = support v
-  support (VUndef _ v)          = support v
   support (VApp u v)            = support (u,v)
   support (VLam _ u v)          = support (u,v)
   support (VAppFormula u phi)   = support (u,phi)
@@ -91,7 +90,6 @@ instance Nominal Val where
          VCon c vs  -> VCon c (acti vs)
          VPCon c a vs phi -> pcon c (acti a) (acti vs) (acti phi)
          VVar x v   -> VVar x (acti v)
-         VUndef x v -> VUndef x (acti v)
          VAppFormula u psi -> acti u @@ acti psi
          VApp u v   -> app (acti u) (acti v)
          VLam x t u -> VLam x (acti t) (acti u)
@@ -120,7 +118,6 @@ instance Nominal Val where
          VCon c vs           -> VCon c (sw vs)
          VPCon c a vs phi    -> VPCon c (sw a) (sw vs) (sw phi)
          VVar x v            -> VVar x (sw v)
-         VUndef x v          -> VUndef x (sw v)
          VAppFormula u psi   -> VAppFormula (sw u) (sw psi)
          VApp u v            -> VApp (sw u) (sw v)
          VLam x u v          -> VLam x (sw u) (sw v)
@@ -138,7 +135,6 @@ eval rho v = case v of
   U                   -> VU
   App r s             -> app (eval rho r) (eval rho s)
   Var i               -> look i rho
-  Undef l t           -> VUndef l (eval rho t)
   Pi t@(Lam _ a _)    -> VPi (eval rho a) (eval rho t)
   Lam{}               -> Ter v rho
   Sigma t@(Lam _ a _) -> VSigma (eval rho a) (eval rho t)
@@ -163,6 +159,7 @@ eval rho v = case v of
   CompElem a es u us -> compElem (eval rho a) (evalSystem rho es) (eval rho u)
                          (evalSystem rho us)
   ElimComp a es u    -> elimComp (eval rho a) (evalSystem rho es) (eval rho u)
+  _ -> error $ "Cannot evaluate " ++ show v
 
 evalFormula :: Env -> Formula -> Formula
 evalFormula rho phi = case phi of
@@ -234,7 +231,7 @@ sndVal u               = error $ "sndVal: " ++ show u ++ " is not neutral."
 inferType :: Val -> Val
 inferType v = case v of
   VVar _ t -> t
-  VUndef _ t -> t
+  Ter (Undef _ t) rho -> eval rho t
   VFst t -> case inferType t of
     VSigma a _ -> a
     ty         -> error $ "inferType: expected Sigma type for " ++ show v
@@ -700,7 +697,7 @@ instance Convertible Val where
         in conv (k+1) (app u' v) (eval (Upd e (x,v)) u)
       (Ter (Split _ p _ _) e,Ter (Split _ p' _ _) e') -> (p == p') && conv k e e'
       (Ter (Sum p _ _) e,Ter (Sum p' _ _) e')         -> (p == p') && conv k e e'
-      (VUndef p _,VUndef p' _) -> p == p'
+      (Ter (Undef p _) e,Ter (Undef p' _) e') -> p == p' && conv k e e'
       (VPi u v,VPi u' v') ->
         let w = mkVar k u
         in conv k u u' && conv (k+1) (app v w) (app v' w)