cebd1b4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1315 from david-christiansen/serialized-terms

cebd1b4David Christiansen12 years ago

idris.cabal+3−1

compare with master

unifiedsplit

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

514Library

515 hs-source-dirs: src

516 Exposed-modules:

517− Idris.Core.CaseTree

517+ Idris.Core.Binary

518+ , Idris.Core.CaseTree

518 , Idris.Core.Constraints

519 , Idris.Core.Constraints

519 , Idris.Core.DeepSeq

520 , Idris.Core.DeepSeq

520 , Idris.Core.Elaborate

521 , Idris.Core.Elaborate

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

611 , annotated-wl-pprint >= 0.5.3

612 , annotated-wl-pprint >= 0.5.3

612 , ansi-terminal

613 , ansi-terminal

613 , ansi-wl-pprint

614 , ansi-wl-pprint

615+ , base64-bytestring

614 , binary

616 , binary

615 , blaze-html >= 0.6.1.3

617 , blaze-html >= 0.6.1.3

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

618 , 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)

1164 where colour BoldText = IdrisColour Nothing True False True False

1165 colour UnderlineText = IdrisColour Nothing True True False False

1166 colour ItalicText = IdrisColour Nothing True False False True

1167+consoleDecorate ist (AnnTerm _ _) = id

1167

1168

1168isPostulateName :: Name -> IState -> Bool

1169isPostulateName :: Name -> IState -> Bool

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

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

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

1174 -> Doc OutputAnnotation

1175 -> Doc OutputAnnotation

1175prettyImp impl = pprintPTerm impl [] [] []

1176prettyImp impl = pprintPTerm impl [] [] []

1176

1177

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

1179+

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

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

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

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

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

1182prettyIst 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/Evaluate.hs+15−2

@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTyName, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

11+ lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

@@ -868,8 +868,9 @@ lookupNames n ctxt

868 = let ns = lookupCtxtName n (definitions ctxt) in

869 map fst ns

870

871+-- | Get the list of pairs of fully-qualified names and their types that match some name

871lookupTyName :: Name -> Context -> [(Name, Type)]

872lookupTyName :: Name -> Context -> [(Name, Type)]

872−lookupTyName n ctxt = do

873+lookupTyName n ctxt = do

873 (name, def) <- lookupCtxtName n (definitions ctxt)

874 (name, def) <- lookupCtxtName n (definitions ctxt)

874 ty <- case tfst def of

875 ty <- case tfst def of

875 (Function ty _) -> return ty

876 (Function ty _) -> return ty

@@ -878,10 +879,22 @@ lookupTyName n ctxt = do

878 (CaseOp _ ty _ _ _ _) -> return ty

879 (CaseOp _ ty _ _ _ _) -> return ty

879 return (name, ty)

880 return (name, ty)

880

881

882+-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.

883+lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)

884+lookupTyNameExact n ctxt = case lookupTyName n ctxt of

885+ [x] -> Just x

886+ _ -> Nothing

881

887

888+-- | Get the types that match some name

882lookupTy :: Name -> Context -> [Type]

889lookupTy :: Name -> Context -> [Type]

883lookupTy n ctxt = map snd (lookupTyName n ctxt)

890lookupTy n ctxt = map snd (lookupTyName n ctxt)

884

891

892+-- | Get the single type that matches some name precisely

893+lookupTyExact :: Name -> Context -> Maybe Type

894+lookupTyExact n ctxt = case lookupTy n ctxt of

895+ [t] -> Just t

896+ _ -> Nothing

897+

885isConName :: Name -> Context -> Bool

898isConName :: Name -> Context -> Bool

886isConName n ctxt = isTConName n ctxt || isDConName n ctxt

899isConName n ctxt = isTConName n ctxt || isDConName n ctxt

887

900

src/Idris/Core/TT.hs+1

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

99 | AnnKeyword

100 | AnnFC FC

101 | AnnTextFmt TextFormatting

