d1a832a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Send serialized versions of TT terms in pprint

This is the basis for commands that manipulate previously-output terms.

commitd1a832ae93f728c2087f04eb16f122e46ca14d31 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 13 Jun 2014, 18:28 (12 years ago) parentf48942b

9 files changed+392−353

compare with master

unifiedsplit

idris.cabal+3−1 src/Idris/AbsSyntaxTree.hs+3 src/Idris/Core/Binary.hs+356 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+15−1 src/Idris/IBC.hs+1−346 src/Idris/IdeSlave.hs+6 src/Idris/Prover.hs+3−1 src/Idris/REPL.hs+4−4

idris.cabal+3−1

@@ -514,7 +514,8 @@ Flag release

514514Library

515515 hs-source-dirs: src

516516 Exposed-modules:

517− Idris.Core.CaseTree

517+ Idris.Core.Binary

518+ , Idris.Core.CaseTree

518519 , Idris.Core.Constraints

519520 , Idris.Core.DeepSeq

520521 , Idris.Core.Elaborate

@@ -611,6 +612,7 @@ Library

611612 , annotated-wl-pprint >= 0.5.3

612613 , ansi-terminal

613614 , ansi-wl-pprint

615+ , base64-bytestring

614616 , binary

615617 , blaze-html >= 0.6.1.3

616618 , blaze-markup >= 0.5.2.1 && < 0.7.0.0

src/Idris/AbsSyntaxTree.hs+3

@@ -1164,6 +1164,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

11641164 where colour BoldText = IdrisColour Nothing True False True False

11651165 colour UnderlineText = IdrisColour Nothing True True False False

11661166 colour ItalicText = IdrisColour Nothing True False False True

1167+consoleDecorate ist (AnnTerm _) = id

11671168

11681169isPostulateName :: Name -> IState -> Bool

11691170isPostulateName n ist = S.member n (idris_postulates ist)

@@ -1174,6 +1175,8 @@ prettyImp :: PPOption -- ^^ pretty printing options

11741175 -> Doc OutputAnnotation

11751176prettyImp impl = pprintPTerm impl [] [] []

11761177

1178+-- | Serialise something to base64 using its Binary instance.

1179+

11771180-- | Do the right thing for rendering a term in an IState

11781181prettyIst :: IState -> PTerm -> Doc OutputAnnotation

11791182prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

src/Idris/Core/Binary.hsnew file+356

@@ -0,0 +1,356 @@

1+{-| Binary instances for the core datatypes -}

2+module Idris.Core.Binary where

4+import Data.Binary

5+import Data.Vector.Binary

6+import qualified Data.Text as T

8+import Idris.Core.TT

10+----- Generated by 'derive'

11+

12+instance Binary FC where

13+ put (FC x1 (x2, x3) (x4, x5))

14+ = do put x1

15+ put (x2 * 65536 + x3)

16+ put (x4 * 65536 + x5)

17+ get

18+ = do x1 <- get

19+ x2x3 <- get

20+ x4x5 <- get

21+ return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))

22+

23+

24+instance Binary Name where

25+ put x

26+ = case x of

27+ UN x1 -> do putWord8 0

28+ put x1

29+ NS x1 x2 -> do putWord8 1

30+ put x1

31+ put x2

32+ MN x1 x2 -> do putWord8 2

33+ put x1

34+ put x2

35+ NErased -> putWord8 3

36+ SN x1 -> do putWord8 4

37+ put x1

38+ SymRef x1 -> do putWord8 5

39+ put x1

40+ get

41+ = do i <- getWord8

42+ case i of

43+ 0 -> do x1 <- get

44+ return (UN x1)

45+ 1 -> do x1 <- get

46+ x2 <- get

47+ return (NS x1 x2)

48+ 2 -> do x1 <- get

49+ x2 <- get

50+ return (MN x1 x2)

51+ 3 -> return NErased

52+ 4 -> do x1 <- get

53+ return (SN x1)

54+ 5 -> do x1 <- get

55+ return (SymRef x1)

56+ _ -> error "Corrupted binary data for Name"

57+

58+instance Binary T.Text where

59+ put x = put (str x)

60+ get = do x <- get

61+ return (txt x)

62+

63+instance Binary SpecialName where

64+ put x

