8c64e9c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Got pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!

commit8c64e9c1f2ba4b95f73c7be24805c8766a5bc541 authorDominic Mulligan <dominic.p.mulligan@googlemail.com> dateTue 28 Feb 2012, 13:52 (15 years ago) parent7162b6e

8 files changed+256−11

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+142−1 src/Idris/AbsSyntax.hs+37−3 src/Idris/Prover.hs+8−1 src/Util/Pretty.hs+16−1

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

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

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

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

33module Core.TT where

@@ -36,6 +36,9 @@ data FC = FC { fc_fname :: String,

3636deriving instance Binary FC

3737!-}

3838

39+instance Sized FC where

40+ size (FC f l) = 1 + length f

41+

3942instance Show FC where

4043 show (FC f l) = f ++ ":" ++ show l

4144

@@ -50,6 +53,17 @@ data Err = Msg String

5053 | At FC Err

5154 deriving Eq

5255

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+

5367score :: Err -> Int

5468score (CantUnify _ _ m s) = s + score m

5569score (CantResolve _) = 20

@@ -62,10 +76,30 @@ instance Show Err where

6276 ++ show e ++ " " ++ show i

6377 show _ = "Error"

6478

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+

6591data TC a = OK a

6692 | Error Err

6793 deriving (Eq, Functor)

6894

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+

69103instance Show a => Show (TC a) where

70104 show (OK x) = show x

71105 show (Error str) = "Error: " ++ show str

@@ -120,6 +154,16 @@ data Name = UN String

120154deriving instance Binary Name

121155!-}

122156

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+

123167instance Show Name where

124168 show (UN n) = n

125169 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

@@ -192,6 +236,23 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

192236deriving instance Binary Const

193237!-}

194238

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+

195256data Raw = Var Name

196257 | RBind Name (Binder Raw) Raw

197258 | RApp Raw Raw

@@ -229,6 +290,17 @@ data Binder b = Lam { binderTy :: b }

229290deriving instance Binary Binder

230291!-}

231292

293+instance Sized a => Sized (Binder a) where

294+ size (Lam ty) = 1 + size ty

295+ size (Pi ty) = 1 + size ty

296+ size (Let ty val) = 1 + size ty + size val

297+ size (NLet ty val) = 1 + size ty + size val

298+ size (Hole ty) = 1 + size ty

299+ size (GHole ty) = 1 + size ty

300+ size (Guess ty val) = 1 + size ty + size val

301+ size (PVar ty) = 1 + size ty

302+ size (PVTy ty) = 1 + size ty

303+

232304fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

233305fmapMB f (Let t v) = liftM2 Let (f t) (f v)

234306fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)

@@ -270,6 +342,9 @@ data UExp = UVar Int -- universe variable

270342 | UVal Int -- explicit universe level

271343 deriving (Eq, Ord)

272344

345+instance Sized UExp where

346+ size _ = 1

347+

273348-- We assume that universe levels have been checked, so anything external

274349-- can just have the same universe variable and we won't get any new

275350-- cycles.

@@ -300,6 +375,12 @@ data NameType = Bound | Ref | DCon Int Int | TCon Int Int

300375deriving instance Binary NameType

301376!-}

302377

378+instance Sized NameType where

379+ size _ = 1

380+

381+instance Pretty NameType where

382+ pretty = text . show

383+

303384instance Eq NameType where

304385 Bound == Bound = True

305386 Ref == Ref = True

@@ -319,6 +400,18 @@ data TT n = P NameType n (TT n) -- embed type

319400deriving instance Binary TT

320401!-}

321402

403+instance Sized a => Sized (TT a) where

404+ size (P name n trm) = 1 + size name + size n + size trm

405+ size (V v) = 1

406+ size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy

407+ size (App l r) = 1 + size l + size r

408+ size (Constant c) = size c

409+ size Erased = 1

410+ size (Set u) = 1 + size u

411+

412+instance Pretty a => Pretty (TT a) where

413+ pretty

414+

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

323416

324417data Datatype n = Data { d_typename :: n,

@@ -507,6 +600,54 @@ instance Show Const where

507600showEnv env t = showEnv' env t False

508601showEnvDbg env t = showEnv' env t True

509602

603+prettyEnv env t = prettyEnv' env t False

604+ where

605+ prettyEnv' env t dbg = prettySe 10 env t dbg

606+

607+ bracket outer inner p

608+ | inner > outer = lparen <> p <> rparen

609+ | otherwise = p

610+

611+ prettySe p env (P nt n t) debug =

612+ pretty n <+>

613+ if debug then

614+ lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack

615+ else

616+ empty

617+ prettySe p env (V i) debug

618+ | i < length env =

619+ if debug then

620+ text . show . fst $ env!!i

621+ else

622+ lbrack <+> text (show i) <+> rbrack

623+ | otherwise = text "unbound" <+> text (show i) <+> text "!"

624+ prettySe p env (Bind n b@(Pi t) sc) debug

625+ | noOccurrence n sc && not debug =

626+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

627+ prettySe p env (Bind n b sc) debug =

628+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

629+ prettySe p env (App f a) debug =

630+ bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug

631+ prettySe p env (Constant c) debug = pretty c

632+ prettySe p env Erased debug = text "[_]"

633+ prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)

