Support monomorphisation with set constrained integers

Also, to support this,
constant propagation for integer multiply,
fix substitution of concrete values for nvars,
size parameters in single argument functions,
fix kind for itself,
add eq_atom to prelude

2 files changed, 30 insertions, 0 deletions

diff --git a/test/mono/set.sail b/test/mono/set.sail
new file mode 100644
index 00000000..ecc06137
--- /dev/null
+++ b/test/mono/set.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+(* A function which is merely parametrised by a size does not need to be
+   monomorphised *)
+
+val forall 'n, 'n in {32,64}. [:'n:] -> bit[64] effect pure parametric
+
+function parametric(n) = {
+  let (bit['n]) x = exts(0x80000000) in
+  extz(x)
+}
+
+(* But if we do a calculation on the size then we'll need to case split *)
+
+val forall 'n, 'n in {16,32}. [:'n:] -> bit[64] effect pure depends
+
+function depends(n) = {
+  let 'm = 2 * n in
+  let (bit['m]) x = exts(0x80000000) in
+  extz(x)
+}
+
+val unit -> bool effect pure run
+
+function run () =
+  parametric(32) == 0x0000000080000000 &
+  parametric(64) == 0xffffffff80000000 &
+  depends(16) == 0x0000000080000000 &
+  depends(32) == 0xffffffff80000000
diff --git a/test/mono/tests b/test/mono/tests
index b589afe0..27e161cf 100644
--- a/test/mono/tests
+++ b/test/mono/tests
@@ -6,3 +6,4 @@ fnreduce -auto_mono
 varmatch -auto_mono
 vector -auto_mono
 union-exist -auto_mono
+set -auto_mono