Add alternative definitions of aarch64 functions for monomorphisation

1 files changed, 10 insertions, 0 deletions

diff --git a/aarch64/mono/BigEndianReverse.sail b/aarch64/mono/BigEndianReverse.sail
new file mode 100644
index 00000000..23b222f4
--- /dev/null
+++ b/aarch64/mono/BigEndianReverse.sail
@@ -0,0 +1,10 @@
+val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0.
+  bits('width) -> bits('width) effect {escape}
+
+function BigEndianReverse value_name = {
+  assert(('width == 8) | (('width == 16) | (('width == 32) | (('width == 64) | ('width == 128)))));
+  result : bits('width) = replicate_bits(0b0,'width);
+  foreach (i from 0 to ('width - 1) by 8)
+    result[i+7 .. i] = (value_name['width-i - 1 .. 'width-i - 8] : bits(8));
+  return result
+}