GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

Add arrayCopy, arraySet, arrayRangeEqual array primitives. (#1268)

Browse Source 
* Add arrayCopy, arraySet, arrayRangeEqual array primitives. Add arrayRangeLookup and arrayRangeUpdate.

* Address comments.

* Address comments.

* Fix test.
This commit is contained in:
Andrei Stefanescu 2021-08-25 12:02:55 -07:00 committed by GitHub
parent b8bff7b9b3
commit 052228e79a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 55 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
lib/Array.cry
View File

@ -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, 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, 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] | val <- vals ]

11
tests/regression/array.icry.stdout
View File

@ -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