Monomorphisation improvements for aarch64_small

- additional rewrites (signed extend of subrange@zeros, subrange assignment,
  variants with casts)
- drop # from new top-level type variables (e.g., n_times_8) so that the
  rewriter knows that they're safe to include in casts
- add casts in else-branches when only one possible value for a size is left
- add casts when assertions force a size to be a particular value
- don't use types to detect set constraints in analysis because we won't
  know which part of the assertion should be replaced
- also use non-top-level type variables when simplifying sizes in analysis
  (useful when it can from pattern matching on an ast)
- cope with repeated int('n) in a pattern match (!)

3 files changed, 39 insertions, 1 deletions

diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index bb1bc952..e8fbabb0 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -33,6 +33,14 @@ function foo(n, x) =
     64 => let z = y@y@y@y in let dfsf = 4 in z
   }
 
+val foo_if : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure
+
+function foo_if(n, x) =
+  let y : bits(16) = extzv(x) in
+  if n == 32
+  then y@y
+  else /* 64 */ let z = y@y@y@y in let dfsf = 4 in z
+
 val use : bits(16) -> unit effect pure
 
 function use(x) = ()
@@ -45,6 +53,13 @@ function bar(x) =
    16 => use(x)
   }
 
+val bar_if : forall 'n, 'n in {8,16}. bits('n) -> unit effect pure
+
+function bar_if(x) =
+  if 'n == 8
+  then use(x@x)
+  else /* 16 */ use(x)
+
 val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef}
 
 function ret(n, x) =
@@ -116,4 +131,4 @@ function run () = {
     assert(foo2(64,0x12) == 0x0012001200120012);
     assert(foo3(4,0x12) == 0x00120012);
     assert(foo3(8,0x12) == 0x0012001200120012);
-}
\ No newline at end of file
+}
diff --git a/test/mono/pass/repeatedint b/test/mono/pass/repeatedint
new file mode 100644
index 00000000..ff26c84d
--- /dev/null
+++ b/test/mono/pass/repeatedint
@@ -0,0 +1 @@
+repeatedint.sail -auto_mono
diff --git a/test/mono/repeatedint.sail b/test/mono/repeatedint.sail
new file mode 100644
index 00000000..2d01e814
--- /dev/null
+++ b/test/mono/repeatedint.sail
@@ -0,0 +1,22 @@
+/* Silly, but it did appear in a model, and we didn't handle it... */
+
+default Order dec
+$include <prelude.sail>
+
+union ast = {
+  SomeInstr : {'size, 'size in {8,16}. (int('size), int('size))}
+}
+
+val test : ast -> bits(32)
+
+function test(SomeInstr(s as int('size),r)) = {
+  x : bits('size) = sail_zero_extend(0x80, s);
+  sail_sign_extend(x,32)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+  assert(test(SomeInstr(8,8)) == 0xffffff80);
+  assert(test(SomeInstr(16,16)) == 0x00000080);
+}