65+ = case x of

66+ WhereN x1 x2 x3 -> do putWord8 0

67+ put x1

68+ put x2

69+ put x3

70+ InstanceN x1 x2 -> do putWord8 1

71+ put x1

72+ put x2

73+ ParentN x1 x2 -> do putWord8 2

74+ put x1

75+ put x2

76+ MethodN x1 -> do putWord8 3

77+ put x1

78+ CaseN x1 -> do putWord8 4; put x1

79+ ElimN x1 -> do putWord8 5; put x1

80+ InstanceCtorN x1 -> do putWord8 6; put x1

81+ get

82+ = do i <- getWord8

83+ case i of

84+ 0 -> do x1 <- get

85+ x2 <- get

86+ x3 <- get

87+ return (WhereN x1 x2 x3)

88+ 1 -> do x1 <- get

89+ x2 <- get

90+ return (InstanceN x1 x2)

91+ 2 -> do x1 <- get

92+ x2 <- get

93+ return (ParentN x1 x2)

94+ 3 -> do x1 <- get

95+ return (MethodN x1)

96+ 4 -> do x1 <- get

97+ return (CaseN x1)

98+ 5 -> do x1 <- get

99+ return (ElimN x1)

100+ 6 -> do x1 <- get

101+ return (InstanceCtorN x1)

102+ _ -> error "Corrupted binary data for SpecialName"

103+

104+

105+instance Binary Const where

106+ put x

107+ = case x of

108+ I x1 -> do putWord8 0

109+ put x1

110+ BI x1 -> do putWord8 1

111+ put x1

112+ Fl x1 -> do putWord8 2

113+ put x1

114+ Ch x1 -> do putWord8 3

115+ put x1

116+ Str x1 -> do putWord8 4

117+ put x1

118+ B8 x1 -> putWord8 5 >> put x1

119+ B16 x1 -> putWord8 6 >> put x1

120+ B32 x1 -> putWord8 7 >> put x1

121+ B64 x1 -> putWord8 8 >> put x1

122+

123+ (AType (ATInt ITNative)) -> putWord8 9

124+ (AType (ATInt ITBig)) -> putWord8 10

125+ (AType ATFloat) -> putWord8 11

126+ (AType (ATInt ITChar)) -> putWord8 12

127+ StrType -> putWord8 13

128+ PtrType -> putWord8 14

129+ Forgot -> putWord8 15

130+ (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive

131+ (AType (ATInt (ITVec ity count))) -> do

132+ putWord8 20

133+ putWord8 (fromIntegral . fromEnum $ ity)

134+ putWord8 (fromIntegral count)

135+

136+ B8V x1 -> putWord8 21 >> put x1

137+ B16V x1 -> putWord8 22 >> put x1

138+ B32V x1 -> putWord8 23 >> put x1

139+ B64V x1 -> putWord8 24 >> put x1

140+ BufferType -> putWord8 25

141+ ManagedPtrType -> putWord8 26

142+ get

143+ = do i <- getWord8

144+ case i of

145+ 0 -> do x1 <- get

146+ return (I x1)

147+ 1 -> do x1 <- get

148+ return (BI x1)

149+ 2 -> do x1 <- get

150+ return (Fl x1)

151+ 3 -> do x1 <- get

152+ return (Ch x1)

153+ 4 -> do x1 <- get

154+ return (Str x1)

155+ 5 -> fmap B8 get

156+ 6 -> fmap B16 get

157+ 7 -> fmap B32 get

158+ 8 -> fmap B64 get

159+

160+ 9 -> return (AType (ATInt ITNative))

161+ 10 -> return (AType (ATInt ITBig))

162+ 11 -> return (AType ATFloat)

163+ 12 -> return (AType (ATInt ITChar))

164+ 13 -> return StrType

165+ 14 -> return PtrType

166+ 15 -> return Forgot

167+

168+ 16 -> return (AType (ATInt (ITFixed IT8)))

169+ 17 -> return (AType (ATInt (ITFixed IT16)))

170+ 18 -> return (AType (ATInt (ITFixed IT32)))

171+ 19 -> return (AType (ATInt (ITFixed IT64)))

172+

173+ 20 -> do

174+ e <- getWord8

175+ c <- getWord8

176+ return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))

