0 | module Decidable.HDec
 1 |
 2 | import public Data.List.Quantifiers
 3 | import public Data.Maybe0
 4 |
 5 | %default total
 6 |
 7 | --------------------------------------------------------------------------------
 8 | --          HDec0
 9 | --------------------------------------------------------------------------------
10 |
11 | ||| Hemi-decidability for erased predicates
12 | public export
13 | interface HDec0 (0 a : Type) (0 p : a -> Type) | p where
14 |   hdec0 : (v : a) -> Maybe0 (p v)
15 |
16 | public export
17 | hdec0All : HDec0 a p => (vs : List a) -> Maybe0 (All p vs)
18 | hdec0All (x :: xs) = case hdec0 {p} x of
19 |   Just0 v  => map (v::) $ hdec0All xs
20 |   Nothing0 => Nothing0
21 | hdec0All [] = Just0 []
22 |
23 | public export %inline
24 | HDec0 a p => HDec0 (List a) (All p) where hdec0 = hdec0All
25 |
26 | public export
27 | hdec0Any : HDec0 a p => (vs : List a) -> Maybe0 (Any p vs)
28 | hdec0Any (x :: xs) = case hdec0 {p} x of
29 |   Just0 v  => Just0 $ Here v
30 |   Nothing0 => map There $ hdec0Any xs
31 | hdec0Any [] = Nothing0
32 |
33 | public export %inline
34 | HDec0 a p => HDec0 (List a) (Any p) where hdec0 = hdec0Any
35 |
36 | --------------------------------------------------------------------------------
37 | --          HDec
38 | --------------------------------------------------------------------------------
39 |
40 | ||| Hemi-decidability for non-erased predicates
41 | public export
42 | interface HDec (0 a : Type) (0 p : a -> Type) | p where
43 |   hdec : (v : a) -> Maybe (p v)
44 |
45 | public export
46 | hdecAll : HDec a p => (vs : List a) -> Maybe (All p vs)
47 | hdecAll (x :: xs) = case hdec {p} x of
48 |   Just v  => map (v::) $ hdecAll xs
49 |   Nothing => Nothing
50 | hdecAll [] = Just []
51 |
52 | public export %inline
53 | HDec a p => HDec (List a) (All p) where hdec = hdecAll
54 |