Make undefined only occur as a declaration so that the type can be inferred

diff --git a/CTT.hs b/CTT.hs
index c4940da5b1ddad66ab4c69486f65c32e56f121f7..fb8d42e7e6507a60f373f30bbd78e47bf0363fc5 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -95,7 +95,7 @@ data Ter = App Ter Ter
            -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors)
          | Sum Loc Ident [Label]
            -- undefined
-         | Undef Loc
+         | Undef Loc Ter -- Location and type
 
            -- Id type
          | IdP Ter Ter Ter
@@ -155,6 +155,7 @@ data Val = VU
 
            -- Neutral values:
          | VVar Ident Val
+         | VUndef Loc Val
          | VFst Val
          | VSnd Val
          | VSplit Val Val
@@ -165,7 +166,7 @@ data Val = VU
 
 isNeutral :: Val -> Bool
 isNeutral v = case v of
-  Ter (Undef _) _   -> True
+  VUndef _ _        -> True
   VVar _ _          -> True
   VFst v            -> isNeutral v
   VSnd v            -> isNeutral v
@@ -311,7 +312,7 @@ showTer v = case v of
                           showTers es <+> showFormula phi
   Split f _ _ _      -> text f
   Sum _ n _          -> text n
-  Undef _            -> text "undefined"
+  Undef _ _          -> text "undefined"
   IdP e0 e1 e2       -> text "IdP" <+> showTers [e0,e1,e2]
   Path i e           -> char '<' <> text (show i) <> char '>' <+> showTer e
   AppFormula e phi   -> showTer1 e <+> char '@' <+> showFormula phi
@@ -359,6 +360,7 @@ 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]

diff --git a/Eval.hs b/Eval.hs
index 695f39e15c9de22ecf40369341215d662c286114..3118272595779f13243f2effcffb9b88b99946c9 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -59,6 +59,7 @@ 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)
@@ -90,6 +91,7 @@ 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)
@@ -118,6 +120,7 @@ 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)
@@ -132,10 +135,10 @@ instance Nominal Val where
 
 eval :: Env -> Ter -> Val
 eval rho v = case v of
-  Undef{}             -> Ter v rho
   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)
@@ -231,6 +234,7 @@ sndVal u               = error $ "sndVal: " ++ show u ++ " is not neutral."
 inferType :: Val -> Val
 inferType v = case v of
   VVar _ t -> t
+  VUndef _ t -> t
   VFst t -> case inferType t of
     VSigma a _ -> a
     ty         -> error $ "inferType: expected Sigma type for " ++ show v
@@ -695,8 +699,8 @@ instance Convertible Val where
         let v = mkVar k (eval e a)
         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'
