git.iko.soy/Idris-dev
on master help sign in
Temporarily remove function argument error reflection
be0bf4cDavid Raymond Christiansen
src/Idris/ElabTerm.hs+3
compare with master
unifiedsplit
@@ -1643,6 +1643,9 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1643 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
1643 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
1644 err' <- handle err
1644 err' <- handle err
1645 return (Elaborating what n err')
1645 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')
1646 -- TODO: argument-specific error handlers go here for ElaboratingArg
1649 -- TODO: argument-specific error handlers go here for ElaboratingArg
1647 handle e = do ist <- getIState
1650 handle e = do ist <- getIState
1648 let err = fmap (errReverse ist) e
1651 let err = fmap (errReverse ist) e
test/error004/FunErrTest.idr+3−5
@@ -6,6 +6,7 @@ import Language.Reflection.Utils
6
6
7%language ErrorReflection
7%language ErrorReflection
8
8
9+
9total
10total
10cadr : (xs : List a)
11cadr : (xs : List a)
11 -> {auto cons1 : isCons xs = True}
12 -> {auto cons1 : isCons xs = True}
@@ -18,7 +19,7 @@ extractList : TT -> Maybe TT
18extractList (App (App reflCon (App isCons lst)) _) = Just lst
19extractList (App (App reflCon (App isCons lst)) _) = Just lst
19extractList _ = Nothing
20extractList _ = Nothing
20
21
21−
22+%error_handler
22total
23total
23has2elts : Err -> Maybe (List ErrorReportPart)
24has2elts : Err -> Maybe (List ErrorReportPart)
24has2elts (CantSolveGoal tm _) = do lst <- extractList tm
25has2elts (CantSolveGoal tm _) = do lst <- extractList tm
@@ -28,9 +29,6 @@ has2elts (CantSolveGoal tm _) = do lst <- extractList tm
28 ]
29 ]
29has2elts e = Just [TextPart (show e)]
30has2elts e = Just [TextPart (show e)]
30
31
31−%error_handlers cadr cons1 has2elts
32−%error_handlers cadr cons2 has2elts
33−
34badCadr1 : Int
32badCadr1 : Int
35badCadr1 = cadr []
33badCadr1 = cadr []
36
34
@@ -38,4 +36,4 @@ badCadr2 : Int
38badCadr2 = cadr [1]
36badCadr2 = cadr [1]
39
37
40goodCadr : Int
38goodCadr : 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:
2Could not prove that [] has at least two elements.
2Could 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:
4Could not prove that tail [(fromInteger 1)] refl has at least two elements.
4Could not prove that tail [(fromInteger 1)] refl has at least two elements.