Merge remote-tracking branch 'origin/experiments' into sail2

1 files changed, 29 insertions, 0 deletions

diff --git a/test/mono/set2.sail b/test/mono/set2.sail
new file mode 100644
index 00000000..3bb76870
--- /dev/null
+++ b/test/mono/set2.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[32]) -> bit[64] effect pure parametric
+
+function parametric(n,v) = {
+  let (bit['n]) x = exts(v) 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[32]) -> bit[64] effect pure depends
+
+function depends(n,v) = {
+  let 'm = 2 * n in
+  let (bit['m]) x = exts(v) in
+  extz(x)
+}
+
+val unit -> bool effect pure run
+
+function run () =
+  parametric(32,0x80000000) == 0x0000000080000000 &
+  parametric(64,0x80000000) == 0xffffffff80000000 &
+  depends(16,0x80000000) == 0x0000000080000000 &
+  depends(32,0x80000000) == 0xffffffff80000000