Add experimental support for linear arrays

Backed by Data.IOArray. Also moved the array external primitives to a
separate module Data.IOArray.Prims, since the next step is to add a
linear bounded array type where the bounds checks are done at compile
time, so we'll want to read and write without bounds likes.

libs/base/Data/IOArray.idr

@@ -1,17 +1,8 @@
 module Data.IOArray
 
+import Data.IOArray.Prims
 import Data.List
 
--- Implemented externally
-data ArrayData : Type -> Type where
-
--- 'unsafe' primitive access, backend dependent
--- get and set assume that the bounds have been checked. Behavious is undefined
--- otherwise.
-%extern prim__newArray : forall a . Int -> a -> PrimIO (ArrayData a)
-%extern prim__arrayGet : forall a . ArrayData a -> Int -> PrimIO a
-%extern prim__arraySet : forall a . ArrayData a -> Int -> a -> PrimIO ()
-
 export
 record IOArray elem where
   constructor MkIOArray

libs/base/Data/IOArray/Prims.idr

@@ -0,0 +1,11 @@
+module Data.IOArray.Prims
+
+export
+data ArrayData : Type -> Type where [external]
+
+-- 'unsafe' primitive access, backend dependent
+-- get and set assume that the bounds have been checked. Behaviour is undefined
+-- otherwise.
+export %extern prim__newArray : forall a . Int -> a -> PrimIO (ArrayData a)
+export %extern prim__arrayGet : forall a . ArrayData a -> Int -> PrimIO a
+export %extern prim__arraySet : forall a . ArrayData a -> Int -> a -> PrimIO ()

libs/base/base.ipkg

@@ -13,6 +13,7 @@ modules = Control.App,
           Data.Either,
           Data.Fin,
           Data.IOArray,
+          Data.IOArray.Prims,
           Data.IORef,
           Data.List,
           Data.List.Elem,

libs/contrib/Data/Linear/Array.idr

@@ -0,0 +1,74 @@
+module Data.Linear.Array
+
+import Data.IOArray
+
+-- Linear arrays. General idea: mutable arrays are constructed linearly,
+-- using newArray. Once everything is set up, they can be converted to
+-- read only arrays with constant time, pure, access, using toIArray.
+
+-- Immutable arrays which can be read in constant time, but not updated
+public export
+interface Array arr where
+  read : (1 _ : arr t) -> Int -> Maybe t
+  size : (1 _ : arr t) -> Int
+
+-- Mutable arrays which can be used linearly
+public export
+interface Array arr => MArray arr where
+  newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> a) -> a
+  -- Array is unchanged if the index is out of bounds
+  write : (1 _ : arr t) -> Int -> t -> arr t
+
+  mread : (1 _ : arr t) -> Int -> LPair (Maybe t) (arr t)
+  msize : (1 _ : arr t) -> LPair Int (arr t)
+
+export
+data IArray : Type -> Type where
+     MkIArray : IOArray t -> IArray t
+
+export
+data LinArray : Type -> Type where
+     MkLinArray : IOArray t -> LinArray t
+
+-- Convert a mutable array to an immutable array
+export
+toIArray : (1 _ : LinArray t) -> (IArray t -> a) -> a
+toIArray (MkLinArray arr) k = k (MkIArray arr)
+
+export
+Array LinArray where
+  read (MkLinArray a) i = unsafePerformIO (readArray a i)
+  size (MkLinArray a) = max a
+
+export
+MArray LinArray where
+  newArray size k = k (MkLinArray (unsafePerformIO (newArray size)))
+
+  write (MkLinArray a) i el
+      = unsafePerformIO (do writeArray a i el
+                            pure (MkLinArray a))
+  msize (MkLinArray a) = max a # MkLinArray a
+  mread (MkLinArray a) i
+      = unsafePerformIO (readArray a i) # MkLinArray a
+
+export
+Array IArray where
+  read (MkIArray a) i = unsafePerformIO (readArray a i)
+  size (MkIArray a) = max a
+
+export
+copyArray : MArray arr => (newsize : Int) -> (1 _ : arr t) -> (arr t, arr t)
+copyArray newsize a
+    = let size # a = msize a in
+          newArray newsize $
+            (\a' => copyContent (min (newsize - 1) (size - 1)) a a')
+  where
+    copyContent : Int -> (1 _ : arr t) -> (1 _ : arr t) -> (arr t, arr t)
+    copyContent pos a a'
+        = if pos < 0
+             then (a, a')
+             else let val # a = mread a pos
+                      a' = case val of
+                                  Nothing => a'
+                                  Just v => write a' pos v in
+                      copyContent (pos - 1) a a'

libs/contrib/contrib.ipkg

@@ -2,6 +2,8 @@ package contrib
 
 modules = Control.Delayed,
 
+          Data.Linear.Array,
+
           Data.List.TailRec,
           Data.List.Equalities,
           Data.List.Reverse,