Monomorphisation tweaks for v8.5

Various tweaks to the monomorphisation rewrites.  Disable old sizeof
rewriting for Lem backend and rely on the type checker rewriting
implicit arguments.  Also avoid unifying nexps with sums, as this can
easily fail due to commutativity and associativity.

2 files changed, 60 insertions, 34 deletions

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 8259ec47..90d74149 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -19,13 +19,9 @@ overload operator >> = {shiftright}
 val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order).
     (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
 
-val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extzv(v) = extz_vec(sizeof('m),v)
+val extzv = "extz_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
 
-val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extsv(v) = exts_vec(sizeof('m),v)
+val extsv = "exts_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
 
 /* This is generated internally to deal with case splits which reveal the size
    of a bitvector */
@@ -34,9 +30,9 @@ val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect p
 
 /* Definitions for the rewrites */
 
-val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure
-function slice_mask(i,l) =
-  let one : bits('n) = extzv(0b1) in
+val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) effect pure
+function slice_mask(n,i,l) =
+  let one : bits('n) = extzv(n, 0b1) in
   ((one << l) - one) << i
 
 val is_zero_subrange : forall 'n, 'n >= 0.
@@ -46,6 +42,13 @@ function is_zero_subrange (xs, i, j) = {
   (xs & slice_mask(j, i-j+1)) == extzv(0b0)
 }
 
+val is_zeros_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect pure
+
+function is_zeros_slice (xs, i, l) = {
+  (xs & slice_mask(i, l)) == extzv(0b0)
+}
+
 val is_ones_subrange : forall 'n, 'n >= 0.
   (bits('n), int, int) -> bool effect pure
 
@@ -54,21 +57,29 @@ function is_ones_subrange (xs, i, j) = {
   (xs & m) == m
 }
 
+val is_ones_slice : forall 'n, 'n >= 0.
+  (bits('n), int, int) -> bool effect pure
+
+function is_ones_slice (xs, i, j) = {
+  let m : bits('n) = slice_mask(i,j) in
+  (xs & m) == m
+}
+
 val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0.
-  (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure
+  (implicit('r), bits('n), int, int, bits('m), int, int) -> bits('r) effect pure
 
-function slice_slice_concat (xs, i, l, ys, i', l') = {
+function slice_slice_concat (r, xs, i, l, ys, i', l') = {
   let xs = (xs & slice_mask(i,l)) >> i in
   let ys = (ys & slice_mask(i',l')) >> i' in
-  extzv(xs) << l' | extzv(ys)
+  extzv(r, xs) << l' | extzv(r, ys)
 }
 
-val slice_zeros_concat : forall 'n 'p 'q 'r, 'r == 'p + 'q & 'n >= 0 & /*'p >= 0 & 'q >= 0 &*/ 'r >= 0.
-  (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure
+val slice_zeros_concat : forall 'n 'p 'q, 'n >= 0 & 'p + 'q >= 0.
+  (bits('n), int, atom('p), atom('q)) -> bits('p + 'q) effect pure
 
 function slice_zeros_concat (xs, i, l, l') = {
   let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs) << l'
+  extzv(l + l', xs) << l'
 }
 
 /* Assumes initial vectors are of equal size */
@@ -83,44 +94,59 @@ function subrange_subrange_eq (xs, i, j, ys, i', j') = {
 }
 
 val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's >= 0 & 'n >= 0 & 'm >= 0.
-  (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
+  (implicit('s), bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
 
-function subrange_subrange_concat (xs, i, j, ys, i', j') = {
+function subrange_subrange_concat (s, xs, i, j, ys, i', j') = {
   let xs = (xs & slice_mask(j,i-j+1)) >> j in
   let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in
-  extzv(xs) << (i' - j' + 1) | extzv(ys)
+  extzv(s, xs) << (i' - j' + 1) | extzv(s, ys)
 }
 
 val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
-function place_subrange(xs,i,j,shift) = {
+function place_subrange(m,xs,i,j,shift) = {
   let xs = (xs & slice_mask(j,i-j+1)) >> j in
-  extzv(xs) << shift
+  extzv(m, xs) << shift
 }
 
 val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
-function place_slice(xs,i,l,shift) = {
+function place_slice(m,xs,i,l,shift) = {
   let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs) << shift
+  extzv(m, xs) << shift
+}
+
+val set_slice_zeros : forall 'n, 'n >= 0.
+  (atom('n), int, bits('n), int) -> bits('n) effect pure
+
+function set_slice_zeros(n, i, xs, l) = {
+  let ys : bits('n) = slice_mask(n, i, l) in
+  xs & ~(ys)
 }
 
 val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int) -> bits('m) effect pure
 
-function zext_slice(xs,i,l) = {
+function zext_slice(m,xs,i,l) = {
   let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs)
+  extzv(m, xs)
 }
 
 val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int) -> bits('m) effect pure
+  (implicit('m), bits('n), int, int) -> bits('m) effect pure
 
-function sext_slice(xs,i,l) = {
+function sext_slice(m,xs,i,l) = {
   let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in
-  extsv(xs)
+  extsv(m, xs)
+}
+
+val place_slice_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
+  (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
+
+function place_slice_signed(m,xs,i,l,shift) = {
+  sext_slice(m, xs, i, l) << shift
 }
 
 /* This has different names in the aarch64 prelude (UInt) and the other
@@ -150,9 +176,9 @@ function unsigned_subrange(xs,i,j) = {
 }
 
 
-val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure
+val zext_ones : forall 'n, 'n >= 0. (implicit('n), int) -> bits('n) effect pure
 
-function zext_ones(m) = {
+function zext_ones(n, m) = {
   let v : bits('n) = extsv(0b1) in
-  v >> ('n - m)
+  v >> (n - m)
 }
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 166db243..8c6426d4 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -166,6 +166,6 @@ val signed = {
   _: "sint"
 } : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
-overload __size = {length}
+overload __size = {__id, length}
 
 $endif