@@ -1,10 +1,12 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
3−module Idris.Delaborate where
3+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) 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.
8import Idris.AbsSyntax
10import Idris.AbsSyntax
9import Idris.Core.TT
11import Idris.Core.TT
10import Idris.Core.Evaluate
12import Idris.Core.Evaluate
@@ -33,7 +35,7 @@ delab' :: IState -> Term -> Bool -> Bool -> PTerm
33delab' i t f mvs = delabTy' i [] t f mvs
35delab' i t f mvs = delabTy' i [] t f mvs
35delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
37delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
37 -> Bool -- ^ use full names
39 -> Bool -- ^ use full names
38 -> Bool -- ^ Don't treat metavariables specially
40 -> Bool -- ^ Don't treat metavariables specially
@@ -115,86 +117,109 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
115 imp (PConstraint p l _ d) arg = PConstraint p l arg d
117 imp (PConstraint p l _ d) arg = PConstraint p l arg d
116 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
118 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
120+-- | How far to indent sub-errors
124+-- | Actually indent a sub-error - no line at end because a newline can end
125+-- multiple layers of indent
126+indented :: Doc a -> Doc a
127+indented = nest errorIndent . (line <>)
119−indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where
129+pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
120− boxIt c text = (c:text) ++ if last text == c
130+pprintTerm ist = prettyImp (opt_showimp (idris_options ist))
124pshow :: IState -> Err -> String
132pshow :: IState -> Err -> String
133+pshow ist err = displayDecorated (consoleDecorate ist) .
134+ renderPretty 1.0 80 .
135+ fmap (fancifyAnnots ist) $ pprintErr ist err
137+pprintErr :: IState -> Err -> Doc OutputAnnotation
125−pshow i err = pshow' i (fmap (errReverse i) err)
138+pprintErr i err = pprintErr' i (fmap (errReverse i) err)
127−pshow' i (Msg s) = s
140+pprintErr' i (Msg s) = text s
141+pprintErr' i (InternalMsg s) =
128−pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
142+ vsep [ text "INTERNAL ERROR:" <+> text s,
129− "\nThis is probably a bug, or a missing error message.\n" ++
143+ text "This is probably a bug, or a missing error message.",
130− "Please consider reporting at " ++ bugaddr
144+ text ("Please consider reporting at " ++ bugaddr)
131−pshow' i (CantUnify _ x y e sc s) =
146+pprintErr' i (CantUnify _ x y e sc s) =
132− "Can't unify" ++ indented (showTm i (delab i x)) ++
147+ text "Can't unify" <> indented (pprintTerm i (delab i x)) <$>
133− "with" ++ indented (showTm i (delab i y)) ++
148+ text "with" <> indented (pprintTerm i (delab i y)) <>
134 case e of
149 case e of
135− Msg "" -> ""
150+ Msg "" -> empty
136− _ -> "\nSpecifically:" ++
151+ _ -> line <> line <> text "Specifically:" <>
137− indented (pshow' i e) ++
152+ indented (pprintErr' i e) <>
138− if (opt_errContext (idris_options i)) then showSc i sc else ""
153+ if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
139−pshow' i (CantConvert x y env) =
154+pprintErr' i (CantConvert x y env) =
140− "Can't convert" ++ indented (showTm i (delab i x)) ++
155+ text "Can't convert" <> indented (pprintTerm i (delab i x)) <>
141− "with" ++ indented (showTm i (delab i y)) ++
156+ text "with" <> indented (pprintTerm i (delab i y)) <>
142− if (opt_errContext (idris_options i)) then showSc i env else ""
157+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty
143−pshow' i (UnifyScope n out tm env) =
158+pprintErr' i (UnifyScope n out tm env) =
144− "Can't unify" ++ indented (show n) ++
159+ text "Can't unify" <> indented (annName n) <+>
145− "with" ++ indented (showTm i (delab i tm)) ++
160+ text "with" <> indented (pprintTerm i (delab i tm)) <+>
146− "as" ++ indented (show out) ++ "is not in scope" ++
161+ text "as" <> indented (annName out) <> text "is not in scope" <>
147− if (opt_errContext (idris_options i)) then showSc i env else ""
162+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty
148−pshow' i (CantInferType t) = "Can't infer type for " ++ t
163+pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
149−pshow' i (NonFunctionType f ty) =
164+pprintErr' i (NonFunctionType f ty) =
150− showTm i (delab i f) ++
165+ pprintTerm i (delab i f) <+>
151− " does not have a function type (" ++
166+ text "does not have a function type" <+>
152− showTm i (delab i ty) ++ ")"
167+ parens (pprintTerm i (delab i ty))
153−pshow' i (NotEquality tm ty) =
168+pprintErr' i (NotEquality tm ty) =
154− showTm i (delab i tm) ++
169+ pprintTerm i (delab i tm) <+>
155− " does not have an equality type (" ++
170+ text "does not have an equality type" <+>
156− showTm i (delab i ty) ++ ")"
171+ parens (pprintTerm i (delab i ty))
157−pshow' i (TooManyArguments f) = "Too many arguments for " ++ show f
172+pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
158−pshow' i (CantIntroduce ty) =
173+pprintErr' i (CantIntroduce ty) =
159− "Can't use lambda here: type is " ++ showTm i (delab i ty)
174+ text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)
160−pshow' i (InfiniteUnify x tm env)
175+pprintErr' i (InfiniteUnify x tm env) =
161− = "Unifying " ++ showbasic x ++ " and " ++ showTm i (delab i tm) ++
176+ text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>
162− " would lead to infinite value" ++
177+ text "would lead to infinite value" <>
163− if (opt_errContext (idris_options i)) then showSc i env else ""
178+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty
164−pshow' i (NotInjective p x y) =
179+pprintErr' i (NotInjective p x y) =
165− "Can't verify injectivity of " ++ showTm i (delab i p) ++
180+ text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
166− " when unifying " ++ showTm i (delab i x) ++ " and " ++
181+ text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
167− showTm i (delab i y)
182+ pprintTerm i (delab i y)
168−pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
183+pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
169−pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
184+pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
185+ cat (punctuate comma (map text as))
170−pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n
186+pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
171−pshow' i (NoSuchVariable n) = "No such variable " ++ show n
187+pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
172−pshow' i (IncompleteTerm t) = "Incomplete term " ++ showTm i (delab i t)
188+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)
173−pshow' i UniverseError = "Universe inconsistency"
189+pprintErr' i UniverseError = text "Universe inconsistency"
174−pshow' i ProgramLineComment = "Program line next to comment"
190+pprintErr' i ProgramLineComment = text "Program line next to comment"
175−pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
191+pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
176−pshow' i (NonCollapsiblePostulate n) = "The return type of postulate " ++ show n ++ " is not collapsible"
192+pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>
193+ annName n <+> text "is not collapsible"
194+pprintErr' i (AlreadyDefined n) = annName n<+>
177−pshow' i (AlreadyDefined n) = show n ++ " is already defined"
195+ text "is already defined"
178−pshow' i (ProofSearchFail e) = pshow' i e
196+pprintErr' i (ProofSearchFail e) = pprintErr' i e
179−pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)
197+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> pprintTerm i (delab i tm)
180−pshow' i (At f e) = show f ++ ":" ++ pshow' i e
198+pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
181−pshow' i (Elaborating s n e) = "When elaborating " ++ s ++
199+pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
182− showqual i n ++ ":\n" ++ pshow' i e
200+ annName' n (showqual i n) <> colon <$>
183−pshow' i (ProviderError msg) = "Type provider error: " ++ msg
202+pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)
184−pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e
203+pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e
204+pprintErr' i (ReflectionError parts orig) =
185−pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
205+ let parts' = map (hsep . map showPart) parts in
186− concat (intersperse "\n" parts') ++
206+ vsep parts' <> line <> line <>
187− "\nOriginal error:\n" ++ indented (pshow' i orig)
207+ text "Original error:" <$> indented (pprintErr' i orig)
188− where showPart :: ErrorReportPart -> String
208+ where showPart :: ErrorReportPart -> Doc OutputAnnotation
189− showPart (TextPart str) = str
209+ showPart (TextPart str) = text str
190− showPart (NamePart n) = let colour = idris_colourRepl i in
210+ showPart (NamePart n) = annName n
191− showName (Just i) [] False colour n
192− showPart (TermPart tm) = showTm i (delab i tm)
211+ showPart (TermPart tm) = pprintTerm i (delab i tm)
193− showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
212+ showPart (SubReport rs) = indented . hsep . map showPart $ rs
213+pprintErr' i (ReflectionFailed msg err) =
194−pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
214+ text "When attempting to perform error reflection, the following internal error occurred:" <>
195− indented (pshow' i err) ++
215+ indented (pprintErr' i err) <>
196− "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr
216+ text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
218+annName :: Name -> Doc OutputAnnotation
219+annName n = annName' n (show n)
221+annName' :: Name -> String -> Doc OutputAnnotation
222+annName' n str = annotate (AnnName n Nothing Nothing) (text str)
199showSc i [] = ""
224showSc i [] = ""
200showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))
225showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))