177+

178+ 21 -> fmap B8V get

179+ 22 -> fmap B16V get

180+ 23 -> fmap B32V get

181+ 24 -> fmap B64V get

182+ 25 -> return BufferType

183+ 26 -> return ManagedPtrType

184+

185+ _ -> error "Corrupted binary data for Const"

186+

187+

188+instance Binary Raw where

189+ put x

190+ = case x of

191+ Var x1 -> do putWord8 0

192+ put x1

193+ RBind x1 x2 x3 -> do putWord8 1

194+ put x1

195+ put x2

196+ put x3

197+ RApp x1 x2 -> do putWord8 2

198+ put x1

199+ put x2

200+ RType -> putWord8 3

201+ RConstant x1 -> do putWord8 4

202+ put x1

203+ RForce x1 -> do putWord8 5

204+ put x1

205+ get

206+ = do i <- getWord8

207+ case i of

208+ 0 -> do x1 <- get

209+ return (Var x1)

210+ 1 -> do x1 <- get

211+ x2 <- get

212+ x3 <- get

213+ return (RBind x1 x2 x3)

214+ 2 -> do x1 <- get

215+ x2 <- get

216+ return (RApp x1 x2)

217+ 3 -> return RType

218+ 4 -> do x1 <- get

219+ return (RConstant x1)

220+ 5 -> do x1 <- get

221+ return (RForce x1)

222+ _ -> error "Corrupted binary data for Raw"

223+

224+

225+instance (Binary b) => Binary (Binder b) where

226+ put x

227+ = case x of

228+ Lam x1 -> do putWord8 0

229+ put x1

230+ Pi x1 -> do putWord8 1

231+ put x1

232+ Let x1 x2 -> do putWord8 2

233+ put x1

234+ put x2

235+ NLet x1 x2 -> do putWord8 3

236+ put x1

237+ put x2

238+ Hole x1 -> do putWord8 4

239+ put x1

240+ GHole x1 x2 -> do putWord8 5

241+ put x1

242+ put x2

243+ Guess x1 x2 -> do putWord8 6

244+ put x1

245+ put x2

246+ PVar x1 -> do putWord8 7

247+ put x1

248+ PVTy x1 -> do putWord8 8

249+ put x1

250+ get

251+ = do i <- getWord8

252+ case i of

253+ 0 -> do x1 <- get

254+ return (Lam x1)

255+ 1 -> do x1 <- get

256+ return (Pi x1)

257+ 2 -> do x1 <- get

258+ x2 <- get

259+ return (Let x1 x2)

260+ 3 -> do x1 <- get

261+ x2 <- get

262+ return (NLet x1 x2)

263+ 4 -> do x1 <- get

264+ return (Hole x1)

265+ 5 -> do x1 <- get

266+ x2 <- get

267+ return (GHole x1 x2)

268+ 6 -> do x1 <- get

269+ x2 <- get

270+ return (Guess x1 x2)

271+ 7 -> do x1 <- get

272+ return (PVar x1)

273+ 8 -> do x1 <- get

274+ return (PVTy x1)

275+ _ -> error "Corrupted binary data for Binder"

276+

277+

278+instance Binary NameType where

279+ put x

280+ = case x of

281+ Bound -> putWord8 0

282+ Ref -> putWord8 1

283+ DCon x1 x2 -> do putWord8 2

284+ put (x1 * 65536 + x2)

285+ TCon x1 x2 -> do putWord8 3

286+ put (x1 * 65536 + x2)

287+ get

288+ = do i <- getWord8

289+ case i of

290+ 0 -> return Bound

291+ 1 -> return Ref

292+ 2 -> do x1x2 <- get

293+ return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

294+ 3 -> do x1x2 <- get

295+ return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

296+ _ -> error "Corrupted binary data for NameType"

297+

298+

299+instance {- (Binary n) => -} Binary (TT Name) where

300+ put x

