diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/mono/set.sail | 29 | ||||
| -rw-r--r-- | test/mono/tests | 1 |
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 |
