0 | module Data.Vect.Elem
  1 |
  2 | import Data.Singleton
  3 | import Data.Vect
  4 | import Decidable.Equality
  5 |
  6 | %default total
  7 |
  8 | --------------------------------------------------------------------------------
  9 | -- Vector membership proof
 10 | --------------------------------------------------------------------------------
 11 |
 12 | ||| A proof that some element is found in a vector
 13 | public export
 14 | data Elem : a -> Vect k a -> Type where
 15 |   Here : Elem x (x::xs)
 16 |   There : (later : Elem x xs) -> Elem x (y::xs)
 17 |
 18 | export
 19 | Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs = xs'} e) where
 20 |   uninhabited Refl impossible
 21 |
 22 | export
 23 | Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs = xs'}) where
 24 |   uninhabited Refl impossible
 25 |
 26 | export
 27 | Injective (There {x} {y} {xs}) where
 28 |   injective Refl = Refl
 29 |
 30 | export
 31 | DecEq (Elem x xs) where
 32 |   decEq Here Here = Yes Refl
 33 |   decEq (There this) (There that) = decEqCong $ decEq this that
 34 |   decEq Here (There later) = No absurd
 35 |   decEq (There later) Here = No absurd
 36 |
 37 | export
 38 | Uninhabited (Elem x []) where
 39 |   uninhabited Here impossible
 40 |
 41 | export
 42 | Uninhabited (x = z) => Uninhabited (Elem z xs) => Uninhabited (Elem z $ x::xs) where
 43 |   uninhabited Here @{xz} = uninhabited Refl @{xz}
 44 |   uninhabited (There y) = uninhabited y
 45 |
 46 | ||| An item not in the head and not in the tail is not in the Vect at all
 47 | export
 48 | neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
 49 | neitherHereNorThere xneqy xninxs  Here         = xneqy Refl
 50 | neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs
 51 |
 52 | ||| A decision procedure for Elem
 53 | public export
 54 | isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
 55 | isElem x [] = No uninhabited
 56 | isElem x (y::xs) with (decEq x y)
 57 |   isElem x (x::xs) | (Yes Refl) = Yes Here
 58 |   isElem x (y::xs) | (No xneqy) with (isElem x xs)
 59 |     isElem x (y::xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
 60 |     isElem x (y::xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
 61 |
 62 | ||| Get the element at the given position.
 63 | public export
 64 | get : (xs : Vect n a) -> (p : Elem x xs) -> a
 65 | get (x :: _) Here = x
 66 | get (_ :: xs) (There p) = get xs p
 67 |
 68 | ||| Get the element at the given position, with proof that it is the desired element.
 69 | public export
 70 | lookup : (xs : Vect n a) -> (p : Elem x xs) -> Singleton x
 71 | lookup (x :: _) Here = Val x
 72 | lookup (_ :: xs) (There p) = lookup xs p
 73 |
 74 | public export
 75 | replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
 76 | replaceElem (x::xs) Here y = (y :: xs ** Here)
 77 | replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
 78 |   replaceElem (x::xs) (There xinxs) y | (ys ** yinys) = (x :: ys ** There yinys)
 79 |
 80 | public export
 81 | replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t
 82 | replaceByElem (x::xs)  Here         y = y :: xs
 83 | replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y
 84 |
 85 | public export
 86 | mapElem : {0 xs : Vect k t} -> {0 f : t -> u} ->
 87 |           (1 _ : Elem x xs) -> Elem (f x) (map f xs)
 88 | mapElem  Here     = Here
 89 | mapElem (There e) = There (mapElem e)
 90 |
 91 | ||| Remove the element at the given position.
 92 | |||
 93 | ||| @xs The vector to be removed from
 94 | ||| @p A proof that the element to be removed is in the vector
 95 | public export
 96 | dropElem : (xs : Vect (S k) t) -> Elem x xs -> Vect k t
 97 | dropElem (x::ys)         Here         = ys
 98 | dropElem (x::ys@(_::_)) (There later) = x :: dropElem ys later
 99 |
100 | ||| Erase the indices, returning the bounded numeric position of the element
101 | public export
102 | elemToFin : {0 xs : Vect n a} -> Elem x xs -> Fin n
103 | elemToFin  Here     = FZ
104 | elemToFin (There p) = FS (elemToFin p)
105 |
106 | ||| Find the element with a proof at a given bounded position
107 | public export
108 | indexElem : (1 _ : Fin n) -> (xs : Vect n a) -> (x ** Elem x xs)
109 | indexElem  FZ    (y::_)  = (y ** Here)
110 | indexElem (FS n) (_::ys) = let (x ** p) = indexElem n ys in
111 |                            (x ** There p)
112 |