git.iko.soy/Idris-dev
on master help sign in
Major improvement to pretty printing of proof states, especially when the goal is a large term.
c824099Dominic Mulligan
src/Core/TT.hs+4−1
compare with master
unifiedsplit
@@ -269,6 +269,9 @@ instance Sized Raw where
269 size (RForce raw) = 1 + size raw
269 size (RForce raw) = 1 + size raw
270 size (RConstant const) = size const
270 size (RConstant const) = size const
271
271
272+instance Pretty Raw where
273+ pretty = text . show
274+
272{-!
275{-!
273deriving instance Binary Raw
276deriving instance Binary Raw
274!-}
277!-}
@@ -410,7 +413,7 @@ instance Sized a => Sized (TT a) where
410 size (Set u) = 1 + size u
413 size (Set u) = 1 + size u
411
414
412instance Pretty a => Pretty (TT a) where
415instance Pretty a => Pretty (TT a) where
413− pretty
416+ pretty _ = text "test"
414
417
415type EnvTT n = [(n, Binder (TT n))]
418type EnvTT n = [(n, Binder (TT n))]
416
419
src/Idris/AbsSyntax.hs+183
@@ -751,6 +751,9 @@ expandNS syn n = case syn_namespace syn of
751instance Show PTerm where
751instance Show PTerm where
752 show tm = showImp False tm
752 show tm = showImp False tm
753
753
754+instance Pretty PTerm where
755+ pretty = prettyImp False
756+
754instance Show PDecl where
757instance Show PDecl where
755 show d = showDeclImp False d
758 show d = showDeclImp False d
756
759
@@ -804,6 +807,186 @@ getConsts (_ : xs) = getConsts xs
804getAll :: [PArg] -> [PTerm]
807getAll :: [PArg] -> [PTerm]
805getAll = map getTm
808getAll = map getTm
806
809
810+prettyImp :: Bool -> PTerm -> Doc
811+prettyImp impl = prettySe 10
812+ where
813+ prettySe p (PQuote r) =
814+ if size r > breakingSize then
815+ text "![" $$ pretty r <> text "]"
816+ else
817+ text "![" <> pretty r <> text "]"
818+ prettySe p (PRef fc n) =
819+ if impl then
820+ pretty n
821+ else
822+ prettyBasic n
823+ where
824+ prettyBasic n@(UN _) = pretty n
825+ prettyBasic (MN _ s) = text s
826+ prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
827+ prettySe p (PLam n ty sc) =
828+ bracket p 2 $
829+ if size sc > breakingSize then
830+ text "λ" <> pretty n <+> text "=>" $+$ pretty sc
831+ else
832+ text "λ" <> pretty n <+> text "=>" <+> pretty sc
833+ prettySe p (PLet n ty v sc) =
834+ bracket p 2 $
835+ if size sc > breakingSize then
836+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
837+ nest nestingSize (prettySe 10 sc)
838+ else
839+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
840+ prettySe 10 sc
841+ prettySe p (PPi (Exp l s) n ty sc)
842+ | n `elem` allNamesIn sc || impl =
843+ let open = if l then text "|" <> lparen else lparen in
844+ bracket p 2 $
845+ if size sc > breakingSize then
846+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
847+ st <+> text "->" $+$ prettySe 10 sc
848+ else
849+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
850+ st <+> text "->" <+> prettySe 10 sc
851+ | otherwise =
852+ bracket p 2 $
853+ if size sc > breakingSize then
854+ prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
855+ else
856+ prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
857+ where
858+ st =
859+ case s of
860+ Static -> text "[static]"
861+ _ -> empty
862+ prettySe p (PPi (Imp l s) n ty sc)
863+ | impl =
864+ let open = if l then text "|" <> lbrace else lbrace in
865+ bracket p 2 $
866+ if size sc > breakingSize then
867+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
868+ st <+> text "->" <+> prettySe 10 sc
869+ else
870+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
871+ st <+> text "->" <+> prettySe 10 sc
872+ | otherwise = prettySe 10 sc
873+ where
874+ st =
875+ case s of
876+ Static -> text $ "[static]"
877+ _ -> empty
878+ prettySe p (PPi (Constraint _ _) n ty sc) =
879+ bracket p 2 $
880+ if size sc > breakingSize then
881+ prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
882+ else
883+ prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
884+ prettySe p (PPi (TacImp _ _ s) n ty sc) =
885+ bracket p 2 $
886+ if size sc > breakingSize then
887+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
888+ rbrace <+> text "->" $+$ prettySe 10 sc
889+ else
890+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
891+ rbrace <+> text "->" <+> prettySe 10 sc
892+ prettySe p (PApp _ (PRef _ f) [])
893+ | not impl = pretty f
894+ prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
895+ | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
896+ let [l, r] = getExps args in
897+ bracket p 1 $
898+ if size r > breakingSize then
899+ prettySe 1 l <+> pretty op $+$ prettySe 0 r
900+ else
901+ prettySe 1 l <+> pretty op <+> prettySe 0 r
902+ prettySe p (PApp _ f as) =
903+ let args = getExps as in
904+ bracket p 1 $
905+ prettySe 1 f <+>
906+ if impl then
907+ foldl fS empty as
908+ -- foldr (<+>) empty $ map prettyArgS as
909+ else
910+ foldl fSe empty args
911+ -- foldr (<+>) empty $ map prettyArgSe args
912+ where
913+ fS l r =
914+ if size r > breakingSize then
915+ l $+$ prettyArgS r
916+ else
917+ l <+> prettyArgS r
918+
919+ fSe l r =
920+ if size r > breakingSize then
921+ l $+$ prettyArgSe r
922+ else
923+ l <+> prettyArgSe r
924+ prettySe p (PCase _ scr opts) =
925+ text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
926+ where
927+ prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
928+
929+ sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
930+ prettySe p (PHidden tm) = text "." <> prettySe 0 tm
931+ prettySe p (PRefl _) = text "refl"
932+ prettySe p (PResolveTC _) = text "resolvetc"
933+ prettySe p (PTrue _) = text "()"
934+ prettySe p (PFalse _) = text "_|_"
935+ prettySe p (PEq _ l r) =
936+ bracket p 2 $
937+ if size r > breakingSize then
938+ prettySe 10 l <+> text "=" $+$ prettySe 10 r
939+ else
940+ hang (prettySe 10 l <+> text "=") nestingSize $ prettySe 10 r
941+ prettySe p (PTyped l r) =
942+ lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
943+ prettySe p (PPair _ l r) =
944+ if size r > breakingSize then
945+ lparen <> prettySe 10 l <> text "," $+$
946+ prettySe 10 r <> rparen
947+ else
948+ lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
949+ prettySe p (PDPair _ l t r) =
950+ if size r > breakingSize then
951+ lparen <> prettySe 10 l <+> text "**" $+$
952+ prettySe 10 r <> rparen
953+ else
954+ lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
955+ prettySe p (PAlternative as) =
956+ lparen <> text "|" <> prettyAs <> text "|" <> rparen
957+ where
958+ prettyAs =
959+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
960+ prettySe p PSet = text "Set"
961+ prettySe p (PConstant c) = pretty c
962+ -- XXX: add pretty for tactics
963+ prettySe p (PProof ts) =
964+ text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
965+ prettySe p (PTactics ts) =
966+ text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
967+ prettySe p (PMetavar n) = text "?" <> pretty n
968+ prettySe p (PReturn f) = text "return"
969+ prettySe p PImpossible = text "impossible"
970+ prettySe p Placeholder = text "_"
971+ prettySe p (PDoBlock _) = text "do block pretty not implemented"
972+ prettySe p (PElabError s) = pretty s
973+
974+ prettySe p _ = text "test"
975+
976+ prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
977+ prettyArgS (PExp _ _ tm) = prettyArgSe tm
978+ prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
979+ prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
980+
981+ prettyArgSe arg = prettySe 0 arg
982+ prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
983+ prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
984+ prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
985+
986+ bracket outer inner doc
987+ | inner > outer = lparen <> doc <> rparen
988+ | otherwise = doc
989+
807showImp :: Bool -> PTerm -> String
990showImp :: Bool -> PTerm -> String
808showImp impl tm = se 10 tm where
991showImp impl tm = se 10 tm where
809 se p (PQuote r) = "![" ++ show r ++ "]"
992 se p (PQuote r) = "![" ++ show r ++ "]"
src/Idris/Prover.hs+43−1
@@ -59,7 +59,49 @@ elabStep st e = do case runStateT e st of
59 fail (pshow i a)
59 fail (pshow i a)
60
60
61dumpState :: IState -> ProofState -> IO ()
61dumpState :: IState -> ProofState -> IO ()
62−dumpState _ pst = putStrLn . render . pretty $ pst
62+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) =
63+ putStrLn . render $ pretty nm <> colon <+> text "No more goals."
64+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
65+ let OK ty = goalAtFocus ps
66+ let OK env = envAtFocus ps
67+ putStrLn . render $
68+ prettyOtherGoals hs $$
69+ prettyAssumptions env $$
70+ prettyGoal ty
71+ where
72+ -- XXX
73+ tPretty t = pretty $ delab ist t
74+
75+ prettyPs [] = empty
76+ prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs
77+ prettyPs ((n, Let t v) : bs) =
78+ nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
79+ tPretty t $$ prettyPs bs)
80+ prettyPs ((n, b) : bs) =
81+ pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
82+
83+ prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
84+ prettyG b = tPretty $ binderTy b
85+
86+ prettyGoal ty =
87+ text "----------" <+> text "Metavariable currently in focus" <> colon
88+ <+> pretty nm <+> text "----------" $$
89+ pretty h <> colon $$ nest nestingSize (prettyG ty)
90+
91+ prettyAssumptions env =
92+ if length env == 0 then
93+ empty
94+ else
95+ text "---------- Assumptions: ----------" $$
96+ nest nestingSize (prettyPs $ reverse env)
97+
98+ prettyOtherGoals hs =
99+ if length hs == 0 then
100+ empty
101+ else
102+ text "---------- Other goals: ----------" $$
103+ pretty hs
104+
63
105
64{-
106{-
65dumpState :: IState -> ProofState -> IO ()
107dumpState :: IState -> ProofState -> IO ()
src/Util/Pretty.hs+2−2
@@ -18,7 +18,7 @@ instance Sized a => Sized [a] where
18
18
19-- The maximum size before we break on to another line.
19-- The maximum size before we break on to another line.
20breakingSize :: Int
20breakingSize :: Int
21−breakingSize = 5
21+breakingSize = 14
22
22
23nestingSize :: Int
23nestingSize :: Int
24nestingSize = 2
24nestingSize = 2
@@ -30,4 +30,4 @@ instance Pretty () where
30 pretty () = text "()"
30 pretty () = text "()"
31
31
32instance Pretty a => Pretty [a] where
32instance Pretty a => Pretty [a] where
33− pretty l = foldr (<+>) empty $ map pretty l
33+ pretty l = foldr ($$) empty $ map pretty l