From 1c576cb068c8d2a18e672f3b0ca07d3d83064077 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Fri, 12 Jun 2020 14:08:00 +0100
Subject: [PATCH] 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         | 11 +----
 libs/base/Data/IOArray/Prims.idr   | 11 +++++
 libs/base/base.ipkg                |  1 +
 libs/contrib/Data/Linear/Array.idr | 74 ++++++++++++++++++++++++++++++
 libs/contrib/contrib.ipkg          |  2 +
 5 files changed, 89 insertions(+), 10 deletions(-)
 create mode 100644 libs/base/Data/IOArray/Prims.idr
 create mode 100644 libs/contrib/Data/Linear/Array.idr

diff --git a/libs/base/Data/IOArray.idr b/libs/base/Data/IOArray.idr
index 487127e1b..3d87dda01 100644
--- a/libs/base/Data/IOArray.idr
+++ b/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
diff --git a/libs/base/Data/IOArray/Prims.idr b/libs/base/Data/IOArray/Prims.idr
new file mode 100644
index 000000000..087da583e
--- /dev/null
+++ b/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 ()
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index b0e955755..a2c770f89 100644
--- a/libs/base/base.ipkg
+++ b/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,
diff --git a/libs/contrib/Data/Linear/Array.idr b/libs/contrib/Data/Linear/Array.idr
new file mode 100644
index 000000000..46706f411
--- /dev/null
+++ b/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'
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index cb3514d51..04af84a7f 100644
--- a/libs/contrib/contrib.ipkg
+++ b/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,