@@ -1,6 +1,6 @@
11{-# LANGUAGE PatternGuards #-}
22{-# 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
44
55-- Convert core TT back into high level syntax, primarily for display
66-- purposes.
@@ -15,6 +15,7 @@ import Idris.ErrReverse
1515
1616import Prelude hiding ((<$>))
1717
18+import Data.Generics.Uniplate.Data (transform)
1819import Data.Maybe (mapMaybe)
1920import Data.List (intersperse, nub)
2021import qualified Data.Text as T
@@ -24,6 +25,26 @@ import Debug.Trace
2425
2526bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
2627
28+-- | Re-add syntactic sugar in a term
29+resugar :: PTerm -> PTerm
30+resugar = transform resugarApp
31+ where
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)
36+ resugarApp tm = tm
37+ dedelay (PApp _ (PRef _ delay) [_, _, obj])
38+ | delay == sUN "Delay" = getTm obj
39+ dedelay x = x
40+ explicitTerm (PExp {getTm = tm}) = Just tm
41+ explicitTerm _ = Nothing
42+
43+-- | Delaborate and resugar a term
44+delabSugared :: IState -> Term -> PTerm
45+delabSugared ist tm = resugar $ delab ist tm
46+
47+-- | Delaborate a term without resugaring
2748delab :: IState -> Term -> PTerm
2849delab i tm = delab' i tm False False
2950
@@ -50,7 +71,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
5071 where
5172 un = fileFC "(val)"
5273
53− de env _ (App _ f a) = resugarApp env $ deFn env f [a]
74+ de env _ (App _ f a) = deFn env f [a]
5475 de env _ (V i) | i < length env = PRef un (snd (env!!i))
5576 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))
5677 de env _ (P _ n _) | n == unitTy = PTrue un IsType
@@ -147,17 +168,6 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
147168 isCN (SN (CaseN _)) = True
148169 isCN _ = False
149170
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
156− dedelay x = x
157− explicitTerm (PExp {getTm = tm}) = Just tm
158− explicitTerm _ = Nothing
159− resugarApp env tm = tm
160−
161171 delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm
162172 delabCase env imps scvar scrutinee caseName caseArgs =
163173 do cases <- case lookupCtxt caseName (idris_patdefs ist) of
@@ -187,7 +197,7 @@ indented = nest errorIndent . (line <>)
187197-- | Pretty-print a core term using delaboration
188198pprintDelab :: IState -> Term -> Doc OutputAnnotation
189199pprintDelab ist tm = annotate (AnnTerm [] tm)
190− (prettyIst ist (delab ist tm))
200+ (prettyIst ist (delabSugared ist tm))
191201
192202-- | Pretty-print the type of some name
193203pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
@@ -195,8 +205,8 @@ pprintDelabTy i n
195205 = case lookupTy n (tt_ctxt i) of
196206 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
197207 case lookupCtxt n (idris_implicits i) of
198− (imps:_) -> delabTy' i imps ty False False
199− _ -> delabTy' i [] ty False False
208+ (imps:_) -> resugar $ delabTy' i imps ty False False
209+ _ -> resugar $ delabTy' i [] ty False False
200210 [] -> error "pprintDelabTy got a name that doesn't exist"
201211
202212pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
@@ -212,11 +222,11 @@ pprintProv i e GivenVal = text "Given value"
212222pprintProv i e (SourceTerm tm)
213223 = text "Type of " <>
214224 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))
216226pprintProv i e (TooManyArgs tm)
217227 = text "Is " <>
218228 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))
220230 <> text " applied to too many arguments?"
221231
222232pprintErr :: IState -> Err -> Doc OutputAnnotation
@@ -230,7 +240,7 @@ pprintErr' i (InternalMsg s) =
230240 ]
231241pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
232242 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
234244 text "Type mismatch between" <> indented (annTm x_ns
235245 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
236246 ++ zip nms (repeat False)) x))
@@ -255,8 +265,8 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
255265 if (opt_errContext (idris_options i)) then showSc i sc else empty
256266pprintErr' i (CantConvert x_in y_in env) =
257267 let (x_ns, y_ns, nms) = renameMNs x_in y_in
258− (x, y) = addImplicitDiffs (delab i (flagUnique x_ns))
259− (delab i (flagUnique y_ns)) in
268+ (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))
269+ (delabSugared i (flagUnique y_ns)) in
260270 text "Type mismatch between" <>
261271 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
262272 x)) <$>
@@ -272,37 +282,37 @@ pprintErr' i (CantConvert x_in y_in env) =
272282 flagUnique t = t
273283pprintErr' i (CantSolveGoal x env) =
274284 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))) <>
276286 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
277287pprintErr' i (UnifyScope n out tm env) =
278288 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))) <+>
280290 text "as" <> indented (annName out) <> text "is not in scope" <>
281291 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
282292pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
283293pprintErr' i (NonFunctionType f ty) =
284− annTm f (pprintTerm i (delab i f)) <+>
294+ annTm f (pprintTerm i (delabSugared i f)) <+>
285295 text "does not have a function type" <+>
286− parens (pprintTerm i (delab i ty))
296+ parens (pprintTerm i (delabSugared i ty))
287297pprintErr' i (NotEquality tm ty) =
288− annTm tm (pprintTerm i (delab i tm)) <+>
298+ annTm tm (pprintTerm i (delabSugared i tm)) <+>
289299 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)))
291301pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
292302pprintErr' 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))
294304pprintErr' i (InfiniteUnify x tm env) =
295305 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)) <+>
297307 text "would lead to infinite value" <>
298308 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
299309pprintErr' i (NotInjective p x y) =
300− text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>
301− text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>
302− annTm y (pprintTerm i (delab i y))
303−pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
310+ text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delabSugared i p)) <+>
311+ text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>
312+ annTm y (pprintTerm i (delabSugared i y))
313+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delabSugared i c)
304314pprintErr' 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 "
306316 <> annName n <$>
307317 text "(Type class arguments must be injective)"
308318pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
@@ -310,13 +320,13 @@ pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
310320pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
311321pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
312322pprintErr' 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))
314324pprintErr' i (CantMatch t) =
315− text "Can't match on" <+> annTm t (pprintTerm i (delab i t))
316−pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))
325+ text "Can't match on" <+> annTm t (pprintTerm i (delabSugared i t))
326+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))
317327pprintErr' i (NoEliminator s t)
318328 = text "No " <> text s <> text " for type " <+>
319− annTm t (pprintTerm i (delab i t)) <$>
329+ annTm t (pprintTerm i (delabSugared i t)) <$>
320330 text "Please note that 'induction' is experimental." <$>
321331 text "Only types declared with '%elim' can be used." <$>
322332 text "Consider writing a pattern matching definition instead."
@@ -344,7 +354,7 @@ pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <
344354pprintErr' i (AlreadyDefined n) = annName n<+>
345355 text "is already defined"
346356pprintErr' 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))
348358pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
349359pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
350360 annName' n (showqual i n) <> colon <$>
@@ -384,7 +394,7 @@ pprintErr' i (ReflectionError parts orig) =
384394 where showPart :: ErrorReportPart -> Doc OutputAnnotation
385395 showPart (TextPart str) = fillSep . map text . words $ str
386396 showPart (NamePart n) = annName n
387− showPart (TermPart tm) = pprintTerm i (delab i tm)
397+ showPart (TermPart tm) = pprintTerm i (delabSugared i tm)
388398 showPart (SubReport rs) = indented . hsep . map showPart $ rs
389399pprintErr' i (ReflectionFailed msg err) =
390400 text "When attempting to perform error reflection, the following internal error occurred:" <>
@@ -554,7 +564,7 @@ fancifyAnnots ist meta annot@(AnnName n _ _ _) =
554564 return (out "")
555565 getTy :: IState -> Name -> String -- fails if name not already extant!
556566 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
557− delabTy ist n
567+ resugar $ delabTy ist n
558568 in (displayS . renderPretty 1.0 50 $ theTy) ""
559569fancifyAnnots _ _ annot = annot
560570
@@ -564,7 +574,7 @@ showSc i xs = line <> line <> text "In context:" <>
564574 indented (vsep (reverse (showSc' [] xs)))
565575 where showSc' bnd [] = []
566576 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)
568578 in this : showSc' ((n,False):bnd) ctxt
569579
570580