Add alternative definitions of aarch64 functions for monomorphisation

1 files changed, 35 insertions, 0 deletions

diff --git a/aarch64/mono/_slice.sail b/aarch64/mono/_slice.sail
new file mode 100644
index 00000000..2bac9f8c
--- /dev/null
+++ b/aarch64/mono/_slice.sail
@@ -0,0 +1,35 @@
+val IsZero_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect {escape}
+
+function IsZero_slice (xs, i, 'l) = {
+  assert(constraint('l >= 0));
+  IsZero(xs & slice_mask(i, l))
+}
+
+val IsOnes_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect {escape}
+
+function IsOnes_slice (xs, i, 'l) = {
+  assert(constraint('l >= 0));
+  let m : bits('n) = slice_mask(i,l) in
+  (xs & m) == m
+}
+
+val ZeroExtend_slice_append : forall 'n 'm 'o, 'n >= 0 & 'm >= 0 & 'o >= 0.
+  (bits('n), int, int, bits('m)) -> bits('o) effect {escape}
+
+function ZeroExtend_slice_append (xs, i, 'l, ys) = {
+  assert(constraint('l >= 0));
+  let xs = xs & slice_mask(i,l) in
+  let xs : bits('o) = ZeroExtend(xs >> i) << 'm in
+  let ys : bits('o) = ZeroExtend(ys) in
+  xs | ys
+}
+
+val IsZero_slice2 : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect {escape}
+
+function IsZero_slice2 (xs, i, 'l) = {
+  assert(constraint('l >= 0));
+  IsZero(xs & slice_mask(i, l))
+}