diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/mono/control_deps.sail | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/test/mono/control_deps.sail b/test/mono/control_deps.sail new file mode 100644 index 00000000..eaefd129 --- /dev/null +++ b/test/mono/control_deps.sail @@ -0,0 +1,44 @@ +(* Test monomorphisation control dependencies *) + +default Order dec + +val (bool,bool) -> unit effect pure f + +function f(nosplit,split) = { + if nosplit then { + let (exist 'x, true. [:'x:]) 'x = if split then 16 else 32 in + let (bit['x]) v = extz(0b0) in + () + } else () +} + +val (bool,bool) -> unit effect pure g + +function g(split,nosplit) = { + (exist 'x, true. [:'x:]) x := 16; + (exist 'y, true. [:'y:]) y := 16; + if split then + x := 32 + else + (); + if nosplit then + y := 32 + else + (); + let (exist 'z, true. [:'z:]) 'z = x in + let (bit['z]) v = extz(0b0) in + () +} + +typedef exception = unit + +val bool -> unit effect {escape} h + +(* Note: we don't really need to split on b, but it's awkward to avoid. + The important bit is not to overreact to the exception. *) +function h(b) = { + let (exist 'x, true. [:'x:]) 'x = + if b then 16 else throw () in + let (bit['x]) v = extz(0b0) in + () +} |
