ec9ac38 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #966 from david-christiansen/error-reflection

Error reflection

commitec9ac3825d2ade11f9643b1a3b6900015be12210 authorEdwin Brady <edwin.brady@gmail.com> dateThu 13 Mar 2014, 10:15 (13 years ago) parent4ba5460 f707c76

8 files changed+22−46

compare with master

unifiedsplit

libs/base/Language/Reflection/Errors.idr−2 libs/base/Language/Reflection/Utils.idr−2 src/Idris/AbsSyntax.hs+5−4 src/Idris/Core/Elaborate.hs+2 src/Idris/Delaborate.hs+3−3 src/Idris/ElabTerm.hs+10−21 test/error003/ErrorReflection.idr−11 test/error003/expected+2−3

libs/base/Language/Reflection/Errors.idr−2

@@ -35,8 +35,6 @@ data Err = Msg String

3535 | AlreadyDefined TTName

3636 | ProofSearchFail Err

3737 | NoRewriting TT

38− | At SourceLocation Err

39− | Elaborating String TTName Err

4038 | ProviderError String

4139 | LoadingFailed String Err

4240

libs/base/Language/Reflection/Utils.idr−2

@@ -252,8 +252,6 @@ instance Show Err where

252252 show (AlreadyDefined n) = "AlreadyDefined " ++ show n

253253 show (ProofSearchFail err) = "ProofSearchFail " ++ show err

254254 show (NoRewriting tm) = "NoRewriting " ++ show tm

255− show (At loc err) = "At " ++ show loc ++ " " ++ show err

256− show (Elaborating x n err) = "Elaborating " ++ show x ++ " " ++ show x ++ " " ++ show n ++ " (" ++ show err ++ ")"

257255 show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""

258256 show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"

259257

src/Idris/AbsSyntax.hs+5−4

@@ -643,13 +643,14 @@ isetPrompt p = do i <- getIState

643643

644644ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()

645645ihWarn h fc err = do i <- getIState

646− err' <- iRender . fmap (fancifyAnnots i) $ err

647646 case idris_outputmode i of

648647 RawOutput ->

649− runIO $

650− hPutStrLn h (show fc ++ ":" ++ displayDecorated (consoleDecorate i) err')

648+ do err' <- iRender . fmap (fancifyAnnots i) $

649+ text (show fc) <> colon <//> err

650+ runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

651651 IdeSlave n ->

652− do let (str, spans) = displaySpans err'

652+ do err' <- iRender . fmap (fancifyAnnots i) $ err

653+ let (str, spans) = displaySpans err'

653654 runIO . hPutStrLn h $

654655 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

655656

src/Idris/Core/Elaborate.hs+2

@@ -147,6 +147,8 @@ getUnifyLog :: Elab' aux Bool

147147getUnifyLog = do ES (ps, a) l p <- get

148148 return (unifylog ps)

149149

150+-- | Process a tactic within the current elaborator state

151+processTactic' :: Tactic -> Elab' aux ()

150152processTactic' t = do ES (p, a) logs prev <- get

151153 (p', log) <- lift $ processTactic t p

152154 put (ES (p', a) (logs ++ log) prev)

src/Idris/Delaborate.hs+3−3

@@ -220,13 +220,13 @@ pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

220220pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

221221pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

222222pprintErr' i (ReflectionError parts orig) =

223− let parts' = map (hsep . map showPart) parts in

224− vsep parts' <>

223+ let parts' = map (fillSep . map showPart) parts in

224+ align (fillSep parts') <>

225225 if (opt_origerr (idris_options i))

226226 then line <> line <> text "Original error:" <$> indented (pprintErr' i orig)

227227 else empty

228228 where showPart :: ErrorReportPart -> Doc OutputAnnotation

229− showPart (TextPart str) = text str

229+ showPart (TextPart str) = fillSep . map text . words $ str

230230 showPart (NamePart n) = annName n

231231 showPart (TermPart tm) = pprintTerm i (delab i tm)

232232 showPart (SubReport rs) = indented . hsep . map showPart $ rs

src/Idris/ElabTerm.hs+10−21

@@ -13,6 +13,7 @@ import Idris.Core.TT

1313import Idris.Core.Evaluate

1414import Idris.Core.Unify

1515import Idris.Core.Typecheck (check)

16+import Idris.ErrReverse (errReverse)

1617

1718import Control.Applicative ((<$>))

1819import Control.Monad

@@ -1619,26 +1620,6 @@ reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollab

16191620reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

16201621reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

16211622reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]

1622−reflectErr (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err]

1623− where reflectFC (FC source (sl, sc) (el, ec)) = raw_apply (Var $ reflErrName "FileLoc")

1624− [ RConstant (Str source)

1625− , raw_apply (Var pairCon) [

1626− RConstant (AType (ATInt ITNative)),

1627− RConstant (AType (ATInt ITNative)),

1628− RConstant (I sl),

1629− RConstant (I sc)]

1630− , raw_apply (Var pairCon) [

1631− RConstant (AType (ATInt ITNative)),

1632− RConstant (AType (ATInt ITNative)),

1633− RConstant (I el),

1634− RConstant (I ec)]

1635− ]

1636−reflectErr (Elaborating str n e) =

1637− raw_apply (Var $ reflErrName "Elaborating")

1638− [ RConstant (Str str)

1639− , reflectName n

1640− , reflectErr e

1641− ]

16421623reflectErr (ProviderError str) =

16431624 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

16441625reflectErr (LoadingFailed str err) =

@@ -1653,11 +1634,19 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

16531634 return e -- Don't do meta-reflection of errors

16541635 handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"

16551636 return e

1637+ -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them

1638+ handle e@(At fc err) = do logLvl 3 "Reflecting body of At"

1639+ err' <- handle err

1640+ return (At fc err')

1641+ handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"

1642+ err' <- handle err

1643+ return (Elaborating what n err')

16561644 handle e = do ist <- getIState

1645+ let err = fmap (errReverse ist) e

16571646 logLvl 2 "Starting error reflection"

16581647 let handlers = idris_errorhandlers ist

16591648 logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))

1660− let reports = map (\n -> RApp (Var n) (reflectErr e)) handlers

1649+ let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers

16611650

16621651 -- Typecheck error handlers - if this fails, then something else was wrong earlier!

16631652 handlers <- case mapM (check (tt_ctxt ist) []) reports of

test/error003/ErrorReflection.idr−11

@@ -59,17 +59,6 @@ dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1

5959 ty1 <- reifyTy tm1'

6060 ty2 <- reifyTy tm2'

6161 return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]

62−dslerr (At (FileLoc f s e) err) = do err' <- dslerr err

63− return [ TextPart "In file"

64− , TextPart f

65− , TextPart "start", TextPart (show s)

66− , TextPart "end", TextPart (show e)

67− , SubReport err']

68−dslerr (Elaborating s n err) = do err' <- dslerr err

69− return ([ TextPart $ "When elaborating " ++ s

70− , NamePart n

71− , TextPart ":"

72− , SubReport err'])

7362dslerr _ = Nothing

7463

7564

test/error003/expected+2−3

@@ -1,3 +1,2 @@

1−In file ErrorReflection.idr start (78, 5) end (78, 5)

2− When elaborating right hand side of Main.bad :

3− DSL type error: (t'(504) => t'(504)) doesn't match ()

1+ErrorReflection.idr:67:5:When elaborating right hand side of bad:

2+DSL type error: (t'(504) => t'(504)) doesn't match ()