
  0 | module Data.Compress.Utils.ConstantTable
  1 | 
  2 | import Data.Vect
  3 | import Data.Fin
  4 | import Data.IOArray.Prims
  5 | import PrimIO
  6 | 
  7 | ||| A constant table that can be read in O(1) time
  8 | export
  9 | data ConstantTable : Nat -> Type -> Type where
 10 |   MkFromArray : ArrayData e -> ConstantTable (S n) e
 11 | 
 12 | export
 13 | length : {n : Nat} -> ConstantTable n e -> Nat
 14 | length _ = n
 15 | 
 16 | export
 17 | index : Fin (S n) -> ConstantTable (S n) a -> a
 18 | index n (MkFromArray array) = unsafePerformIO $ primIO $ prim__arrayGet array (cast $ finToInteger n)
 19 | 
 20 | export
 21 | index_bits8 : Bits8 -> ConstantTable 256 a -> a
 22 | index_bits8 n (MkFromArray array) = unsafePerformIO $ primIO $ prim__arrayGet array (cast n)
 23 | 
 24 | export
 25 | from_vect : {n : Nat} -> Vect (S n) a -> ConstantTable (S n) a
 26 | from_vect (x :: xs) = unsafePerformIO $ do
 27 |   array <- primIO $ prim__newArray (cast (S n)) x
 28 |   let indexed_array = zip (drop 1 Fin.range) xs
 29 |   traverse_ (\(i,v) => primIO $ prim__arraySet array (cast $ finToInteger i) v) indexed_array
 30 |   pure $ MkFromArray array
 31 |