diff --git a/test/semantics/under-mask.t/run.t b/test/semantics/under-mask.t/run.t new file mode 100644 index 0000000..7534b5b --- /dev/null +++ b/test/semantics/under-mask.t/run.t @@ -0,0 +1,9 @@ +`fun` opertions may be run at the perform-site, but they should +appear to run at the handler-site + $ koka-zero interpret under.kk + 1 + + $ export PROJECT_ROOT=../../.. + $ ../compile.sh under.kk + $ ./under + 1 diff --git a/test/semantics/under-mask.t/under.kk b/test/semantics/under-mask.t/under.kk new file mode 100644 index 0000000..359f729 --- /dev/null +++ b/test/semantics/under-mask.t/under.kk @@ -0,0 +1,28 @@ +effect ask { + fun ask(x : ()) : int; +}; + +effect fail { + control fail(x : ()) : (); +}; + +fun main() { + with handler { + control fail(_) { // fail must be handled here + print-int(1) + }; + }; + with handler { + fun ask(_) { // runs in-place at the perform-site of ask(()) + fail(()); -1; + }; + }; + with handler { + control fail(_) { // fail must not be handled here + print-int(0); + }; + }; + // perform ask(()) + ask(()); + (); +}; diff --git a/test/semantics/underk-refinding.t/run.t b/test/semantics/underk-refinding.t/run.t new file mode 100644 index 0000000..92f994f --- /dev/null +++ b/test/semantics/underk-refinding.t/run.t @@ -0,0 +1,17 @@ +Fixing the handler-site vector `w_handler` in `under` neglects +the possiblity of the handler itself being suspended and resumed +somewhere else. + +Taken from Section 2.9.2 of "Generalized Evidence Passing for Effect Handlers +(or, Efficient Compilation of Effect Handlers to C)" +by Ningning Xie and Daan Leijen + + $ koka-zero interpret underk.kk + 1 + 2 + + $ export PROJECT_ROOT=../../.. + $ ../compile.sh underk.kk + $ ./underk + 1 + 2 diff --git a/test/semantics/underk-refinding.t/underk.kk b/test/semantics/underk-refinding.t/underk.kk new file mode 100644 index 0000000..583c917 --- /dev/null +++ b/test/semantics/underk-refinding.t/underk.kk @@ -0,0 +1,45 @@ +effect evil { + control evil(x : ()) : (); +}; + +// not relevant that `read` is tail-resumptive +effect read { + fun ask(x : ()) : int; +}; + +// relevant that `tl` is tail resumptive! +effect tl { + fun tl(x : ()) : int; +}; + +// run a resumption under a different handler context +fun f(k) { + with handler { // h_read2 + fun ask(_) { 2 }; + }; + k(()); // 5: resume `evil` now with a different `ask` handler +}; + +fun g() { + with handler { // h_read1 + fun ask(_) { 1 }; + }; + with handler { // h_evil + control evil(_) { + // 4: leak resumption to later resume under changed handler context + resume; // FIXME: leaking like this fails the occurs check :/ + }; + }; + with handler { // h_tl + fun tl(_) { + ask(()).print-int(); // 2: receive value 1 + evil(()); // 3: perform `evil` within tail-resumptive operation clause + ask(()).print-int(); // 6: recieve value 2 + }; + }; + tl(); // 1: perform `tl` +}; + +fun main() { + f(g()); +};