git.iko.soy/Idris-dev
on master help sign in
Update error reflection for CantSolveGoal
b4943a2David Raymond Christiansen
libs/base/Language/Reflection/Utils.idr+1
compare with master
unifiedsplit
@@ -232,6 +232,7 @@ instance Show Err where
232 show xs ++ " " ++ show y
232 show xs ++ " " ++ show y
233 show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
233 show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
234 show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
234 show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
235+ show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt
235 show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
236 show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
236 show (CantInferType x) = "CantInferType " ++ show x
237 show (CantInferType x) = "CantInferType " ++ show x
237 show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
238 show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
test/test038/FunErrTest.idr+9−25
@@ -14,36 +14,20 @@ cadr : (xs : List a)
14cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y
14cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y
15cadr (x :: []) {cons1=refl} {cons2=refl} impossible
15cadr (x :: []) {cons1=refl} {cons2=refl} impossible
16
16
17−total
17+extractList : TT -> Maybe TT
18−eltsErr : TT -> TT -> Maybe (List ErrorReportPart)
18+extractList (App (App reflCon (App isCons lst)) _) = Just lst
19−eltsErr (P (DCon _ _) (NS (UN "False") _) _) (P (DCon _ _) (NS (UN "True") _) _) =
20− Just [ NamePart (NS (UN "cadr") ["FunErrTest"])
21− , TextPart "requires that its argument contain at least two elements."
22− ]
23−eltsErr (P (DCon _ _) (NS (UN "True") _) _) (App (App isCons ty) xs) =
24− Just [ NamePart (NS (UN "cadr") ["FunErrTest"])
25− , TextPart "requires that its argument contain at least two elements."
26− , TextPart "This fails because: "
27− , SubReport [ TextPart "There is no proof that"
28− , TermPart xs
29− , TextPart "is non-empty."
30− ]
31− ]
32−eltsErr _ _ = Nothing
19+extractList _ = Nothing
20+
33
21
34total
22total
35has2elts : Err -> Maybe (List ErrorReportPart)
23has2elts : Err -> Maybe (List ErrorReportPart)
36−has2elts (CantUnify _ tm1 tm2 e _ _) = eltsErr tm1 tm2 <|> has2elts e
24+has2elts (CantSolveGoal tm _) = do lst <- extractList tm
25+ return [ TextPart "Could not prove that"
26+ , TermPart lst
27+ , TextPart "has at least two elements."
28+ ]
37has2elts e = Just [TextPart (show e)]
29has2elts e = Just [TextPart (show e)]
38
30
39%error_handlers cadr cons1 has2elts
31%error_handlers cadr cons1 has2elts
40%error_handlers cadr cons2 has2elts
32%error_handlers cadr cons2 has2elts
41
33
42−problem1 : List a -> a
43−problem1 xs = cadr xs
44−
45−problem2 : Int
46−problem2 = cadr [1]
47−
48−problem3 : Int
49−problem3 = cadr []
test/test038/expected−47
@@ -1,47 +0,0 @@
1−FunErrTest.idr:43:10:When elaborating right hand side of problem1:
2−FunErrTest.cadr requires that its argument contain at least two elements. This fails because:
3− There is no proof that xs is non-empty.
4−
5−Original error:
6−
7− Can't unify
8− True = True
9− with
10− isCons xs = True
11−
12− Specifically:
13− Can't unify
14− True
15− with
16− isCons xs
17−
18−FunErrTest.idr:46:10:When elaborating right hand side of problem2:
19−FunErrTest.cadr requires that its argument contain at least two elements.
20−Original error:
21−
22− Can't unify
23− x = x
24− with
25− False = True
26−
27− Specifically:
28− Can't unify
29− False
30− with
31− True
32−
33−FunErrTest.idr:49:10:When elaborating right hand side of problem3:
34−FunErrTest.cadr requires that its argument contain at least two elements.
35−Original error:
36−
37− Can't unify
38− x = x
39− with
40− False = True
41−
42− Specifically:
43− Can't unify
44− False
45− with
46− True
47−