5e0a984 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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.

commit5e0a9849b6bc10cc4bd274f5eb5b1c24093b2aa5 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 10 Mar 2014, 14:40 (13 years ago) parent91120ab

5 files changed+9−30

compare with master

unifiedsplit

libs/base/Language/Reflection/Errors.idr−2 libs/base/Language/Reflection/Utils.idr−2 src/Idris/ElabTerm.hs+7−12 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/ElabTerm.hs+7−12

@@ -1605,18 +1605,6 @@ reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollab

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

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

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

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

1609− where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc")

1610− [ RConstant (Str source)

1611− , RConstant (I line)

1612− , RConstant (I col)

1613− ]

1614−reflectErr (Elaborating str n e) =

1615− raw_apply (Var $ reflErrName "Elaborating")

1616− [ RConstant (Str str)

1617− , reflectName n

1618− , reflectErr e

1619− ]

16201608reflectErr (ProviderError str) =

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

16221610reflectErr (LoadingFailed str err) =

@@ -1631,6 +1619,13 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

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

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

16331621 return e

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

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

1624+ err' <- handle err

1625+ return (At fc err')

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

1627+ err' <- handle err

1628+ return (Elaborating what n err')

16341629 handle e = do ist <- getIState

16351630 logLvl 2 "Starting error reflection"

16361631 let handlers = idris_errorhandlers ist

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 l c) err) = do err' <- dslerr err

63− return [ TextPart "In file"

64− , TextPart f

65− , TextPart "line", TextPart (cast l)

66− , TextPart "column", TextPart (cast c)

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 line 78 column 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 ()