From 5e0a9849b6bc10cc4bd274f5eb5b1c24093b2aa5 Mon Sep 17 00:00:00 2001 From: David Raymond Christiansen Date: Mon, 10 Mar 2014 14:40:17 +0100 Subject: [PATCH] Remove the ability to reflect At and Elaborating 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. --- libs/base/Language/Reflection/Errors.idr | 2 -- libs/base/Language/Reflection/Utils.idr | 2 -- src/Idris/ElabTerm.hs | 19 +++++++------------ test/error003/ErrorReflection.idr | 11 ----------- test/error003/expected | 5 ++--- 5 files changed, 9 insertions(+), 30 deletions(-) diff --git a/libs/base/Language/Reflection/Errors.idr b/libs/base/Language/Reflection/Errors.idr index 3096dac6f..391c09e5b 100644 --- a/libs/base/Language/Reflection/Errors.idr +++ b/libs/base/Language/Reflection/Errors.idr @@ -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 diff --git a/libs/base/Language/Reflection/Utils.idr b/libs/base/Language/Reflection/Utils.idr index 0450cd69d..21e1335ba 100644 --- a/libs/base/Language/Reflection/Utils.idr +++ b/libs/base/Language/Reflection/Utils.idr @@ -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 ++ ")" diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs index 106553edc..f0513a5a5 100644 --- a/src/Idris/ElabTerm.hs +++ b/src/Idris/ElabTerm.hs @@ -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 diff --git a/test/error003/ErrorReflection.idr b/test/error003/ErrorReflection.idr index 79e9a9502..7c8fe4c25 100644 --- a/test/error003/ErrorReflection.idr +++ b/test/error003/ErrorReflection.idr @@ -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 diff --git a/test/error003/expected b/test/error003/expected index 7839a87f7..8bbe3380f 100644 --- a/test/error003/expected +++ b/test/error003/expected @@ -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 ()