9d8c0c4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow a hierarchical structure in reflected errors

commit9d8c0c49dea2067c972e5447033d4513c4290b1b authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 10 Jan 2014, 14:45 (13 years ago) parent5eda188

4 files changed+9

compare with master

unifiedsplit

libs/base/Language/Reflection/Errors.idr+1 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+1 src/Idris/ElabTerm.hs+6

libs/base/Language/Reflection/Errors.idr+1

@@ -40,6 +40,7 @@ data Err = Msg String

4040data ErrorReportPart = TextPart String

4141 | NamePart TTName

4242 | TermPart TT

43+ | SubReport (List ErrorReportPart)

4344

4445

4546-- Error reports become functions in List (String, TT) -> Err -> ErrorReport

src/Idris/Core/TT.hs+1

@@ -78,6 +78,7 @@ instance Show FC where

7878data ErrorReportPart = TextPart String

7979 | NamePart Name

8080 | TermPart Term

81+ | SubReport [ErrorReportPart]

8182 deriving (Show, Eq)

8283

8384

src/Idris/Delaborate.hs+1

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

201201 showName (Just i) [] False colour n

202202 showPart (TermPart tm) = let colour = idris_colourRepl i

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

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

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

205206 indented (pshow i err) ++

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

src/Idris/ElabTerm.hs+6

@@ -1513,6 +1513,12 @@ reifyReportPart (App (P (DCon _ _) n _) tm)

15131513 show tm ++

15141514 " when reflecting an error"

15151515 OK (tm', _) -> return $ TermPart tm'

1516+reifyReportPart (App (P (DCon _ _) n _) tm)

1517+ | n == reflErrName "SubReport" =

1518+ case unList tm of

1519+ Just xs -> do subParts <- mapM reifyReportPart xs

1520+ return (SubReport subParts)

1521+ Nothing -> ierror . InternalMsg $ "could not reify subreport " ++ show tm

15161522reifyReportPart x = ierror . InternalMsg $ "could not reify " ++ show x

15171523

15181524envTupleType :: Raw