git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1315 from david-christiansen/serialized-terms

Serialize original TT terms, and annotate pretty-printer output

commitcebd1b4384e999bd34ce14e2a27fc00d114c3bf5 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 16 Jun 2014, 00:14 (12 years ago) parentbc88c8a144dfcf
10 files changed+533−400
compare with master
unifiedsplit
idris.cabal+3−1 src/Idris/AbsSyntaxTree.hs+3 src/Idris/Core/Binary.hs+356 src/Idris/Core/Evaluate.hs+15−2 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+35−18 src/Idris/IBC.hs+1−346 src/Idris/IdeSlave.hs+21 src/Idris/Prover.hs+3−1 src/Idris/REPL.hs+95−32
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
3+
4+import Data.Binary
5+import Data.Vector.Binary
6+import qualified Data.Text as T
7+
8+import Idris.Core.TT
9+
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,
88 Context, initContext, ctxtAlist, uconstraints, next_tvar,
99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
1010 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,
1212 mapDefCtxt,
1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
1414 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where
@@ -868,8 +868,9 @@ lookupNames n ctxt
868868 = let ns = lookupCtxtName n (definitions ctxt) in
869869 map fst ns
870870
871+-- | Get the list of pairs of fully-qualified names and their types that match some name
871872lookupTyName :: Name -> Context -> [(Name, Type)]
872−lookupTyName n ctxt = do
873+lookupTyName n ctxt = do
873874 (name, def) <- lookupCtxtName n (definitions ctxt)
874875 ty <- case tfst def of
875876 (Function ty _) -> return ty
@@ -878,10 +879,22 @@ lookupTyName n ctxt = do
878879 (CaseOp _ ty _ _ _ _) -> return ty
879880 return (name, ty)
880881
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
881887
888+-- | Get the types that match some name
882889lookupTy :: Name -> Context -> [Type]
883890lookupTy n ctxt = map snd (lookupTyName n ctxt)
884891
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+
885898isConName :: Name -> Context -> Bool
886899isConName n ctxt = isTConName n ctxt || isDConName n ctxt
887900
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 [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
102103
103104-- | Used for error reflection
104105data ErrorReportPart = TextPart String
src/Idris/Delaborate.hs+35−18
@@ -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
33
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
@@ -151,8 +165,8 @@ pprintErr' i (InternalMsg s) =
151165 text ("Please consider reporting at " ++ bugaddr)
152166 ]
153167pprintErr' i (CantUnify _ x y e sc s) =
154− text "Can't unify" <> indented (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)) <>
168+ text "Can't unify" <> indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x))) <$>
169+ text "with" <> indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y))) <>
156170 case e of
157171 Msg "" -> empty
158172 _ -> line <> line <> text "Specifically:" <>
@@ -160,46 +174,46 @@ pprintErr' i (CantUnify _ x y e sc s) =
160174 if (opt_errContext (idris_options i)) then showSc i sc else empty
161175pprintErr' i (CantConvert x y env) =
162176 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))) <$>
164178 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))) <>
166180 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
167181pprintErr' i (CantSolveGoal x env) =
168182 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))) <>
170184 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
171185pprintErr' i (UnifyScope n out tm env) =
172186 text "Can't unify" <> indented (annName n) <+>
173− text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
174− text "as" <> indented (annName out) <> text "is not in scope" <>
187+ text "with" <> indented (annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm))) <+>
188+ text "as" <> indented (annName out) <> text "is not in scope" <>
175189 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
176190pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
177191pprintErr' i (NonFunctionType f ty) =
178− pprintTerm i (delab i f) <+>
192+ annTm f (pprintTerm i (delab i f)) <+>
179193 text "does not have a function type" <+>
180194 parens (pprintTerm i (delab i ty))
181195pprintErr' i (NotEquality tm ty) =
182− pprintTerm i (delab i tm) <+>
196+ annTm tm (pprintTerm i (delab i tm)) <+>
183197 text "does not have an equality type" <+>
184− parens (pprintTerm i (delab i ty))
198+ annTm ty (parens (pprintTerm i (delab i ty)))
185199pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
186200pprintErr' 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))
188202pprintErr' i (InfiniteUnify x tm env) =
189203 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)) <+>
191205 text "would lead to infinite value" <>
192206 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
193207pprintErr' i (NotInjective p x y) =
194− text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
195− text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
196− pprintTerm i (delab i y)
208+ text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>
209+ text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>
210+ annTm y (pprintTerm i (delab i y))
197211pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
198212pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
199213 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))
200214pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
201215pprintErr' 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))
203217pprintErr' i UniverseError = text "Universe inconsistency"
204218pprintErr' i ProgramLineComment = text "Program line next to comment"
205219pprintErr' 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" <
208222pprintErr' i (AlreadyDefined n) = annName n<+>
209223 text "is already defined"
210224pprintErr' 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))
212226pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
213227pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
214228 annName' n (showqual i n) <> colon <$>
@@ -259,6 +273,9 @@ annName n = annName' n (showbasic n)
259273annName' :: Name -> String -> Doc OutputAnnotation
260274annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)
261275
276+annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
277+annTm tm = annotate (AnnTerm [] tm)
278+
262279fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
263280fancifyAnnots ist annot@(AnnName n _ _ _) =
264281 do let ctxt = tt_ctxt ist
src/Idris/IBC.hs+1−346
@@ -4,6 +4,7 @@ module Idris.IBC where
44
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+21
@@ -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,14 @@ instance SExpable OutputAnnotation where
128132 BoldText -> "bold"
129133 ItalicText -> "italic"
130134 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
131143
132144instance SExpable FC where
133145 toSExp (FC f (sl, sc) (el, ec)) =
@@ -185,6 +197,9 @@ data IdeSlaveCommand = REPLCompletions String
185197 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
186198 | WhoCalls String
187199 | CallsWho String
200+ | TermNormalise [(Name, Bool)] Term
201+ | TermShowImplicits [(Name, Bool)] Term
202+ | TermNoImplicits [(Name, Bool)] Term
188203
189204sexpToCommand :: SExp -> Maybe IdeSlaveCommand
190205sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -221,6 +236,12 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
221236sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
222237sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
223238sexpToCommand (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)
224245sexpToCommand _ = Nothing
225246
226247parseMessage :: 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 _ _ _ _) =
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 bnd 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+95−32
@@ -342,34 +342,63 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
342342 do ist <- getIState
343343 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
344344 let ppo = ppOptionIst ist
345− let mvarTys = map (delabTy ist) mvs
346− let res = (IdeSlave.SymbolAtom "ok",
347− zipWith (\ n (prems, concl) -> (n, prems, concl))
348− (map (IdeSlave.StringAtom . show) mvs)
349− (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
350− runIO . putStrLn $ IdeSlave.convSExp "return" res id
351− where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
352− getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
353− in ((n, t):prems, conc)
354− getGoal tm = ([], tm)
355− sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
356− -> ([(String, String, SpanList OutputAnnotation)],
357− (String, SpanList OutputAnnotation))
358− sexpGoal ist cols ppo ns ([], concl) =
359− let infixes = idris_infixes ist
360− concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
361− pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
362− in ([], concl')
363− sexpGoal ist cols ppo ns ((n, t):ps, concl) =
364− let n' = case n of
365− NS (UN nm) ns -> str nm
366− UN nm | ('_':'_':_) <- str nm -> "_"
367− | otherwise -> str nm
368− _ -> "_"
369− (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
370− pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
371− rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
372− in ((n', t', spans) : fst rest, snd rest)
345+ -- splitMvs is a list of pairs of names and their split types
346+ let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)
347+ -- mvOutput is the pretty-printed version ready for conversion to SExpr
348+ let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
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 $
358+ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id
359+ where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
360+ mapSnd f xs = zip (map fst xs) (map (f . snd) xs)
361+
362+ -- | Split a function type into a pair of premises, conclusion.
363+ -- Each maintains both the original and delaborated versions.
364+ splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
365+ splitPi ist (Bind n (Pi t) rest) =
366+ let (hs, c, pc) = splitPi ist rest in
367+ ((n, t, delabTy' ist [] t False False):hs,
368+ c, delabTy' ist [] c False False)
369+ splitPi ist tm = ([], tm, delabTy' ist [] tm False False)
370+
371+ -- | Get the types of a list of metavariable names
372+ mvTys :: IState -> [Name] -> [(Name, Type)]
373+ mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))
374+
375+ -- | Show a type and its corresponding PTerm in a format suitable
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 .
387+ fmap (fancifyAnnots ist) .
388+ annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $
389+ prettyT
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+
373402runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
374403 case splitName n of
375404 Left err -> iPrintError err
@@ -394,6 +423,40 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
394423 renderPretty 0.9 1000 .
395424 fmap (fancifyAnnots ist) .
396425 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+
397460
398461splitName :: String -> Either String Name
399462splitName s = case reverse $ splitOn "." s of
@@ -594,8 +657,8 @@ process h fn (Eval t)
594657 ist <- getIState
595658 logLvl 3 $ "Raw: " ++ show (tm', ty')
596659 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
597− let tmDoc = prettyIst ist (delab ist tm')
598− tyDoc = prettyIst ist (delab ist ty')
660+ let tmDoc = pprintDelab ist tm'
661+ tyDoc = pprintDelab ist ty'
599662 ihPrintTermWithType h tmDoc tyDoc
600663
601664process h fn (ExecVal t)
@@ -653,8 +716,8 @@ process h fn (Check t)
653716 case tm of
654717 TType _ ->
655718 ihPrintTermWithType h (prettyIst ist PType) type1Doc
656− _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))
657− (prettyIst ist (delab ist ty))
719+ _ -> ihPrintTermWithType h (pprintDelab ist tm)
720+ (pprintDelab ist ty)
658721
659722process h fn (DocStr (Left n))
660723 = do ist <- getIState