
   0 | module Data.Buffer.Mutable
   1 | 
   2 | import public Data.Array.Index
   3 | import public Data.Buffer.Core
   4 | import public Data.Linear.Token
   5 | import Data.List
   6 | import Data.Vect
   7 | 
   8 | import Syntax.T1
   9 | 
  10 | %default total
  11 | 
  12 | --------------------------------------------------------------------------------
  13 | --          Reading and writing mutable byte arrays
  14 | --------------------------------------------------------------------------------
  15 | 
  16 | ||| Set a value in a mutable byte array corresponding to a position in a list
  17 | ||| used for filling said array.
  18 | export %inline
  19 | setAtSuffix : MBuffer s (length ys) -> Suffix (x::xs) ys -> Bits8 -> F1' s
  20 | setAtSuffix r v = set r (suffixToFin v)
  21 | 
  22 | ||| Safely access a value at the given byte position.
  23 | export %inline
  24 | setBits8 : MBuffer s 256 -> Bits8 -> Bits8 -> F1' s
  25 | setBits8 r x = set r (bits8ToFin x)
  26 | 
  27 | ||| Safely access a value at the given byte position.
  28 | export %inline
  29 | getBits8 : MBuffer s 256 -> Bits8 -> F1 s Bits8
  30 | getBits8 r x = get r (bits8ToFin x)
  31 | 
  32 | parameters (r : MBuffer s n)
  33 | 
  34 |   ||| Set a value at index `n - m` in a mutable byte array.
  35 |   |||
  36 |   ||| This actually uses the auto implicit argument for accessing the
  37 |   ||| the array. It is mainly useful for iterating over an array from the left
  38 |   ||| by using a natural number for counting down (see also the documentation
  39 |   ||| for `Ix`).
  40 |   export %inline
  41 |   setIx : (0 m : Nat) -> (x : Ix (S m) n) => Bits8 -> F1' s
  42 |   setIx _ = set r (ixToFin x)
  43 | 
  44 |   ||| Set a value at index `m` in a mutable byte array.
  45 |   export %inline
  46 |   setNat : (m : Nat) -> (0 lt : LT m n) => Bits8 -> F1' s
  47 |   setNat x = set r (natToFinLT x)
  48 | 
  49 |   ||| Read a value at index `n - m` from a mutable byte array.
  50 |   |||
  51 |   ||| This actually uses the auto implicit argument for accessing the
  52 |   ||| the array. It is mainly useful for iterating over an array from the left
  53 |   ||| by using a natural number for counting down (see also the documentation
  54 |   ||| for `Ix`).
  55 |   export %inline
  56 |   getIx : (0 m : Nat) -> (x : Ix (S m) n) => F1 s Bits8
  57 |   getIx _ = get r (ixToFin x)
  58 | 
  59 |   ||| Read a value at index `m` from a mutable byte array.
  60 |   |||
  61 |   ||| Since mutable arrays must be used in a linear context, and this
  62 |   ||| function "uses up" its input as far as the linearity checker is
  63 |   ||| concerned, this also returns a new `MBuffer` wrapper, which must then
  64 |   ||| again be used exactly once.
  65 |   export %inline
  66 |   getNat : (m : Nat) -> (0 lt : LT m n) => F1 s Bits8
  67 |   getNat x = get r (natToFinLT x)
  68 | 
  69 |   ||| Modify a value at index `n - m` in a mutable byte array.
  70 |   |||
  71 |   ||| This actually uses the auto implicit argument for accessing the
  72 |   ||| the array. It is mainly useful for iterating over an array from the left
  73 |   ||| by using a natural number for counting down (see also the documentation
  74 |   ||| for `Ix`).
  75 |   export %inline
  76 |   modifyIx : (0 m : Nat) -> (x : Ix (S m) n) => (Bits8 -> Bits8) -> F1' s
  77 |   modifyIx _ = modify r (ixToFin x)
  78 | 
  79 |   ||| Modify a value at index `m` in a mutable byte array.
  80 |   export %inline
  81 |   modifyNat : (m : Nat) -> (0 lt : LT m n) => (Bits8 -> Bits8) -> F1' s
  82 |   modifyNat m = modify r (natToFinLT m)
  83 | 
  84 | --------------------------------------------------------------------------------
  85 | --          Allocating Buffers
  86 | --------------------------------------------------------------------------------
  87 | 
  88 | ||| Writes the data from a list to a mutable byte array.
  89 | export
  90 | writeList :
  91 |      MBuffer s (length xs)
  92 |   -> (ys : List Bits8)
  93 |   -> {auto p : Suffix ys xs}
  94 |   -> F1' s
  95 | writeList r []        t = () # t
  96 | writeList r (y :: ys) t =
  97 |   let _ # t := setAtSuffix r p y t
  98 |    in writeList {xs} r ys t
  99 | 
 100 | parameters (r : MBuffer s n)
 101 | 
 102 |   ||| Writes the data from a vector to a mutable byte array.
 103 |   export
 104 |   writeVect : Vect k Bits8 -> Ix k n => F1' s
 105 |   writeVect           []        t = () # t
 106 |   writeVect {k = S m} (y :: ys) t =
 107 |     let _ # t := setIx r m y t
 108 |      in writeVect ys t
 109 | 
 110 |   ||| Writes the data from a vector to a mutable byte array in reverse order.
 111 |   export
 112 |   writeVectRev : (m : Nat) -> Vect k Bits8 -> (0 _ : LTE m n) => F1' s
 113 |   writeVectRev (S l) (y :: ys) t =
 114 |     let _ # t := setNat r l y t
 115 |      in writeVectRev l ys t
 116 |   writeVectRev _     _         t = () # t
 117 | 
 118 |   ||| Overwrite the values in a mutable byte array from the
 119 |   ||| given index downward with the result of the given function.
 120 |   export
 121 |   genFrom : (m : Nat) -> (0 _ : LTE m n) => (Fin n -> Bits8) -> F1' s
 122 |   genFrom 0     f t = () # t
 123 |   genFrom (S k) f t =
 124 |     let _ # t := setNat r k (f $ natToFinLT k) t
 125 |      in genFrom k f t
 126 | 
 127 |   ||| Overwrite the values in a mutable buffer from the
 128 |   ||| given index downward with the result of the given function.
 129 |   export
 130 |   genFrom' : (m : Nat) -> (0 _ : LTE m n) => (Fin n -> F1 s Bits8) -> F1' s
 131 |   genFrom' 0     f t = () # t
 132 |   genFrom' (S k) f t =
 133 |     let f' # t := f (natToFinLT k) t
 134 |         _  # t := setNat r k f' t
 135 |       in genFrom' k f t
 136 | 
 137 |   ||| Overwrite the values in a mutable byte array from the
 138 |   ||| given index upward with the results of applying the given
 139 |   ||| function repeatedly.
 140 |   export
 141 |   iterateFrom : (m : Nat) -> (ix : Ix m n) => (Bits8 -> Bits8) -> Bits8 -> F1' s
 142 |   iterateFrom 0     f v t = () # t
 143 |   iterateFrom (S k) f v t =
 144 |     let _ # t := setIx r k v t
 145 |      in iterateFrom k f (f v) t
 146 | 
 147 | --------------------------------------------------------------------------------
 148 | --          Growing Buffers
 149 | --------------------------------------------------------------------------------
 150 | 
 151 | parameters {n : Nat}
 152 |            (r : MBuffer s n)
 153 |   ||| Allocates a new mutable byte array and adds the elements from `r`
 154 |   ||| at its beginning.
 155 |   export
 156 |   mgrow : (m : Nat) -> F1 s (MBuffer s (m+n))
 157 |   mgrow m t =
 158 |     let tgt # t := mbuffer1 (m+n) t
 159 |         _   # t := copy r 0 0 n @{reflexive} @{lteAddLeft n} tgt t
 160 |      in tgt # t
 161 | 
 162 | --------------------------------------------------------------------------------
 163 | --          Appending Buffers
 164 | --------------------------------------------------------------------------------
 165 | 
 166 | parameters {m, n : Nat}
 167 |            (p : MBuffer s m)
 168 |            (q : MBuffer s n)
 169 | 
 170 |   ||| Allocates a new mutable byte array and adds the elements from `p`
 171 |   ||| at its beginning, followed by adding the elements from `q`.
 172 |   export
 173 |   mappend : F1 s (MBuffer s (m+n))
 174 |   mappend t =
 175 |     let tgt # t := mbuffer1 (m+n) t
 176 |         _   # t := copy p 0 0 m @{reflexive} @{lteAddRight m} tgt t
 177 |         _   # t := copy q 0 m n @{reflexive} tgt t
 178 |       in tgt # t
 179 | 
 180 | --------------------------------------------------------------------------------
 181 | --          Sub-Buffers
 182 | --------------------------------------------------------------------------------
 183 | 
 184 | 0 curLTE : (s : Ix m n) -> LTE c (ixToNat s) -> LTE c n
 185 | curLTE s lte = transitive lte $ ixLTE s
 186 | 
 187 | 0 curLT : (s : Ix (S m) n) -> LTE c (ixToNat s) -> LT c n
 188 | curLT s lte = let LTESucc p := ixLT s in LTESucc $ transitive lte p
 189 | 
 190 | parameters {n : Nat}
 191 |            (f : Bits8 -> Bool)
 192 |            (p : MBuffer s n)
 193 | 
 194 |   ||| Filters the values in a mutable byte array according to the given predicate.
 195 |   export
 196 |   mfilter : F1 s (m ** MBuffer s m)
 197 |   mfilter t =
 198 |     let tft # t := mbuffer1 n t
 199 |       in go 0 n tft t
 200 |     where
 201 |       go :  (m, x : Nat)
 202 |          -> (q : MBuffer s n)
 203 |          -> {auto v : Ix x n}
 204 |          -> {auto 0 prf : LTE m $ ixToNat v}
 205 |          -> F1 s (m ** MBuffer s m)
 206 |       go m Z     q t =
 207 |         let q' # t := mtake q m @{curLTE v prf} t
 208 |           in (m ** q') # t
 209 |       go m (S j) q t =
 210 |         let j' # t := getIx p j t
 211 |           in case f j' of
 212 |                True  =>
 213 |                  let () # t := setNat q m @{curLT v prf} j' t
 214 |                    in go (S m) j q t
 215 |                False =>
 216 |                  go m j q t
 217 | 
 218 | parameters {n : Nat}
 219 |            (m : Nat)
 220 |            (r : MBuffer s n)
 221 | 
 222 |   ||| Drop `m` elements from a mutable byte array.
 223 |   export
 224 |   mdrop : F1 s (MBuffer s (n `minus` m))
 225 |   mdrop t =
 226 |     let tdt # t := mbuffer1 (n `minus` m) t
 227 |         _   # t := copy r (n `minus` (n `minus` m)) 0 (n `minus` m) @{dropLemma m n} tdt t
 228 |      in tdt # t
 229 | 
 230 | --------------------------------------------------------------------------------
 231 | --          Maps and Folds
 232 | --------------------------------------------------------------------------------
 233 | 
 234 | ||| Apply a function `f` to each element of the mutable buffer.
 235 | export
 236 | mmap1 :  {n : Nat}
 237 |       -> (f : Bits8 -> F1 s Bits8)
 238 |       -> (r : MBuffer s n)
 239 |       -> F1 s (MBuffer s n)
 240 | mmap1 f r t =
 241 |   let tmt # t := mbuffer1 n t
 242 |       _   # t := genFrom' tmt n go t
 243 |     in tmt # t
 244 |   where
 245 |     go :  Fin n
 246 |        -> F1 s Bits8
 247 |     go x t =
 248 |       let x'  # t := get r x t
 249 |           x'' # t := f x' t
 250 |         in x'' # t
 251 | 
 252 | ||| Apply a function `f` to each element of the mutable buffer.
 253 | export
 254 | mmap :  {n : Nat}
 255 |      -> (f : Bits8 -> Bits8)
 256 |      -> (r : MBuffer s n)
 257 |      -> F1 s (MBuffer s n)
 258 | mmap f r t = mmap1 (\x => pure (f x)) r t
 259 | 
 260 | --------------------------------------------------------------------------------
 261 | --          Reversing Buffers
 262 | --------------------------------------------------------------------------------
 263 | 
 264 | parameters {n : Nat}
 265 |            (p : MBuffer s n)
 266 | 
 267 |   ||| Reverse the order of elements in a mutable buffer.
 268 |   export
 269 |   mreverse : F1 s (MBuffer s n)
 270 |   mreverse t =
 271 |     let trt # t := mbuffer1 n t
 272 |      in go n trt t
 273 |     where
 274 |       go :  (x : Nat)
 275 |          -> (q : MBuffer s n)
 276 |          -> {auto v : Ix x n}
 277 |          -> {auto 0 _ : LTE x n}
 278 |          -> F1 s (MBuffer s n)
 279 |       go Z     q t =
 280 |         q # t
 281 |       go (S j) q t =
 282 |         let j' # t := getIx p j t
 283 |             () # t := setNat q j j' t
 284 |           in go j q t
 285 |