301+ = {-# SCC "putTT" #-}

302+ case x of

303+ P x1 x2 x3 -> do putWord8 0

304+ put x1

305+ put x2

306+-- put x3

307+ V x1 -> if (x1 >= 0 && x1 < 256)

308+ then do putWord8 1

309+ putWord8 (toEnum (x1 + 1))

310+ else do putWord8 9

311+ put x1

312+ Bind x1 x2 x3 -> do putWord8 2

313+ put x1

314+ put x2

315+ put x3

316+ App x1 x2 -> do putWord8 3

317+ put x1

318+ put x2

319+ Constant x1 -> do putWord8 4

320+ put x1

321+ Proj x1 x2 -> do putWord8 5

322+ put x1

323+ putWord8 (toEnum (x2 + 1))

324+ Erased -> putWord8 6

325+ TType x1 -> do putWord8 7

326+ put x1

327+ Impossible -> putWord8 8

328+ get

329+ = do i <- getWord8

330+ case i of

331+ 0 -> do x1 <- get

332+ x2 <- get

333+-- x3 <- get

334+ return (P x1 x2 Erased)

335+ 1 -> do x1 <- getWord8

336+ return (V ((fromEnum x1) - 1))

337+ 2 -> do x1 <- get

338+ x2 <- get

339+ x3 <- get

340+ return (Bind x1 x2 x3)

341+ 3 -> do x1 <- get

342+ x2 <- get

343+ return (App x1 x2)

344+ 4 -> do x1 <- get

345+ return (Constant x1)

346+ 5 -> do x1 <- get

347+ x2 <- getWord8

348+ return (Proj x1 ((fromEnum x2)-1))

349+ 6 -> return Erased

350+ 7 -> do x1 <- get

351+ return (TType x1)

352+ 8 -> return Impossible

353+ 9 -> do x1 <- get

354+ return (V x1)

355+ _ -> error "Corrupted binary data for TT"

356+

src/Idris/Core/TT.hs+1

@@ -99,6 +99,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

9999 | AnnKeyword

100100 | AnnFC FC

101101 | AnnTextFmt TextFormatting

102+ | AnnTerm (TT Name)

102103

103104-- | Used for error reflection

104105data ErrorReportPart = TextPart String

src/Idris/Delaborate.hs+15−1

@@ -1,5 +1,5 @@

11{-# LANGUAGE PatternGuards #-}

2−module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintErr) where

2+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where

44-- Convert core TT back into high level syntax, primarily for display

55-- purposes.

@@ -135,6 +135,20 @@ errorIndent = 8

135135indented :: Doc a -> Doc a

136136indented = nest errorIndent . (line <>)

137137

138+-- | Pretty-print a core term using delaboration

139+pprintDelab :: IState -> Term -> Doc OutputAnnotation

140+pprintDelab ist tm = annotate (AnnTerm tm)

141+ (prettyIst ist (delab ist tm))

142+

143+-- | Pretty-print the type of some name

144+pprintDelabTy :: IState -> Name -> Doc OutputAnnotation

145+pprintDelabTy i n

146+ = case lookupTy n (tt_ctxt i) of

147+ (ty:_) -> annotate (AnnTerm ty) . prettyIst i $

148+ case lookupCtxt n (idris_implicits i) of

149+ (imps:_) -> delabTy' i imps ty False False

150+ _ -> delabTy' i [] ty False False

151+

138152pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

139153pprintTerm ist = pprintTerm' ist []

140154

src/Idris/IBC.hs+1−346

@@ -4,6 +4,7 @@ module Idris.IBC where

55import Idris.Core.Evaluate

66import Idris.Core.TT

7+import Idris.Core.Binary

78import Idris.Core.CaseTree

89import Idris.AbsSyntax

910import Idris.Imports

@@ -617,352 +618,6 @@ instance Binary CGInfo where

617618 x4 <- get

618619 x5 <- get

619620 return (CGInfo x1 x2 [] x4 x5)

620−

621−instance Binary FC where

622− put (FC x1 (x2, x3) (x4, x5))

623− = do put x1

624− put (x2 * 65536 + x3)

625− put (x4 * 65536 + x5)

626− get

627− = do x1 <- get

628− x2x3 <- get

629− x4x5 <- get

630− return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))

631−

632−

633−instance Binary Name where

634− put x

635− = case x of

636− UN x1 -> do putWord8 0

637− put x1

638− NS x1 x2 -> do putWord8 1

639− put x1

640− put x2

641− MN x1 x2 -> do putWord8 2

642− put x1

643− put x2

644− NErased -> putWord8 3

645− SN x1 -> do putWord8 4

