@@ -1,6 +1,6 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where
3+module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabSugared, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr, resugar) where
5-- Convert core TT back into high level syntax, primarily for display
5-- Convert core TT back into high level syntax, primarily for display
6-- purposes.
6-- purposes.
@@ -15,6 +15,7 @@ import Idris.ErrReverse
16import Prelude hiding ((<$>))
16import Prelude hiding ((<$>))
18+import Data.Generics.Uniplate.Data (transform)
18import Data.Maybe (mapMaybe)
19import Data.Maybe (mapMaybe)
19import Data.List (intersperse, nub)
20import Data.List (intersperse, nub)
20import qualified Data.Text as T
21import qualified Data.Text as T
@@ -24,6 +25,26 @@ import Debug.Trace
25bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
26bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
28+-- | Re-add syntactic sugar in a term
29+resugar :: PTerm -> PTerm
30+resugar = transform resugarApp
32+ resugarApp (PApp fc (PRef _ n) args)
33+ | [c, t, f] <- mapMaybe explicitTerm args
34+ , basename n == sUN "ifThenElse"
35+ = PIfThenElse fc c (dedelay t) (dedelay f)
37+ dedelay (PApp _ (PRef _ delay) [_, _, obj])
38+ | delay == sUN "Delay" = getTm obj
40+ explicitTerm (PExp {getTm = tm}) = Just tm
41+ explicitTerm _ = Nothing
43+-- | Delaborate and resugar a term
44+delabSugared :: IState -> Term -> PTerm
45+delabSugared ist tm = resugar $ delab ist tm
47+-- | Delaborate a term without resugaring
27delab :: IState -> Term -> PTerm
48delab :: IState -> Term -> PTerm
28delab i tm = delab' i tm False False
49delab i tm = delab' i tm False False
@@ -50,7 +71,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
51 un = fileFC "(val)"
72 un = fileFC "(val)"
53− de env _ (App _ f a) = resugarApp env $ deFn env f [a]
74+ de env _ (App _ f a) = deFn env f [a]
54 de env _ (V i) | i < length env = PRef un (snd (env!!i))
75 de env _ (V i) | i < length env = PRef un (snd (env!!i))
55 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))
76 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))
56 de env _ (P _ n _) | n == unitTy = PTrue un IsType
77 de env _ (P _ n _) | n == unitTy = PTrue un IsType
@@ -147,17 +168,6 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
147 isCN (SN (CaseN _)) = True
168 isCN (SN (CaseN _)) = True
148 isCN _ = False
169 isCN _ = False
150− resugarApp env (PApp _ (PRef _ n) args)
151− | [c, t, f] <- mapMaybe explicitTerm args
152− , basename n == sUN "ifThenElse"
153− = PIfThenElse un c (dedelay t) (dedelay f)
154− where dedelay (PApp _ (PRef _ delay) [_, _, obj])
155− | delay == sUN "Delay" = getTm obj
157− explicitTerm (PExp {getTm = tm}) = Just tm
158− explicitTerm _ = Nothing
159− resugarApp env tm = tm
161 delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm
171 delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm
162 delabCase env imps scvar scrutinee caseName caseArgs =
172 delabCase env imps scvar scrutinee caseName caseArgs =
163 do cases <- case lookupCtxt caseName (idris_patdefs ist) of
173 do cases <- case lookupCtxt caseName (idris_patdefs ist) of
@@ -187,7 +197,7 @@ indented = nest errorIndent . (line <>)
187-- | Pretty-print a core term using delaboration
197-- | Pretty-print a core term using delaboration
188pprintDelab :: IState -> Term -> Doc OutputAnnotation
198pprintDelab :: IState -> Term -> Doc OutputAnnotation
189pprintDelab ist tm = annotate (AnnTerm [] tm)
199pprintDelab ist tm = annotate (AnnTerm [] tm)
190− (prettyIst ist (delab ist tm))
200+ (prettyIst ist (delabSugared ist tm))
192-- | Pretty-print the type of some name
202-- | Pretty-print the type of some name
193pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
203pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
@@ -195,8 +205,8 @@ pprintDelabTy i n
195 = case lookupTy n (tt_ctxt i) of
205 = case lookupTy n (tt_ctxt i) of
196 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
206 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
197 case lookupCtxt n (idris_implicits i) of
207 case lookupCtxt n (idris_implicits i) of
198− (imps:_) -> delabTy' i imps ty False False
208+ (imps:_) -> resugar $ delabTy' i imps ty False False
199− _ -> delabTy' i [] ty False False
209+ _ -> resugar $ delabTy' i [] ty False False
200 [] -> error "pprintDelabTy got a name that doesn't exist"
210 [] -> error "pprintDelabTy got a name that doesn't exist"
202pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
212pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
@@ -212,11 +222,11 @@ pprintProv i e GivenVal = text "Given value"
212pprintProv i e (SourceTerm tm)
222pprintProv i e (SourceTerm tm)
213 = text "Type of " <>
223 = text "Type of " <>
214 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
224 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
215− (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))
225+ (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))
216pprintProv i e (TooManyArgs tm)
226pprintProv i e (TooManyArgs tm)
217 = text "Is " <>
227 = text "Is " <>
218 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
228 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
219− (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))
229+ (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))
220 <> text " applied to too many arguments?"
230 <> text " applied to too many arguments?"
222pprintErr :: IState -> Err -> Doc OutputAnnotation
232pprintErr :: IState -> Err -> Doc OutputAnnotation
@@ -230,7 +240,7 @@ pprintErr' i (InternalMsg s) =
231pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
241pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
232 let (x_ns, y_ns, nms) = renameMNs x_in y_in
242 let (x_ns, y_ns, nms) = renameMNs x_in y_in
233− (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in
243+ (x, y) = addImplicitDiffs (delabSugared i x_ns) (delabSugared i y_ns) in
234 text "Type mismatch between" <> indented (annTm x_ns
244 text "Type mismatch between" <> indented (annTm x_ns
235 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
245 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
236 ++ zip nms (repeat False)) x))
246 ++ zip nms (repeat False)) x))
@@ -255,8 +265,8 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
255 if (opt_errContext (idris_options i)) then showSc i sc else empty
265 if (opt_errContext (idris_options i)) then showSc i sc else empty
256pprintErr' i (CantConvert x_in y_in env) =
266pprintErr' i (CantConvert x_in y_in env) =
257 let (x_ns, y_ns, nms) = renameMNs x_in y_in
267 let (x_ns, y_ns, nms) = renameMNs x_in y_in
258− (x, y) = addImplicitDiffs (delab i (flagUnique x_ns))
268+ (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))
259− (delab i (flagUnique y_ns)) in
269+ (delabSugared i (flagUnique y_ns)) in
260 text "Type mismatch between" <>
270 text "Type mismatch between" <>
261 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
271 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
@@ -272,37 +282,37 @@ pprintErr' i (CantConvert x_in y_in env) =
272 flagUnique t = t
282 flagUnique t = t
273pprintErr' i (CantSolveGoal x env) =
283pprintErr' i (CantSolveGoal x env) =
274 text "Can't solve goal " <>
284 text "Can't solve goal " <>
275− indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <>
285+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delabSugared i x))) <>
276 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
286 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
277pprintErr' i (UnifyScope n out tm env) =
287pprintErr' i (UnifyScope n out tm env) =
278 text "Can't unify" <> indented (annName n) <+>
288 text "Can't unify" <> indented (annName n) <+>
279− text "with" <> indented (annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm))) <+>
289+ text "with" <> indented (annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delabSugared i tm))) <+>
280 text "as" <> indented (annName out) <> text "is not in scope" <>
290 text "as" <> indented (annName out) <> text "is not in scope" <>
281 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
291 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
282pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
292pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
283pprintErr' i (NonFunctionType f ty) =
293pprintErr' i (NonFunctionType f ty) =
284− annTm f (pprintTerm i (delab i f)) <+>
294+ annTm f (pprintTerm i (delabSugared i f)) <+>
285 text "does not have a function type" <+>
295 text "does not have a function type" <+>
286− parens (pprintTerm i (delab i ty))
296+ parens (pprintTerm i (delabSugared i ty))
287pprintErr' i (NotEquality tm ty) =
297pprintErr' i (NotEquality tm ty) =
288− annTm tm (pprintTerm i (delab i tm)) <+>
298+ annTm tm (pprintTerm i (delabSugared i tm)) <+>
289 text "does not have an equality type" <+>
299 text "does not have an equality type" <+>
290− annTm ty (parens (pprintTerm i (delab i ty)))
300+ annTm ty (parens (pprintTerm i (delabSugared i ty)))
291pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
301pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
292pprintErr' i (CantIntroduce ty) =
302pprintErr' i (CantIntroduce ty) =
293− text "Can't use lambda here: type is" <+> annTm ty (pprintTerm i (delab i ty))
303+ text "Can't use lambda here: type is" <+> annTm ty (pprintTerm i (delabSugared i ty))
294pprintErr' i (InfiniteUnify x tm env) =
304pprintErr' i (InfiniteUnify x tm env) =
295 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
305 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
296− annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
306+ annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delabSugared i tm)) <+>
297 text "would lead to infinite value" <>
307 text "would lead to infinite value" <>
298 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
308 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
299pprintErr' i (NotInjective p x y) =
309pprintErr' i (NotInjective p x y) =
300− text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>
310+ text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delabSugared i p)) <+>
301− text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>
311+ text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>
302− annTm y (pprintTerm i (delab i y))
312+ annTm y (pprintTerm i (delabSugared i y))
303−pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
313+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delabSugared i c)
304pprintErr' i (InvalidTCArg n t)
314pprintErr' i (InvalidTCArg n t)
305− = annTm t (pprintTerm i (delab i t)) <+> text " cannot be a parameter of "
315+ = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "
306 <> annName n <$>
316 <> annName n <$>
307 text "(Type class arguments must be injective)"
317 text "(Type class arguments must be injective)"
308pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
318pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
@@ -310,13 +320,13 @@ pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
310pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
320pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
311pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
321pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
312pprintErr' i (WithFnType ty) =
322pprintErr' i (WithFnType ty) =
313− text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delab i ty))
323+ text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delabSugared i ty))
314pprintErr' i (CantMatch t) =
324pprintErr' i (CantMatch t) =
315− text "Can't match on" <+> annTm t (pprintTerm i (delab i t))
325+ text "Can't match on" <+> annTm t (pprintTerm i (delabSugared i t))
316−pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))
326+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))
317pprintErr' i (NoEliminator s t)
327pprintErr' i (NoEliminator s t)
318 = text "No " <> text s <> text " for type " <+>
328 = text "No " <> text s <> text " for type " <+>
319− annTm t (pprintTerm i (delab i t)) <$>
329+ annTm t (pprintTerm i (delabSugared i t)) <$>
320 text "Please note that 'induction' is experimental." <$>
330 text "Please note that 'induction' is experimental." <$>
321 text "Only types declared with '%elim' can be used." <$>
331 text "Only types declared with '%elim' can be used." <$>
322 text "Consider writing a pattern matching definition instead."
332 text "Consider writing a pattern matching definition instead."
@@ -344,7 +354,7 @@ pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <
344pprintErr' i (AlreadyDefined n) = annName n<+>
354pprintErr' i (AlreadyDefined n) = annName n<+>
345 text "is already defined"
355 text "is already defined"
346pprintErr' i (ProofSearchFail e) = pprintErr' i e
356pprintErr' i (ProofSearchFail e) = pprintErr' i e
347−pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delab i tm))
357+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delabSugared i tm))
348pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
358pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
349pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
359pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
350 annName' n (showqual i n) <> colon <$>
360 annName' n (showqual i n) <> colon <$>
@@ -384,7 +394,7 @@ pprintErr' i (ReflectionError parts orig) =
384 where showPart :: ErrorReportPart -> Doc OutputAnnotation
394 where showPart :: ErrorReportPart -> Doc OutputAnnotation
385 showPart (TextPart str) = fillSep . map text . words $ str
395 showPart (TextPart str) = fillSep . map text . words $ str
386 showPart (NamePart n) = annName n
396 showPart (NamePart n) = annName n
387− showPart (TermPart tm) = pprintTerm i (delab i tm)
397+ showPart (TermPart tm) = pprintTerm i (delabSugared i tm)
388 showPart (SubReport rs) = indented . hsep . map showPart $ rs
398 showPart (SubReport rs) = indented . hsep . map showPart $ rs
389pprintErr' i (ReflectionFailed msg err) =
399pprintErr' i (ReflectionFailed msg err) =
390 text "When attempting to perform error reflection, the following internal error occurred:" <>
400 text "When attempting to perform error reflection, the following internal error occurred:" <>
@@ -554,7 +564,7 @@ fancifyAnnots ist meta annot@(AnnName n _ _ _) =
554 return (out "")
564 return (out "")
555 getTy :: IState -> Name -> String -- fails if name not already extant!
565 getTy :: IState -> Name -> String -- fails if name not already extant!
556 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
566 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
557− delabTy ist n
567+ resugar $ delabTy ist n
558 in (displayS . renderPretty 1.0 50 $ theTy) ""
568 in (displayS . renderPretty 1.0 50 $ theTy) ""
559fancifyAnnots _ _ annot = annot
569fancifyAnnots _ _ annot = annot
@@ -564,7 +574,7 @@ showSc i xs = line <> line <> text "In context:" <>
564 indented (vsep (reverse (showSc' [] xs)))
574 indented (vsep (reverse (showSc' [] xs)))
565 where showSc' bnd [] = []
575 where showSc' bnd [] = []
566 showSc' bnd ((n, ty):ctxt) =
576 showSc' bnd ((n, ty):ctxt) =
567− let this = bindingOf n False <+> colon <+> pprintTerm' i bnd (delab i ty)
577+ let this = bindingOf n False <+> colon <+> pprintTerm' i bnd (delabSugared i ty)
568 in this : showSc' ((n,False):bnd) ctxt
578 in this : showSc' ((n,False):bnd) ctxt