Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Major improvement to pretty printing of proof states, especially when…

… the goal is a large term.
  • Loading branch information...
commit c824099565164e2e6932805fa4046353e5621aad 1 parent 8c64e9c
@dpmulligan authored
View
5 src/Core/TT.hs
@@ -269,6 +269,9 @@ instance Sized Raw where
size (RForce raw) = 1 + size raw
size (RConstant const) = size const
+instance Pretty Raw where
+ pretty = text . show
+
{-!
deriving instance Binary Raw
!-}
@@ -410,7 +413,7 @@ instance Sized a => Sized (TT a) where
size (Set u) = 1 + size u
instance Pretty a => Pretty (TT a) where
- pretty
+ pretty _ = text "test"
type EnvTT n = [(n, Binder (TT n))]
View
183 src/Idris/AbsSyntax.hs
@@ -751,6 +751,9 @@ expandNS syn n = case syn_namespace syn of
instance Show PTerm where
show tm = showImp False tm
+instance Pretty PTerm where
+ pretty = prettyImp False
+
instance Show PDecl where
show d = showDeclImp False d
@@ -804,6 +807,186 @@ getConsts (_ : xs) = getConsts xs
getAll :: [PArg] -> [PTerm]
getAll = map getTm
+prettyImp :: Bool -> PTerm -> Doc
+prettyImp impl = prettySe 10
+ where
+ prettySe p (PQuote r) =
+ if size r > breakingSize then
+ text "![" $$ pretty r <> text "]"
+ else
+ text "![" <> pretty r <> text "]"
+ prettySe p (PRef fc n) =
+ if impl then
+ pretty n
+ else
+ prettyBasic n
+ where
+ prettyBasic n@(UN _) = pretty n
+ prettyBasic (MN _ s) = text s
+ prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
+ prettySe p (PLam n ty sc) =
+ bracket p 2 $
+ if size sc > breakingSize then
+ text "λ" <> pretty n <+> text "=>" $+$ pretty sc
+ else
+ text "λ" <> pretty n <+> text "=>" <+> pretty sc
+ prettySe p (PLet n ty v sc) =
+ bracket p 2 $
+ if size sc > breakingSize then
+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
+ nest nestingSize (prettySe 10 sc)
+ else
+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
+ prettySe 10 sc
+ prettySe p (PPi (Exp l s) n ty sc)
+ | n `elem` allNamesIn sc || impl =
+ let open = if l then text "|" <> lparen else lparen in
+ bracket p 2 $
+ if size sc > breakingSize then
+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
+ st <+> text "->" $+$ prettySe 10 sc
+ else
+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
+ st <+> text "->" <+> prettySe 10 sc
+ | otherwise =
+ bracket p 2 $
+ if size sc > breakingSize then
+ prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
+ else
+ prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
+ where
+ st =
+ case s of
+ Static -> text "[static]"
+ _ -> empty
+ prettySe p (PPi (Imp l s) n ty sc)
+ | impl =
+ let open = if l then text "|" <> lbrace else lbrace in
+ bracket p 2 $
+ if size sc > breakingSize then
+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
+ st <+> text "->" <+> prettySe 10 sc
+ else
+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
+ st <+> text "->" <+> prettySe 10 sc
+ | otherwise = prettySe 10 sc
+ where
+ st =
+ case s of
+ Static -> text $ "[static]"
+ _ -> empty
+ prettySe p (PPi (Constraint _ _) n ty sc) =
+ bracket p 2 $
+ if size sc > breakingSize then
+ prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
+ else
+ prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
+ prettySe p (PPi (TacImp _ _ s) n ty sc) =
+ bracket p 2 $
+ if size sc > breakingSize then
+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
+ rbrace <+> text "->" $+$ prettySe 10 sc
+ else
+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
+ rbrace <+> text "->" <+> prettySe 10 sc
+ prettySe p (PApp _ (PRef _ f) [])
+ | not impl = pretty f
+ prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
+ | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
+ let [l, r] = getExps args in
+ bracket p 1 $
+ if size r > breakingSize then
+ prettySe 1 l <+> pretty op $+$ prettySe 0 r
+ else
+ prettySe 1 l <+> pretty op <+> prettySe 0 r
+ prettySe p (PApp _ f as) =
+ let args = getExps as in
+ bracket p 1 $
+ prettySe 1 f <+>
+ if impl then
+ foldl fS empty as
+ -- foldr (<+>) empty $ map prettyArgS as
+ else
+ foldl fSe empty args
+ -- foldr (<+>) empty $ map prettyArgSe args
+ where
+ fS l r =
+ if size r > breakingSize then
+ l $+$ prettyArgS r
+ else
+ l <+> prettyArgS r
+
+ fSe l r =
+ if size r > breakingSize then
+ l $+$ prettyArgSe r
+ else
+ l <+> prettyArgSe r
+ prettySe p (PCase _ scr opts) =
+ text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
+ where
+ prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
+
+ sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
+ prettySe p (PHidden tm) = text "." <> prettySe 0 tm
+ prettySe p (PRefl _) = text "refl"
+ prettySe p (PResolveTC _) = text "resolvetc"
+ prettySe p (PTrue _) = text "()"
+ prettySe p (PFalse _) = text "_|_"
+ prettySe p (PEq _ l r) =
+ bracket p 2 $
+ if size r > breakingSize then
+ prettySe 10 l <+> text "=" $+$ prettySe 10 r
+ else
+ hang (prettySe 10 l <+> text "=") nestingSize $ prettySe 10 r
+ prettySe p (PTyped l r) =
+ lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
+ prettySe p (PPair _ l r) =
+ if size r > breakingSize then
+ lparen <> prettySe 10 l <> text "," $+$
+ prettySe 10 r <> rparen
+ else
+ lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
+ prettySe p (PDPair _ l t r) =
+ if size r > breakingSize then
+ lparen <> prettySe 10 l <+> text "**" $+$
+ prettySe 10 r <> rparen
+ else
+ lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
+ prettySe p (PAlternative as) =
+ lparen <> text "|" <> prettyAs <> text "|" <> rparen
+ where
+ prettyAs =
+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
+ prettySe p PSet = text "Set"
+ prettySe p (PConstant c) = pretty c
+ -- XXX: add pretty for tactics
+ prettySe p (PProof ts) =
+ text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
+ prettySe p (PTactics ts) =
+ text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
+ prettySe p (PMetavar n) = text "?" <> pretty n
+ prettySe p (PReturn f) = text "return"
+ prettySe p PImpossible = text "impossible"
+ prettySe p Placeholder = text "_"
+ prettySe p (PDoBlock _) = text "do block pretty not implemented"
+ prettySe p (PElabError s) = pretty s
+
+ prettySe p _ = text "test"
+
+ prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
+ prettyArgS (PExp _ _ tm) = prettyArgSe tm
+ prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
+ prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
+
+ prettyArgSe arg = prettySe 0 arg
+ prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
+ prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
+ prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
+
+ bracket outer inner doc
+ | inner > outer = lparen <> doc <> rparen
+ | otherwise = doc
+
showImp :: Bool -> PTerm -> String
showImp impl tm = se 10 tm where
se p (PQuote r) = "![" ++ show r ++ "]"
View
44 src/Idris/Prover.hs
@@ -59,7 +59,49 @@ elabStep st e = do case runStateT e st of
fail (pshow i a)
dumpState :: IState -> ProofState -> IO ()
-dumpState _ pst = putStrLn . render . pretty $ pst
+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) =
+ putStrLn . render $ pretty nm <> colon <+> text "No more goals."
+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
+ let OK ty = goalAtFocus ps
+ let OK env = envAtFocus ps
+ putStrLn . render $
+ prettyOtherGoals hs $$
+ prettyAssumptions env $$
+ prettyGoal ty
+ where
+ -- XXX
+ tPretty t = pretty $ delab ist t
+
+ prettyPs [] = empty
+ prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs
+ prettyPs ((n, Let t v) : bs) =
+ nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
+ tPretty t $$ prettyPs bs)
+ prettyPs ((n, b) : bs) =
+ pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
+
+ prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
+ prettyG b = tPretty $ binderTy b
+
+ prettyGoal ty =
+ text "----------" <+> text "Metavariable currently in focus" <> colon
+ <+> pretty nm <+> text "----------" $$
+ pretty h <> colon $$ nest nestingSize (prettyG ty)
+
+ prettyAssumptions env =
+ if length env == 0 then
+ empty
+ else
+ text "---------- Assumptions: ----------" $$
+ nest nestingSize (prettyPs $ reverse env)
+
+ prettyOtherGoals hs =
+ if length hs == 0 then
+ empty
+ else
+ text "---------- Other goals: ----------" $$
+ pretty hs
+
{-
dumpState :: IState -> ProofState -> IO ()
View
4 src/Util/Pretty.hs
@@ -18,7 +18,7 @@ instance Sized a => Sized [a] where
-- The maximum size before we break on to another line.
breakingSize :: Int
-breakingSize = 5
+breakingSize = 14
nestingSize :: Int
nestingSize = 2
@@ -30,4 +30,4 @@ instance Pretty () where
pretty () = text "()"
instance Pretty a => Pretty [a] where
- pretty l = foldr (<+>) empty $ map pretty l
+ pretty l = foldr ($$) empty $ map pretty l
Please sign in to comment.
Something went wrong with that request. Please try again.