From 3df7a4ce50624468a3677e0a59bbfe0e0fd1b86e Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Thu, 6 May 2021 18:19:51 +0000
Subject: [PATCH 1/4] Add arrayCopy, arraySet, arrayRangeEqual array
 primitives. Add arrayRangeLookup and arrayRangeUpdate.

---
 lib/Array.cry | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/lib/Array.cry b/lib/Array.cry
index e178d7ff3..fdb0ec8c9 100644
--- a/lib/Array.cry
+++ b/lib/Array.cry
@@ -11,3 +11,47 @@ primitive arrayConstant : {a, b} b -> (Array a b)
 primitive arrayLookup : {a, b} (Array a b) -> a -> b
 primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)
 
+/**
+ * Copy elements from the source array to the destination array.
+ *
+ * 'arrayCopy dest_arr dest_idx src_arr src_idx len' copies the
+ * elements from 'src_arr' at indices '[src_idx .. (src_idx + len)]' into
+ * 'dest_arr' at indices '[dest_idx .. (dest_idx + len)]'.
+ *
+ * The result is undefined if either 'dest_idx + len' or 'src_idx + len'
+ * wraps around.
+ */
+primitive arrayCopy : {n, a} (Array [n] a) -> [n] -> (Array [n] a) -> [n] -> [n] -> (Array [n] a)
+/**
+ * Set elements of the given array.
+ *
+ * 'arraySet' arr idx val len' sets the elements of 'arr' at indices
+ * '[idx .. (idx + len)]' to 'val'.
+ *
+ * The result is undefined if 'idx + len' wraps around.
+ */
+primitive arraySet : {n, a} (Array [n] a) -> [n] -> a -> [n] -> (Array [n] a)
+/**
+ * Check whether the lhs array and rhs array are equal at a range of
+ * indices.
+ *
+ * 'arrayRangeEq sym lhs_arr lhs_idx rhs_arr rhs_idx len' checks whether
+ * the elements of 'lhs_arr' at indices '[lhs_idx .. (lhs_idx + len)]' and
+ * the elements of 'rhs_arr' at indices '[rhs_idx .. (rhs_idx + len)]' are
+ * equal.
+ *
+ * The result is undefined if either 'lhs_idx + len' or 'rhs_idx + len'
+ * wraps around.
+ */
+primitive arrayRangeEqual : {n, a} (Array [n] a) -> [n] -> (Array [n] a) -> [n] -> [n] -> Bool
+
+arrayRangeLookup : {a, b, n} (Integral a, fin n, n >= 1, LiteralLessThan n a) => (Array a b) -> a -> [n]b
+arrayRangeLookup arr idx = res
+  where
+    res @ i = arrayLookup arr (idx + i)
+
+arrayRangeUpdate : {a, b, n} (Integral a, fin n, n >= 1, Literal (n - 1) a) => (Array a b) -> a -> [n]b -> (Array a b)
+arrayRangeUpdate arr idx vals = arrs ! 0
+  where
+    arrs = [arr] # [ arrayUpdate acc (idx + i) val | acc <- arrs | i <- [0 .. (n - 1)] | val <- vals ]
+

From 264265f18c4c6f12ea087f5f0cd7bbd0f07d581a Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Sat, 21 Aug 2021 02:38:18 +0000
Subject: [PATCH 2/4] Address comments.

---
 lib/Array.cry | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/Array.cry b/lib/Array.cry
index fdb0ec8c9..8c06a415b 100644
--- a/lib/Array.cry
+++ b/lib/Array.cry
@@ -45,13 +45,13 @@ primitive arraySet : {n, a} (Array [n] a) -> [n] -> a -> [n] -> (Array [n] a)
  */
 primitive arrayRangeEqual : {n, a} (Array [n] a) -> [n] -> (Array [n] a) -> [n] -> [n] -> Bool
 
-arrayRangeLookup : {a, b, n} (Integral a, fin n, n >= 1, LiteralLessThan n a) => (Array a b) -> a -> [n]b
+arrayRangeLookup : {a, b, n} (Integral a, fin n, LiteralLessThan n a) => (Array a b) -> a -> [n]b
 arrayRangeLookup arr idx = res
   where
     res @ i = arrayLookup arr (idx + i)
 
