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