ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Remove the ability to reflect At and Elaborating

Browse Source 
This is because they are primarily "plumbing" for tracking error
locations, so it's better for error reflection to work on their
payloads. Any reasonable implementation would have just copied what the
compiler does with them anyway.
This commit is contained in:
David Raymond Christiansen 2014-03-10 14:40:17 +01:00
parent 91120ab8f4
commit 5e0a9849b6
5 changed files with 9 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Language/Reflection/Errors.idr
View File

@ -35,8 +35,6 @@ data Err = Msg String
| AlreadyDefined TTName
| ProofSearchFail Err
| NoRewriting TT
| At SourceLocation Err
| Elaborating String TTName Err
| ProviderError String
| LoadingFailed String Err

2
libs/base/Language/Reflection/Utils.idr
View File

@ -252,8 +252,6 @@ instance Show Err where
show (AlreadyDefined n) = "AlreadyDefined " ++ show n
show (ProofSearchFail err) = "ProofSearchFail " ++ show err
show (NoRewriting tm) = "NoRewriting " ++ show tm
show (At loc err) = "At " ++ show loc ++ " " ++ show err
show (Elaborating x n err) = "Elaborating " ++ show x ++ " " ++ show x ++ " " ++ show n ++ " (" ++ show err ++ ")"
show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"

19
src/Idris/ElabTerm.hs
View File

@ -1605,18 +1605,6 @@ reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollab
reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
reflectErr (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err]
where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc")
[ RConstant (Str source)
, RConstant (I line)
, RConstant (I col)
]
reflectErr (Elaborating str n e) =
raw_apply (Var $ reflErrName "Elaborating")
[ RConstant (Str str)
, reflectName n
, reflectErr e
]
reflectErr (ProviderError str) =
raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
reflectErr (LoadingFailed str err) =
@ -1631,6 +1619,13 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
return e -- Don't do meta-reflection of errors
handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
return e
-- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
handle e@(At fc err) = do logLvl 3 "Reflecting body of At"
err' <- handle err
return (At fc err')
handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
err' <- handle err
return (Elaborating what n err')
handle e = do ist <- getIState
logLvl 2 "Starting error reflection"
let handlers = idris_errorhandlers ist

11
test/error003/ErrorReflection.idr
View File

@ -59,17 +59,6 @@ dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1
ty1 <- reifyTy tm1'
ty2 <- reifyTy tm2'
return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]
dslerr (At (FileLoc f l c) err) = do err' <- dslerr err
return [ TextPart "In file"
, TextPart f
, TextPart "line", TextPart (cast l)
, TextPart "column", TextPart (cast c)
, SubReport err']
dslerr (Elaborating s n err) = do err' <- dslerr err
return ([ TextPart $ "When elaborating " ++ s
, NamePart n
, TextPart ":"
, SubReport err'])
dslerr _ = Nothing

5
test/error003/expected
View File

@ -1,3 +1,2 @@
In file ErrorReflection.idr line 78 column 5
When elaborating right hand side of Main.bad :
DSL type error: (t'(504) => t'(504)) doesn't match ()
ErrorReflection.idr:67:5:When elaborating right hand side of bad:
DSL type error: (t'(504) => t'(504)) doesn't match ()