From: Anders Mörtberg <mortberg@chalmers.se>
Date: Wed, 15 Apr 2015 08:14:27 +0000 (+0200)
Subject: Add very simple support for holes
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=15f1f1d9667a3bb420b0dbefdcef006ec6715bc2;p=cubicaltt.git

Add very simple support for holes
---

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