git.iko.soy/Idris-dev
on master help sign in
Update error reflection for CantSolveGoal
commitb4943a2214230293442bfe22d51ed309b3ee8231 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 23 Jan 2014, 16:29 (13 years ago) parentbab6c7b
3 files changed+10−72
compare with master
unifiedsplit
libs/base/Language/Reflection/Utils.idr+1 test/test038/FunErrTest.idr+9−25 test/test038/expected−47
libs/base/Language/Reflection/Utils.idr+1
@@ -232,6 +232,7 @@ instance Show Err where
232232 show xs ++ " " ++ show y
233233 show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
234234 show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
235+ show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt
235236 show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
236237 show (CantInferType x) = "CantInferType " ++ show x
237238 show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
test/test038/FunErrTest.idr+9−25
@@ -14,36 +14,20 @@ cadr : (xs : List a)
1414cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y
1515cadr (x :: []) {cons1=refl} {cons2=refl} impossible
1616
17−total
18−eltsErr : TT -> TT -> Maybe (List ErrorReportPart)
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
17+extractList : TT -> Maybe TT
18+extractList (App (App reflCon (App isCons lst)) _) = Just lst
19+extractList _ = Nothing
20+
3321
3422total
3523has2elts : 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+ ]
3729has2elts e = Just [TextPart (show e)]
3830
3931%error_handlers cadr cons1 has2elts
4032%error_handlers cadr cons2 has2elts
4133
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−