646− put x1

647− SymRef x1 -> do putWord8 5

648− put x1

649− get

650− = do i <- getWord8

651− case i of

652− 0 -> do x1 <- get

653− return (UN x1)

654− 1 -> do x1 <- get

655− x2 <- get

656− return (NS x1 x2)

657− 2 -> do x1 <- get

658− x2 <- get

659− return (MN x1 x2)

660− 3 -> return NErased

661− 4 -> do x1 <- get

662− return (SN x1)

663− 5 -> do x1 <- get

664− return (SymRef x1)

665− _ -> error "Corrupted binary data for Name"

666−

667−instance Binary T.Text where

668− put x = put (str x)

669− get = do x <- get

670− return (txt x)

671−

672−instance Binary SpecialName where

673− put x

674− = case x of

675− WhereN x1 x2 x3 -> do putWord8 0

676− put x1

677− put x2

678− put x3

679− InstanceN x1 x2 -> do putWord8 1

680− put x1

681− put x2

682− ParentN x1 x2 -> do putWord8 2

683− put x1

684− put x2

685− MethodN x1 -> do putWord8 3

686− put x1

687− CaseN x1 -> do putWord8 4; put x1

688− ElimN x1 -> do putWord8 5; put x1

689− InstanceCtorN x1 -> do putWord8 6; put x1

690− get

691− = do i <- getWord8

692− case i of

693− 0 -> do x1 <- get

694− x2 <- get

695− x3 <- get

696− return (WhereN x1 x2 x3)

697− 1 -> do x1 <- get

698− x2 <- get

699− return (InstanceN x1 x2)

700− 2 -> do x1 <- get

701− x2 <- get

702− return (ParentN x1 x2)

703− 3 -> do x1 <- get

704− return (MethodN x1)

705− 4 -> do x1 <- get

706− return (CaseN x1)

707− 5 -> do x1 <- get

708− return (ElimN x1)

709− 6 -> do x1 <- get

710− return (InstanceCtorN x1)

711− _ -> error "Corrupted binary data for SpecialName"

712−

713−

714−instance Binary Const where

715− put x

716− = case x of

717− I x1 -> do putWord8 0

718− put x1

719− BI x1 -> do putWord8 1

720− put x1

721− Fl x1 -> do putWord8 2

722− put x1

723− Ch x1 -> do putWord8 3

724− put x1

725− Str x1 -> do putWord8 4

726− put x1

727− B8 x1 -> putWord8 5 >> put x1

728− B16 x1 -> putWord8 6 >> put x1

729− B32 x1 -> putWord8 7 >> put x1

730− B64 x1 -> putWord8 8 >> put x1

731−

732− (AType (ATInt ITNative)) -> putWord8 9

733− (AType (ATInt ITBig)) -> putWord8 10

734− (AType ATFloat) -> putWord8 11

735− (AType (ATInt ITChar)) -> putWord8 12

736− StrType -> putWord8 13

737− PtrType -> putWord8 14

738− Forgot -> putWord8 15

739− (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive

740− (AType (ATInt (ITVec ity count))) -> do

741− putWord8 20

742− putWord8 (fromIntegral . fromEnum $ ity)

743− putWord8 (fromIntegral count)

744−

745− B8V x1 -> putWord8 21 >> put x1

746− B16V x1 -> putWord8 22 >> put x1

747− B32V x1 -> putWord8 23 >> put x1

748− B64V x1 -> putWord8 24 >> put x1

749− BufferType -> putWord8 25

750− ManagedPtrType -> putWord8 26

751− get

752− = do i <- getWord8

753− case i of

754− 0 -> do x1 <- get

755− return (I x1)

756− 1 -> do x1 <- get

757− return (BI x1)

758− 2 -> do x1 <- get

759− return (Fl x1)

760− 3 -> do x1 <- get

761− return (Ch x1)

762− 4 -> do x1 <- get

763− return (Str x1)

764− 5 -> fmap B8 get

765− 6 -> fmap B16 get

766− 7 -> fmap B32 get

767− 8 -> fmap B64 get

768−

769− 9 -> return (AType (ATInt ITNative))

770− 10 -> return (AType (ATInt ITBig))

771− 11 -> return (AType ATFloat)

772− 12 -> return (AType (ATInt ITChar))

773− 13 -> return StrType

774− 14 -> return PtrType

775− 15 -> return Forgot

776−

777− 16 -> return (AType (ATInt (ITFixed IT8)))

778− 17 -> return (AType (ATInt (ITFixed IT16)))

779− 18 -> return (AType (ATInt (ITFixed IT32)))

780− 19 -> return (AType (ATInt (ITFixed IT64)))

781−

782− 20 -> do

783− e <- getWord8

784− c <- getWord8

785− return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))