634+

635+ prettySb env n (Lam t) = prettyB env "λ" "=>" n t

636+ prettySb env n (Hole t) = prettyB env "?defer" "." n t

637+ prettySb env n (Pi t) = prettyB env "(" ") ->" n t

638+ prettySb env n (PVar t) = prettyB env "pat" "." n t

639+ prettySb env n (PVTy t) = prettyB env "pty" "." n t

640+ prettySb env n (Let t v) = prettyBv env "let" "in" n t v

641+ prettySb env n (Guess t v) = prettyBv env "??" "in" n t v

642+

643+ prettyB env op sc n t debug =

644+ text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc

645+

646+ prettyBv env op sc n t v debug =

647+ text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>

648+ prettySe 10 env v debug <> text sc

649+

650+

510651showEnv' env t dbg = se 10 env t where

511652 se p env (P nt n t) = show n

512653 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

src/Idris/AbsSyntax.hs+37−3

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

@@ -576,6 +576,26 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

576576deriving instance Binary PTactic'

577577!-}

578578

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+

579599type PTactic = PTactic' PTerm

580600

581601data PDo' t = DoExp FC t

@@ -588,6 +608,13 @@ data PDo' t = DoExp FC t

588608deriving instance Binary PDo'

589609!-}

590610

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+

591618type PDo = PDo' PTerm

592619

593620-- The priority gives a hint as to elaboration order. Best to elaborate

@@ -605,6 +632,13 @@ data PArg' t = PImp { priority :: Int,

605632 getScript :: t,

606633 getTm :: t }

607634 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+

608642{-!

609643deriving instance Binary PArg'

610644!-}

@@ -886,7 +920,7 @@ instance Sized PTerm where

886920 size (PQuote rawTerm) = size rawTerm

887921 size (PRef fc name) = size name

888922 size (PLam name ty bdy) = 1 + size ty + size bdy

889− size (PPi name ty bdy) = 1 + size ty + size bdy

923+ size (PPi plicity name ty bdy) = 1 + size ty + size bdy

890924 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy

891925 size (PTyped trm ty) = 1 + size trm + size ty

892926 size (PApp fc name args) = 1 + size args

@@ -897,7 +931,7 @@ instance Sized PTerm where

897931 size (PResolveTC fc) = 1

898932 size (PEq fc left right) = 1 + size left + size right

899933 size (PPair fc left right) = 1 + size left + size right

900− size (PDPair fs left right) = 1 + size left + size right

934+ size (PDPair fs left ty right) = 1 + size left + size ty + size right

901935 size (PAlternative alts) = 1 + size alts

902936 size (PHidden hidden) = size hidden

903937 size PSet = 1

src/Idris/Prover.hs+8−1

@@ -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,7 +57,11 @@ 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+

61+dumpState :: IState -> ProofState -> IO ()

62+dumpState _ pst = putStrLn . render . pretty $ pst

63+

64+{-

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

6066dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

6167dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)

@@ -80,6 +86,7 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)

8086

8187 showG (Guess t v) = tshow t ++ " =?= " ++ tshow v

8288 showG b = tshow (binderTy b)

89+-}

8390

8491lifte :: ElabState [PDecl] -> ElabD a -> Idris a

8592lifte st e = do (v, _) <- elabStep st e

src/Util/Pretty.hs+16−1

@@ -1,10 +1,12 @@

11module Util.Pretty (

22 module Text.PrettyPrint.HughesPJ,

3− Sized(..), Pretty(..)

3+ Sized(..), breakingSize, nestingSize,

4+ Pretty(..)

45) where

67import Text.PrettyPrint.HughesPJ

9+-- A rough notion of size for pretty printing various types.

810class Sized a where

911 size :: a -> Int

1012

@@ -14,5 +16,18 @@ instance (Sized a, Sized b) => Sized (a, b) where

1416instance Sized a => Sized [a] where

1517 size = sum . map size

1618

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

20+breakingSize :: Int

21+breakingSize = 5

22+

23+nestingSize :: Int

24+nestingSize = 2

25+

1726class Pretty a where

1827 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