git.iko.soy/Idris-dev
on master help sign in
Temporarily remove function argument error reflection

It needs to be done right, with the new unification info

commitbe0bf4cbe846425f44ba64059cbe07adb49293b9 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Mar 2014, 18:27 (13 years ago) parentf569155
3 files changed+8−7
compare with master
unifiedsplit
src/Idris/ElabTerm.hs+3 test/error004/FunErrTest.idr+3−5 test/error004/expected+2−2
src/Idris/ElabTerm.hs+3
@@ -1643,6 +1643,9 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
16431643 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
16441644 err' <- handle err
16451645 return (Elaborating what n err')
1646+ handle e@(ElaboratingArg f a err) = do logLvl 3 "Reflecting body of ElaboratingArg"
1647+ err' <- handle err
1648+ return (ElaboratingArg f a err')
16461649 -- TODO: argument-specific error handlers go here for ElaboratingArg
16471650 handle e = do ist <- getIState
16481651 let err = fmap (errReverse ist) e
test/error004/FunErrTest.idr+3−5
@@ -6,6 +6,7 @@ import Language.Reflection.Utils
66
77%language ErrorReflection
88
9+
910total
1011cadr : (xs : List a)
1112 -> {auto cons1 : isCons xs = True}
@@ -18,7 +19,7 @@ extractList : TT -> Maybe TT
1819extractList (App (App reflCon (App isCons lst)) _) = Just lst
1920extractList _ = Nothing
2021
21−
22+%error_handler
2223total
2324has2elts : Err -> Maybe (List ErrorReportPart)
2425has2elts (CantSolveGoal tm _) = do lst <- extractList tm
@@ -28,9 +29,6 @@ has2elts (CantSolveGoal tm _) = do lst <- extractList tm
2829 ]
2930has2elts e = Just [TextPart (show e)]
3031
31−%error_handlers cadr cons1 has2elts
32−%error_handlers cadr cons2 has2elts
33−
3432badCadr1 : Int
3533badCadr1 = cadr []
3634
@@ -38,4 +36,4 @@ badCadr2 : Int
3836badCadr2 = cadr [1]
3937
4038goodCadr : Int
41−goodCadr = cadr [1, 2]
39+goodCadr = cadr [1, 2]
test/error004/expected+2−2
@@ -1,4 +1,4 @@
1−FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:
1+FunErrTest.idr:33:10:When elaborating right hand side of badCadr1:
22Could not prove that [] has at least two elements.
3−FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
3+FunErrTest.idr:36:10:When elaborating right hand side of badCadr2:
44Could not prove that tail [(fromInteger 1)] refl has at least two elements.