@@ -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,52 @@ import Debug.Trace
2425
2526bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
2627
28+-- | Re-add syntactic sugar in a term
29+resugar :: IState -> PTerm -> PTerm
30+resugar ist = transform flattenDoLet . 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 (PApp fc (PRef _ n) args)
37+ | [v, PLam _ bn _ _ next] <- mapMaybe explicitTerm args
38+ , basename n == sUN ">>="
39+ = let step = if bn `elem` namesIn [] ist next
40+ then DoBind fc bn NoFC v
41+ else DoExp NoFC v
42+ in case resugarApp next of
43+ PDoBlock dos -> PDoBlock (step : dos)
44+ expr -> PDoBlock [step, DoExp NoFC expr]
45+ resugarApp (PApp fc (PRef _ n) args)
46+ | [PConstant fc (BI i)] <- mapMaybe explicitTerm args
47+ , basename n == sUN "fromInteger"
48+ = PConstant fc (BI i)
49+ resugarApp tm = tm
50+
51+ flattenDoLet (PLet _ ln _ ty v bdy)
52+ | PDoBlock dos <- flattenDoLet bdy
53+ = PDoBlock (DoLet NoFC ln NoFC ty v : dos)
54+ flattenDoLet (PDoBlock dos) =
55+ PDoBlock $ concatMap fixExp dos
56+ where fixExp (DoExp _ (PLet _ ln _ ty v bdy)) =
57+ DoLet NoFC ln NoFC ty v : fixExp (DoExp NoFC bdy)
58+ fixExp d = [d]
59+ flattenDoLet tm = tm
60+
61+ dedelay (PApp _ (PRef _ delay) [_, _, obj])
62+ | delay == sUN "Delay" = getTm obj
63+ dedelay x = x
64+
65+ explicitTerm (PExp {getTm = tm}) = Just tm
66+ explicitTerm _ = Nothing
67+
68+
69+-- | Delaborate and resugar a term
70+delabSugared :: IState -> Term -> PTerm
71+delabSugared ist tm = resugar ist $ delab ist tm
72+
73+-- | Delaborate a term without resugaring
2774delab :: IState -> Term -> PTerm
2875delab i tm = delab' i tm False False
2976
@@ -50,7 +97,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
5097 where
5198 un = fileFC "(val)"
5299
53− de env _ (App _ f a) = resugarApp env $ deFn env f [a]
100+ de env _ (App _ f a) = deFn env f [a]
54101 de env _ (V i) | i < length env = PRef un (snd (env!!i))
55102 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))
56103 de env _ (P _ n _) | n == unitTy = PTrue un IsType
@@ -147,17 +194,6 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
147194 isCN (SN (CaseN _)) = True
148195 isCN _ = False
149196
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−
161197 delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm
162198 delabCase env imps scvar scrutinee caseName caseArgs =
163199 do cases <- case lookupCtxt caseName (idris_patdefs ist) of
@@ -187,7 +223,7 @@ indented = nest errorIndent . (line <>)
187223-- | Pretty-print a core term using delaboration
188224pprintDelab :: IState -> Term -> Doc OutputAnnotation
189225pprintDelab ist tm = annotate (AnnTerm [] tm)
190− (prettyIst ist (delab ist tm))
226+ (prettyIst ist (delabSugared ist tm))
191227
192228-- | Pretty-print the type of some name
193229pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
@@ -195,8 +231,8 @@ pprintDelabTy i n
195231 = case lookupTy n (tt_ctxt i) of
196232 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
197233 case lookupCtxt n (idris_implicits i) of
198− (imps:_) -> delabTy' i imps ty False False
199− _ -> delabTy' i [] ty False False
234+ (imps:_) -> resugar i $ delabTy' i imps ty False False
235+ _ -> resugar i $ delabTy' i [] ty False False
200236 [] -> error "pprintDelabTy got a name that doesn't exist"
201237
202238pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
@@ -212,11 +248,11 @@ pprintProv i e GivenVal = text "Given value"
212248pprintProv i e (SourceTerm tm)
213249 = text "Type of " <>
214250 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
215− (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))
251+ (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))
216252pprintProv i e (TooManyArgs tm)
217253 = text "Is " <>
218254 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
219− (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))
255+ (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))
220256 <> text " applied to too many arguments?"
221257
222258pprintErr :: IState -> Err -> Doc OutputAnnotation
@@ -230,7 +266,7 @@ pprintErr' i (InternalMsg s) =
230266 ]
231267pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
232268 let (x_ns, y_ns, nms) = renameMNs x_in y_in
233− (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in
269+ (x, y) = addImplicitDiffs (delabSugared i x_ns) (delabSugared i y_ns) in
234270 text "Type mismatch between" <> indented (annTm x_ns
235271 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
236272 ++ zip nms (repeat False)) x))
@@ -255,8 +291,8 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
255291 if (opt_errContext (idris_options i)) then showSc i sc else empty
256292pprintErr' i (CantConvert x_in y_in env) =
257293 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
294+ (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))
295+ (delabSugared i (flagUnique y_ns)) in
260296 text "Type mismatch between" <>
261297 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
262298 x)) <$>
@@ -272,37 +308,37 @@ pprintErr' i (CantConvert x_in y_in env) =
272308 flagUnique t = t
273309pprintErr' i (CantSolveGoal x env) =
274310 text "Can't solve goal " <>
275− indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <>
311+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delabSugared i x))) <>
276312 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
277313pprintErr' i (UnifyScope n out tm env) =
278314 text "Can't unify" <> indented (annName n) <+>
279− text "with" <> indented (annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm))) <+>
315+ text "with" <> indented (annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delabSugared i tm))) <+>
280316 text "as" <> indented (annName out) <> text "is not in scope" <>
281317 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
282318pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
283319pprintErr' i (NonFunctionType f ty) =
284− annTm f (pprintTerm i (delab i f)) <+>
320+ annTm f (pprintTerm i (delabSugared i f)) <+>
285321 text "does not have a function type" <+>
286− parens (pprintTerm i (delab i ty))
322+ parens (pprintTerm i (delabSugared i ty))
287323pprintErr' i (NotEquality tm ty) =
288− annTm tm (pprintTerm i (delab i tm)) <+>
324+ annTm tm (pprintTerm i (delabSugared i tm)) <+>
289325 text "does not have an equality type" <+>
290− annTm ty (parens (pprintTerm i (delab i ty)))
326+ annTm ty (parens (pprintTerm i (delabSugared i ty)))
291327pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
292328pprintErr' i (CantIntroduce ty) =
293− text "Can't use lambda here: type is" <+> annTm ty (pprintTerm i (delab i ty))
329+ text "Can't use lambda here: type is" <+> annTm ty (pprintTerm i (delabSugared i ty))
294330pprintErr' i (InfiniteUnify x tm env) =
295331 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
296− annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
332+ annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delabSugared i tm)) <+>
297333 text "would lead to infinite value" <>
298334 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
299335pprintErr' 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)
336+ text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delabSugared i p)) <+>
337+ text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>
338+ annTm y (pprintTerm i (delabSugared i y))
339+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delabSugared i c)
304340pprintErr' i (InvalidTCArg n t)
305− = annTm t (pprintTerm i (delab i t)) <+> text " cannot be a parameter of "
341+ = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "
306342 <> annName n <$>
307343 text "(Type class arguments must be injective)"
308344pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
@@ -310,13 +346,13 @@ pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
310346pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
311347pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
312348pprintErr' i (WithFnType ty) =
313− text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delab i ty))
349+ text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delabSugared i ty))
314350pprintErr' 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))
351+ text "Can't match on" <+> annTm t (pprintTerm i (delabSugared i t))
352+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))
317353pprintErr' i (NoEliminator s t)
318354 = text "No " <> text s <> text " for type " <+>
319− annTm t (pprintTerm i (delab i t)) <$>
355+ annTm t (pprintTerm i (delabSugared i t)) <$>
320356 text "Please note that 'induction' is experimental." <$>
321357 text "Only types declared with '%elim' can be used." <$>
322358 text "Consider writing a pattern matching definition instead."
@@ -344,7 +380,7 @@ pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <
344380pprintErr' i (AlreadyDefined n) = annName n<+>
345381 text "is already defined"
346382pprintErr' i (ProofSearchFail e) = pprintErr' i e
347−pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delab i tm))
383+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delabSugared i tm))
348384pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
349385pprintErr' i (Elaborating s n e) = text "When checking" <+> text s <>
350386 annName' n (showqual i n) <> colon <$>
@@ -414,7 +450,7 @@ pprintErr' i (ElabScriptStuck tm) =
414450showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
415451showPart ist (TextPart str) = fillSep . map text . words $ str
416452showPart ist (NamePart n) = annName n
417−showPart ist (TermPart tm) = pprintTerm ist (delab ist tm)
453+showPart ist (TermPart tm) = pprintTerm ist (delabSugared ist tm)
418454showPart ist (RawPart tm) = pprintRaw [] tm
419455showPart ist (SubReport rs) = indented . hsep . map (showPart ist) $ rs
420456
@@ -556,7 +592,7 @@ fancifyAnnots ist meta annot@(AnnName n _ _ _) =
556592 return (out "")
557593 getTy :: IState -> Name -> String -- fails if name not already extant!
558594 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
559− delabTy ist n
595+ resugar ist $ delabTy ist n
560596 in (displayS . renderPretty 1.0 50 $ theTy) ""
561597fancifyAnnots _ _ annot = annot
562598
@@ -566,7 +602,7 @@ showSc i xs = line <> line <> text "In context:" <>
566602 indented (vsep (reverse (showSc' [] xs)))
567603 where showSc' bnd [] = []
568604 showSc' bnd ((n, ty):ctxt) =
569− let this = bindingOf n False <+> colon <+> pprintTerm' i bnd (delab i ty)
605+ let this = bindingOf n False <+> colon <+> pprintTerm' i bnd (delabSugared i ty)
570606 in this : showSc' ((n,False):bnd) ctxt
571607
572608