102+ | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term

102

103

103-- | Used for error reflection

104-- | Used for error reflection

104data ErrorReportPart = TextPart String

105data ErrorReportPart = TextPart String

src/Idris/Delaborate.hs+35−18

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

1{-# 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

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

5-- purposes.

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

135indented :: Doc a -> Doc a

136indented = nest errorIndent . (line <>)

137

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+

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

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

139pprintTerm ist = pprintTerm' ist []

153pprintTerm ist = pprintTerm' ist []

140

154

@@ -151,8 +165,8 @@ pprintErr' i (InternalMsg s) =

151 text ("Please consider reporting at " ++ bugaddr)

165 text ("Please consider reporting at " ++ bugaddr)

152 ]

166 ]

153pprintErr' i (CantUnify _ x y e sc s) =

167pprintErr' i (CantUnify _ x y e sc s) =

154− text "Can't unify" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x)) <$>

168+ text "Can't unify" <> indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x))) <$>

155− text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y)) <>

169+ text "with" <> indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y))) <>

156 case e of

170 case e of

157 Msg "" -> empty

171 Msg "" -> empty

158 _ -> line <> line <> text "Specifically:" <>

172 _ -> line <> line <> text "Specifically:" <>

@@ -160,46 +174,46 @@ pprintErr' i (CantUnify _ x y e sc s) =

160 if (opt_errContext (idris_options i)) then showSc i sc else empty

174 if (opt_errContext (idris_options i)) then showSc i sc else empty

161pprintErr' i (CantConvert x y env) =

175pprintErr' i (CantConvert x y env) =

162 text "Can't convert" <>

176 text "Can't convert" <>

163− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>

177+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <$>

164 text "with" <>

178 text "with" <>

165− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y)) <>

179+ indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y))) <>

166 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

180 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

167pprintErr' i (CantSolveGoal x env) =

181pprintErr' i (CantSolveGoal x env) =

168 text "Can't solve goal " <>

182 text "Can't solve goal " <>

169− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <>

183+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <>

170 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

184 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

171pprintErr' i (UnifyScope n out tm env) =

185pprintErr' i (UnifyScope n out tm env) =

172 text "Can't unify" <> indented (annName n) <+>

186 text "Can't unify" <> indented (annName n) <+>

173− text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>

187+ text "with" <> indented (annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm))) <+>

174− text "as" <> indented (annName out) <> text "is not in scope" <>

188+ text "as" <> indented (annName out) <> text "is not in scope" <>

175 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

189 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

176pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t

190pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t

177pprintErr' i (NonFunctionType f ty) =

191pprintErr' i (NonFunctionType f ty) =

178− pprintTerm i (delab i f) <+>

192+ annTm f (pprintTerm i (delab i f)) <+>

179 text "does not have a function type" <+>

193 text "does not have a function type" <+>

180 parens (pprintTerm i (delab i ty))

194 parens (pprintTerm i (delab i ty))

181pprintErr' i (NotEquality tm ty) =

195pprintErr' i (NotEquality tm ty) =

182− pprintTerm i (delab i tm) <+>

196+ annTm tm (pprintTerm i (delab i tm)) <+>

183 text "does not have an equality type" <+>

197 text "does not have an equality type" <+>

184− parens (pprintTerm i (delab i ty))

198+ annTm ty (parens (pprintTerm i (delab i ty)))

185pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f

199pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f

186pprintErr' i (CantIntroduce ty) =

200pprintErr' i (CantIntroduce ty) =

187− text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)

201+ text "Can't use lambda here: type is" <+> annTm ty (pprintTerm i (delab i ty))

188pprintErr' i (InfiniteUnify x tm env) =

202pprintErr' i (InfiniteUnify x tm env) =

189 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>

203 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>

190− pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>

204+ annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>

191 text "would lead to infinite value" <>

205 text "would lead to infinite value" <>

192 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

