Make holes print the context

diff --git a/CTT.hs b/CTT.hs
index ee1f020590eec484a53a44f6ac98cd3c6313d5ff..2ddb021db5e2afca5ad510e298e3fb80cb4bce26 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -97,7 +97,7 @@ data Ter = App Ter Ter
 
            -- undefined and holes
          | Undef Loc Ter -- Location and type
-         | Hole
+         | Hole Loc
 
            -- Id type
          | IdP Ter Ter Ter
@@ -168,6 +168,7 @@ data Val = VU
 isNeutral :: Val -> Bool
 isNeutral v = case v of
   Ter Undef{} _     -> True
+  Ter Hole{} _      -> True
   VVar _ _          -> True
   VFst v            -> isNeutral v
   VSnd v            -> isNeutral v
@@ -265,6 +266,14 @@ domainEnv rho = case rho of
   Def ts e    -> domainEnv e
   Sub e (i,_) -> i : domainEnv e
 
+-- Extract the context from the environment, used when printing holes
+contextOfEnv :: Env -> [String]
+contextOfEnv rho = case rho of
+  Empty         -> []
+  Upd e (x,v)   -> (x ++ " : " ++ show v) : contextOfEnv e
+  Def ts e      -> contextOfEnv e
+  Sub e (i,phi) -> (show i ++ " = " ++ show phi) : contextOfEnv e
+
 --------------------------------------------------------------------------------
 -- | Pretty printing
 
@@ -284,7 +293,7 @@ instance Show Loc where
   show = render . showLoc
 
 showLoc :: Loc -> Doc
-showLoc (Loc name (i,j)) = hcat [text name,text "_L",int i,text "_C",int j]
+showLoc (Loc name (i,j)) = text (show (i,j) ++ " in " ++ name)
 
 showFormula :: Formula -> Doc
 showFormula phi = case phi of
@@ -313,8 +322,8 @@ showTer v = case v of
                           showTers es <+> showFormula phi
   Split f _ _ _      -> text f
   Sum _ n _          -> text n
-  Undef _ _          -> text "undefined"
-  Hole               -> text "?"
+  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
@@ -337,7 +346,7 @@ showTer1 t = case t of
   Con c [] -> text c
   Var{}    -> showTer t
   Undef{}  -> showTer t
-  Hole     -> showTer t
+  Hole{}   -> showTer t
   Split{}  -> showTer t
   Sum{}    -> showTer t
   _        -> parens (showTer t)

diff --git a/Eval.hs b/Eval.hs
index 2629d0beda9bb0e926d17407715d34262fdd2ec2..9c8fcfd7080599e3aa8f201f5a28c41f8c1bcda3 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -260,6 +260,7 @@ inferType v = case v of
 
 (@@) :: ToFormula a => Val -> a -> Val
 (VPath i u) @@ phi = u `act` (i,toFormula phi)
+v@(Ter Hole{} _) @@ phi = VAppFormula v (toFormula phi)
 v @@ phi | isNeutral v = case (inferType v,toFormula phi) of
   (VIdP  _ a0 _,Dir 0) -> a0
   (VIdP  _ _ a1,Dir 1) -> a1
@@ -700,6 +701,9 @@ instance Convertible Val where
       (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 Hole{} e,Ter Hole{} e') -> conv k e e'
+      (Ter Hole{} e,_) -> True
+      (_,Ter Hole{} e') -> True
       (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 681918eba50f932b5254052295b90449c4bd88c6..79dd771ded8834204365637270bfe10683cf54b9 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -43,7 +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 ::= "?" ;
+Hole.       Exp5 ::= HoleIdent ;
 coercions Exp 5 ;
 separator nonempty Exp "," ;
 
@@ -84,7 +84,9 @@ terminator Tele "" ;
 PTele.    PTele ::= "(" Exp ":" Exp ")" ;
 terminator nonempty PTele "" ;
 
-position token AIdent (letter|'_')(letter|digit|'\''|'_')* ;
+position token AIdent (letter|'_')(letter|digit|'\'')* ;
 separator AIdent "" ;
 
-token CIdent '/''\\' ;
\ No newline at end of file
+token CIdent '/''\\' ;
+
+position token HoleIdent '?' ;
\ No newline at end of file

diff --git a/Resolver.hs b/Resolver.hs
index c789f67b4aa17cf0c76f8fcb19559505a55356f3..79d4529a8d87f187f74a8d90eccaca7239a82dc0 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -165,7 +165,6 @@ 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]
@@ -189,6 +188,7 @@ resolveExp e = case e of
     (rdecls,names) <- resolveDecls decls
     CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e)
   Path is e     -> paths is (resolveExp e)
+  Hole (HoleIdent (l,_)) -> CTT.Hole <$> getLoc l
   AppFormula e phi ->
     let (x,xs) = unApps e []
     in case x of

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 4d85f3b7141249e2dc8d90562c82c541f1af1610..9728f4731170c6bbc22d57015c6191214765470f 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -144,6 +144,11 @@ evalTyping t = eval <$> asks env <*> pure t
 check :: Val -> Ter -> Typing ()\r
 check a t = case (a,t) of\r
   (_,Undef{}) -> return ()\r
+  (_,Hole l)  -> do\r
+      rho <- asks env\r
+      let e = unlines (reverse (contextOfEnv rho))\r
+      trace $ "\nHole at " ++ show l ++ ":\n\n" ++\r
+              e ++ replicate 80 '-' ++ "\n" ++ show a ++ "\n"\r
   (_,Con c es) -> do\r
     (bs,nu) <- getLblType c a\r
     checks (bs,nu) es\r
@@ -198,9 +203,6 @@ 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
@@ -361,7 +363,6 @@ infer :: Ter -> Typing Val
 infer e = case e of\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