git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/error004/FunErrTest.idr
42 lines 1.2 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 : NonEmpty xs}
12 -> {auto cons2 : NonEmpty (tail xs)}
13 -> a
14cadr (x :: (y :: _)) {cons1=IsNonEmpty} {cons2=IsNonEmpty} = y
15cadr (x :: []) {cons1=IsNonEmpty} {cons2=IsNonEmpty} impossible
16cadr [] {cons1=IsNonEmpty} {cons2=IsNonEmpty} impossible
18extractList : TT -> Maybe TT
19extractList (App (App neType _) lst) = Just lst
20extractList t = Just t -- Nothing
22total
23has2elts : Err -> Maybe (List ErrorReportPart)
24has2elts (CantSolveGoal tm _) = do lst <- extractList tm
25 pure [ 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]