c824099 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Major improvement to pretty printing of proof states, especially when the goal is a large term.

commitc824099565164e2e6932805fa4046353e5621aad authorDominic Mulligan <dominic.p.mulligan@googlemail.com> dateThu 1 Mar 2012, 14:07 (15 years ago) parent8c64e9c

4 files changed+232−4

compare with master

unifiedsplit

src/Core/TT.hs+4−1 src/Idris/AbsSyntax.hs+183 src/Idris/Prover.hs+43−1 src/Util/Pretty.hs+2−2

src/Core/TT.hs+4−1

@@ -269,6 +269,9 @@ instance Sized Raw where

269269 size (RForce raw) = 1 + size raw

270270 size (RConstant const) = size const

271271

272+instance Pretty Raw where

273+ pretty = text . show

274+

272275{-!

273276deriving instance Binary Raw

274277!-}

@@ -410,7 +413,7 @@ instance Sized a => Sized (TT a) where

410413 size (Set u) = 1 + size u

411414

412415instance Pretty a => Pretty (TT a) where

413− pretty

416+ pretty _ = text "test"

414417

415418type EnvTT n = [(n, Binder (TT n))]

416419

src/Idris/AbsSyntax.hs+183

@@ -751,6 +751,9 @@ expandNS syn n = case syn_namespace syn of

751751instance Show PTerm where

752752 show tm = showImp False tm

753753

754+instance Pretty PTerm where

755+ pretty = prettyImp False

756+

754757instance Show PDecl where

755758 show d = showDeclImp False d

756759

@@ -804,6 +807,186 @@ getConsts (_ : xs) = getConsts xs

804807getAll :: [PArg] -> [PTerm]

805808getAll = map getTm

806809

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+

807990showImp :: Bool -> PTerm -> String

808991showImp impl tm = se 10 tm where

809992 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

5959 fail (pshow i a)

6060

6161dumpState :: 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+

63105

64106{-

65107dumpState :: IState -> ProofState -> IO ()

src/Util/Pretty.hs+2−2

@@ -18,7 +18,7 @@ instance Sized a => Sized [a] where

1818

1919-- The maximum size before we break on to another line.

2020breakingSize :: Int

21−breakingSize = 5

21+breakingSize = 14

2222

2323nestingSize :: Int

2424nestingSize = 2

@@ -30,4 +30,4 @@ instance Pretty () where

3030 pretty () = text "()"

3131

3232instance Pretty a => Pretty [a] where

33− pretty l = foldr (<+>) empty $ map pretty l

33+ pretty l = foldr ($$) empty $ map pretty l