2ba8712 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branches 'improved-pretty-printing' and 'master'

commit2ba8712075811f53885cf829072580d5970f2caa authorDominic Mulligan <dominic.p.mulligan@googlemail.com> dateThu 1 Mar 2012, 14:25 (15 years ago) parent3541c70 368fdf6

8 files changed+568−30

compare with master

unifiedsplit

idris.cabal+1−1 src/Core/Elaborate.hs+6−1 src/Core/ProofShell.hs+4−2 src/Core/ProofState.hs+42−1 src/Core/TT.hs+156−1 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

src/Core/Elaborate.hs+6−1

@@ -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

@@ -29,7 +31,10 @@ data Command = Theorem Name Raw

2931 | Tac (Elab ())

3032

3133data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

32− deriving Show

34+

35+instance Pretty aux => Pretty (ElabState aux) where

36+ pretty (ES (pState, aux) str _) = text "test"

37+

3338type Elab' aux a = StateT (ElabState aux) TC a

3439type Elab a = Elab' () a

3540

src/Core/ProofShell.hs+4−2

@@ -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,

@@ -50,13 +52,13 @@ processCommand (Tac e) state

5052 (pterm ps')

5153 (ptype ps')

5254 (context ps') }, resp)

53− err -> (state, show err)

55+ err -> (state, show . render . pretty $ err)

5456 | otherwise = (state, "No proof in progress")

5557

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+156−1

@@ -1,4 +1,4 @@

1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

1+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, FlexibleInstances #-}

33module Core.TT where

@@ -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

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

7+import Text.PrettyPrint.HughesPJ

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