206 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

193pprintErr' i (NotInjective p x y) =

207pprintErr' i (NotInjective p x y) =

194− text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>

208+ text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>

195− text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>

209+ text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

196− pprintTerm i (delab i y)

210+ annTm y (pprintTerm i (delab i y))

197pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

211pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

198pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

212pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

199 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

213 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

200pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

214pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

201pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

215pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

202−pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

216+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

203pprintErr' i UniverseError = text "Universe inconsistency"

217pprintErr' i UniverseError = text "Universe inconsistency"

204pprintErr' i ProgramLineComment = text "Program line next to comment"

218pprintErr' i ProgramLineComment = text "Program line next to comment"

205pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

219pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

@@ -208,7 +222,7 @@ pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <

208pprintErr' i (AlreadyDefined n) = annName n<+>

222pprintErr' i (AlreadyDefined n) = annName n<+>

209 text "is already defined"

223 text "is already defined"

210pprintErr' i (ProofSearchFail e) = pprintErr' i e

224pprintErr' i (ProofSearchFail e) = pprintErr' i e

211−pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> pprintTerm i (delab i tm)

225+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delab i tm))

212pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e

226pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e

213pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

227pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

214 annName' n (showqual i n) <> colon <$>

228 annName' n (showqual i n) <> colon <$>

@@ -259,6 +273,9 @@ annName n = annName' n (showbasic n)

259annName' :: Name -> String -> Doc OutputAnnotation

273annName' :: Name -> String -> Doc OutputAnnotation

260annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

274annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

261

275

276+annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation

277+annTm tm = annotate (AnnTerm [] tm)

278+

262fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

279fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

263fancifyAnnots ist annot@(AnnName n _ _ _) =

280fancifyAnnots ist annot@(AnnName n _ _ _) =

264 do let ctxt = tt_ctxt ist

281 do let ctxt = tt_ctxt ist

src/Idris/IBC.hs+1−346

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

5import Idris.Core.Evaluate

6import Idris.Core.TT

7+import Idris.Core.Binary

7import Idris.Core.CaseTree

8import Idris.Core.CaseTree

8import Idris.AbsSyntax

9import Idris.AbsSyntax

9import Idris.Imports

10import Idris.Imports

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

617 x4 <- get

618 x4 <- get

618 x5 <- get

619 x5 <- get

619 return (CGInfo x1 x2 [] x4 x5)

620 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−

966instance Binary SC where

621instance Binary SC where

967 put x

622 put x

968 = case x of

623 = case x of

src/Idris/IdeSlave.hs+21

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

5import Text.Printf

6import Numeric

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

8import qualified Data.ByteString.UTF8 as UTF8

11import qualified Data.ByteString.UTF8 as UTF8

9-- import qualified Data.Text as T

12-- import qualified Data.Text as T

10import Text.Trifecta hiding (Err)

13import Text.Trifecta hiding (Err)

11import Text.Trifecta.Delta

14import Text.Trifecta.Delta

13import Idris.Core.TT

16import Idris.Core.TT

17+import Idris.Core.Binary

15import Control.Applicative hiding (Const)

19import Control.Applicative hiding (Const)

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

128 BoldText -> "bold"

132 BoldText -> "bold"

129 ItalicText -> "italic"

133 ItalicText -> "italic"

130 UnderlineText -> "underline"

134 UnderlineText -> "underline"

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

136+

137+encodeTerm :: [(Name, Bool)] -> Term -> String

138+encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

139+ (bnd, tm)

140+

141+decodeTerm :: String -> ([(Name, Bool)], Term)

142+decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

131

143

132instance SExpable FC where

144instance SExpable FC where

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

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

@@ -185,6 +197,9 @@ data IdeSlaveCommand = REPLCompletions String

185 | Metavariables Int -- ^^ the Int is the column count for pretty-printing

197 | Metavariables Int -- ^^ the Int is the column count for pretty-printing

