
  0 | module Data.FVect.Capacity
  1 | 
  2 | import Data.FVect
  3 | import Data.Nat
  4 | import Decidable.Equality
  5 | 
  6 | finPrf : {n : Nat}
  7 |       -> (x : Fin (S n))
  8 |       -> Either (finToNat x `LT` n) (finToNat x = n)
  9 | finPrf {n = 0} FZ = Right Refl
 10 | finPrf {n = (S k)} FZ = Left (LTESucc LTEZero)
 11 | finPrf {n = (S k)} (FS x) = bimap LTESucc (\p => cong S p) $ finPrf x
 12 | 
 13 | ||| A representation of the remaining capacity an FVect has for storage.
 14 | ||| A `Full` value has proof that there are `n` values in a vect with
 15 | ||| capacity `n`.
 16 | ||| A `NotFull` value has exactly what you need to cons an additional
 17 | ||| value onto an FVect.
 18 | public export
 19 | data Capacity : Type -> Type where
 20 |   Full : (0 eqPrf : finToNat l = c)
 21 |       -> Capacity (FVect c l e)
 22 |   NotFull : {0 n : Nat}
 23 |          -> {0 len : Fin (S (S n))}
 24 |          -> (0 ltPrf : (finToNat len) `LT` (S n))
 25 |          -> Capacity (FVect (S n) len e)
 26 | 
 27 | ||| Determine if the given FVect has more capacity for storage or not.
 28 | export
 29 | capacity : {c : Nat}
 30 |         -> {l : Fin (S c)}
 31 |         -> (0 _ : FVect c l e)
 32 |         -> Capacity (FVect c l e)
 33 | capacity {c} _ with (finPrf l)
 34 |   capacity {c}         _ | (Right eq) = Full eq
 35 |   capacity {c = (S k)} _ | (Left lte) = NotFull lte
 36 | 
 37 | ||| Calculate if the given FVect has more capacity for storage or not.
 38 | export
 39 | capacity' : {c : Nat}
 40 |          -> {0 l : Fin (S c)}
 41 |          -> FVect c l e
 42 |          -> Capacity (FVect c l e)
 43 | capacity' {c = 0} [] = Full Refl
 44 | capacity' {c = (S k)} [] = NotFull (LTESucc LTEZero)
 45 | capacity' {c = (S k)} (x :: xs) with (capacity' xs)
 46 |   capacity' {c = (S k)} (x :: xs) | (Full eqPrf) =
 47 |     Full (rewrite eqPrf in Refl)
 48 |   capacity' {c = (S (S n))} (x :: xs) | (NotFull ltPrf) =
 49 |     NotFull (LTESucc ltPrf)
 50 | 
 51 |