Add very simple support for holes

diff --git a/CTT.hs b/CTT.hs
index fb8d42e7e6507a60f373f30bbd78e47bf0363fc5..b8c462e9656ce31e160b33594abb2a34561e4175 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -94,8 +94,10 @@ data Ter = App Ter Ter
          | Split Ident Loc Ter [Branch]
            -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors)
          | Sum Loc Ident [Label]
-           -- undefined
+
+           -- undefined and holes
          | Undef Loc Ter -- Location and type
+         | Hole
 
            -- Id type
          | IdP Ter Ter Ter
@@ -313,6 +315,7 @@ showTer v = case v of
   Split f _ _ _      -> text f
   Sum _ n _          -> text n
   Undef _ _          -> text "undefined"
+  Hole               -> text "?"
   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
@@ -333,7 +336,9 @@ showTer1 :: Ter -> Doc
 showTer1 t = case t of
   U        -> char 'U'
   Con c [] -> text c
-  Var x    -> text x
+  Var{}    -> showTer t
+  Undef{}  -> showTer t
+  Hole     -> showTer t
   Split{}  -> showTer t
   Sum{}    -> showTer t
   _        -> parens (showTer t)
@@ -380,6 +385,7 @@ 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/Exp.cf b/Exp.cf
index 4c8d347265342d53815160ab08c98cd2755341bb..681918eba50f932b5254052295b90449c4bd88c6 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -43,6 +43,7 @@ Pair.       Exp5 ::= "(" Exp "," [Exp] ")" ;
 Var.        Exp5 ::= AIdent ;
 PCon.       Exp5 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi
 U.          Exp5 ::= "U" ;
+Hole.       Exp5 ::= "?" ;
 coercions Exp 5 ;
 separator nonempty Exp "," ;
 

diff --git a/Resolver.hs b/Resolver.hs
index 2492949bddedca928bd96ad414056e7d17f7a171..c789f67b4aa17cf0c76f8fcb19559505a55356f3 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -165,6 +165,7 @@ resolveApps x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs
 resolveExp :: Exp -> Resolver Ter
 resolveExp e = case e of
   U             -> return CTT.U
+  Hole          -> return CTT.Hole
   Var x         -> resolveVar x
   App t s       -> resolveApps x xs
     where (x,xs) = unApps t [s]

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 588d22ea048bf58302941a9a9762aa1c74bf1811..39e920be1eb777f3cb727f1ec42d6f9044749580 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -187,7 +187,8 @@ check a t = case (a,t) of
     (u0,u1) <- checkPath p t\r
     k <- asks index\r
     unless (conv k a0 u0 && conv k a1 u1) $\r
-      throwError $ "path endpoints don't match " ++ show e\r
+      throwError $ "path endpoints don't match for " ++ show e ++ ", got " ++\r
+                   show (u0,u1) ++ ", but expected " ++ show (a0,a1)\r
   (VU,Glue a ts) -> do\r
     check VU a\r
     rho <- asks env\r
@@ -196,6 +197,9 @@ check a t = case (a,t) of
     check va u\r
     vu <- evalTyping u\r
     checkGlueElem vu ts us\r
+  (_,Hole) -> do\r
+    trace $ "Hole expects: " ++ show a\r
+    return ()\r
   _ -> do\r
     v <- infer t\r
     unlessM (v === a) $\r