186 | WhoCalls String

198 | WhoCalls String

187 | CallsWho String

199 | CallsWho String

200+ | TermNormalise [(Name, Bool)] Term

201+ | TermShowImplicits [(Name, Bool)] Term

202+ | TermNoImplicits [(Name, Bool)] Term

188

203

189sexpToCommand :: SExp -> Maybe IdeSlaveCommand

204sexpToCommand :: SExp -> Maybe IdeSlaveCommand

190sexpToCommand (SexpList (x:[])) = sexpToCommand x

205sexpToCommand (SexpList (x:[])) = sexpToCommand x

@@ -221,6 +236,12 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

221sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

236sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

222sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)

237sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)

223sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)

238sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)

239+sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

240+ Just (TermNormalise bnd tm)

241+sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

242+ Just (TermShowImplicits bnd tm)

243+sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

244+ Just (TermNoImplicits bnd tm)

224sexpToCommand _ = Nothing

245sexpToCommand _ = Nothing

225

246

226parseMessage :: String -> Either Err (SExp, Integer)

247parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/Prover.hs+3−1

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

121 where

122 ppo = ppOptionIst ist

123

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

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

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

126+ delab ist t

125

127

126 assumptionNames :: Env -> [Name]

128 assumptionNames :: Env -> [Name]

127 assumptionNames = map fst

129 assumptionNames = map fst

src/Idris/REPL.hs+95−32

@@ -342,34 +342,63 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

342 do ist <- getIState

343 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

344 let ppo = ppOptionIst ist

345− let mvarTys = map (delabTy ist) mvs

345+ -- splitMvs is a list of pairs of names and their split types

346− let res = (IdeSlave.SymbolAtom "ok",

346+ let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)

347− zipWith (\ n (prems, concl) -> (n, prems, concl))

347+ -- mvOutput is the pretty-printed version ready for conversion to SExpr

348− (map (IdeSlave.StringAtom . show) mvs)

348+ let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $

349− (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))

349+ mapPair show

350+ (\(hs, c, pc) ->

351+ let bnd = [ n | (n,_,_) <- hs ] in

352+ let bnds = inits bnd in

353+ (map (\(bnd, h) -> processPremise ist bnd h)

354+ (zip bnds hs),

355+ render ist bnd c pc))

356+ splitMvs

357+ runIO . putStrLn $

350− runIO . putStrLn $ IdeSlave.convSExp "return" res id

358+ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id

351− where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

359+ where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)

352− getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

360+ mapSnd f xs = zip (map fst xs) (map (f . snd) xs)

353− in ((n, t):prems, conc)

361+

354− getGoal tm = ([], tm)

362+ -- | Split a function type into a pair of premises, conclusion.

355− sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)

363+ -- Each maintains both the original and delaborated versions.

356− -> ([(String, String, SpanList OutputAnnotation)],

364+ splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

357− (String, SpanList OutputAnnotation))

365+ splitPi ist (Bind n (Pi t) rest) =

358− sexpGoal ist cols ppo ns ([], concl) =

366+ let (hs, c, pc) = splitPi ist rest in

359− let infixes = idris_infixes ist

