git.iko.soy/Idris-dev
on master help sign in
Merge pull request #17 from dpmulligan/master

Improved pretty printing support for proof states

commit8d4a93bb2e6af4072c0c2c5a516a8b07eb5c1983 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 5 Mar 2012, 02:47 (15 years ago) parentdca8f9f5602ea7
9 files changed+589−27
compare with master
unifiedsplit
idris.cabal+1−1 lib/prelude/heap.idr+26 src/Core/Elaborate.hs+3 src/Core/ProofShell.hs+3−1 src/Core/ProofState.hs+42−1 src/Core/TT.hs+155 src/Idris/AbsSyntax.hs+283−1 src/Idris/Prover.hs+43−23 src/Util/Pretty.hs+33
idris.cabal+1−1
@@ -67,7 +67,7 @@ Executable idris
6767
6868 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,
6969 containers, process, transformers, filepath, directory,
70− binary, bytestring, epic>=0.9.3
70+ binary, bytestring, epic>=0.9.3, pretty
7171
7272 Extensions: MultiParamTypeClasses, FunctionalDependencies,
7373 FlexibleInstances, TemplateHaskell
lib/prelude/heap.idr+26
@@ -30,6 +30,15 @@ total size : MaxiphobicHeap a -> Nat
3030size Empty = O
3131size (Node s l e r) = s
3232
33+isValidHeap : Ord a => MaxiphobicHeap a -> Bool
34+isValidHeap Empty = True
35+isValidHeap (Node s l e r) =
36+ dominates e l && dominates e r && s == S (size l + size r)
37+ where
38+ dominates : Ord a => a -> MaxiphobicHeap a -> Bool
39+ dominates e Empty = True
40+ dominates e (Node s l e' r) = e' <= e
41+
3342--------------------------------------------------------------------------------
3443-- Basic heaps
3544--------------------------------------------------------------------------------
@@ -141,6 +150,23 @@ total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h =
141150isEmptySizeZero Empty p = refl
142151isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
143152
153+total emptyHeapValid : Ord a => isValidHeap empty = True
154+emptyHeapValid = refl
155+
156+total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
157+singletonHeapValid e = refl
158+
159+{-
160+total mergePreservesValidHeaps : Ord a => (left : MaxiphobicHeap a) ->
161+ (right : MaxiphobicHeap a) -> (leftValid : isValidHeap left = True) ->
162+ (rightValid : isValidHeap right = True) -> isValidHeap $ merge left right = True
163+mergePreservesValidHeaps Empty Empty lp rp = refl
164+mergePreservesValidHeaps Empty (Node rs rl re rr) lp rp = rp
165+mergePreservesValidHeaps (Node ls ll le lr) Empty lp rp = lp
166+mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =
167+ ?mergePreservesValidHeapsBody
168+-}
169+
144170--------------------------------------------------------------------------------
145171-- Proofs
146172--------------------------------------------------------------------------------
src/Core/Elaborate.hs+3
@@ -21,6 +21,8 @@ import Data.Char
2121import Data.List
2222import Debug.Trace
2323
24+import Util.Pretty
25+
2426-- I don't really want this here, but it's useful for the test shell
2527data Command = Theorem Name Raw
2628 | Eval Raw
@@ -30,6 +32,7 @@ data Command = Theorem Name Raw
3032
3133data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
3234 deriving Show
35+
3336type Elab' aux a = StateT (ElabState aux) TC a
3437type Elab a = Elab' () a
3538
src/Core/ProofShell.hs+3−1
@@ -11,6 +11,8 @@ import Core.Elaborate
1111import Control.Monad.State
1212import System.Console.Haskeline
1313
14+import Util.Pretty
15+
1416data ShellState = ShellState
1517 { ctxt :: Context,
1618 prf :: Maybe ProofState,
@@ -56,7 +58,7 @@ processCommand (Tac e) state
5658runShell :: ShellState -> InputT IO ShellState
5759runShell st = do (prompt, parser) <-
5860 maybe (return ("TT# ", parseCommand))
59− (\st -> do outputStrLn (show st)
61+ (\st -> do outputStrLn . render . pretty $ st
6062 return (show (thname st) ++ "# ", parseTactic))
6163 (prf st)
6264 x <- getInputLine prompt
src/Core/ProofState.hs+42−1
@@ -13,10 +13,12 @@ import Core.TT
1313import Core.Unify
1414
1515import Control.Monad.State
16−import Control.Applicative
16+import Control.Applicative hiding (empty)
1717import Data.List
1818import Debug.Trace
1919
20+import Util.Pretty
21+
2022data ProofState = PS { thname :: Name,
2123 holes :: [Name], -- holes still to be solved
2224 nextname :: Int, -- name supply
@@ -94,6 +96,45 @@ instance Show ProofState where
9496 " =?= " ++ showEnv ps v
9597 showG ps b = showEnv ps (binderTy b)
9698
99+instance Pretty ProofState where
100+ pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _) =
101+ if size nm > breakingSize then
102+ pretty nm <> colon $$ nest nestingSize (text " no more goals.")
103+ else
104+ pretty nm <> colon <+> text " no more goals."
105+ pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _) =
106+ let OK g = goal (Just h) tm in
107+ let wkEnv = premises g in
108+ text "Other goals" <+> colon <+> pretty hs $$
109+ prettyPs wkEnv (reverse wkEnv) $$
110+ text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
111+ pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
112+ where
113+ prettyGoal ps (Guess t v) =
114+ if size v > breakingSize then
115+ prettyEnv ps t <+> text "=?=" $$
116+ nest nestingSize (prettyEnv ps v)
117+ else
118+ prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
119+ prettyGoal ps b = prettyEnv ps $ binderTy b
120+
121+ prettyPs env [] = empty
122+ prettyPs env ((n, Let t v):bs) =
123+ nest nestingSize (pretty n <+> colon <+>
124+ if size v > breakingSize then
125+ prettyEnv env t <+> text "=" $$
126+ nest nestingSize (prettyEnv env v) $$
127+ nest nestingSize (prettyPs env bs)
128+ else
129+ prettyEnv env t <+> text "=" <+> prettyEnv env v $$
130+ nest nestingSize (prettyPs env bs))
131+ prettyPs env ((n, b):bs) =
132+ if size (binderTy b) > breakingSize then
133+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
134+ else
135+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
136+ nest nestingSize (prettyPs env bs))
137+
97138same Nothing n = True
98139same (Just x) n = x == n
99140
src/Core/TT.hs+155
@@ -10,6 +10,8 @@ import Data.List
1010import qualified Data.Binary as B
1111import Data.Binary hiding (get, put)
1212
13+import Util.Pretty hiding (Str)
14+
1315{- The language has:
1416 * Full dependent types
1517 * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...
@@ -34,6 +36,9 @@ data FC = FC { fc_fname :: String,
3436deriving instance Binary FC
3537!-}
3638
39+instance Sized FC where
40+ size (FC f l) = 1 + length f
41+
3742instance Show FC where
3843 show (FC f l) = f ++ ":" ++ show l
3944
@@ -48,6 +53,17 @@ data Err = Msg String
4853 | At FC Err
4954 deriving Eq
5055
56+instance Sized Err where
57+ size (Msg msg) = length msg
58+ size (CantUnify left right err score) = size left + size right + size err
59+ size (NoSuchVariable name) = size name
60+ size (NotInjective l c r) = size l + size c + size r
61+ size (CantResolve trm) = size trm
62+ size (IncompleteTerm trm) = size trm
63+ size UniverseError = 1
64+ size ProgramLineComment = 1
65+ size (At fc err) = size fc + size err
66+
5167score :: Err -> Int
5268score (CantUnify _ _ m s) = s + score m
5369score (CantResolve _) = 20
@@ -60,10 +76,30 @@ instance Show Err where
6076 ++ show e ++ " " ++ show i
6177 show _ = "Error"
6278
79+instance Pretty Err where
80+ pretty (Msg m) = text m
81+ pretty (CantUnify l r e i) =
82+ if size l + size r > breakingSize then
83+ text "Cannot unify" <+> colon $$
84+ nest nestingSize (pretty l <+> text "and" <+> pretty r) $$
85+ nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
86+ else
87+ text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$
88+ nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
89+ pretty _ = text "Error"
90+
6391data TC a = OK a
6492 | Error Err
6593 deriving (Eq, Functor)
6694
95+instance Pretty a => Pretty (TC a) where
96+ pretty (OK ok) = pretty ok
97+ pretty (Error err) =
98+ if size err > breakingSize then
99+ text "Error" <+> colon $$ (nest nestingSize $ pretty err)
100+ else
101+ text "Error" <+> colon <+> pretty err
102+
67103instance Show a => Show (TC a) where
68104 show (OK x) = show x
69105 show (Error str) = "Error: " ++ show str
@@ -118,6 +154,16 @@ data Name = UN String
118154deriving instance Binary Name
119155!-}
120156
157+instance Sized Name where
158+ size (UN n) = 1
159+ size (NS n els) = 1 + length els
160+ size (MN i n) = 1
161+
162+instance Pretty Name where
163+ pretty (UN n) = text n
164+ pretty (NS n s) = pretty n
165+ pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace
166+
121167instance Show Name where
122168 show (UN n) = n
123169 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n
@@ -190,6 +236,23 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
190236deriving instance Binary Const
191237!-}
192238
239+instance Sized Const where
240+ size _ = 1
241+
242+instance Pretty Const where
243+ pretty (I i) = text . show $ i
244+ pretty (BI i) = text . show $ i
245+ pretty (Fl f) = text . show $ f
246+ pretty (Ch c) = text . show $ c
247+ pretty (Str s) = text s
248+ pretty IType = text "Int"
249+ pretty BIType = text "BigInt"
250+ pretty FlType = text "Float"
251+ pretty ChType = text "Char"
252+ pretty StrType = text "String"
253+ pretty PtrType = text "Ptr"
254+ pretty Forgot = text "Forgot"
255+
193256data Raw = Var Name
194257 | RBind Name (Binder Raw) Raw
195258 | RApp Raw Raw
@@ -197,6 +260,18 @@ data Raw = Var Name
197260 | RForce Raw
198261 | RConstant Const
199262 deriving (Show, Eq)
263+
264+instance Sized Raw where
265+ size (Var name) = 1
266+ size (RBind name bind right) = 1 + size bind + size right
267+ size (RApp left right) = 1 + size left + size right
268+ size RSet = 1
269+ size (RForce raw) = 1 + size raw
270+ size (RConstant const) = size const
271+
272+instance Pretty Raw where
273+ pretty = text . show
274+
200275{-!
201276deriving instance Binary Raw
202277!-}
@@ -218,6 +293,17 @@ data Binder b = Lam { binderTy :: b }
218293deriving instance Binary Binder
219294!-}
220295
296+instance Sized a => Sized (Binder a) where
297+ size (Lam ty) = 1 + size ty
298+ size (Pi ty) = 1 + size ty
299+ size (Let ty val) = 1 + size ty + size val
300+ size (NLet ty val) = 1 + size ty + size val
301+ size (Hole ty) = 1 + size ty
302+ size (GHole ty) = 1 + size ty
303+ size (Guess ty val) = 1 + size ty + size val
304+ size (PVar ty) = 1 + size ty
305+ size (PVTy ty) = 1 + size ty
306+
221307fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
222308fmapMB f (Let t v) = liftM2 Let (f t) (f v)
223309fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)
@@ -259,6 +345,9 @@ data UExp = UVar Int -- universe variable
259345 | UVal Int -- explicit universe level
260346 deriving (Eq, Ord)
261347
348+instance Sized UExp where
349+ size _ = 1
350+
262351-- We assume that universe levels have been checked, so anything external
263352-- can just have the same universe variable and we won't get any new
264353-- cycles.
@@ -289,6 +378,12 @@ data NameType = Bound | Ref | DCon Int Int | TCon Int Int
289378deriving instance Binary NameType
290379!-}
291380
381+instance Sized NameType where
382+ size _ = 1
383+
384+instance Pretty NameType where
385+ pretty = text . show
386+
292387instance Eq NameType where
293388 Bound == Bound = True
294389 Ref == Ref = True
@@ -308,6 +403,18 @@ data TT n = P NameType n (TT n) -- embed type
308403deriving instance Binary TT
309404!-}
310405
406+instance Sized a => Sized (TT a) where
407+ size (P name n trm) = 1 + size name + size n + size trm
408+ size (V v) = 1
409+ size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
410+ size (App l r) = 1 + size l + size r
411+ size (Constant c) = size c
412+ size Erased = 1
413+ size (Set u) = 1 + size u
414+
415+instance Pretty a => Pretty (TT a) where
416+ pretty _ = text "test"
417+
311418type EnvTT n = [(n, Binder (TT n))]
312419
313420data Datatype n = Data { d_typename :: n,
@@ -496,6 +603,54 @@ instance Show Const where
496603showEnv env t = showEnv' env t False
497604showEnvDbg env t = showEnv' env t True
498605
606+prettyEnv env t = prettyEnv' env t False
607+ where
608+ prettyEnv' env t dbg = prettySe 10 env t dbg
609+
610+ bracket outer inner p
611+ | inner > outer = lparen <> p <> rparen
612+ | otherwise = p
613+
614+ prettySe p env (P nt n t) debug =
615+ pretty n <+>
616+ if debug then
617+ lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack
618+ else
619+ empty
620+ prettySe p env (V i) debug
621+ | i < length env =
622+ if debug then
623+ text . show . fst $ env!!i
624+ else
625+ lbrack <+> text (show i) <+> rbrack
626+ | otherwise = text "unbound" <+> text (show i) <+> text "!"
627+ prettySe p env (Bind n b@(Pi t) sc) debug
628+ | noOccurrence n sc && not debug =
629+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
630+ prettySe p env (Bind n b sc) debug =
631+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
632+ prettySe p env (App f a) debug =
633+ bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
634+ prettySe p env (Constant c) debug = pretty c
635+ prettySe p env Erased debug = text "[_]"
636+ prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)
637+
638+ prettySb env n (Lam t) = prettyB env "λ" "=>" n t
639+ prettySb env n (Hole t) = prettyB env "?defer" "." n t
640+ prettySb env n (Pi t) = prettyB env "(" ") ->" n t
641+ prettySb env n (PVar t) = prettyB env "pat" "." n t
642+ prettySb env n (PVTy t) = prettyB env "pty" "." n t
643+ prettySb env n (Let t v) = prettyBv env "let" "in" n t v
644+ prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
645+
646+ prettyB env op sc n t debug =
647+ text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
648+
649+ prettyBv env op sc n t v debug =
650+ text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
651+ prettySe 10 env v debug <> text sc
652+
653+
499654showEnv' env t dbg = se 10 env t where
500655 se p env (P nt n t) = show n
501656 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
src/Idris/AbsSyntax.hs+283−1
@@ -5,18 +5,23 @@ module Idris.AbsSyntax where
55
66import Core.TT
77import Core.Evaluate
8−import Core.Elaborate
8+import Core.Elaborate hiding (Tactic(..))
99import Core.Typecheck
1010
1111import System.Console.Haskeline
12+
1213import Control.Monad.State
14+
1315import Data.List
1416import Data.Char
1517import Data.Either
18+
1619import Debug.Trace
1720
1821import qualified Epic.Epic as E
1922
23+import Util.Pretty
24+
2025data IOption = IOption { opt_logLevel :: Int,
2126 opt_typecase :: Bool,
2227 opt_typeintype :: Bool,
@@ -571,6 +576,26 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
571576deriving instance Binary PTactic'
572577!-}
573578
579+instance Sized a => Sized (PTactic' a) where
580+ size (Intro nms) = 1 + size nms
581+ size Intros = 1
582+ size (Focus nm) = 1 + size nm
583+ size (Refine nm bs) = 1 + size nm + length bs
584+ size (Rewrite t) = 1 + size t
585+ size (LetTac nm t) = 1 + size nm + size t
586+ size (Exact t) = 1 + size t
587+ size Compute = 1
588+ size Trivial = 1
589+ size Solve = 1
590+ size Attack = 1
591+ size ProofState = 1
592+ size ProofTerm = 1
593+ size Undo = 1
594+ size (Try l r) = 1 + size l + size r
595+ size (TSeq l r) = 1 + size l + size r
596+ size Qed = 1
597+ size Abandon = 1
598+
574599type PTactic = PTactic' PTerm
575600
576601data PDo' t = DoExp FC t
@@ -583,6 +608,13 @@ data PDo' t = DoExp FC t
583608deriving instance Binary PDo'
584609!-}
585610
611+instance Sized a => Sized (PDo' a) where
612+ size (DoExp fc t) = 1 + size fc + size t
613+ size (DoBind fc nm t) = 1 + size fc + size nm + size t
614+ size (DoBindP fc l r) = 1 + size fc + size l + size r
615+ size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
616+ size (DoLetP fc l r) = 1 + size fc + size l + size r
617+
586618type PDo = PDo' PTerm
587619
588620-- The priority gives a hint as to elaboration order. Best to elaborate
@@ -600,6 +632,13 @@ data PArg' t = PImp { priority :: Int,
600632 getScript :: t,
601633 getTm :: t }
602634 deriving (Show, Eq, Functor)
635+
636+instance Sized a => Sized (PArg' a) where
637+ size (PImp p l nm trm) = 1 + size nm + size trm
638+ size (PExp p l trm) = 1 + size trm
639+ size (PConstraint p l trm) = 1 + size trm
640+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
641+
603642{-!
604643deriving instance Binary PArg'
605644!-}
@@ -712,6 +751,9 @@ expandNS syn n = case syn_namespace syn of
712751instance Show PTerm where
713752 show tm = showImp False tm
714753
754+instance Pretty PTerm where
755+ pretty = prettyImp False
756+
715757instance Show PDecl where
716758 show d = showDeclImp False d
717759
@@ -765,6 +807,186 @@ getConsts (_ : xs) = getConsts xs
765807getAll :: [PArg] -> [PTerm]
766808getAll = map getTm
767809
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 $+$ nest nestingSize (prettyArgS r)
916+ else
917+ l <+> prettyArgS r
918+
919+ fSe l r =
920+ if size r > breakingSize then
921+ l $+$ nest nestingSize (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 "=" $$ nest nestingSize (prettySe 10 r)
939+ else
940+ prettySe 10 l <+> text "=" <+> 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+
768990showImp :: Bool -> PTerm -> String
769991showImp impl tm = se 10 tm where
770992 se p (PQuote r) = "![" ++ show r ++ "]"
@@ -846,6 +1068,66 @@ showImp impl tm = se 10 tm where
8461068 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
8471069 | otherwise = str
8481070
1071+{-
1072+ PQuote Raw
1073+ | PRef FC Name
1074+ | PLam Name PTerm PTerm
1075+ | PPi Plicity Name PTerm PTerm
1076+ | PLet Name PTerm PTerm PTerm
1077+ | PTyped PTerm PTerm -- term with explicit type
1078+ | PApp FC PTerm [PArg]
1079+ | PCase FC PTerm [(PTerm, PTerm)]
1080+ | PTrue FC
1081+ | PFalse FC
1082+ | PRefl FC
1083+ | PResolveTC FC
1084+ | PEq FC PTerm PTerm
1085+ | PPair FC PTerm PTerm
1086+ | PDPair FC PTerm PTerm PTerm
1087+ | PAlternative [PTerm]
1088+ | PHidden PTerm -- irrelevant or hidden pattern
1089+ | PSet
1090+ | PConstant Const
1091+ | Placeholder
1092+ | PDoBlock [PDo]
1093+ | PIdiom FC PTerm
1094+ | PReturn FC
1095+ | PMetavar Name
1096+ | PProof [PTactic]
1097+ | PTactics [PTactic] -- as PProof, but no auto solving
1098+ | PElabError Err -- error to report on elaboration
1099+ | PImpossible -- special case for declaring when an LHS can't typecheck
1100+-}
1101+
1102+instance Sized PTerm where
1103+ size (PQuote rawTerm) = size rawTerm
1104+ size (PRef fc name) = size name
1105+ size (PLam name ty bdy) = 1 + size ty + size bdy
1106+ size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1107+ size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1108+ size (PTyped trm ty) = 1 + size trm + size ty
1109+ size (PApp fc name args) = 1 + size args
1110+ size (PCase fc trm bdy) = 1 + size trm + size bdy
1111+ size (PTrue fc) = 1
1112+ size (PFalse fc) = 1
1113+ size (PRefl fc) = 1
1114+ size (PResolveTC fc) = 1
1115+ size (PEq fc left right) = 1 + size left + size right
1116+ size (PPair fc left right) = 1 + size left + size right
1117+ size (PDPair fs left ty right) = 1 + size left + size ty + size right
1118+ size (PAlternative alts) = 1 + size alts
1119+ size (PHidden hidden) = size hidden
1120+ size PSet = 1
1121+ size (PConstant const) = 1 + size const
1122+ size Placeholder = 1
1123+ size (PDoBlock dos) = 1 + size dos
1124+ size (PIdiom fc term) = 1 + size term
1125+ size (PReturn fc) = 1
1126+ size (PMetavar name) = 1
1127+ size (PProof tactics) = size tactics
1128+ size (PElabError err) = size err
1129+ size PImpossible = 1
1130+
8491131allNamesIn :: PTerm -> [Name]
8501132allNamesIn tm = nub $ ni [] tm
8511133 where
src/Idris/Prover.hs+43−23
@@ -17,6 +17,8 @@ import Idris.DataOpts
1717import System.Console.Haskeline
1818import Control.Monad.State
1919
20+import Util.Pretty
21+
2022prover :: Bool -> Name -> Idris ()
2123prover lit x =
2224 do ctxt <- getContext
@@ -55,31 +57,49 @@ elabStep st e = do case runStateT e st of
5557 OK (a, st') -> return (a, st')
5658 Error a -> do i <- get
5759 fail (pshow i a)
58−
60+
5961dumpState :: IState -> ProofState -> IO ()
60−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
61−dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)
62− = do let OK ty = goalAtFocus ps
63− let OK env = envAtFocus ps
64−-- putStrLn $ "Other goals: " ++ show hs ++ "\n"
65− putStr $ "\n" ++ showPs (reverse env)
66− putStrLn $ "---------------------------------- (" ++ show nm
67− ++ ") --------"
68− putStrLn $ show h ++ " : " ++ showG ty ++ "\n"
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
6971 where
70− tshow t = show (delab ist t)
71−
72− showPs [] = ""
73− showPs ((MN _ "rewrite_rule", _) : bs) = showPs bs
74− showPs ((n, Let t v) : bs)
75− = " " ++ show n ++ " = " ++ tshow v ++ " : " ++
76− tshow t ++ "\n" ++ showPs bs
77− showPs ((n, b) : bs)
78− = " " ++ show n ++ " : " ++
79− tshow (binderTy b) ++ "\n" ++ showPs bs
80−
81− showG (Guess t v) = tshow t ++ " =?= " ++ tshow v
82− showG b = tshow (binderTy b)
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 "---------- Goal: ----------" $$
88+ pretty h <> colon $$ nest nestingSize (prettyG ty)
89+
90+ prettyAssumptions env =
91+ if length env == 0 then
92+ empty
93+ else
94+ text "---------- Assumptions: ----------" $$
95+ nest nestingSize (prettyPs $ reverse env)
96+
97+ prettyOtherGoals hs =
98+ if length hs == 0 then
99+ empty
100+ else
101+ text "---------- Other goals: ----------" $$
102+ pretty hs
83103
84104lifte :: ElabState [PDecl] -> ElabD a -> Idris a
85105lifte st e = do (v, _) <- elabStep st e
src/Util/Pretty.hsnew file+33
@@ -0,0 +1,33 @@
1+module Util.Pretty (
2+ module Text.PrettyPrint.HughesPJ,
3+ Sized(..), breakingSize, nestingSize,
4+ Pretty(..)
5+) where
6+
7+import Text.PrettyPrint.HughesPJ
8+
9+-- A rough notion of size for pretty printing various types.
10+class Sized a where
11+ size :: a -> Int
12+
13+instance (Sized a, Sized b) => Sized (a, b) where
14+ size (left, right) = 1 + size left + size right
15+
16+instance Sized a => Sized [a] where
17+ size = sum . map size
18+
19+-- The maximum size before we break on to another line.
20+breakingSize :: Int
21+breakingSize = 15
22+
23+nestingSize :: Int
24+nestingSize = 1
25+
26+class Pretty a where
27+ pretty :: a -> Doc
28+
29+instance Pretty () where
30+ pretty () = text "()"
31+
32+instance Pretty a => Pretty [a] where
33+ pretty l = foldr ($$) empty $ map pretty l