git.iko.soy/Idris-dev
on master help sign in
Better debug reports for error reflection
7c39186David Raymond Christiansen
src/Idris/Delaborate.hs+2−1
compare with master
unifiedsplit
@@ -200,7 +200,7 @@ pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e
200pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
200pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
201 concat (intersperse "\n" parts') ++
201 concat (intersperse "\n" parts') ++
202 if (opt_origerr (idris_options i))
202 if (opt_origerr (idris_options i))
203− then "\nOriginal error:\n" ++ indented (pshow i orig)
203+ then "\nOriginal error:\n" ++ indented (pshow i orig)
204 else ""
204 else ""
205 where showPart :: ErrorReportPart -> String
205 where showPart :: ErrorReportPart -> String
206 showPart (TextPart str) = str
206 showPart (TextPart str) = str
@@ -210,6 +210,7 @@ pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse "
210 in showImp (Just i) False colour (delab i tm)
210 in showImp (Just i) False colour (delab i tm)
211 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
211 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
212pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
212pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
213+ indented msg ++
213 indented (pshow i err) ++
214 indented (pshow i err) ++
214 "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr
215 "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr
215
216
src/Idris/ElabTerm.hs+2−2
@@ -1581,7 +1581,7 @@ reifyReportPart (App (P (DCon _ _) n _) ttn)
1581 Error e -> Left . InternalMsg $
1581 Error e -> Left . InternalMsg $
1582 "could not reify name term " ++
1582 "could not reify name term " ++
1583 show ttn ++
1583 show ttn ++
1584− " when reflecting an error"
1584+ " when reflecting an error:" ++ show e
1585 OK (n', _)-> Right $ NamePart n'
1585 OK (n', _)-> Right $ NamePart n'
1586reifyReportPart (App (P (DCon _ _) n _) tm)
1586reifyReportPart (App (P (DCon _ _) n _) tm)
1587 | n == reflErrName "TermPart" =
1587 | n == reflErrName "TermPart" =
@@ -1589,7 +1589,7 @@ reifyReportPart (App (P (DCon _ _) n _) tm)
1589 Error e -> Left . InternalMsg $
1589 Error e -> Left . InternalMsg $
1590 "could not reify reflected term " ++
1590 "could not reify reflected term " ++
1591 show tm ++
1591 show tm ++
1592− " when reflecting an error"
1592+ " when reflecting an error:" ++ show e
1593 OK (tm', _) -> Right $ TermPart tm'
1593 OK (tm', _) -> Right $ TermPart tm'
1594reifyReportPart (App (P (DCon _ _) n _) tm)
1594reifyReportPart (App (P (DCon _ _) n _) tm)
1595 | n == reflErrName "SubReport" =
1595 | n == reflErrName "SubReport" =