786−

787− 21 -> fmap B8V get

788− 22 -> fmap B16V get

789− 23 -> fmap B32V get

790− 24 -> fmap B64V get

791− 25 -> return BufferType

792− 26 -> return ManagedPtrType

793−

794− _ -> error "Corrupted binary data for Const"

795−

796−

797−instance Binary Raw where

798− put x

799− = case x of

800− Var x1 -> do putWord8 0

801− put x1

802− RBind x1 x2 x3 -> do putWord8 1

803− put x1

804− put x2

805− put x3

806− RApp x1 x2 -> do putWord8 2

807− put x1

808− put x2

809− RType -> putWord8 3

810− RConstant x1 -> do putWord8 4

811− put x1

812− RForce x1 -> do putWord8 5

813− put x1

814− get

815− = do i <- getWord8

816− case i of

817− 0 -> do x1 <- get

818− return (Var x1)

819− 1 -> do x1 <- get

820− x2 <- get

821− x3 <- get

822− return (RBind x1 x2 x3)

823− 2 -> do x1 <- get

824− x2 <- get

825− return (RApp x1 x2)

826− 3 -> return RType

827− 4 -> do x1 <- get

828− return (RConstant x1)

829− 5 -> do x1 <- get

830− return (RForce x1)

831− _ -> error "Corrupted binary data for Raw"

832−

833−

834−instance (Binary b) => Binary (Binder b) where

835− put x

836− = case x of

837− Lam x1 -> do putWord8 0

838− put x1

839− Pi x1 -> do putWord8 1

840− put x1

841− Let x1 x2 -> do putWord8 2

842− put x1

843− put x2

844− NLet x1 x2 -> do putWord8 3

845− put x1

846− put x2

847− Hole x1 -> do putWord8 4

848− put x1

849− GHole x1 x2 -> do putWord8 5

850− put x1

851− put x2

852− Guess x1 x2 -> do putWord8 6

853− put x1

854− put x2

855− PVar x1 -> do putWord8 7

856− put x1

857− PVTy x1 -> do putWord8 8

858− put x1

859− get

860− = do i <- getWord8

861− case i of

862− 0 -> do x1 <- get

863− return (Lam x1)

864− 1 -> do x1 <- get

865− return (Pi x1)

866− 2 -> do x1 <- get

867− x2 <- get

868− return (Let x1 x2)

869− 3 -> do x1 <- get

870− x2 <- get

871− return (NLet x1 x2)

872− 4 -> do x1 <- get

873− return (Hole x1)

874− 5 -> do x1 <- get

875− x2 <- get

876− return (GHole x1 x2)

877− 6 -> do x1 <- get

878− x2 <- get

879− return (Guess x1 x2)

880− 7 -> do x1 <- get

881− return (PVar x1)

882− 8 -> do x1 <- get

883− return (PVTy x1)

884− _ -> error "Corrupted binary data for Binder"

885−

886−

887−instance Binary NameType where

888− put x

889− = case x of

890− Bound -> putWord8 0

891− Ref -> putWord8 1

892− DCon x1 x2 -> do putWord8 2

893− put (x1 * 65536 + x2)

894− TCon x1 x2 -> do putWord8 3

895− put (x1 * 65536 + x2)

896− get

897− = do i <- getWord8

898− case i of

899− 0 -> return Bound

900− 1 -> return Ref

901− 2 -> do x1x2 <- get

902− return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

903− 3 -> do x1x2 <- get

904− return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

905− _ -> error "Corrupted binary data for NameType"

906−

907−

908−instance {- (Binary n) => -} Binary (TT Name) where

909− put x