367+ ((n, t, delabTy' ist [] t False False):hs,

360− concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

368+ c, delabTy' ist [] c False False)

361− pprintPTerm ppo (zip ns (repeat False)) [] infixes concl

369+ splitPi ist tm = ([], tm, delabTy' ist [] tm False False)

362− in ([], concl')

370+

363− sexpGoal ist cols ppo ns ((n, t):ps, concl) =

371+ -- | Get the types of a list of metavariable names

364− let n' = case n of

372+ mvTys :: IState -> [Name] -> [(Name, Type)]

365− NS (UN nm) ns -> str nm

373+ mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))

366− UN nm | ('_':'_':_) <- str nm -> "_"

374+

367− | otherwise -> str nm

375+ -- | Show a type and its corresponding PTerm in a format suitable

368− _ -> "_"

376+ -- for the IDE - that is, pretty-printed and annotated.

377+ render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)

378+ render ist bnd t pt =

379+ let prettyT = pprintPTerm (ppOptionIst ist)

380+ (zip bnd (repeat False))

381+ []

382+ (idris_infixes ist)

383+ pt

384+ in

385+ displaySpans .

386+ renderPretty 0.9 cols .

369− (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

387+ fmap (fancifyAnnots ist) .

370− pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t

388+ annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $

371− rest = sexpGoal ist cols ppo (n:ns) (ps, concl)

389+ prettyT

372− in ((n', t', spans) : fst rest, snd rest)

390+

391+ -- | Juggle the bits of a premise to prepare for output.

392+ processPremise :: IState

393+ -> [Name] -- ^ the names to highlight as bound

394+ -> (Name, Type, PTerm)

395+ -> (String,

396+ String,

397+ SpanList OutputAnnotation)

398+ processPremise ist bnd (n, t, pt) =

399+ let (out, spans) = render ist bnd t pt in

400+ (show n , out, spans)

401+

373runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

402runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

374 case splitName n of

403 case splitName n of

375 Left err -> iPrintError err

404 Left err -> iPrintError err

@@ -394,6 +423,40 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =

394 renderPretty 0.9 1000 .

423 renderPretty 0.9 1000 .

395 fmap (fancifyAnnots ist) .

424 fmap (fancifyAnnots ist) .

396 prettyName True []

425 prettyName True []

426+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =

427+ do ctxt <- getContext

428+ ist <- getIState

429+ let tm' = force (normaliseAll ctxt [] tm)

430+ ptm = annotate (AnnTerm bnd tm')

431+ (pprintPTerm (ppOptionIst ist)

432+ bnd

433+ []

434+ (idris_infixes ist)

435+ (delab ist tm'))

436+ msg = (IdeSlave.SymbolAtom "ok",

437+ displaySpans .

438+ renderPretty 0.9 80 .

439+ fmap (fancifyAnnots ist) $ ptm)

440+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

441+runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =

442+ ideSlaveForceTermImplicits id bnd True tm

443+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =

444+ ideSlaveForceTermImplicits id bnd False tm

445+

446+-- | Show a term for IDESlave with the specified implicitness

447+ideSlaveForceTermImplicits :: Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

448+ideSlaveForceTermImplicits id bnd impl tm =

449+ do ist <- getIState

450+ let expl = annotate (AnnTerm bnd tm)

451+ (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })

452+ bnd [] (idris_infixes ist)

453+ (delab ist tm))

454+ msg = (IdeSlave.SymbolAtom "ok",

455+ displaySpans .

456+ renderPretty 0.9 80 .

457+ fmap (fancifyAnnots ist) $ expl)

458+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

459+

397

460

398splitName :: String -> Either String Name

461splitName :: String -> Either String Name

399splitName s = case reverse $ splitOn "." s of

462splitName s = case reverse $ splitOn "." s of

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

594 ist <- getIState

657 ist <- getIState

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

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

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

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

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

660+ let tmDoc = pprintDelab ist tm'

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

661+ tyDoc = pprintDelab ist ty'

599 ihPrintTermWithType h tmDoc tyDoc

662 ihPrintTermWithType h tmDoc tyDoc

600

663

601process h fn (ExecVal t)

664process h fn (ExecVal t)

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

653 case tm of

716 case tm of

654 TType _ ->

717 TType _ ->

655 ihPrintTermWithType h (prettyIst ist PType) type1Doc

718 ihPrintTermWithType h (prettyIst ist PType) type1Doc

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

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

657− (prettyIst ist (delab ist ty))

720+ (pprintDelab ist ty)

658

721

659process h fn (DocStr (Left n))

722process h fn (DocStr (Left n))

660 = do ist <- getIState

723 = do ist <- getIState