0 | module Data.SnocList.Elem
 1 |
 2 | import Data.Singleton
 3 | import Data.SnocList
 4 | import Decidable.Equality
 5 | import Control.Function
 6 |
 7 | ||| A proof that some element is found in a list.
 8 | public export
 9 | data Elem : a -> SnocList a -> Type where
10 |   ||| A proof that the element is at the head of the list
11 |   Here : Elem x (sx :< x)
12 |   ||| A proof that the element is in the tail of the list
13 |   There : {0 x, y : a} -> Elem x sx -> Elem x (sx :< y)
14 |
15 | export
16 | Uninhabited (Here {x} {sx} = There {x = x'} {y} {sx = sx'} e) where
17 |   uninhabited Refl impossible
18 |
19 | export
20 | Uninhabited (There {x} {y} {sx} e = Here {x = x'} {sx = sx'}) where
21 |   uninhabited Refl impossible
22 |
23 | export
24 | Injective (There {x} {y} {sx}) where
25 |   injective Refl = Refl
26 |
27 | export
28 | DecEq (Elem x sx) where
29 |   decEq Here Here = Yes Refl
30 |   decEq (There this) (There that) = decEqCong $ decEq this that
31 |   decEq Here (There later) = No absurd
32 |   decEq (There later) Here = No absurd
33 |
34 | public export
35 | Uninhabited (Elem {a} x [<]) where
36 |   uninhabited Here impossible
37 |   uninhabited (There p) impossible
38 |
39 | ||| An item not in the head and not in the tail is not in the list at all.
40 | public export
41 | neitherHereNorThere : Not (x = y) -> Not (Elem x sx) -> Not (Elem x (sx :< y))
42 | neitherHereNorThere xny _ Here = xny Refl
43 | neitherHereNorThere _ xnxs (There xxs) = xnxs xxs
44 |
45 | ||| Check whether the given element is a member of the given list.
46 | public export
47 | isElem : DecEq a => (x : a) -> (sx : SnocList a) -> Dec (Elem x sx)
48 | isElem x [<] = No absurd
49 | isElem x (sx :< y) with (decEq x y)
50 |   isElem x (sx :< x) | Yes Refl = Yes Here
51 |   isElem x (sx :< y) | No xny with (isElem x sx)
52 |     isElem x (sx :< y) | No xny | Yes xsx = Yes (There xsx)
53 |     isElem x (sx :< y) | No xny | No xnsx = No (neitherHereNorThere xny xnsx)
54 |
55 | ||| Get the element at the given position.
56 | public export
57 | get : (sx : SnocList a) -> (p : Elem x sx) -> a
58 | get (_ :< x) Here = x
59 | get (sx :< _) (There p) = get sx p
60 |
61 | ||| Get the element at the given position, with proof that it is the desired element.
62 | public export
63 | lookup : (sx : SnocList a) -> (p : Elem x sx) -> Singleton x
64 | lookup (_ :< x) Here = Val x
65 | lookup (sx :< _) (There p) = lookup sx p
66 |
67 | ||| Remove the element at the given position.
68 | public export
69 | dropElem : (sx : SnocList a) -> (p : Elem x sx) -> SnocList a
70 | dropElem (sy :< _) Here = sy
71 | dropElem (sy :< y) (There p) = (dropElem sy p) :< y
72 |
73 | ||| Erase the indices, returning the numeric position of the element
74 | public export
75 | elemToNat : Elem x sx -> Nat
76 | elemToNat Here = Z
77 | elemToNat (There p) = S (elemToNat p)
78 |
79 | ||| Find the element with a proof at a given position (in reverse), if it is valid
80 | public export
81 | indexElem : Nat -> (sx : SnocList a) -> Maybe (x ** Elem x sx)
82 | indexElem _ [<] = Nothing
83 | indexElem Z (_ :< y) = Just (y ** Here)
84 | indexElem (S k) (sy :< _) = (\(y ** p) => (y ** There p)) `map` (indexElem k sy)
85 |
86 | ||| Lift the membership proof to a mapped list
87 | export
88 | elemMap : (0 f : a -> b) -> Elem x sx -> Elem (f x) (map f sx)
89 | elemMap f Here = Here
90 | elemMap f (There el) = There $ elemMap f el
91 |