0 | -- Despite the significant difference in the types, idea and function names taken from
  1 | -- https://github.com/idris-lang/Idris2/blob/4e8847b70372d2dffadfe31dbb540eec2280c9e1/libs/base/Data/List/Elem.idr
  2 |
  3 | module Data.CheckedEmpty.List.Lazy.Elem
  4 |
  5 | import Data.CheckedEmpty.List.Lazy
  6 |
  7 | import Data.Singleton
  8 | import Decidable.Equality
  9 | import Control.Function
 10 |
 11 | %default total
 12 |
 13 | --------------------------------------------------------------------------------
 14 | -- List membership proof
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| A proof that some element is found in a list.
 18 | public export
 19 | data Elem : a -> LazyLst ne a -> Type where
 20 |      ||| A proof that the element is at the head of the list
 21 |      Here : {0 u0 : _} -> {0 u1 : _} ->
 22 |             {0 xs : Lazy (LazyLst _ _)} ->
 23 |             Elem x $ (x :: xs) {ne} @{u0} @{u1}
 24 |      ||| A proof that the element is in the tail of the list
 25 |      There : {0 u0 : _} -> {0 u1 : _} ->
 26 |              {0 xs : Lazy (LazyLst _ _)} ->
 27 |              Elem x xs -> Elem x $ (y :: xs) @{u0} @{u1}
 28 |
 29 | export
 30 | Uninhabited (Here {u0} {u1} {x} {xs} = There {u0=u0'} {u1=u1'} {x = x'} {y} {xs=xs'} e) where
 31 |   uninhabited Refl impossible
 32 |
 33 | export
 34 | Uninhabited (There {u0} {u1} {x} {y} {xs} e = Here {u0=u0'} {u1=u1'} {x=x'} {xs=xs'}) where
 35 |   uninhabited Refl impossible
 36 |
 37 | export
 38 | Injective (There {u0} {u1} {x} {y} {xs}) where
 39 |   injective Refl = Refl
 40 |
 41 | export
 42 | DecEq (Elem x xs) where
 43 |   decEq Here          Here         = Yes Refl
 44 |   decEq (There this) (There that)  = decEqCong $ decEq this that
 45 |   decEq Here         (There later) = No absurd
 46 |   decEq (There later) Here         = No absurd
 47 |
 48 | export
 49 | Uninhabited (Elem x []) where
 50 |   uninhabited $ Here     impossible
 51 |   uninhabited $ There p impossible
 52 |
 53 | export
 54 | Uninhabited (x = z) => Uninhabited (Elem z xs) =>
 55 | Uninhabited (Elem z $ (x :: xs) @{u0} @{u1}) where
 56 |   uninhabited Here @{xz} = uninhabited Refl @{xz}
 57 |   uninhabited $ There y  = uninhabited y
 58 |
 59 | ||| An item not in the head and not in the tail is not in the list at all.
 60 | export
 61 | neitherHereNorThere : {0 xs : LazyLst ne a} ->
 62 |                       Not (x = y) -> Not (Elem x xs) ->
 63 |                       Not (Elem x $ (y :: xs) @{u0} @{u1})
 64 | neitherHereNorThere xny _    $ Here      = xny Refl
 65 | neitherHereNorThere _   xnxs $ There xxs = xnxs xxs
 66 |
 67 | ||| Check whether the given element is a member of the given list.
 68 | public export
 69 | isElem : DecEq a => (x : a) -> (xs : LazyLst ne a) -> Dec (Elem x xs)
 70 | isElem x $ [] = No absurd
 71 | isElem x $ y :: xs with (decEq x y)
 72 |   isElem x $ x :: xs | Yes Refl = Yes Here
 73 |   isElem x $ y :: xs | No xny with (isElem x xs)
 74 |     isElem x $ y :: xs       | No xny | Yes xxs = Yes $ There xxs
 75 |     isElem x $ y :: Delay xs | No xny | No xnxs = No $ neitherHereNorThere xny xnxs
 76 |
 77 | ||| Get the element at the given position.
 78 | public export
 79 | get : (xs : LazyLst ne a) -> (p : Elem x xs) -> a
 80 | get (x :: _)  $ Here    = x
 81 | get (_ :: xs) $ There p = get xs p
 82 |
 83 | ||| Get the element at the given position, with proof that it is the desired element.
 84 | public export
 85 | lookup : (xs : LazyLst ne a) -> (p : Elem x xs) -> Singleton x
 86 | lookup (x :: _)    Here    = Val x
 87 | lookup (_ :: xs) $ There p = lookup xs p
 88 |
 89 | -- ||| Remove the element at the given position.
 90 | public export
 91 | dropElem : (xs : LazyLst ne a) -> (p : Elem x xs) -> LazyLst0 a
 92 | dropElem (_ :: ys) $ Here    = relaxF ys
 93 | dropElem (x :: ys) $ There p = x :: dropElem ys p
 94 |
 95 | ||| Erase the indices, returning the numeric position of the element
 96 | public export
 97 | elemToNat : Elem x xs -> Nat
 98 | elemToNat  Here     = Z
 99 | elemToNat (There p) = S $ elemToNat p
100 |
101 | ||| Find the element with a proof at a given position, if it is valid
102 | public export
103 | indexElem : Nat -> (xs : LazyLst ne a) -> Maybe (x ** Elem x xs)
104 | indexElem  _    []        = Nothing
105 | indexElem  Z    (y :: _)  = Just (y ** Here)
106 | indexElem (S n) (_ :: ys) = indexElem n ys <&> \(x ** p) => (x ** There p)
107 |
108 | ||| Lift the membership proof to a mapped list
109 | export
110 | elemMap : {0 xs : LazyLst ne a} -> (0 f : a -> b) ->
111 |           Elem x xs -> Elem (f x) (map f xs)
112 | elemMap f $ Here    = Here
113 | elemMap f $ There e = There $ elemMap f e
114 |