diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/mono/itself_rewriting.sail | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/mono/itself_rewriting.sail b/test/mono/itself_rewriting.sail index 912cb99d..4540f1a5 100644 --- a/test/mono/itself_rewriting.sail +++ b/test/mono/itself_rewriting.sail @@ -83,6 +83,20 @@ function test_execute() = { execute(datasize) } +val transitive_itself : forall 'n. int('n) -> unit + +function transitive_itself(n) = { + needs_size_in_guard(n); + () +} + +val transitive_split : bool -> unit + +function transitive_split(x) = { + let n = if x then 8 else 16; + transitive_itself(n); +} + val run : unit -> unit effect {escape} function run () = { @@ -90,4 +104,7 @@ function run () = { test_execute(); willsplit(true); willsplit(false); + transitive_itself(16); + transitive_split(true); + transitive_split(false); } |
