
   0 | module Data.Unique.Vect
   1 | 
   2 | import Data.Vect
   3 | import Decidable.Equality
   4 | import Decidable.Equality.Core
   5 | import Misc
   6 | 
   7 | %hide Misc.NotElem.NotElem
   8 | 
   9 | -- `UniqueVect` and `NotElem` are defined in terms of each other
  10 | mutual
  11 |   ||| A vector that cannot contain duplicates
  12 |   ||| An element can be inserted only if it is not already in the vector
  13 |   ||| Mathematically can be thought of as an ordered set
  14 |   ||| @ a The type of the elements in the list
  15 |   public export
  16 |   data UniqueVect : (0 n : Nat) -> (0 a : Type) -> DecEq a => Type where
  17 |     Nil : {0 a : Type} -> DecEq a => UniqueVect 0 a
  18 |     (::) : {0 a : Type} -> DecEq a =>
  19 |       (x : a) ->
  20 |       (xs : UniqueVect n a) ->
  21 |       {auto prf : NotElem x xs} ->
  22 |       UniqueVect (S n) a
  23 |   
  24 |   ||| A proof that an element `x` is not found in `xs`
  25 |   public export
  26 |   data NotElem : DecEq a => (x : a) -> (xs : UniqueVect n a) -> Type where
  27 |     NotInEmptyVect : DecEq a => (x : a) -> NotElem {a=a} x []
  28 |     NotInNonEmptyVect : (de : DecEq a) =>
  29 |       {x, y : a} ->
  30 |       (xs : UniqueVect n a) ->
  31 |       (ne : NotElem x xs) ->
  32 |       (neq : IsNo (decEq x y)) =>
  33 |       (prf : NotElem y xs) =>
  34 |       NotElem x (y :: xs)
  35 | 
  36 | ||| A proof that an element `x` is found in `xs`
  37 | public export
  38 | data Elem : DecEq a => (x : a) -> (xs : UniqueVect n a) -> Type where
  39 |   Here : DecEq a =>
  40 |     {x : a} ->
  41 |     {xs : UniqueVect k a} ->
  42 |     (prf : NotElem x xs) =>
  43 |     Elem x (x :: xs)
  44 |   There : DecEq a =>
  45 |     {x : a} ->
  46 |     {xs : UniqueVect k a} ->
  47 |     (prf : NotElem y xs) =>
  48 |     (later : Elem x xs) ->
  49 |     Elem x (y :: xs)
  50 | 
  51 | namespace All
  52 |   ||| A proof that elements of a unique vector satisfy a property
  53 |   public export
  54 |   data All : DecEq a => (0 p : a -> Type) -> UniqueVect rank a -> Type where
  55 |     Nil : DecEq a => {0 p : a -> Type} -> All p []
  56 |     (::) : DecEq a => {0 p : a -> Type} ->
  57 |       {0 x : a} ->
  58 |       {0 xs : UniqueVect k a} ->
  59 |       NotElem x xs =>
  60 |       p x ->
  61 |       All p xs ->
  62 |       All p (x :: xs)
  63 | 
  64 |       
  65 | ||| An element cannot be in an empty vector
  66 | public export
  67 | {x : a} -> DecEq a => Uninhabited (Elem x []) where
  68 |   uninhabited Here impossible
  69 |   uninhabited (There later) impossible
  70 | 
  71 | ||| A decision procedure for determining whether an element `x` is in `xs`
  72 | public export
  73 | decElemInUniqueVect : DecEq a =>
  74 |   (x : a) -> (xs : UniqueVect n a) -> Dec (Elem x xs)
  75 | decElemInUniqueVect x [] = No absurd
  76 | decElemInUniqueVect x (y :: ys) = case decEq x y of
  77 |   Yes Refl => Yes Here
  78 |   No neq => case decElemInUniqueVect x ys of
  79 |     Yes prf => Yes $ There prf
  80 |     No nprf => No $ \case
  81 |       Here => neq Refl
  82 |       (There later) => nprf later
  83 | 
  84 | public export
  85 | notElem : DecEq a =>
  86 |   {x : a} ->
  87 |   {xs : UniqueVect n a} ->
  88 |   Not (Elem x xs) -> NotElem x xs
  89 | notElem {xs = []} f = NotInEmptyVect x
  90 | notElem {xs = (y :: ys)} f with (decEq x y)
  91 |   _ | (Yes Refl) = absurd (f Here)
  92 |   _ | (No neq) = NotInNonEmptyVect
  93 |     {neq=(proofIneqIsNo neq)} ys (notElem (\e => f ?bb))
  94 | 
  95 | public export
  96 | toVect : DecEq a => UniqueVect n a -> Vect n a
  97 | toVect [] = []
  98 | toVect (x :: xs) = x :: toVect xs
  99 | 
 100 | ||| Converts a vector to a unique vector, removing duplicates if they exist
 101 | public export
 102 | fromVect : DecEq a => Vect n a -> (m : Nat ** UniqueVect m a)
 103 | fromVect [] = (0 ** [])
 104 | fromVect (x :: xs) =
 105 |   let (k ** t) = fromVect xs
 106 |   in case decElemInUniqueVect x t of
 107 |     Yes prf => (k ** t)
 108 |     No nprf => (S k ** (::) x t {prf=notElem nprf})
 109 | 
 110 | ||| Turn the proof that an element `x` is in a vector into the index of `x`
 111 | public export
 112 | indexOf : DecEq a => {0 n : Nat} -> {0 xs : UniqueVect n a} ->
 113 |   Elem x xs -> Fin n
 114 | indexOf Here = FZ
 115 | indexOf (There later) = FS (indexOf later)
 116 | 
 117 | public export
 118 | length : DecEq a => UniqueVect n a -> Nat
 119 | length [] = 0
 120 | length (x :: xs) = 1 + length xs
 121 | 
 122 | ||| Drop all the elements up and until the element `x` from a unique vector
 123 | public export
 124 | drop : DecEq a =>
 125 |   (xs : UniqueVect n a) ->
 126 |   (elem : Elem x xs) ->
 127 |   UniqueVect (n `minus` (finToNat (FS (indexOf elem)))) a
 128 | drop {n=S k} (_ :: xs) Here = rewrite minusZeroRight k in xs
 129 | drop (_ :: xs) (There later) = drop xs later
 130 | 
 131 | 
 132 | public export
 133 | Test1 : UniqueVect 5 String
 134 | Test1 = ["a", "b", "c", "d", "e"]
 135 | 
 136 | public export
 137 | wher : Elem "c" Test1
 138 | wher = There $ There $ Here
 139 | 
 140 | mutual
 141 |   ||| Remove element from a unique vector at a given index
 142 |   public export
 143 |   removeIndex : DecEq a =>
 144 |     {n : Nat} ->
 145 |     (xs : UniqueVect (S n) a) ->
 146 |     Fin (S n) ->
 147 |     UniqueVect n a
 148 |   removeIndex (x :: xs) FZ = xs
 149 |   removeIndex {n = (S k)} (x :: xs) (FS i)
 150 |     = (::) x (removeIndex xs i) {prf=removingElemIsStillNotElem}
 151 | 
 152 |   ||| Given a vector `xs` and a proof that `x` is not in `xs`, then even if
 153 |   ||| we remove any elemens from `xs`, `x` will still not be in the result
 154 |   public export
 155 |   removingElemIsStillNotElem : DecEq a =>
 156 |     {n : Nat} ->
 157 |     {x : a} ->
 158 |     {xs : UniqueVect (S n) a} ->
 159 |     {i : Fin (S n)} ->
 160 |     (ne : NotElem x xs) =>
 161 |     NotElem x (removeIndex xs i)
 162 |   removingElemIsStillNotElem {xs = (_ :: _)} {ne = (NotInNonEmptyVect _ ne)} {i = FZ}
 163 |     = ne
 164 |   removingElemIsStillNotElem {n = (S k)} {xs = (y :: ys)} {ne = (NotInNonEmptyVect ys ne)} {i = (FS j)}
 165 |     = NotInNonEmptyVect (removeIndex ys j) removingElemIsStillNotElem {prf=removingElemIsStillNotElem} 
 166 | 
 167 | ||| If `x` is not equal to `y`, then `x` is not in the list `[y]`
 168 | ||| It seems that Idris manages to discover this proof automatically, so 
 169 | ||| this is not needed in practice
 170 | ||| Its dual is needed, hence the %hint in for the declaration below
 171 | public export
 172 | notEqualNotElem : DecEq a =>
 173 |   {x, y : a} ->
 174 |   (neq : IsNo (decEq x y)) ->
 175 |   NotElem x [y]
 176 | notEqualNotElem _ = NotInNonEmptyVect [] (NotInEmptyVect x)
 177 | 
 178 | %hint
 179 | public export
 180 | notEqualNotElem2 : DecEq a =>
 181 |   {x, y : a} ->
 182 |   (neq : IsNo (decEq x y)) ->
 183 |   NotElem y [x]
 184 | notEqualNotElem2 neq = notEqualNotElem {x=y} {y=x} (isNoSym neq)
 185 | 
 186 | ||| Number of elements found in any of two unique vectors
 187 | ||| Effectively, union
 188 | public export
 189 | numUnique : {n, m : Nat} -> DecEq a => UniqueVect n a -> UniqueVect m a -> Nat
 190 | numUnique [] _ = m
 191 | numUnique (x :: xs) ys = case decElemInUniqueVect x ys of
 192 |   Yes _ => numUnique xs ys -- found in ys, so don't count it again
 193 |   No _ => 1 + numUnique xs ys -- not found in ys, so count it
 194 | 
 195 | ||| Number of elements found in both of the two unique vectors
 196 | ||| Effectively, intersection
 197 | public export
 198 | numOverlap : {n, m : Nat} -> DecEq a =>
 199 |   UniqueVect n a -> UniqueVect m a -> Nat
 200 | numOverlap [] ys = 0
 201 | numOverlap (x :: xs) ys = case decElemInUniqueVect x ys of
 202 |   Yes _ => 1 + numOverlap xs ys -- found also in ys, so count it
 203 |   No _ => numOverlap xs ys
 204 | 
 205 | ||| Number of elements that are found in one but not both of the two vectors
 206 | ||| Effectively, symmetric difference
 207 | public export
 208 | numSymmetricDifference : {n, m : Nat} -> DecEq a =>
 209 |   UniqueVect n a -> UniqueVect m a -> Nat
 210 | numSymmetricDifference [] ys = m
 211 | numSymmetricDifference (x :: xs) ys = case decElemInUniqueVect x ys of
 212 |   -- need to pattern match on Elem to propagate length information
 213 |   Yes Here => numSymmetricDifference xs (removeIndex ys FZ)
 214 |   Yes (There later) => numSymmetricDifference xs (removeIndex ys (FS (indexOf later)))
 215 |   No _ => 1 + numSymmetricDifference xs ys
 216 | 
 217 | mutual
 218 |   public export infixr 5 +++
 219 | 
 220 |   ||| Union
 221 |   public export
 222 |   (+++) : DecEq a =>
 223 |     (xs : UniqueVect n a) ->
 224 |     (ys : UniqueVect m a) ->
 225 |     UniqueVect (numUnique xs ys) a
 226 |   [] +++ ys = ys
 227 |   (x :: xs) +++ ys with (decElemInUniqueVect x ys)
 228 |     _ | (Yes prf) = xs +++ ys -- x :: (xs +++ ys)
 229 |     _ | (No nprf) = (::) x (xs +++ ys) {prf=expandUnique {prfy=notElem nprf}}
 230 | 
 231 |   ||| If `x` is not in `xs` nor `ys`, then it also won't be in `xs +++ ys`
 232 |   public export
 233 |   expandUnique : DecEq a =>
 234 |     {x : a} ->
 235 |     {xs : UniqueVect n a} ->
 236 |     {ys : UniqueVect m a} ->
 237 |     (prfx : NotElem x xs) =>
 238 |     (prfy : NotElem x ys) =>
 239 |     NotElem x (xs +++ ys)
 240 |   -- todo implement this
 241 | 
 242 | mutual
 243 |   public export
 244 |   intersect : DecEq a =>
 245 |     (xs : UniqueVect n a) ->
 246 |     (ys : UniqueVect m a) ->
 247 |     UniqueVect (numOverlap xs ys) a
 248 |   intersect [] ys = []
 249 |   intersect (x :: xs) ys with (decElemInUniqueVect x ys)
 250 |     _ | (Yes prf) = (::) x (intersect xs ys) {prf=notElemIntersect}
 251 |     _ | (No nprf) = intersect xs ys
 252 | 
 253 |   ||| If `x` is not in `xs`, then we can intersect `xs` with any other list,
 254 |   ||| and `x` still wont' be in the result (even if `x` was in the other list)
 255 |   public export
 256 |   notElemIntersect : DecEq a =>
 257 |     {x : a} ->
 258 |     {xs : UniqueVect n a} ->
 259 |     {ys : UniqueVect m a} ->
 260 |     (prfx : NotElem x xs) =>
 261 |     (prfy : Elem x ys) =>
 262 |     NotElem x (intersect xs ys)
 263 | 
 264 | 
 265 | ||| All elements of the intersection of two vectors `xs` and `ys`
 266 | ||| will be elements of `xs`
 267 | public export
 268 | allElemIntersectFst : DecEq a => 
 269 |   (xs : UniqueVect n a) ->
 270 |   (ys : UniqueVect m a) ->
 271 |   All (\x => Elem x xs) (intersect xs ys)
 272 | allElemIntersectFst = ?allElemIntersect_rhs
 273 | 
 274 | ||| All elements of the intersection of two vectors `xs` and `ys`
 275 | ||| will be elements of `ys`
 276 | public export
 277 | allElemIntersectSnd : DecEq a => 
 278 |   (xs : UniqueVect n a) ->
 279 |   (ys : UniqueVect m a) ->
 280 |   All (\x => Elem x ys) (intersect xs ys)
 281 | allElemIntersectSnd = ?allElemIntersect_rhs2
 282 | 
 283 | mutual
 284 |   public export
 285 |   symmetricDifference : DecEq a => {n, m : Nat} ->
 286 |     (xs : UniqueVect n a) ->
 287 |     (ys : UniqueVect m a) ->
 288 |     UniqueVect (numSymmetricDifference xs ys) a
 289 |   symmetricDifference [] ys = ys
 290 |   symmetricDifference (x :: xs) ys = ?aaa
 291 |   
 292 |   -- with (decElemInUniqueVect x ys)
 293 |     -- _ | Yes p = ?aaa
 294 |     -- _ | No neq = ?bbb
 295 | 
 296 | 
 297 | 
 298 | 
 299 |   public export
 300 |   l1 : UniqueVect 3 String
 301 |   l1 = ["a", "b", "c"]
 302 | 
 303 |   public export
 304 |   l2 : UniqueVect 3 String
 305 |   l2 = ["c", "d", "e"]
 306 | 
 307 |   public export
 308 |   l3 : UniqueVect 5 String
 309 |   l3 = l1 +++ l2
 310 | 
 311 |   public export
 312 |   l4 : UniqueVect 1 String
 313 |   l4 = intersect l1 l2
 314 | 
 315 |     -- expandUnique {xs = []} {ys = (_ :: _)} prf = prf
 316 |     -- expandUnique {xs = (x :: xs)} {ys = (y :: ys)} prf = case decElemInUniqueVect x ys of
 317 |     --   Yes prf' => expandUnique {prf=prf'} xs ys
 318 | 
 319 |   -- fromVect : DecEq a => Vect n a -> UniqueVect n a
 320 |   -- fromVect [] = []
 321 |   -- fromVect (x :: xs) = case fromVect xs of
 322 |   --   Yes _ => x :: fromVect xs
 323 |   --   No _ => fromVect xs