910− = {-# SCC "putTT" #-}

911− case x of

912− P x1 x2 x3 -> do putWord8 0

913− put x1

914− put x2

915−-- put x3

916− V x1 -> if (x1 >= 0 && x1 < 256)

917− then do putWord8 1

918− putWord8 (toEnum (x1 + 1))

919− else do putWord8 9

920− put x1

921− Bind x1 x2 x3 -> do putWord8 2

922− put x1

923− put x2

924− put x3

925− App x1 x2 -> do putWord8 3

926− put x1

927− put x2

928− Constant x1 -> do putWord8 4

929− put x1

930− Proj x1 x2 -> do putWord8 5

931− put x1

932− putWord8 (toEnum (x2 + 1))

933− Erased -> putWord8 6

934− TType x1 -> do putWord8 7

935− put x1

936− Impossible -> putWord8 8

937− get

938− = do i <- getWord8

939− case i of

940− 0 -> do x1 <- get

941− x2 <- get

942−-- x3 <- get

943− return (P x1 x2 Erased)

944− 1 -> do x1 <- getWord8

945− return (V ((fromEnum x1) - 1))

946− 2 -> do x1 <- get

947− x2 <- get

948− x3 <- get

949− return (Bind x1 x2 x3)

950− 3 -> do x1 <- get

951− x2 <- get

952− return (App x1 x2)

953− 4 -> do x1 <- get

954− return (Constant x1)

955− 5 -> do x1 <- get

956− x2 <- getWord8

957− return (Proj x1 ((fromEnum x2)-1))

958− 6 -> return Erased

959− 7 -> do x1 <- get

960− return (TType x1)

961− 8 -> return Impossible

962− 9 -> do x1 <- get

963− return (V x1)

964− _ -> error "Corrupted binary data for TT"

965−

966621instance Binary SC where

967622 put x

968623 = case x of

src/Idris/IdeSlave.hs+6

@@ -5,12 +5,16 @@ module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand

55import Text.Printf

66import Numeric

77import Data.List

8+import qualified Data.Binary as Binary

9+import qualified Data.ByteString.Base64 as Base64

10+import qualified Data.ByteString.Lazy as Lazy

811import qualified Data.ByteString.UTF8 as UTF8

912-- import qualified Data.Text as T

1013import Text.Trifecta hiding (Err)

1114import Text.Trifecta.Delta

1215

1316import Idris.Core.TT

17+import Idris.Core.Binary

1418

1519import Control.Applicative hiding (Const)

1620

@@ -128,6 +132,8 @@ instance SExpable OutputAnnotation where

128132 BoldText -> "bold"

129133 ItalicText -> "italic"

130134 UnderlineText -> "underline"

135+ toSExp (AnnTerm tm) = toSExp [(SymbolAtom "tt-term", StringAtom encoded)]

136+ where encoded = (UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode) tm

131137

132138instance SExpable FC where

133139 toSExp (FC f (sl, sc) (el, ec)) =

src/Idris/Prover.hs+3−1

@@ -121,7 +121,9 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

121121 where

122122 ppo = ppOptionIst ist

123123

124− tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t

124+ tPretty bnd t = annotate (AnnTerm t) .

125+ pprintPTerm ppo bnd [] (idris_infixes ist) $

126+ delab ist t

125127

126128 assumptionNames :: Env -> [Name]

127129 assumptionNames = map fst

src/Idris/REPL.hs+4−4

@@ -594,8 +594,8 @@ process h fn (Eval t)

594594 ist <- getIState

595595 logLvl 3 $ "Raw: " ++ show (tm', ty')

596596 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

597− let tmDoc = prettyIst ist (delab ist tm')

598− tyDoc = prettyIst ist (delab ist ty')

597+ let tmDoc = pprintDelab ist tm'

598+ tyDoc = pprintDelab ist ty'

599599 ihPrintTermWithType h tmDoc tyDoc

600600

601601process h fn (ExecVal t)

@@ -653,8 +653,8 @@ process h fn (Check t)

653653 case tm of

654654 TType _ ->

655655 ihPrintTermWithType h (prettyIst ist PType) type1Doc

656− _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))

657− (prettyIst ist (delab ist ty))

656+ _ -> ihPrintTermWithType h (pprintDelab ist tm)

657+ (pprintDelab ist ty)

658658

659659process h fn (DocStr (Left n))

660660 = do ist <- getIState