-arrayRangeUpdate : {a, b, n} (Integral a, fin n, n >= 1, Literal (n - 1) a) => (Array a b) -> a -> [n]b -> (Array a b)
+arrayRangeUpdate : {a, b, n} (Integral a, fin n, LiteralLessThan n a) => (Array a b) -> a -> [n]b -> (Array a b)
 arrayRangeUpdate arr idx vals = arrs ! 0
   where
-    arrs = [arr] # [ arrayUpdate acc (idx + i) val | acc <- arrs | i <- [0 .. (n - 1)] | val <- vals ]
+    arrs = [arr] # [ arrayUpdate acc (idx + i) val | acc <- arrs | i <- [0 ..< n] | val <- vals ]
 

From b6d6281a6ff448f42331872530f6f3401d27eb88 Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Tue, 24 Aug 2021 23:10:20 +0000
Subject: [PATCH 3/4] Address comments.

---
 lib/Array.cry | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/lib/Array.cry b/lib/Array.cry
index 8c06a415b..d9aab6100 100644
--- a/lib/Array.cry
+++ b/lib/Array.cry
@@ -15,8 +15,8 @@ primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)
  * Copy elements from the source array to the destination array.
  *
  * 'arrayCopy dest_arr dest_idx src_arr src_idx len' copies the
- * elements from 'src_arr' at indices '[src_idx .. (src_idx + len)]' into
- * 'dest_arr' at indices '[dest_idx .. (dest_idx + len)]'.
+ * elements from 'src_arr' at indices '[src_idx ..< (src_idx + len)]' into
+ * 'dest_arr' at indices '[dest_idx ..< (dest_idx + len)]'.
  *
  * The result is undefined if either 'dest_idx + len' or 'src_idx + len'
  * wraps around.
@@ -26,7 +26,7 @@ primitive arrayCopy : {n, a} (Array [n] a) -> [n] -> (Array [n] a) -> [n] -> [n]
  * Set elements of the given array.
  *
  * 'arraySet' arr idx val len' sets the elements of 'arr' at indices
- * '[idx .. (idx + len)]' to 'val'.
+ * '[idx ..< (idx + len)]' to 'val'.
  *
  * The result is undefined if 'idx + len' wraps around.
  */
@@ -36,8 +36,8 @@ primitive arraySet : {n, a} (Array [n] a) -> [n] -> a -> [n] -> (Array [n] a)
  * indices.
  *
  * 'arrayRangeEq sym lhs_arr lhs_idx rhs_arr rhs_idx len' checks whether
- * the elements of 'lhs_arr' at indices '[lhs_idx .. (lhs_idx + len)]' and
- * the elements of 'rhs_arr' at indices '[rhs_idx .. (rhs_idx + len)]' are
+ * the elements of 'lhs_arr' at indices '[lhs_idx ..< (lhs_idx + len)]' and
+ * the elements of 'rhs_arr' at indices '[rhs_idx ..< (rhs_idx + len)]' are
  * equal.
  *
  * The result is undefined if either 'lhs_idx + len' or 'rhs_idx + len'

From 3fb420b585eb3c0b22607897259c333ea327bcc1 Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Tue, 24 Aug 2021 23:13:54 +0000
Subject: [PATCH 4/4] Fix test.

---
 tests/regression/array.icry.stdout | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/tests/regression/array.icry.stdout b/tests/regression/array.icry.stdout
index cd311dc6c..19b44e782 100644
--- a/tests/regression/array.icry.stdout
+++ b/tests/regression/array.icry.stdout
@@ -10,6 +10,17 @@ Symbols
 =======
     
   arrayConstant : {a, b} b -> Array a b
+  arrayCopy :
+    {n, a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Array [n] a
   arrayLookup : {a, b} Array a b -> a -> b
+  arrayRangeEqual :
+    {n, a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Bool
+  arrayRangeLookup :
+    {a, b, n} (Integral a, fin n, LiteralLessThan n a) => Array a b -> a -> [n]b
+  arrayRangeUpdate :
+    {a, b, n}
+      (Integral a, fin n, LiteralLessThan n a) =>
+      Array a b -> a -> [n]b -> Array a b
+  arraySet : {n, a} Array [n] a -> [n] -> a -> [n] -> Array [n] a
   arrayUpdate : {a, b} Array a b -> a -> b -> Array a b