7c39186 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better debug reports for error reflection

commit7c391862f910aaaccd232544d3fcd01c84cff823 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 24 Jan 2014, 19:47 (13 years ago) parentd006e27

2 files changed+4−3

compare with master

unifiedsplit

src/Idris/Delaborate.hs+2−1 src/Idris/ElabTerm.hs+2−2

src/Idris/Delaborate.hs+2−1

@@ -200,7 +200,7 @@ pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e

200200pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

201201 concat (intersperse "\n" parts') ++

202202 if (opt_origerr (idris_options i))

203− then "\nOriginal error:\n" ++ indented (pshow i orig)

203+ then "\nOriginal error:\n" ++ indented (pshow i orig)

204204 else ""

205205 where showPart :: ErrorReportPart -> String

206206 showPart (TextPart str) = str

@@ -210,6 +210,7 @@ pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse "

210210 in showImp (Just i) False colour (delab i tm)

211211 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

212212pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

213+ indented msg ++

213214 indented (pshow i err) ++

214215 "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

215216

src/Idris/ElabTerm.hs+2−2

@@ -1581,7 +1581,7 @@ reifyReportPart (App (P (DCon _ _) n _) ttn)

15811581 Error e -> Left . InternalMsg $

15821582 "could not reify name term " ++

15831583 show ttn ++

1584− " when reflecting an error"

1584+ " when reflecting an error:" ++ show e

15851585 OK (n', _)-> Right $ NamePart n'

15861586reifyReportPart (App (P (DCon _ _) n _) tm)

15871587 | n == reflErrName "TermPart" =

@@ -1589,7 +1589,7 @@ reifyReportPart (App (P (DCon _ _) n _) tm)

15891589 Error e -> Left . InternalMsg $

15901590 "could not reify reflected term " ++

15911591 show tm ++

1592− " when reflecting an error"

1592+ " when reflecting an error:" ++ show e

15931593 OK (tm', _) -> Right $ TermPart tm'

15941594reifyReportPart (App (P (DCon _ _) n _) tm)

15951595 | n == reflErrName "SubReport" =