@@ -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,52 @@ 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 :: IState -> PTerm -> PTerm
30+resugar ist = transform flattenDoLet . 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)
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
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)
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)
61+ dedelay (PApp _ (PRef _ delay) [_, _, obj])
62+ | delay == sUN "Delay" = getTm obj
65+ explicitTerm (PExp {getTm = tm}) = Just tm
66+ explicitTerm _ = Nothing
69+-- | Delaborate and resugar a term
70+delabSugared :: IState -> Term -> PTerm
71+delabSugared ist tm = resugar ist $ delab ist tm
73+-- | Delaborate a term without resugaring
27delab :: IState -> Term -> PTerm
74delab :: IState -> Term -> PTerm
28delab i tm = delab' i tm False False
75delab i tm = delab' i tm False False
@@ -50,7 +97,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
51 un = fileFC "(val)"
98 un = fileFC "(val)"
53− de env _ (App _ f a) = resugarApp env $ deFn env f [a]
100+ de env _ (App _ f a) = deFn env f [a]
54 de env _ (V i) | i < length env = PRef un (snd (env!!i))
101 de env _ (V i) | i < length env = PRef un (snd (env!!i))
55 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))
102 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))
56 de env _ (P _ n _) | n == unitTy = PTrue un IsType
103 de env _ (P _ n _) | n == unitTy = PTrue un IsType
@@ -147,17 +194,6 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
147 isCN (SN (CaseN _)) = True
194 isCN (SN (CaseN _)) = True
148 isCN _ = False
195 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
197 delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm
162 delabCase env imps scvar scrutinee caseName caseArgs =
198 delabCase env imps scvar scrutinee caseName caseArgs =
163 do cases <- case lookupCtxt caseName (idris_patdefs ist) of
199 do cases <- case lookupCtxt caseName (idris_patdefs ist) of
@@ -187,7 +223,7 @@ indented = nest errorIndent . (line <>)
187-- | Pretty-print a core term using delaboration
223-- | Pretty-print a core term using delaboration
188pprintDelab :: IState -> Term -> Doc OutputAnnotation
224pprintDelab :: IState -> Term -> Doc OutputAnnotation
189pprintDelab ist tm = annotate (AnnTerm [] tm)
225pprintDelab ist tm = annotate (AnnTerm [] tm)
190− (prettyIst ist (delab ist tm))
226+ (prettyIst ist (delabSugared ist tm))
192-- | Pretty-print the type of some name
228-- | Pretty-print the type of some name
193pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
229pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
@@ -195,8 +231,8 @@ pprintDelabTy i n
195 = case lookupTy n (tt_ctxt i) of
231 = case lookupTy n (tt_ctxt i) of
196 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
232 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
197 case lookupCtxt n (idris_implicits i) of
233 case lookupCtxt n (idris_implicits i) of
198− (imps:_) -> delabTy' i imps ty False False
234+ (imps:_) -> resugar i $ delabTy' i imps ty False False
199− _ -> delabTy' i [] ty False False
235+ _ -> resugar i $ delabTy' i [] ty False False
200 [] -> error "pprintDelabTy got a name that doesn't exist"
236 [] -> error "pprintDelabTy got a name that doesn't exist"
202pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
238pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
@@ -212,11 +248,11 @@ pprintProv i e GivenVal = text "Given value"
212pprintProv i e (SourceTerm tm)
248pprintProv i e (SourceTerm tm)
213 = text "Type of " <>
249 = text "Type of " <>
214 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
250 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))
216pprintProv i e (TooManyArgs tm)
252pprintProv i e (TooManyArgs tm)
217 = text "Is " <>
253 = text "Is " <>
218 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
254 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))
220 <> text " applied to too many arguments?"
256 <> text " applied to too many arguments?"
222pprintErr :: IState -> Err -> Doc OutputAnnotation
258pprintErr :: IState -> Err -> Doc OutputAnnotation
@@ -230,7 +266,7 @@ pprintErr' i (InternalMsg s) =
231pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
267pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
232 let (x_ns, y_ns, nms) = renameMNs x_in y_in
268 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
234 text "Type mismatch between" <> indented (annTm x_ns
270 text "Type mismatch between" <> indented (annTm x_ns
235 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
271 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
236 ++ zip nms (repeat False)) x))
272 ++ zip nms (repeat False)) x))
@@ -255,8 +291,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
291 if (opt_errContext (idris_options i)) then showSc i sc else empty
256pprintErr' i (CantConvert x_in y_in env) =
292pprintErr' i (CantConvert x_in y_in env) =
257 let (x_ns, y_ns, nms) = renameMNs x_in y_in
293 let (x_ns, y_ns, nms) = renameMNs x_in y_in
258− (x, y) = addImplicitDiffs (delab i (flagUnique x_ns))
294+ (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))
259− (delab i (flagUnique y_ns)) in
295+ (delabSugared i (flagUnique y_ns)) in
260 text "Type mismatch between" <>
296 text "Type mismatch between" <>
261 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
297 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
@@ -272,37 +308,37 @@ pprintErr' i (CantConvert x_in y_in env) =
272 flagUnique t = t
308 flagUnique t = t
273pprintErr' i (CantSolveGoal x env) =
309pprintErr' i (CantSolveGoal x env) =
274 text "Can't solve goal " <>
310 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))) <>
276 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
312 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
277pprintErr' i (UnifyScope n out tm env) =
313pprintErr' i (UnifyScope n out tm env) =
278 text "Can't unify" <> indented (annName n) <+>
314 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))) <+>
280 text "as" <> indented (annName out) <> text "is not in scope" <>
316 text "as" <> indented (annName out) <> text "is not in scope" <>
281 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
317 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
318pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
283pprintErr' i (NonFunctionType f ty) =
319pprintErr' i (NonFunctionType f ty) =
284− annTm f (pprintTerm i (delab i f)) <+>
320+ annTm f (pprintTerm i (delabSugared i f)) <+>
285 text "does not have a function type" <+>
321 text "does not have a function type" <+>
286− parens (pprintTerm i (delab i ty))
322+ parens (pprintTerm i (delabSugared i ty))
287pprintErr' i (NotEquality tm ty) =
323pprintErr' i (NotEquality tm ty) =
288− annTm tm (pprintTerm i (delab i tm)) <+>
324+ annTm tm (pprintTerm i (delabSugared i tm)) <+>
289 text "does not have an equality type" <+>
325 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)))
291pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
327pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
292pprintErr' i (CantIntroduce ty) =
328pprintErr' 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))
294pprintErr' i (InfiniteUnify x tm env) =
330pprintErr' i (InfiniteUnify x tm env) =
295 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
331 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)) <+>
297 text "would lead to infinite value" <>
333 text "would lead to infinite value" <>
298 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
334 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
299pprintErr' i (NotInjective p x y) =
335pprintErr' i (NotInjective p x y) =
300− text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>
336+ 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" <+>
337+ text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>
302− annTm y (pprintTerm i (delab i y))
338+ annTm y (pprintTerm i (delabSugared i y))
303−pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
339+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delabSugared i c)
304pprintErr' i (InvalidTCArg n t)
340pprintErr' 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 "
306 <> annName n <$>
342 <> annName n <$>
307 text "(Type class arguments must be injective)"
343 text "(Type class arguments must be injective)"
308pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
344pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
@@ -310,13 +346,13 @@ pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
310pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
346pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
311pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
347pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
312pprintErr' i (WithFnType ty) =
348pprintErr' 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))
314pprintErr' i (CantMatch t) =
350pprintErr' i (CantMatch t) =
315− text "Can't match on" <+> annTm t (pprintTerm i (delab i t))
351+ 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))
352+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))
317pprintErr' i (NoEliminator s t)
353pprintErr' i (NoEliminator s t)
318 = text "No " <> text s <> text " for type " <+>
354 = text "No " <> text s <> text " for type " <+>
319− annTm t (pprintTerm i (delab i t)) <$>
355+ annTm t (pprintTerm i (delabSugared i t)) <$>
320 text "Please note that 'induction' is experimental." <$>
356 text "Please note that 'induction' is experimental." <$>
321 text "Only types declared with '%elim' can be used." <$>
357 text "Only types declared with '%elim' can be used." <$>
322 text "Consider writing a pattern matching definition instead."
358 text "Consider writing a pattern matching definition instead."
@@ -344,7 +380,7 @@ pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <
344pprintErr' i (AlreadyDefined n) = annName n<+>
380pprintErr' i (AlreadyDefined n) = annName n<+>
345 text "is already defined"
381 text "is already defined"
346pprintErr' i (ProofSearchFail e) = pprintErr' i e
382pprintErr' 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))
348pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
384pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
349pprintErr' i (Elaborating s n e) = text "When checking" <+> text s <>
385pprintErr' i (Elaborating s n e) = text "When checking" <+> text s <>
350 annName' n (showqual i n) <> colon <$>
386 annName' n (showqual i n) <> colon <$>
@@ -414,7 +450,7 @@ pprintErr' i (ElabScriptStuck tm) =
414showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
450showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
415showPart ist (TextPart str) = fillSep . map text . words $ str
451showPart ist (TextPart str) = fillSep . map text . words $ str
416showPart ist (NamePart n) = annName n
452showPart 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)
418showPart ist (RawPart tm) = pprintRaw [] tm
454showPart ist (RawPart tm) = pprintRaw [] tm
419showPart ist (SubReport rs) = indented . hsep . map (showPart ist) $ rs
455showPart ist (SubReport rs) = indented . hsep . map (showPart ist) $ rs
@@ -556,7 +592,7 @@ fancifyAnnots ist meta annot@(AnnName n _ _ _) =
556 return (out "")
592 return (out "")
557 getTy :: IState -> Name -> String -- fails if name not already extant!
593 getTy :: IState -> Name -> String -- fails if name not already extant!
558 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
594 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
559− delabTy ist n
595+ resugar ist $ delabTy ist n
560 in (displayS . renderPretty 1.0 50 $ theTy) ""
596 in (displayS . renderPretty 1.0 50 $ theTy) ""
561fancifyAnnots _ _ annot = annot
597fancifyAnnots _ _ annot = annot
@@ -566,7 +602,7 @@ showSc i xs = line <> line <> text "In context:" <>
566 indented (vsep (reverse (showSc' [] xs)))
602 indented (vsep (reverse (showSc' [] xs)))
567 where showSc' bnd [] = []
603 where showSc' bnd [] = []
568 showSc' bnd ((n, ty):ctxt) =
604 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)
570 in this : showSc' ((n,False):bnd) ctxt
606 in this : showSc' ((n,False):bnd) ctxt