Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions test/semantics/under-mask.t/run.t
Original file line number Diff line number Diff line change
@@ -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
28 changes: 28 additions & 0 deletions test/semantics/under-mask.t/under.kk
Original file line number Diff line number Diff line change
@@ -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(());
();
};
17 changes: 17 additions & 0 deletions test/semantics/underk-refinding.t/run.t
Original file line number Diff line number Diff line change
@@ -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
45 changes: 45 additions & 0 deletions test/semantics/underk-refinding.t/underk.kk
Original file line number Diff line number Diff line change
@@ -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());
};