-      (Ter (Undef p) e,Ter (Undef 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'
       (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)

diff --git a/Exp.cf b/Exp.cf
index f65dc3572becb3383f9c8a031c697a64ef92ebb0..4c8d347265342d53815160ab08c98cd2755341bb 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -15,6 +15,7 @@ separator Imp ";" ;
 DeclDef.    Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ;
 DeclData.   Decl ::= "data" AIdent [Tele] "=" [Label] ;
 DeclSplit.  Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ;
+DeclUndef.  Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ;
 -- DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ;
 separator   Decl ";" ;
 

diff --git a/Resolver.hs b/Resolver.hs
index 5cb5ddc8dd9faa4595f34b6b615c0f2e71f7ca63..2492949bddedca928bd96ad414056e7d17f7a171 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -87,8 +87,8 @@ updateModule mod e = e{envModule = mod}
 
 insertIdent :: (Ident,SymKind) -> Env -> Env
 insertIdent (n,var) e
-  | n == "_" || n == "undefined" = e
-  | otherwise                    = e{variables = (n,var) : variables e}
+  | n == "_"  = e
+  | otherwise = e{variables = (n,var) : variables e}
 
 insertIdents :: [(Ident,SymKind)] -> Env -> Env
 insertIdents = flip $ foldr insertIdent
@@ -111,12 +111,6 @@ insertAIdents  = flip $ foldr insertAIdent
 getLoc :: (Int,Int) -> Resolver CTT.Loc
 getLoc l = CTT.Loc <$> asks envModule <*> pure l
 
--- noLoc :: AIdent
--- noLoc = AIdent ((0,0),"_")
-
--- resolveAIdent :: AIdent -> Resolver (Ident,CTT.Loc)
--- resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l
-
 unAIdent :: AIdent -> Ident
 unAIdent (AIdent (_,x)) = x
 
@@ -130,23 +124,21 @@ resolveName (AIdent (l,x)) = do
                       show l ++ " in module " ++ modName
 
 resolveVar :: AIdent -> Resolver Ter
-resolveVar (AIdent (l,x))
-  | (x == "_") || (x == "undefined") = CTT.Undef <$> getLoc l
-  | otherwise = do
-    modName <- asks envModule
-    vars    <- asks variables
-    case lookup x vars of
-      Just Variable    -> return $ CTT.Var x
-      Just Constructor -> return $ CTT.Con x []
-      Just PConstructor -> throwError $ "The path constructor " ++ x ++ " is used as a"
-                                     ++ " variable at " ++ show l ++ " in " ++ modName
-                                     ++ " (path constructors should have their type in"
-                                     ++ " curly braces as first argument)"
-      Just Name        ->
-        throwError $ "Name " ++ x ++ " used as a variable at position " ++
-                     show l ++ " in module " ++ modName
-      _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++
-                        show l ++ " in module " ++ modName
+resolveVar (AIdent (l,x)) = do
+  modName <- asks envModule
+  vars    <- asks variables
+  case lookup x vars of
+    Just Variable    -> return $ CTT.Var x
+    Just Constructor -> return $ CTT.Con x []
+    Just PConstructor -> throwError $ "The path constructor " ++ x ++ " is used as a"
+                                   ++ " variable at " ++ show l ++ " in " ++ modName
+                                   ++ " (path constructors should have their type in"
+                                   ++ " curly braces as first argument)"
+    Just Name        ->
+     throwError $ "Name " ++ x ++ " used as a variable at position " ++
+                   show l ++ " in module " ++ modName
+    _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++
+                      show l ++ " in module " ++ modName
 
 lam :: (Ident,Exp) -> Resolver Ter -> Resolver Ter
 lam (a,t) e = CTT.Lam a <$> resolveExp t <*> local (insertVar a) e
@@ -240,13 +232,13 @@ resolveDir Dir0 = return 0
 resolveDir Dir1 = return 1
 
 resolveFormula :: Formula -> Resolver C.Formula
-resolveFormula (Dir d)        = C.Dir <$> resolveDir d
-resolveFormula (Atom i)       = C.Atom <$> resolveName i
-resolveFormula (Neg phi)      = C.negFormula <$> resolveFormula phi
-resolveFormula (Conj phi _ psi) = C.andFormula <$> resolveFormula phi
-                                <*> resolveFormula psi
-resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi
-                                <*> resolveFormula psi
+resolveFormula (Dir d)          = C.Dir <$> resolveDir d
+resolveFormula (Atom i)         = C.Atom <$> resolveName i
+resolveFormula (Neg phi)        = C.negFormula <$> resolveFormula phi
+resolveFormula (Conj phi _ psi) =
+    C.andFormula <$> resolveFormula phi <*> resolveFormula psi
+resolveFormula (Disj phi psi)   =
+    C.orFormula <$> resolveFormula phi <*> resolveFormula psi
 
 resolveBranch :: Branch -> Resolver CTT.Branch
 resolveBranch (OBranch (AIdent (_,lbl)) args e) = do
@@ -296,13 +288,18 @@ resolveDecl d = case d of
     brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs)
     body <- lams tele' (return $ CTT.Split f loc ty brs')
     return ((f,(a,body)),[(f,Variable)])
+  DeclUndef (AIdent (l,f)) tele t -> do
+    let tele' = flattenTele tele
+    a <- binds CTT.Pi tele' (resolveExp t)
+    d <- CTT.Undef <$> getLoc l <*> pure a
+    return ((f,(a,d)),[(f,Variable)])
 
 resolveDecls :: [Decl] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)])
 resolveDecls []     = return ([],[])
 resolveDecls (d:ds) = do
-    (rtd,names)  <- resolveDecl d
-    (rds,names') <- local (insertIdents names) $ resolveDecls ds
-    return ([rtd] : rds, names' ++ names)
+  (rtd,names)  <- resolveDecl d
+  (rds,names') <- local (insertIdents names) $ resolveDecls ds
+  return ([rtd] : rds, names' ++ names)
 
 resolveModule :: Module -> Resolver ([[CTT.Decl]],[(Ident,SymKind)])
 resolveModule (Module (AIdent (_,n)) _ decls) =

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 25bedd1dfc65698a89b4d266017d49cc39c05ea0..588d22ea048bf58302941a9a9762aa1c74bf1811 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -179,7 +179,6 @@ check a t = case (a,t) of
   (_,Where e d) -> do\r
     checkDecls d\r
     local (addDecls d) $ check a e\r
-  (_,Undef _) -> return ()\r
   (VU,IdP a e0 e1) -> do\r
     (a0,a1) <- checkPath (constPath VU) a\r
     check a0 e0\r
@@ -354,8 +353,9 @@ checks _              _      = throwError "checks"
 -- infer the type of e\r
 infer :: Ter -> Typing Val\r
 infer e = case e of\r
-  U     -> return VU  -- U : U\r
-  Var n -> lookType n <$> asks env\r
+  U         -> return VU  -- U : U\r
+  Var n     -> lookType n <$> asks env\r
+  Undef _ t -> evalTyping t\r
   App t u -> do\r
     c <- infer t\r
     case c of\r

diff --git a/examples/integer.ctt b/examples/integer.ctt
index da9b4b31277f27d96423e3219b5ca00c647dabe0..58e8d99f5b0afa276a88e6a212ef9306fc07aeca 100644 (file)
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -59,8 +59,7 @@ fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split
     where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split
       zero -> zeroP'
       suc n -> refl int (neg (suc n))
-  zeroP @ i -> temp
-    where temp : Id int (pos zero) (zeroP{int} @ i) = undefined
+  zeroP @ i -> sq @ i
 
 isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK