git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/test/error004/FunErrTest.idr
41 lines 1.1 kB history raw
1module FunErrTest
3import Language.Reflection
4import Language.Reflection.Errors
5import Language.Reflection.Utils
7%language ErrorReflection
9total
10cadr : (xs : List a)
11 -> {auto cons1 : isCons xs = True}
12 -> {auto cons2 : isCons (tail xs) = True}
13 -> a
14cadr (x :: (y :: _)) {cons1=Refl} {cons2=Refl} = y
15cadr (x :: []) {cons1=Refl} {cons2=Refl} impossible
16cadr [] {cons1=Refl} {cons2=Refl} impossible
18extractList : TT -> Maybe TT
19extractList (App (App reflCon (App isCons lst)) _) = Just lst
20extractList _ = Nothing
22total
23has2elts : Err -> Maybe (List ErrorReportPart)
24has2elts (CantSolveGoal tm _) = do lst <- extractList tm
25 return [ TextPart "Could not prove that"
26 , TermPart lst
27 , TextPart "has at least two elements."
28 ]
29has2elts e = Just [TextPart (show e)]
31%error_handlers cadr cons1 has2elts
32%error_handlers cadr cons2 has2elts
34badCadr1 : Int
35badCadr1 = cadr []
37badCadr2 : Int
38badCadr2 = cadr [1]
40goodCadr : Int
41goodCadr = cadr [1, 2]