From 0fdc3053965c91263800b51724bc977b63a4ea71 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 16 Apr 2015 11:16:03 +0200 Subject: [PATCH] Make holes print the context --- CTT.hs | 19 ++++++++++++++----- Eval.hs | 4 ++++ Exp.cf | 8 +++++--- Resolver.hs | 2 +- TypeChecker.hs | 9 +++++---- 5 files changed, 29 insertions(+), 13 deletions(-) diff --git a/CTT.hs b/CTT.hs index ee1f020..2ddb021 100644 --- 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 2629d0b..9c8fcfd 100644 --- 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 681918e..79dd771 100644 --- 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 c789f67..79d4529 100644 --- 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 4d85f3b..9728f47 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -144,6 +144,11 @@ evalTyping t = eval <$> asks env <*> pure t check :: Val -> Ter -> Typing () check a t = case (a,t) of (_,Undef{}) -> return () + (_,Hole l) -> do + rho <- asks env + let e = unlines (reverse (contextOfEnv rho)) + trace $ "\nHole at " ++ show l ++ ":\n\n" ++ + e ++ replicate 80 '-' ++ "\n" ++ show a ++ "\n" (_,Con c es) -> do (bs,nu) <- getLblType c a checks (bs,nu) es @@ -198,9 +203,6 @@ 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) $ @@ -361,7 +363,6 @@ infer :: Ter -> Typing Val infer e = case e of U -> return VU -- U : U Var n -> lookType n <$> asks env --- Undef _ t -> evalTyping t App t u -> do c <- infer t case c of -- 2.34.1