ec9ac38 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

ec9ac38Edwin Brady13 years ago

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

compare with master

unifiedsplit

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

35 | AlreadyDefined TTName

36 | ProofSearchFail Err

37 | NoRewriting TT

38− | At SourceLocation Err

39− | Elaborating String TTName Err

40 | ProviderError String

38 | ProviderError String

41 | LoadingFailed String Err

39 | LoadingFailed String Err

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

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

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

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

254 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 ++ ")"

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

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

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

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

259

257

src/Idris/AbsSyntax.hs+5−4

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

643

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

645ihWarn h fc err = do i <- getIState

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

647 case idris_outputmode i of

646 case idris_outputmode i of

648 RawOutput ->

647 RawOutput ->

649− runIO $

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

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

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

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

651 IdeSlave n ->

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

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

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

653 runIO . hPutStrLn h $

654 runIO . hPutStrLn h $

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

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

655

656

src/Idris/Core/Elaborate.hs+2

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

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

148 return (unifylog ps)

149

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

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

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

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

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

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

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

154 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 <>

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

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

222pprintErr' i (ReflectionError parts orig) =

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

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

224− vsep parts' <>

224+ align (fillSep parts') <>

225 if (opt_origerr (idris_options i))

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

227 else empty

228 where showPart :: ErrorReportPart -> Doc OutputAnnotation

229− showPart (TextPart str) = text str

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

230 showPart (NamePart n) = annName n

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

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

src/Idris/ElabTerm.hs+10−21

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

13import Idris.Core.Evaluate

14import Idris.Core.Unify

15import Idris.Core.Typecheck (check)

16+import Idris.ErrReverse (errReverse)

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

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

18import Control.Monad

19import Control.Monad

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

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

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

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

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

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

1622reflectErr (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− ]

1642reflectErr (ProviderError str) =

1623reflectErr (ProviderError str) =

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

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

1644reflectErr (LoadingFailed str err) =

1625reflectErr (LoadingFailed str err) =

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

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

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

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

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

1655 return e

1636 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')

1656 handle e = do ist <- getIState

1644 handle e = do ist <- getIState

1645+ let err = fmap (errReverse ist) e

1657 logLvl 2 "Starting error reflection"

1646 logLvl 2 "Starting error reflection"

1658 let handlers = idris_errorhandlers ist

1647 let handlers = idris_errorhandlers ist

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

1648 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

1661

1650

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

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

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

1652 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

59 ty1 <- reifyTy tm1'

60 ty2 <- reifyTy tm2'

61 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'])

73dslerr _ = Nothing

62dslerr _ = Nothing

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 :

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

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

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