From 645db983e6e89abfd9257201cfd335c65349c2db Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Mon, 18 Nov 2024 16:56:30 +0100
Subject: [PATCH 01/25] add parser and lexer support for new try clauses

---
 .../scala/effekt/RecursiveDescentTests.scala  | 31 ++++++++++++
 .../shared/src/main/scala/effekt/Lexer.scala  |  6 ++-
 .../main/scala/effekt/RecursiveDescent.scala  | 49 ++++++++++++++++++-
 3 files changed, 83 insertions(+), 3 deletions(-)

diff --git a/effekt/jvm/src/test/scala/effekt/RecursiveDescentTests.scala b/effekt/jvm/src/test/scala/effekt/RecursiveDescentTests.scala
index 7f426ffa8..8e43f94be 100644
--- a/effekt/jvm/src/test/scala/effekt/RecursiveDescentTests.scala
+++ b/effekt/jvm/src/test/scala/effekt/RecursiveDescentTests.scala
@@ -448,6 +448,37 @@ class RecursiveDescentTests extends munit.FunSuite {
       with Eff3 { def op(x, y) = { x } def op2() = { () }}
       """
     )
+    parseTry(
+      """try { 42 }
+      with Empty {}
+      suspend { println("hello") }
+      resume { x => println("resuming...")}
+      return { x => x}
+      """
+    )
+    parseTry(
+      """try 42 with Empty {}
+      return { (x: Int) => x }
+      """
+    )
+    parseTry(
+      """try 42
+      return { (x: Int) => x }
+      """
+    )
+    parseTry(
+      """try "a"
+      with Empty {}
+      finally { _ => println("done") }
+      """
+    )
+    intercept[Throwable] {
+      parseTry(
+        """try { 42 }
+        resume { println("resuming") }
+        """
+      )
+    }
   }
 
   test("Type definition") {
diff --git a/effekt/shared/src/main/scala/effekt/Lexer.scala b/effekt/shared/src/main/scala/effekt/Lexer.scala
index 32049d7c1..74d8d0423 100644
--- a/effekt/shared/src/main/scala/effekt/Lexer.scala
+++ b/effekt/shared/src/main/scala/effekt/Lexer.scala
@@ -108,6 +108,9 @@ enum TokenKind {
   case `is`
   case `namespace`
   case `pure`
+  // case `on`
+  case `suspend`
+  case `finally`
 }
 object TokenKind {
   // "Soft" keywords
@@ -135,7 +138,8 @@ object TokenKind {
     `let`, `true`, `false`, `val`, `var`, `if`, `else`, `while`, `type`, `effect`, `interface`,
     `try`, `with`, `case`, `do`, `fun`, `match`, `def`, `module`, `import`, `export`, `extern`,
     `include`, `record`, `box`, `unbox`, `return`, `region`, `resource`, `new`, `and`, `is`,
-    `namespace`, `pure`)
+    `namespace`, `pure`, `suspend`, `resume`, `finally`
+  )
 
 }
 
diff --git a/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala b/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
index 8dcffbeb7..3a3c6082f 100644
--- a/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
+++ b/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
@@ -659,8 +659,17 @@ class RecursiveDescent(positions: Positions, tokens: Seq[Token], source: Source)
   */
   def tryExpr(): Term =
     nonterminal:
-      `try` ~> stmt() ~ someWhile(handler(), `with`) match {
-        case s ~ hs => TryHandle(s, hs)
+      `try` ~> stmt() ~ manyWhile(handler(), `with`) ~ maybeOnSuspend() ~ maybeOnResume() ~ maybeOnReturn() ~ maybeFinally() match {
+        case _ ~ _ ~ None ~ Some(_) ~ _ ~ _ =>
+          fail("Got `on resume` clause but no `on suspend` clause.")
+        case _ ~ _ ~ _ ~ Some(_) ~ _ ~ Some(_) =>
+          fail("Got both an `on return` and `finally` clause.")
+        case _ ~ _ ~ _ ~ _ ~ Some(_) ~ Some(_) =>
+          fail("got both an `on resume` and `finally` clause.")
+        case s ~ hs ~ susp ~ None ~ None ~ Some(Finally(vparam, body)) =>
+          TryHandle(s, hs, susp, Some(OnResume(vparam, body)), Some(OnReturn(vparam, body)))
+        case s ~ hs ~ susp ~ res ~ retrn ~ fin => 
+          TryHandle(s, hs, susp, res, retrn)
       }
 
   def regionExpr(): Term =
@@ -698,6 +707,42 @@ class RecursiveDescent(positions: Positions, tokens: Seq[Token], source: Source)
           Handler(capability, impl)
       }
 
+  def maybeOnSuspend(): Option[OnSuspend] =
+    nonterminal:
+      backtrack(consume(`suspend`))
+      .map { _ => OnSuspend(braces { stmts() }) }
+
+  def maybeOnResume(): Option[OnResume] =
+    nonterminal:
+      backtrack(consume(`resume`))
+      .map { _ =>
+        braces { (singleValueParamOpt() <~ `=>`) ~ stmts() } match {
+          case vparam ~ body => OnResume(vparam, body)
+        }
+      }
+
+  def maybeOnReturn(): Option[OnReturn] =
+    nonterminal:
+      backtrack(consume(`return`))
+      .map { _ =>
+        braces { (singleValueParamOpt() <~ `=>`) ~ stmts() } match {
+          case vparam ~ body => OnReturn(vparam, body)
+        }
+      }
+
+  def maybeFinally(): Option[Finally] =
+    nonterminal:
+      if (!peek(`finally`)) None
+      else {
+        `finally` ~> braces { (singleValueParamOpt() <~ `=>`) ~ stmts() } match {
+          case vparam ~ body => Some(Finally(vparam, body))
+        }
+      }
+
+  def singleValueParamOpt(): ValueParam =
+    nonterminal:
+      if (isVariable) { ValueParam(idDef(), None) } else { parens { valueParam() } }
+
   // This nonterminal uses limited backtracking: It parses the interface type multiple times.
   def implementation(): Implementation =
     nonterminal:

From 110bfd080f197398286868016141ef589da3aea7 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 19 Nov 2024 16:07:13 +0100
Subject: [PATCH 02/25] refactor finalize clause parsing and AST rep.

---
 .../scala/effekt/RecursiveDescentTests.scala  |  2 +-
 .../main/scala/effekt/RecursiveDescent.scala  | 57 +++++++------------
 .../src/main/scala/effekt/source/Tree.scala   |  6 +-
 3 files changed, 26 insertions(+), 39 deletions(-)

diff --git a/effekt/jvm/src/test/scala/effekt/RecursiveDescentTests.scala b/effekt/jvm/src/test/scala/effekt/RecursiveDescentTests.scala
index 8e43f94be..57d42787d 100644
--- a/effekt/jvm/src/test/scala/effekt/RecursiveDescentTests.scala
+++ b/effekt/jvm/src/test/scala/effekt/RecursiveDescentTests.scala
@@ -452,7 +452,7 @@ class RecursiveDescentTests extends munit.FunSuite {
       """try { 42 }
       with Empty {}
       suspend { println("hello") }
-      resume { x => println("resuming...")}
+      resume { x => println("resuming...") }
       return { x => x}
       """
     )
diff --git a/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala b/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
index 3a3c6082f..bafdae3b4 100644
--- a/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
+++ b/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
@@ -659,15 +659,15 @@ class RecursiveDescent(positions: Positions, tokens: Seq[Token], source: Source)
   */
   def tryExpr(): Term =
     nonterminal:
-      `try` ~> stmt() ~ manyWhile(handler(), `with`) ~ maybeOnSuspend() ~ maybeOnResume() ~ maybeOnReturn() ~ maybeFinally() match {
+      `try` ~> stmt() ~ manyWhile(handler(), `with`) ~ finalizerClause(`suspend`, false) ~ finalizerClause(`resume`, true) ~ finalizerClause(`return`, true) ~ finalizerClause(`finally`, true) match {
         case _ ~ _ ~ None ~ Some(_) ~ _ ~ _ =>
-          fail("Got `on resume` clause but no `on suspend` clause.")
+          fail("Got `resume` clause but no `suspend` clause.")
         case _ ~ _ ~ _ ~ Some(_) ~ _ ~ Some(_) =>
-          fail("Got both an `on return` and `finally` clause.")
+          fail("Got both an `resume` and `finally` clause.")
         case _ ~ _ ~ _ ~ _ ~ Some(_) ~ Some(_) =>
-          fail("got both an `on resume` and `finally` clause.")
-        case s ~ hs ~ susp ~ None ~ None ~ Some(Finally(vparam, body)) =>
-          TryHandle(s, hs, susp, Some(OnResume(vparam, body)), Some(OnReturn(vparam, body)))
+          fail("got both an `return` and `finally` clause.")
+        case s ~ hs ~ susp ~ None ~ None ~ Some(prog) =>
+          TryHandle(s, hs, susp, Some(prog), Some(prog))
         case s ~ hs ~ susp ~ res ~ retrn ~ fin => 
           TryHandle(s, hs, susp, res, retrn)
       }
@@ -707,42 +707,25 @@ class RecursiveDescent(positions: Positions, tokens: Seq[Token], source: Source)
           Handler(capability, impl)
       }
 
-  def maybeOnSuspend(): Option[OnSuspend] =
+  def finalizerClause(clause: TokenKind, vparam: Boolean): Option[FinalizerClause] =
     nonterminal:
-      backtrack(consume(`suspend`))
-      .map { _ => OnSuspend(braces { stmts() }) }
-
-  def maybeOnResume(): Option[OnResume] =
-    nonterminal:
-      backtrack(consume(`resume`))
-      .map { _ =>
-        braces { (singleValueParamOpt() <~ `=>`) ~ stmts() } match {
-          case vparam ~ body => OnResume(vparam, body)
-        }
-      }
-
-  def maybeOnReturn(): Option[OnReturn] =
-    nonterminal:
-      backtrack(consume(`return`))
+      backtrack { consume(clause) }
       .map { _ =>
-        braces { (singleValueParamOpt() <~ `=>`) ~ stmts() } match {
-          case vparam ~ body => OnReturn(vparam, body)
-        }
-      }
-
-  def maybeFinally(): Option[Finally] =
-    nonterminal:
-      if (!peek(`finally`)) None
-      else {
-        `finally` ~> braces { (singleValueParamOpt() <~ `=>`) ~ stmts() } match {
-          case vparam ~ body => Some(Finally(vparam, body))
+        braces {
+          backtrack { lambdaParams() <~ `=>` } ~ stmts() match {
+            // TODO better erros
+            case Some(Nil, vps, Nil) ~ body =>
+              if (!vps.isEmpty != vparam) fail(s"$clause value parameter mismatch")
+              else FinalizerClause(vps.headOption, body)
+            case Some(_, _, _) ~ _ =>
+              fail(s"$clause only expects value parameters")
+            case None ~ body =>
+              if (vparam) fail(s"$clause expects one value parameter but none were found")
+              else FinalizerClause(None, body)
+          }
         }
       }
 
-  def singleValueParamOpt(): ValueParam =
-    nonterminal:
-      if (isVariable) { ValueParam(idDef(), None) } else { parens { valueParam() } }
-
   // This nonterminal uses limited backtracking: It parses the interface type multiple times.
   def implementation(): Implementation =
     nonterminal:
diff --git a/effekt/shared/src/main/scala/effekt/source/Tree.scala b/effekt/shared/src/main/scala/effekt/source/Tree.scala
index 194b551e2..7116d7173 100644
--- a/effekt/shared/src/main/scala/effekt/source/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/source/Tree.scala
@@ -393,7 +393,8 @@ enum Term extends Tree {
    *
    * Each with-clause is modeled as an instance of type [[Handler]].
    */
-  case TryHandle(prog: Stmt, handlers: List[Handler])
+  case TryHandle(prog: Stmt, handlers: List[Handler], suspend: Option[FinalizerClause], resume: Option[FinalizerClause], retrn: Option[FinalizerClause])
+
   case Region(id: IdDef, body: Stmt) extends Term, Definition
 
   /**
@@ -461,6 +462,8 @@ case class Handler(capability: Option[BlockParam] = None, impl: Implementation)
 // currently the annotation is rejected by [[Typer]] -- after that phase, `ret` should always be `None`
 case class OpClause(id: IdRef,  tparams: List[Id], vparams: List[ValueParam], bparams: List[BlockParam], ret: Option[Effectful], body: Stmt, resume: IdDef) extends Reference
 
+case class FinalizerClause(vparam: Option[ValueParam], body: Stmt) extends Tree
+
 // Pattern Matching
 // ----------------
 
@@ -787,6 +790,7 @@ object Tree {
     def query(h: Handler)(using Context, Ctx): Res = structuralQuery(h)
     def query(h: Implementation)(using Context, Ctx): Res = structuralQuery(h)
     def query(h: OpClause)(using Context, Ctx): Res = structuralQuery(h)
+    def query(c: FinalizerClause)(using Context, Ctx): Res = structuralQuery(c)
     def query(c: MatchClause)(using Context, Ctx): Res = structuralQuery(c)
     def query(c: MatchGuard)(using Context, Ctx): Res = structuralQuery(c)
     def query(b: ExternBody)(using Context, Ctx): Res = structuralQuery(b)

From b507f3a699267d26b74c5a1e7594c453f1e77713 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 19 Nov 2024 16:08:46 +0100
Subject: [PATCH 03/25] adapt Namer

---
 effekt/shared/src/main/scala/effekt/Namer.scala | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/effekt/shared/src/main/scala/effekt/Namer.scala b/effekt/shared/src/main/scala/effekt/Namer.scala
index d97dd4fe4..a5fb0d8e5 100644
--- a/effekt/shared/src/main/scala/effekt/Namer.scala
+++ b/effekt/shared/src/main/scala/effekt/Namer.scala
@@ -397,7 +397,7 @@ object Namer extends Phase[Parsed, NameResolved] {
     case source.BlockStmt(block) =>
       Context scoped { resolveGeneric(block) }
 
-    case tree @ source.TryHandle(body, handlers) =>
+    case tree @ source.TryHandle(body, handlers, suspend, resume, ret) =>
       resolveAll(handlers)
 
       Context scoped {
@@ -411,6 +411,9 @@ object Namer extends Phase[Parsed, NameResolved] {
 
         resolveGeneric(body)
       }
+      Context scoped { suspend foreach { resolveGeneric } }
+      Context scoped { resume foreach { resolveGeneric } }
+      Context scoped { ret foreach { resolveGeneric } }
 
     case tree @ source.Region(name, body) =>
       val reg = BlockParam(Name.local(name.name), Some(builtins.TRegion))
@@ -586,6 +589,14 @@ object Namer extends Phase[Parsed, NameResolved] {
     case leaf           => ()
   }
 
+  def resolve(c: source.FinalizerClause)(using Context): Unit = {
+    val source.FinalizerClause(vp, body) = c
+    Context.scoped {
+      vp foreach { case v => Context.bind(resolve(v)) }
+      resolveGeneric(body)
+    }
+  }
+
   /**
    * Resolve Parameters as part of resolving function signatures
    *

From f59f5b5458603a50a6ebd3bdaf53d843a9d67b53 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 19 Nov 2024 16:09:12 +0100
Subject: [PATCH 04/25] adapt core and Transformer

---
 .../src/main/scala/effekt/core/Transformer.scala    | 13 +++++++++++--
 effekt/shared/src/main/scala/effekt/core/Tree.scala |  2 ++
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/core/Transformer.scala b/effekt/shared/src/main/scala/effekt/core/Transformer.scala
index c32774a1f..f3a692bff 100644
--- a/effekt/shared/src/main/scala/effekt/core/Transformer.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Transformer.scala
@@ -425,9 +425,13 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
       val compiledMatch = PatternMatchingCompiler.compile(clauses ++ defaultClause)
       Context.bind(compiledMatch)
 
-    case source.TryHandle(prog, handlers) =>
+    case source.TryHandle(prog, handlers, suspend, resume, retrn) =>
 
       val transformedProg = transform(prog)
+      // TODO
+      val transformedSuspend = suspend map { transform }
+      val transformedResume = resume map { transform }
+      val transformedReturn = retrn map { transform }
 
       val answerType = transformedProg.tpe
 
@@ -445,7 +449,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
       }
 
       val body: BlockLit = BlockLit(Nil, List(promptCapt), Nil, List(promptParam),
-        Scope(transformedHandlers, transform(prog)))
+        Scope(transformedHandlers, transformedProg))
 
       Context.bind(Reset(body))
 
@@ -641,6 +645,11 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
     })
   }
 
+  def transform(clause: source.FinalizerClause)(using Context): FinalizerClause = {
+    val source.FinalizerClause(vp, prog) = clause
+    FinalizerClause(vp map transform, transform(prog))
+  }
+
   def preprocess(sc: ValueVar, clause: source.MatchClause)(using Context): Clause =
     preprocess(List((sc, clause.pattern)), clause.guards, transform(clause.body))
 
diff --git a/effekt/shared/src/main/scala/effekt/core/Tree.scala b/effekt/shared/src/main/scala/effekt/core/Tree.scala
index 485c56e67..731aad388 100644
--- a/effekt/shared/src/main/scala/effekt/core/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Tree.scala
@@ -497,6 +497,8 @@ case class Operation(name: Id, tparams: List[Id], cparams: List[Id], vparams: Li
   val capt = body.capt -- cparams.toSet
 }
 
+case class FinalizerClause(vp: Option[ValueParam], body: Stmt) extends Tree
+
 
 object Tree {
 

From 8d89d80e1b458fd256f9b6b9bb26cb93fe085067 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 19 Nov 2024 16:09:27 +0100
Subject: [PATCH 05/25] adapt Typer

---
 .../shared/src/main/scala/effekt/Typer.scala  | 57 ++++++++++++++++++-
 1 file changed, 54 insertions(+), 3 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/Typer.scala b/effekt/shared/src/main/scala/effekt/Typer.scala
index 48849181c..7f2fea608 100644
--- a/effekt/shared/src/main/scala/effekt/Typer.scala
+++ b/effekt/shared/src/main/scala/effekt/Typer.scala
@@ -210,7 +210,14 @@ object Typer extends Phase[NameResolved, Typechecked] {
           checkStmt(body, expected)
         }
 
-      case tree @ source.TryHandle(prog, handlers) =>
+      case tree @ source.TryHandle(prog, handlers, suspend, resume, retrn) =>
+        /*
+        try { _: A }
+        with Eff { (x: B, resume: C => D) => _: D }
+        suspend { _: E }
+        resume { (x: E) => _: Unit }
+        return { (x: A) => _: D }
+        */
 
         // (1) extract all handled effects and capabilities
         val providedCapabilities: List[symbols.BlockParam] = handlers map Context.withFocus { h =>
@@ -226,13 +233,57 @@ object Typer extends Phase[NameResolved, Typechecked] {
 
         // All used captures flow into the continuation capture, except the ones handled by this handler.
         val continuationCaptHandled = Context.without(continuationCapt, providedCapabilities.map(_.capture))
+        
+        val Result(res, _) = Context.bindingCapabilities(tree, providedCapabilities) {
+          flowingInto(continuationCaptHandled) {
+            checkStmt(prog, expected)
+          }
+        }
+
+        val Result(suspendType, suspendEffs) = suspend.map {
+          case source.FinalizerClause(None, body) =>
+            checkStmt(body, None)
+          case source.FinalizerClause(Some(_), _) =>
+            INTERNAL_ERROR("Parser should ensure that the suspend clause has no value parameter")
+        }.getOrElse { Result(TUnit, Pure) }
+
+        val Result(resumeType, resumeEffs) = resume.map {
+          case source.FinalizerClause(Some(vp), body) =>
+            // check potentially annotated parameter type matches type of suspend clause
+            vp.symbol.tpe.foreach { matchExpected(_, suspendType) }
+            Context.bind(vp.symbol, suspendType)
+            // ensure that the body returns a result of type Unit
+            checkStmt(body, Some(TUnit))
+          case source.FinalizerClause(None, _) =>
+            INTERNAL_ERROR("Parser should ensure that the resume clause has a value parameter")
+        }.getOrElse { Result(TUnit, Pure) }
+
+        val Result(ret, retEffs) = retrn.map {
+          case source.FinalizerClause(Some(vp), body) =>
+            // check potentially annotated parameter type matches type of try body
+            vp.symbol.tpe.foreach { matchExpected(_, res) }
+            Context.bind(vp.symbol, res)
+            checkStmt(body, expected)
+          case source.FinalizerClause(None, _) =>
+            INTERNAL_ERROR("Parser should ensure that the return clause has a value parameter")
+        }.getOrElse {
+          // (2) Check the handled program
+          val Result(ret, effs) = Context.bindingCapabilities(tree, providedCapabilities) {
+            flowingInto(continuationCaptHandled) {
+              checkStmt(prog, expected)
+            }
+          }
+          Result(ret, Pure)
+        }
+
+        val finalizerEffs = suspendEffs ++ resumeEffs ++ retEffs
 
         // (2) Check the handled program
-        val Result(ret, effs) = Context.bindingCapabilities(tree, providedCapabilities) {
+         val Result(_, effs) = Context.bindingCapabilities(tree, providedCapabilities) {
           flowingInto(continuationCaptHandled) {
             checkStmt(prog, expected)
           }
-        }
+        } 
 
         // (3) Check the handlers
         // Also all capabilities used by the handler flow into the capture of the continuation

From 6165ac04b7d4cb0521201fd24dc7174a6ae054fb Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 19 Nov 2024 16:09:59 +0100
Subject: [PATCH 06/25] adapt Wellformedness

---
 .../shared/src/main/scala/effekt/typer/Wellformedness.scala  | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/effekt/shared/src/main/scala/effekt/typer/Wellformedness.scala b/effekt/shared/src/main/scala/effekt/typer/Wellformedness.scala
index ecfd7330b..a92f5c122 100644
--- a/effekt/shared/src/main/scala/effekt/typer/Wellformedness.scala
+++ b/effekt/shared/src/main/scala/effekt/typer/Wellformedness.scala
@@ -125,7 +125,7 @@ object Wellformedness extends Phase[Typechecked, Typechecked], Visit[WFContext]
     /**
      * For handlers we check that the return type does not mention any bound capabilities
      */
-    case tree @ source.TryHandle(prog, handlers) =>
+    case tree @ source.TryHandle(prog, handlers, suspend, resume, retrn) =>
       val bound = Context.annotation(Annotations.BoundCapabilities, tree).map(_.capture).toSet
       val usedEffects = Context.annotation(Annotations.InferredEffect, tree)
       val tpe = Context.inferredTypeOf(prog)
@@ -136,6 +136,9 @@ object Wellformedness extends Phase[Typechecked, Typechecked], Visit[WFContext]
       binding(captures = bound) { query(prog) }
 
       handlers foreach { query }
+      suspend foreach { query }
+      resume foreach { query }
+      retrn foreach { query }
 
       // Now check the return type ...
       wellformed(tpe, prog, " inferred as return type of the handled statement",

From 9b7b13d5b04764d205e38b4571b562f8530f905d Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 19 Nov 2024 16:10:23 +0100
Subject: [PATCH 07/25] adapt BoxUnboxInference

---
 .../main/scala/effekt/typer/BoxUnboxInference.scala | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/typer/BoxUnboxInference.scala b/effekt/shared/src/main/scala/effekt/typer/BoxUnboxInference.scala
index 7b0a47daf..f95ac63ac 100644
--- a/effekt/shared/src/main/scala/effekt/typer/BoxUnboxInference.scala
+++ b/effekt/shared/src/main/scala/effekt/typer/BoxUnboxInference.scala
@@ -106,8 +106,12 @@ object BoxUnboxInference extends Phase[NameResolved, NameResolved] {
         Call(IdTarget(id).inheritPosition(id), targs, rewriteAsExpr(receiver) :: vargsTransformed, bargsTransformed)
       }
 
-    case TryHandle(prog, handlers) =>
-      TryHandle(rewrite(prog), handlers.map(rewrite))
+    case TryHandle(prog, handlers, suspend, resume, retrn) =>
+      val rewrittenSusp = suspend.map { rewrite }
+      val rewrittenRes = resume.map { rewrite }
+      val rewrittenRet = retrn.map { rewrite }
+
+      TryHandle(rewrite(prog), handlers.map(rewrite), rewrittenSusp, rewrittenRes, rewrittenRet)
 
     case Region(name, body) =>
       Region(name, rewrite(body))
@@ -204,6 +208,11 @@ object BoxUnboxInference extends Phase[NameResolved, NameResolved] {
       OpClause(id, tparams, vparams, bparams, ret, rewrite(body), resume)
   }
 
+  def rewrite(c: FinalizerClause)(using Context): FinalizerClause = visit(c) {
+    case FinalizerClause(vp, body) =>
+      FinalizerClause(vp, rewrite(body))
+  }
+
   def rewrite(c: MatchClause)(using Context): MatchClause = visit(c) {
     case MatchClause(pattern, guards, body) =>
       MatchClause(pattern, guards.map(rewrite), rewrite(body))

From 180e9d4613c08af97734f9a6b34ca2ccc91fc951 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 19 Nov 2024 16:10:44 +0100
Subject: [PATCH 08/25] adapt ExplicitCapabilities

---
 .../scala/effekt/source/ExplicitCapabilities.scala   | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
index 1816ad48c..67709a906 100644
--- a/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
+++ b/effekt/shared/src/main/scala/effekt/source/ExplicitCapabilities.scala
@@ -91,8 +91,11 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
 
       Call(receiver, typeArgs, valueArgs, blockArgs ++ capabilityArgs)
 
-    case h @ TryHandle(prog, handlers) =>
+    case h @ TryHandle(prog, handlers, suspend, resume, retrn) =>
       val body = rewrite(prog)
+      val susp = suspend map { rewrite }
+      val res = resume map { rewrite }
+      val ret = retrn map { rewrite }
 
       val capabilities = Context.annotation(Annotations.BoundCapabilities, h)
 
@@ -107,7 +110,7 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
         }
       }
 
-      TryHandle(body, hs)
+      TryHandle(body, hs, susp, res, ret)
 
     case n @ source.New(impl @ Implementation(interface, clauses)) => {
       val cs = clauses map {
@@ -129,6 +132,11 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
       source.BlockLiteral(tps, vps, bps ++ capParams, rewrite(body))
   }
 
+  def rewrite(c: FinalizerClause)(using Context): FinalizerClause = {
+    val FinalizerClause(vp, body) = c
+    FinalizerClause(vp, rewrite(body))
+  }
+
   override def rewrite(body: ExternBody)(using context.Context): ExternBody = 
     body match {
       case b @ source.ExternBody.StringExternBody(ff, body) =>

From a557b152e79b5fa8496cbeac8fab16551d217e81 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 19 Nov 2024 16:10:57 +0100
Subject: [PATCH 09/25] adapt AnnotateCaptures

---
 .../src/main/scala/effekt/source/AnnotateCaptures.scala   | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/source/AnnotateCaptures.scala b/effekt/shared/src/main/scala/effekt/source/AnnotateCaptures.scala
index 2f7e520e9..75b916a03 100644
--- a/effekt/shared/src/main/scala/effekt/source/AnnotateCaptures.scala
+++ b/effekt/shared/src/main/scala/effekt/source/AnnotateCaptures.scala
@@ -55,11 +55,15 @@ object AnnotateCaptures extends Phase[Typechecked, Typechecked], Query[Unit, Cap
       val cap = Context.annotation(Annotations.CapabilityReceiver, t)
       combineAll(vargs.map(query)) ++ combineAll(bargs.map(query)) ++ CaptureSet(cap.capture)
 
-    case t @ source.TryHandle(prog, handlers) =>
+    case t @ source.TryHandle(prog, handlers, suspend, resume, retrn) =>
       val progCapture = query(prog)
+      val suspCapture = suspend map { query } getOrElse CaptureSet()
+      val resCapture = resume map { query } getOrElse CaptureSet()
+      val retCapture = retrn map { query } getOrElse CaptureSet()
+
       val boundCapture = boundCapabilities(t)
       val usedCapture = combineAll(handlers.map(query))
-      (progCapture -- boundCapture) ++ usedCapture
+      (progCapture -- boundCapture) ++ usedCapture ++ suspCapture ++ resCapture ++ retCapture
 
     case t @ source.Region(id, body) =>
       query(body) -- captureOf(id.symbol.asBlockSymbol)

From 4e2d7cf766f86b740d33959357338d1b3e9109d0 Mon Sep 17 00:00:00 2001
From: dvdvgt <40773635+dvdvgt@users.noreply.github.com>
Date: Fri, 22 Nov 2024 22:14:58 +0100
Subject: [PATCH 10/25] cherry-pick from #708: Extract `RESUME` function

---
 .../main/scala/effekt/cps/Transformer.scala   |  4 +--
 .../src/main/scala/effekt/cps/Tree.scala      |  4 +++
 .../effekt/generator/js/TransformerCps.scala  |  4 +++
 libraries/js/effekt_runtime.js                | 27 ++++++++++---------
 4 files changed, 24 insertions(+), 15 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/cps/Transformer.scala b/effekt/shared/src/main/scala/effekt/cps/Transformer.scala
index 0b7ffc54c..a1e1d6cc9 100644
--- a/effekt/shared/src/main/scala/effekt/cps/Transformer.scala
+++ b/effekt/shared/src/main/scala/effekt/cps/Transformer.scala
@@ -138,8 +138,8 @@ object Transformer {
     case core.Stmt.Resume(cont, body) =>
       val ks2 = Id("ks")
       val k2 = Id("k")
-      val thunk: BlockLit = Block.BlockLit(Nil, Nil, ks2, k2, transform(body, ks2, Continuation.Dynamic(k2)))
-      App(Block.BlockVar(cont.id), Nil, List(thunk), MetaCont(ks), k.reify)
+      Resume(cont.id, Block.BlockLit(Nil, Nil, ks2, k2, transform(body, ks2, Continuation.Dynamic(k2))),
+        MetaCont(ks), k.reify)
 
     case core.Stmt.Hole() => Hole()
 
diff --git a/effekt/shared/src/main/scala/effekt/cps/Tree.scala b/effekt/shared/src/main/scala/effekt/cps/Tree.scala
index 8c262c301..a2dbb18c9 100644
--- a/effekt/shared/src/main/scala/effekt/cps/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/cps/Tree.scala
@@ -139,6 +139,9 @@ enum Stmt extends Tree {
   // shift(p, { (resume, ks, k) => STMT }, ks, k)
   case Shift(prompt: Id, body: BlockLit, ks: MetaCont, k: Cont)
 
+  // resume(r, (ks, k) => STMT, ks, k)
+  case Resume(resumption: Id, body: BlockLit, ks: MetaCont, k: Cont)
+
   // Others
   case Hole()
 }
@@ -219,6 +222,7 @@ object Variables {
 
     case Stmt.Reset(prog, ks, k) => free(prog) ++ free(ks) ++ free(k)
     case Stmt.Shift(prompt, body, ks, k) => block(prompt) ++ free(body) ++ free(ks) ++ free(k)
+    case Stmt.Resume(r, body, ks, k) => block(r) ++ free(body) ++ free(ks) ++ free(k)
     case Stmt.Hole() => empty
   }
 
diff --git a/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala b/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
index 36b5d88b6..7478c41dd 100644
--- a/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
+++ b/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
@@ -14,6 +14,7 @@ object TransformerCps extends Transformer {
   val RUN_TOPLEVEL = Variable(JSName("RUN_TOPLEVEL"))
   val RESET = Variable(JSName("RESET"))
   val SHIFT = Variable(JSName("SHIFT"))
+  val RESUME = Variable(JSName("RESUME"))
   val THUNK = Variable(JSName("THUNK"))
   val DEALLOC = Variable(JSName("DEALLOC"))
   val TRAMPOLINE = Variable(JSName("TRAMPOLINE"))
@@ -257,6 +258,9 @@ object TransformerCps extends Transformer {
     case cps.Stmt.Shift(prompt, body, ks, k) =>
       pure(js.Return(Call(SHIFT, nameRef(prompt), noThunking { toJS(body) }, toJS(ks), toJS(k))))
 
+    case cps.Stmt.Resume(r, b, ks2, k2) =>
+      pure(js.Return(js.Call(RESUME, nameRef(r), toJS(b), toJS(ks2), toJS(k2))))
+
     case cps.Stmt.Hole() =>
       pure(js.Return($effekt.call("hole")))
   }
diff --git a/libraries/js/effekt_runtime.js b/libraries/js/effekt_runtime.js
index a57ce2db2..b1b5ff2e1 100644
--- a/libraries/js/effekt_runtime.js
+++ b/libraries/js/effekt_runtime.js
@@ -113,22 +113,23 @@ function SHIFT(p, body, ks, k) {
   cont = { stack: meta.stack, prompt: meta.prompt, backup: meta.arena.backup(), rest: cont }
   meta = meta.rest
 
-  function resumeComp(c, ks, k) {
-    let meta = { stack: k, prompt: ks.prompt, arena: ks.arena, rest: ks.rest }
-    let toRewind = cont
-    while (!!toRewind) {
-      meta = { stack: toRewind.stack, prompt: toRewind.prompt, arena: toRewind.backup(), rest: meta }
-      toRewind = toRewind.rest
-    }
+  const k1 = meta.stack
+  meta.stack = null
+  return body(cont, meta, k1)
+}
 
-    const k2 = meta.stack // TODO instead copy meta here, like elsewhere?
-    meta.stack = null
-    return () => c(meta, k2)
+// Rewind stack `cont` back onto `k` :: `ks` and resume with c
+function RESUME(cont, c, ks, k) {
+  let meta = { stack: k, prompt: ks.prompt, arena: ks.arena, rest: ks.rest }
+  let toRewind = cont
+  while (!!toRewind) {
+    meta = { stack: toRewind.stack, prompt: toRewind.prompt, arena: toRewind.backup(), rest: meta }
+    toRewind = toRewind.rest
   }
 
-  let k1 = meta.stack
+  const k1 = meta.stack // TODO instead copy meta here, like elsewhere?
   meta.stack = null
-  return body(resumeComp, meta, k1)
+  return () => c(meta, k1)
 }
 
 function RUN_TOPLEVEL(comp) {
@@ -210,4 +211,4 @@ $effekt.run = RUN
  *
  * If a runtime is available, use `$effekt.run`, instead.
  */
-$effekt.runToplevel = RUN_TOPLEVEL
\ No newline at end of file
+$effekt.runToplevel = RUN_TOPLEVEL

From 37ef6a1715b858241a6a600717f5d799f542f0e5 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 28 Nov 2024 11:19:28 +0100
Subject: [PATCH 11/25] adapt JS runtime

---
 libraries/js/effekt_runtime.js | 49 ++++++++++++++++++++++++----------
 1 file changed, 35 insertions(+), 14 deletions(-)

diff --git a/libraries/js/effekt_runtime.js b/libraries/js/effekt_runtime.js
index b1b5ff2e1..021dcee90 100644
--- a/libraries/js/effekt_runtime.js
+++ b/libraries/js/effekt_runtime.js
@@ -1,4 +1,3 @@
-
 // Common Runtime
 // --------------
 function Cell(init, region) {
@@ -63,7 +62,7 @@ function Arena(_region) {
 let _prompt = 1;
 
 const TOPLEVEL_K = (x, ks) => { throw { computationIsDone: true, result: x } }
-const TOPLEVEL_KS = { prompt: 0, arena: Arena([]), rest: null }
+const TOPLEVEL_KS = { prompt: 0, arena: Arena([]), onSuspend: null, onSuspendData: null, onResume: null, rest: null }
 
 function THUNK(f) {
   f.thunk = true
@@ -84,10 +83,11 @@ const RETURN = (x, ks) => ks.rest.stack(x, ks.rest)
 // const x = r.alloc(init); body
 
 // HANDLE(ks, ks, (p, ks, k) => { STMT })
-function RESET(prog, ks, k) {
+function RESET(prog, onSuspend, onResume, onReturn, ks, k) {
   const prompt = _prompt++;
-  const rest = { stack: k, prompt: ks.prompt, arena: ks.arena, rest: ks.rest }
-  return prog(prompt, { prompt, arena: Arena([]), rest }, RETURN)
+  const rest = { stack: k, prompt: ks.prompt, arena: ks.arena, onSuspend: ks.onSuspend, onSuspendData: ks.onSuspendData, onResume: ks.onResume, rest: ks.rest }
+  const onRet = onReturn ? (x, ks) => onReturn(x, ks.rest, ks.rest.stack) : RETURN
+  return prog(prompt, { prompt, arena: Arena([]), onSuspend: onSuspend, onSuspendData: null, onResume: onResume, rest: rest }, onRet)
 }
 
 function DEALLOC(ks) {
@@ -97,21 +97,31 @@ function DEALLOC(ks) {
   }
 }
 
-function SHIFT(p, body, ks, k) {
+function SHIFT(p, body, ks, k, cont) {
 
   // TODO avoid constructing this object
-  let meta = { stack: k, prompt: ks.prompt, arena: ks.arena, rest: ks.rest }
-  let cont = null
+  let meta = { stack: k, prompt: ks.prompt, arena: ks.arena, onSuspend: ks.onSuspend, onSuspendData: ks.onSuspendData, onResume: ks.onResume, rest: ks.rest }
+  // let cont = null
 
   while (!!meta && meta.prompt !== p) {
-    cont = { stack: meta.stack, prompt: meta.prompt, backup: meta.arena.backup(), rest: cont }
+    cont = { stack: meta.stack, prompt: meta.prompt, backup: meta.arena.backup(), onSuspend: meta.onSuspend, onSuspendData: meta.onSuspendData, onResume: meta.onResume, rest: cont }
+    if (meta.onSuspend) {
+      return meta.onSuspend(meta.rest, (x, ks) => {
+        // TODO what about ks here? It is just ignored -- doesn't seem right
+        // this will probably become a problem once a resumptive effect operation is called in onSuspend
+
+        // just change onSuspendData to retain the value returned by onSuspend
+        const contt = { ...cont, onSuspendData: x }
+        return SHIFT(p, body, meta.rest, meta.rest.stack, contt)
+      })
+    }
     meta = meta.rest
   }
   if (!meta) { throw `Prompt not found ${p}` }
 
   // package the prompt itself
-  cont = { stack: meta.stack, prompt: meta.prompt, backup: meta.arena.backup(), rest: cont }
-  meta = meta.rest
+  cont = { stack: meta.stack, prompt: meta.prompt, backup: meta.arena.backup(), onSuspend: meta.onSuspend, onSuspendData: meta.onSuspendData, onResume: meta.onResume, rest: cont }
+   meta = meta.rest
 
   const k1 = meta.stack
   meta.stack = null
@@ -119,11 +129,22 @@ function SHIFT(p, body, ks, k) {
 }
 
 // Rewind stack `cont` back onto `k` :: `ks` and resume with c
-function RESUME(cont, c, ks, k) {
-  let meta = { stack: k, prompt: ks.prompt, arena: ks.arena, rest: ks.rest }
+// TODO I do not like the additional argument b here.
+// It is needed because when resuming, that is, rewinding cont onto k :: ks, we would
+// execute the on resume clause of the top-most stack frame, however, these are not the desired semantics.
+function RESUME(cont, c, b, ks, k) {
+  let meta = { stack: k, prompt: ks.prompt, arena: ks.arena, onSuspend: ks.onSuspend, onSuspendData: ks.onSuspendData, onResume: ks.onResume, rest: ks.rest }
   let toRewind = cont
   while (!!toRewind) {
-    meta = { stack: toRewind.stack, prompt: toRewind.prompt, arena: toRewind.backup(), rest: meta }
+    if (toRewind.onResume && b) {
+      return toRewind.onResume(toRewind.onSuspendData, meta, (x, ks) => {
+        // TODO what about ks here?
+        meta = { stack: toRewind.stack, prompt: toRewind.prompt, arena: toRewind.backup(), onSuspend: toRewind.onSuspend, onSuspendData: toRewind.onSuspendData, onResume: toRewind.onResume, rest: meta }
+        return RESUME(toRewind.rest, c, true, meta, meta.stack)
+      })
+    }
+    b = true
+    meta = { stack: toRewind.stack, prompt: toRewind.prompt, arena: toRewind.backup(), onSuspend: toRewind.onSuspend, onSuspendData: toRewind.onSuspendData, onResume: toRewind.onResume, rest: meta }
     toRewind = toRewind.rest
   }
 

From c39f550637b2a7729e95532ec0a2e74269e0cc71 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 28 Nov 2024 11:19:59 +0100
Subject: [PATCH 12/25] add finally clause desugaring

---
 .../src/main/scala/effekt/RecursiveDescent.scala     | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala b/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
index bafdae3b4..908b7be91 100644
--- a/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
+++ b/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
@@ -659,15 +659,15 @@ class RecursiveDescent(positions: Positions, tokens: Seq[Token], source: Source)
   */
   def tryExpr(): Term =
     nonterminal:
-      `try` ~> stmt() ~ manyWhile(handler(), `with`) ~ finalizerClause(`suspend`, false) ~ finalizerClause(`resume`, true) ~ finalizerClause(`return`, true) ~ finalizerClause(`finally`, true) match {
-        case _ ~ _ ~ None ~ Some(_) ~ _ ~ _ =>
+      `try` ~> stmt() ~ manyWhile(handler(), `with`) ~ finalizerClause(`suspend`, false) ~ finalizerClause(`resume`, true) ~ finalizerClause(`return`, true) ~ finalizerClause(`finally`, false) match {
+        case _ ~ _ ~ None ~ Some(_) ~ _ ~ None =>
           fail("Got `resume` clause but no `suspend` clause.")
-        case _ ~ _ ~ _ ~ Some(_) ~ _ ~ Some(_) =>
-          fail("Got both an `resume` and `finally` clause.")
+        case _ ~ _ ~ Some(_) ~ _ ~ _ ~ Some(_) =>
+          fail("Got both an `suspend` and `finally` clause.")
         case _ ~ _ ~ _ ~ _ ~ Some(_) ~ Some(_) =>
           fail("got both an `return` and `finally` clause.")
-        case s ~ hs ~ susp ~ None ~ None ~ Some(prog) =>
-          TryHandle(s, hs, susp, Some(prog), Some(prog))
+        case s ~ hs ~ susp ~ None ~ None ~ Some(fin) =>
+          TryHandle(s, hs, Some(fin), None, Some(FinalizerClause(Some(ValueParam(IdDef("x"), None)), fin.body)))
         case s ~ hs ~ susp ~ res ~ retrn ~ fin => 
           TryHandle(s, hs, susp, res, retrn)
       }

From d4a5a6b25aa91b92a85a62741b7dc609b388f8a0 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 28 Nov 2024 11:20:49 +0100
Subject: [PATCH 13/25] adapt backend transformations

---
 .../src/main/scala/effekt/core/Inline.scala     | 16 +++++++++-------
 .../scala/effekt/core/PolymorphismBoxing.scala  |  4 ++--
 .../main/scala/effekt/core/PrettyPrinter.scala  |  4 ++--
 .../src/main/scala/effekt/core/Reachable.scala  |  2 +-
 .../main/scala/effekt/core/Transformer.scala    | 13 ++++++-------
 .../src/main/scala/effekt/core/Tree.scala       | 17 +++++++++++------
 .../src/main/scala/effekt/core/Type.scala       |  4 ++--
 .../src/main/scala/effekt/cps/Transformer.scala | 15 ++++++++++-----
 .../shared/src/main/scala/effekt/cps/Tree.scala |  4 ++--
 .../effekt/generator/chez/Transformer.scala     |  2 +-
 .../effekt/generator/js/TransformerCps.scala    |  9 ++++++---
 .../main/scala/effekt/machine/Transformer.scala |  2 +-
 12 files changed, 53 insertions(+), 39 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/core/Inline.scala b/effekt/shared/src/main/scala/effekt/core/Inline.scala
index 18f91c607..c5bc9f20c 100644
--- a/effekt/shared/src/main/scala/effekt/core/Inline.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Inline.scala
@@ -131,11 +131,11 @@ object Inline {
     case Stmt.Invoke(b, method, methodTpe, targs, vargs, bargs) =>
       invoke(rewrite(b), method, methodTpe, targs, vargs.map(rewrite), bargs.map(rewrite))
 
-    case Stmt.Reset(body) =>
-      rewrite(body) match {
-        case BlockLit(tparams, cparams, vparams, List(prompt), body) if !used(prompt.id) => body
-        case b => Stmt.Reset(b)
-      }
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) => s
+      // rewrite(body) match {
+      //   case BlockLit(tparams, cparams, vparams, List(prompt), body) if !used(prompt.id) => body
+      //   case b => Stmt.Reset(b)
+      // }
 
     // congruences
     case Stmt.Return(expr) => Return(rewrite(expr))
@@ -238,7 +238,8 @@ object Inline {
       case Stmt.Var(id, init, capture, body) => tailResumptive(k, body) && !freeInExpr(init)
       case Stmt.Get(id, annotatedCapt, annotatedTpe) => false
       case Stmt.Put(id, annotatedCapt, value) => false
-      case Stmt.Reset(BlockLit(tparams, cparams, vparams, bparams, body)) => tailResumptive(k, body) // is this correct?
+      // case Stmt.Reset(BlockLit(tparams, cparams, vparams, bparams, body)) => tailResumptive(k, body) // is this correct?
+      case Stmt.Reset(body, onSuspend, onResume, onReturn) => onReturn.map { blocklit => tailResumptive(k, blocklit.body) }.getOrElse(tailResumptive(k, body.body))
       case Stmt.Shift(prompt, body) => false
       case Stmt.Resume(k2, body) => k2.id == k // what if k is free in body?
       case Stmt.Hole() => true
@@ -256,7 +257,8 @@ object Inline {
     case Stmt.Region(_) => ???
     case Stmt.Alloc(id, init, region, body) => Stmt.Alloc(id, init, region, removeTailResumption(k, body))
     case Stmt.Var(id, init, capture, body) => Stmt.Var(id, init, capture, removeTailResumption(k, body))
-    case Stmt.Reset(body) => Stmt.Reset(removeTailResumption(k, body))
+    // case Stmt.Reset(body, onSuspend, onResume, onReturn) => Stmt.Reset(removeTailResumption(k, body))
+    case Stmt.Reset(_, _, _, _) => ???
     case Stmt.Resume(k2, body) if k2.id == k => body
 
     case Stmt.Resume(k, body) => stmt
diff --git a/effekt/shared/src/main/scala/effekt/core/PolymorphismBoxing.scala b/effekt/shared/src/main/scala/effekt/core/PolymorphismBoxing.scala
index c2057425c..ababdd672 100644
--- a/effekt/shared/src/main/scala/effekt/core/PolymorphismBoxing.scala
+++ b/effekt/shared/src/main/scala/effekt/core/PolymorphismBoxing.scala
@@ -338,8 +338,8 @@ object PolymorphismBoxing extends Phase[CoreTransformed, CoreTransformed] {
       Stmt.Alloc(id, transform(init), region, transform(body))
     case Stmt.Var(id, init, cap, body) =>
       Stmt.Var(id, transform(init), cap, transform(body))
-    case Stmt.Reset(body) =>
-      Stmt.Reset(transform(body))
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) =>
+      Stmt.Reset(transform(body), onSuspend.map { transform }, onResume.map { transform }, onReturn.map { transform })
     case Stmt.Shift(prompt, body) =>
       Stmt.Shift(prompt, transform(body))
     case Stmt.Resume(k, body) =>
diff --git a/effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala b/effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala
index 96d11ed33..1f7847c77 100644
--- a/effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala
+++ b/effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala
@@ -185,8 +185,8 @@ object PrettyPrinter extends ParenPrettyPrinter {
     case If(cond, thn, els) =>
       "if" <+> parens(toDoc(cond)) <+> block(toDoc(thn)) <+> "else" <+> block(toDoc(els))
 
-    case Reset(body) =>
-      "reset" <+> toDoc(body)
+    case Reset(body, onSuspend, onResume, onReturn) =>
+      "reset" <+> toDoc(body) <+> "on Suspend" <+> onSuspend.map { toDoc }.getOrElse("{}") <+> "on Resume" <+> onResume.map { toDoc }.getOrElse("{}") <+> "on Return" <+> onReturn.map { toDoc }.getOrElse("{}")
 
     case Shift(prompt, body) =>
       "shift" <> parens(toDoc(prompt)) <+> toDoc(body)
diff --git a/effekt/shared/src/main/scala/effekt/core/Reachable.scala b/effekt/shared/src/main/scala/effekt/core/Reachable.scala
index 3d51c94f0..719cf4d28 100644
--- a/effekt/shared/src/main/scala/effekt/core/Reachable.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Reachable.scala
@@ -88,7 +88,7 @@ class Reachable(
       process(body)
     case Stmt.Get(id, capt, tpe) => process(id)
     case Stmt.Put(id, tpe, value) => process(id); process(value)
-    case Stmt.Reset(body) => process(body)
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) => process(body); onSuspend.foreach { process }; onResume.foreach { process }; onReturn.foreach { process }
     case Stmt.Shift(prompt, body) => process(prompt); process(body)
     case Stmt.Resume(k, body) => process(k); process(body)
     case Stmt.Region(body) => process(body)
diff --git a/effekt/shared/src/main/scala/effekt/core/Transformer.scala b/effekt/shared/src/main/scala/effekt/core/Transformer.scala
index f3a692bff..fe2800c5f 100644
--- a/effekt/shared/src/main/scala/effekt/core/Transformer.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Transformer.scala
@@ -429,9 +429,9 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
 
       val transformedProg = transform(prog)
       // TODO
-      val transformedSuspend = suspend map { transform }
-      val transformedResume = resume map { transform }
-      val transformedReturn = retrn map { transform }
+      val transformedSuspend = suspend.map { transform }
+      val transformedResume = resume.map { transform }
+      val transformedReturn = retrn.map { transform }
 
       val answerType = transformedProg.tpe
 
@@ -450,8 +450,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
 
       val body: BlockLit = BlockLit(Nil, List(promptCapt), Nil, List(promptParam),
         Scope(transformedHandlers, transformedProg))
-
-      Context.bind(Reset(body))
+      Context.bind(Reset(body, transformedSuspend, transformedResume, transformedReturn))
 
     case r @ source.Region(name, body) =>
       val region = r.symbol
@@ -645,9 +644,9 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
     })
   }
 
-  def transform(clause: source.FinalizerClause)(using Context): FinalizerClause = {
+  def transform(clause: source.FinalizerClause)(using Context): BlockLit = {
     val source.FinalizerClause(vp, prog) = clause
-    FinalizerClause(vp map transform, transform(prog))
+    BlockLit(Nil, Nil, vp.map { transform(_) }.toList, Nil, transform(prog))
   }
 
   def preprocess(sc: ValueVar, clause: source.MatchClause)(using Context): Clause =
diff --git a/effekt/shared/src/main/scala/effekt/core/Tree.scala b/effekt/shared/src/main/scala/effekt/core/Tree.scala
index 731aad388..cfbfe02e5 100644
--- a/effekt/shared/src/main/scala/effekt/core/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Tree.scala
@@ -315,7 +315,7 @@ enum Stmt extends Tree {
 
   // binds a fresh prompt as [[id]] in [[body]] and delimits the scope of captured continuations
   //  Reset({ [cap]{p: Prompt[answer] at cap} => stmt: answer}): answer
-  case Reset(body: BlockLit)
+  case Reset(body: BlockLit, onSuspend: Option[BlockLit], onResume: Option[BlockLit], onReturn: Option[BlockLit])
 
   // captures the continuation up to the given prompt
   // Invariant, it always has the shape:
@@ -394,10 +394,10 @@ object normal {
       case other => Invoke(callee, method, methodTpe, targs, vargs, bargs)
     }
 
-  def reset(body: BlockLit): Stmt = body match {
+  def reset(body: BlockLit, onSuspend: Option[BlockLit], onResume: Option[BlockLit], onReturn: Option[BlockLit]): Stmt = body match {
     //    case BlockLit(tparams, cparams, vparams, List(prompt),
     //      Stmt.Shift(prompt2, body) if prompt.id == prompt2.id => ???
-    case other => Stmt.Reset(body)
+    case other => Stmt.Reset(body, onSuspend, onResume, onSuspend)
   }
 
   def make(tpe: ValueType.Data, tag: Id, vargs: List[Pure]): Pure =
@@ -712,7 +712,7 @@ object Variables {
     case Stmt.Put(id, annotatedCapt, value) =>
       Variables.block(id, core.Type.TState(value.tpe), annotatedCapt) ++ free(value)
 
-    case Stmt.Reset(body) => free(body)
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) => free(body) ++ all(onSuspend, free) ++ all(onResume, free) ++ all(onReturn, free)
     case Stmt.Shift(prompt, body) => free(prompt) ++ free(body)
     case Stmt.Resume(k, body) => free(k) ++ free(body)
     case Stmt.Hole() => Variables.empty
@@ -823,8 +823,13 @@ object substitutions {
       case Put(id, capt, value) =>
         Put(substituteAsVar(id), substitute(capt), substitute(value))
 
-      case Reset(body) =>
-        Reset(substitute(body).asInstanceOf[BlockLit])
+      case Reset(body, onSuspend, onResume, onReturn) =>
+        Reset(
+          substitute(body).asInstanceOf[BlockLit], 
+          onSuspend.map { substitute(_).asInstanceOf[BlockLit] },
+          onResume.map { substitute(_).asInstanceOf[BlockLit] },
+          onReturn.map { substitute(_).asInstanceOf[BlockLit] },
+        )
 
       case Shift(prompt, body) =>
         val after = substitute(body).asInstanceOf[BlockLit]
diff --git a/effekt/shared/src/main/scala/effekt/core/Type.scala b/effekt/shared/src/main/scala/effekt/core/Type.scala
index 0d8fc1f04..526c86288 100644
--- a/effekt/shared/src/main/scala/effekt/core/Type.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Type.scala
@@ -204,7 +204,7 @@ object Type {
     case Stmt.Var(id, init, cap, body) => body.tpe
     case Stmt.Get(id, capt, tpe) => tpe
     case Stmt.Put(id, capt, value) => TUnit
-    case Stmt.Reset(body) => body.returnType
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) => onReturn.map { _.returnType }.getOrElse(body.returnType)
     case Stmt.Shift(prompt, body) => body.bparams match {
       case core.BlockParam(id, BlockType.Interface(ResumeSymbol, List(result, answer)), captures) :: Nil => result
       case _ => ???
@@ -235,7 +235,7 @@ object Type {
     case Stmt.Var(id, init, cap, body) => body.capt -- Set(cap)
     case Stmt.Get(id, capt, tpe) => capt
     case Stmt.Put(id, capt, value) => capt
-    case Stmt.Reset(body) => body.capt
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) => body.capt
     case Stmt.Shift(prompt, body) => prompt.capt ++ body.capt
     case Stmt.Resume(k, body) => k.capt ++ body.capt
     case Stmt.Region(body) => body.capt
diff --git a/effekt/shared/src/main/scala/effekt/cps/Transformer.scala b/effekt/shared/src/main/scala/effekt/cps/Transformer.scala
index a1e1d6cc9..bd86d6805 100644
--- a/effekt/shared/src/main/scala/effekt/cps/Transformer.scala
+++ b/effekt/shared/src/main/scala/effekt/cps/Transformer.scala
@@ -114,13 +114,18 @@ object Transformer {
           default.map(transform(_, ks, k)))
       }
 
-    case core.Stmt.Reset(core.Block.BlockLit(_, _, _, prompt :: Nil, body)) =>
+    case core.Stmt.Reset(core.Block.BlockLit(_, _, _, prompt :: Nil, body), onSuspend, onResume, onReturn) =>
       val ks2 = Id("ks")
       val k2 = Id("k")
-      Reset(Block.BlockLit(Nil, List(prompt.id), ks2, k2, transform(body, ks2, Continuation.Dynamic(k2))),
-        MetaCont(ks), k.reify)
-
-    case core.Stmt.Reset(body) => sys error "Shouldn't happen"
+      Reset(
+        Block.BlockLit(Nil, List(prompt.id), ks2, k2, transform(body, ks2, Continuation.Dynamic(k2))),
+        onSuspend.map { transformBlockLit },
+        onResume.map { transformBlockLit },
+        onReturn.map { transformBlockLit },
+        MetaCont(ks), k.reify
+      )
+
+    case core.Stmt.Reset(body, _, _, _) => sys error "Shouldn't happen"
 
     // Only unidirectional, yet
     // core.Block.BlockLit(tparams, cparams, vparams, List(resume), body)
diff --git a/effekt/shared/src/main/scala/effekt/cps/Tree.scala b/effekt/shared/src/main/scala/effekt/cps/Tree.scala
index a2dbb18c9..cd0ba63f6 100644
--- a/effekt/shared/src/main/scala/effekt/cps/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/cps/Tree.scala
@@ -134,7 +134,7 @@ enum Stmt extends Tree {
   case Put(ref: Id, value: Pure, body: Stmt)
 
   // reset( { (p, ks, k) => STMT }, ks, k)
-  case Reset(prog: BlockLit, ks: MetaCont, k: Cont)
+  case Reset(prog: BlockLit, onSuspend: Option[BlockLit], onResume: Option[BlockLit], onReturn: Option[BlockLit], ks: MetaCont, k: Cont)
 
   // shift(p, { (resume, ks, k) => STMT }, ks, k)
   case Shift(prompt: Id, body: BlockLit, ks: MetaCont, k: Cont)
@@ -220,7 +220,7 @@ object Variables {
     case Stmt.Get(ref, id, body) => block(ref) ++ (free(body) -- value(id))
     case Stmt.Put(ref, value, body) => block(ref) ++ free(value) ++ free(body)
 
-    case Stmt.Reset(prog, ks, k) => free(prog) ++ free(ks) ++ free(k)
+    case Stmt.Reset(prog, onSuspend, onResume, onReturn, ks, k) => free(prog) ++ all(onSuspend, free) ++ all(onResume, free) ++ all(onReturn, free)
     case Stmt.Shift(prompt, body, ks, k) => block(prompt) ++ free(body) ++ free(ks) ++ free(k)
     case Stmt.Resume(r, body, ks, k) => block(r) ++ free(body) ++ free(ks) ++ free(k)
     case Stmt.Hole() => empty
diff --git a/effekt/shared/src/main/scala/effekt/generator/chez/Transformer.scala b/effekt/shared/src/main/scala/effekt/generator/chez/Transformer.scala
index ab983ef7b..fb8248eae 100644
--- a/effekt/shared/src/main/scala/effekt/generator/chez/Transformer.scala
+++ b/effekt/shared/src/main/scala/effekt/generator/chez/Transformer.scala
@@ -110,7 +110,7 @@ trait Transformer {
     case Alloc(id, init, region, body) =>
       chez.Let(List(Binding(nameDef(id), chez.Builtin("fresh", chez.Variable(nameRef(region)), toChez(init)))), toChez(body))
 
-    case Reset(body) => chez.Reset(toChez(body))
+    case Reset(body, _, _, _) => chez.Reset(toChez(body))
 
     case Shift(p, body) => chez.Shift(nameRef(p.id), toChez(body))
 
diff --git a/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala b/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
index 7478c41dd..1e0da0928 100644
--- a/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
+++ b/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
@@ -252,14 +252,17 @@ object TransformerCps extends Transformer {
         toJS(body).run(k)
     }
 
-    case cps.Stmt.Reset(prog, ks, k) =>
-      pure(js.Return(Call(RESET, toJS(prog), toJS(ks), toJS(k))))
+    case cps.Stmt.Reset(prog, onSuspend, onResume, onReturn, ks, k) =>
+      val jsSuspend = onSuspend.map { toJS }.getOrElse(js.RawExpr("null"))
+      val jsResume = onResume.map { toJS }.getOrElse(js.RawExpr("null"))
+      val jsReturn = onReturn.map { toJS }.getOrElse(js.RawExpr("null"))
+      pure(js.Return(Call(RESET, toJS(prog), jsSuspend, jsResume, jsReturn, toJS(ks), toJS(k))))
 
     case cps.Stmt.Shift(prompt, body, ks, k) =>
       pure(js.Return(Call(SHIFT, nameRef(prompt), noThunking { toJS(body) }, toJS(ks), toJS(k))))
 
     case cps.Stmt.Resume(r, b, ks2, k2) =>
-      pure(js.Return(js.Call(RESUME, nameRef(r), toJS(b), toJS(ks2), toJS(k2))))
+      pure(js.Return(js.Call(RESUME, nameRef(r), toJS(b), js.RawLiteral("false"), toJS(ks2), toJS(k2))))
 
     case cps.Stmt.Hole() =>
       pure(js.Return($effekt.call("hole")))
diff --git a/effekt/shared/src/main/scala/effekt/machine/Transformer.scala b/effekt/shared/src/main/scala/effekt/machine/Transformer.scala
index eb6a182ae..ec5f39a5a 100644
--- a/effekt/shared/src/main/scala/effekt/machine/Transformer.scala
+++ b/effekt/shared/src/main/scala/effekt/machine/Transformer.scala
@@ -208,7 +208,7 @@ object Transformer {
           Switch(value, transformedClauses, transformedDefault)
         }
 
-      case core.Reset(core.BlockLit(Nil, cparams, Nil, List(prompt), body)) =>
+      case core.Reset(core.BlockLit(Nil, cparams, Nil, List(prompt), body), _, _, _) =>
         noteParameters(List(prompt))
 
         val variable = Variable(freshName("returned"), transform(body.tpe))

From 4f0bffa46344dc739ef9985cfd08e74082cc3fef Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 28 Nov 2024 11:22:15 +0100
Subject: [PATCH 14/25] add basic test

---
 examples/pos/finalizerSemantics.check  |  5 +++++
 examples/pos/finalizerSemantics.effekt | 27 ++++++++++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 examples/pos/finalizerSemantics.check
 create mode 100644 examples/pos/finalizerSemantics.effekt

diff --git a/examples/pos/finalizerSemantics.check b/examples/pos/finalizerSemantics.check
new file mode 100644
index 000000000..90c85d962
--- /dev/null
+++ b/examples/pos/finalizerSemantics.check
@@ -0,0 +1,5 @@
+suspending inner
+resuming inner
+returning inner
+returning outer
+87
diff --git a/examples/pos/finalizerSemantics.effekt b/examples/pos/finalizerSemantics.effekt
new file mode 100644
index 000000000..ade67b90c
--- /dev/null
+++ b/examples/pos/finalizerSemantics.effekt
@@ -0,0 +1,27 @@
+effect Eff(): Unit
+
+def main() = {
+  val x = 
+    try {
+      try {
+        do Eff(); 42
+      } suspend {
+        println("suspending inner")
+      } resume {
+        _ => println("resuming inner")
+    } return { x =>
+        println("returning inner")
+        x * 2
+      }
+    } with Eff { () => resume(()) }
+    suspend {
+      println("suspending outer")
+    } resume {
+      _ => println("resuming outer")
+    } return { x =>
+      println("returning outer")
+      x + 3
+    }
+  println(x)
+  ()
+}

From 19bce8e4d86b4bb884c1b709c4a4016fd53304c6 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 3 Dec 2024 15:17:58 +0100
Subject: [PATCH 15/25] add 'on' as a soft keyword

---
 effekt/shared/src/main/scala/effekt/Lexer.scala      |  4 ++--
 .../src/main/scala/effekt/RecursiveDescent.scala     | 12 ++++++------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/Lexer.scala b/effekt/shared/src/main/scala/effekt/Lexer.scala
index 74d8d0423..613e3aed9 100644
--- a/effekt/shared/src/main/scala/effekt/Lexer.scala
+++ b/effekt/shared/src/main/scala/effekt/Lexer.scala
@@ -108,7 +108,6 @@ enum TokenKind {
   case `is`
   case `namespace`
   case `pure`
-  // case `on`
   case `suspend`
   case `finally`
 }
@@ -117,6 +116,7 @@ object TokenKind {
   val `resume` = TokenKind.Ident("resume")
   val `in` = TokenKind.Ident("in")
   val `at` = TokenKind.Ident("at")
+  val `on` = TokenKind.Ident("on")
   val `__` = Ident("_")
 
   def explain(kind: TokenKind): String = kind match {
@@ -138,7 +138,7 @@ object TokenKind {
     `let`, `true`, `false`, `val`, `var`, `if`, `else`, `while`, `type`, `effect`, `interface`,
     `try`, `with`, `case`, `do`, `fun`, `match`, `def`, `module`, `import`, `export`, `extern`,
     `include`, `record`, `box`, `unbox`, `return`, `region`, `resource`, `new`, `and`, `is`,
-    `namespace`, `pure`, `suspend`, `resume`, `finally`
+    `namespace`, `pure`, `suspend`, `resume`, `finally`, `on`
   )
 
 }
diff --git a/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala b/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
index 908b7be91..be47150c3 100644
--- a/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
+++ b/effekt/shared/src/main/scala/effekt/RecursiveDescent.scala
@@ -659,7 +659,7 @@ class RecursiveDescent(positions: Positions, tokens: Seq[Token], source: Source)
   */
   def tryExpr(): Term =
     nonterminal:
-      `try` ~> stmt() ~ manyWhile(handler(), `with`) ~ finalizerClause(`suspend`, false) ~ finalizerClause(`resume`, true) ~ finalizerClause(`return`, true) ~ finalizerClause(`finally`, false) match {
+      `try` ~> stmt() ~ manyWhile(handler(), `with`) ~ finalizerClause(`on` ~> consume(`suspend`), "suspend", false) ~ finalizerClause(`on` ~> consume(`resume`), "resume", true) ~ finalizerClause(`on` ~> consume(`return`), "return", true) ~ finalizerClause(consume(`finally`), "finally", false) match {
         case _ ~ _ ~ None ~ Some(_) ~ _ ~ None =>
           fail("Got `resume` clause but no `suspend` clause.")
         case _ ~ _ ~ Some(_) ~ _ ~ _ ~ Some(_) =>
@@ -707,20 +707,20 @@ class RecursiveDescent(positions: Positions, tokens: Seq[Token], source: Source)
           Handler(capability, impl)
       }
 
-  def finalizerClause(clause: TokenKind, vparam: Boolean): Option[FinalizerClause] =
+  def finalizerClause[T](prefix: => T, name: String, vparam: Boolean): Option[FinalizerClause] =
     nonterminal:
-      backtrack { consume(clause) }
+      backtrack { prefix }
       .map { _ =>
         braces {
           backtrack { lambdaParams() <~ `=>` } ~ stmts() match {
             // TODO better erros
             case Some(Nil, vps, Nil) ~ body =>
-              if (!vps.isEmpty != vparam) fail(s"$clause value parameter mismatch")
+              if (!vps.isEmpty != vparam) fail(s"$name value parameter mismatch")
               else FinalizerClause(vps.headOption, body)
             case Some(_, _, _) ~ _ =>
-              fail(s"$clause only expects value parameters")
+              fail(s"$name only expects value parameters")
             case None ~ body =>
-              if (vparam) fail(s"$clause expects one value parameter but none were found")
+              if (vparam) fail(s"$name expects one value parameter but none were found")
               else FinalizerClause(None, body)
           }
         }

From 468bd907113b5e204842fcfc0b874eabd9cff908 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 3 Dec 2024 15:18:43 +0100
Subject: [PATCH 16/25] change SHIFT function such that an empty continuation
 is passed

---
 .../src/main/scala/effekt/generator/js/TransformerCps.scala     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala b/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
index 1e0da0928..87bedac96 100644
--- a/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
+++ b/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
@@ -259,7 +259,7 @@ object TransformerCps extends Transformer {
       pure(js.Return(Call(RESET, toJS(prog), jsSuspend, jsResume, jsReturn, toJS(ks), toJS(k))))
 
     case cps.Stmt.Shift(prompt, body, ks, k) =>
-      pure(js.Return(Call(SHIFT, nameRef(prompt), noThunking { toJS(body) }, toJS(ks), toJS(k))))
+      pure(js.Return(Call(SHIFT, nameRef(prompt), noThunking { toJS(body) }, toJS(ks), toJS(k), js.RawExpr("null"))))
 
     case cps.Stmt.Resume(r, b, ks2, k2) =>
       pure(js.Return(js.Call(RESUME, nameRef(r), toJS(b), js.RawLiteral("false"), toJS(ks2), toJS(k2))))

From 6cde193bd14c4d255e5ff94ff52b48c5fdb989ef Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 3 Dec 2024 15:23:38 +0100
Subject: [PATCH 17/25] add some missing cases for Reachable and PrettyPrinter

---
 .../src/main/scala/effekt/core/Inline.scala   | 27 +++++++++++--------
 .../scala/effekt/core/PrettyPrinter.scala     |  2 +-
 .../main/scala/effekt/core/Reachable.scala    |  6 ++++-
 .../src/main/scala/effekt/core/Tree.scala     |  2 --
 4 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/core/Inline.scala b/effekt/shared/src/main/scala/effekt/core/Inline.scala
index c5bc9f20c..34a1c413a 100644
--- a/effekt/shared/src/main/scala/effekt/core/Inline.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Inline.scala
@@ -99,7 +99,7 @@ object Inline {
   def blockDefFor(id: Id)(using ctx: InlineContext): Option[Block] =
     ctx.defs.get(id) map {
       // TODO rewriting here leads to a stack overflow in one test, why?
-      case Definition.Def(id, block) => block //rewrite(block)
+      case Definition.Def(id, block) => rewrite(block)
       case Definition.Let(id, _, binding) => INTERNAL_ERROR("Should not happen")
     }
 
@@ -131,11 +131,11 @@ object Inline {
     case Stmt.Invoke(b, method, methodTpe, targs, vargs, bargs) =>
       invoke(rewrite(b), method, methodTpe, targs, vargs.map(rewrite), bargs.map(rewrite))
 
-    case Stmt.Reset(body, onSuspend, onResume, onReturn) => s
-      // rewrite(body) match {
-      //   case BlockLit(tparams, cparams, vparams, List(prompt), body) if !used(prompt.id) => body
-      //   case b => Stmt.Reset(b)
-      // }
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) =>
+      // TODO figure out inlining rules for new clauses
+      // conjecture: we cannot inline the body of a reset clause, since even if the prompt is unused, we still need to
+      // account for on suspend and resume clauses when a shift to another prompt occurs.
+      Stmt.Reset(rewrite(body), onSuspend.map { rewrite }, onResume.map { rewrite }, onReturn.map { rewrite })
 
     // congruences
     case Stmt.Return(expr) => Return(rewrite(expr))
@@ -144,9 +144,9 @@ object Inline {
     case Stmt.Match(scrutinee, clauses, default) =>
       patternMatch(rewrite(scrutinee), clauses.map { case (id, value) => id -> rewrite(value) }, default.map(rewrite))
     case Stmt.Alloc(id, init, region, body) => Alloc(id, rewrite(init), region, rewrite(body))
-    case Stmt.Shift(prompt, b @ BlockLit(tparams, cparams, vparams, List(k), body)) if tailResumptive(k.id, body) =>
-      C.inlineCount.next()
-      rewrite(removeTailResumption(k.id, body))
+    // case Stmt.Shift(prompt, b @ BlockLit(tparams, cparams, vparams, List(k), body)) if tailResumptive(k.id, body) =>
+    //   C.inlineCount.next()
+    //   rewrite(removeTailResumption(k.id, body))
 
     case Stmt.Shift(prompt, body) => Shift(prompt, rewrite(body))
 
@@ -239,7 +239,8 @@ object Inline {
       case Stmt.Get(id, annotatedCapt, annotatedTpe) => false
       case Stmt.Put(id, annotatedCapt, value) => false
       // case Stmt.Reset(BlockLit(tparams, cparams, vparams, bparams, body)) => tailResumptive(k, body) // is this correct?
-      case Stmt.Reset(body, onSuspend, onResume, onReturn) => onReturn.map { blocklit => tailResumptive(k, blocklit.body) }.getOrElse(tailResumptive(k, body.body))
+      // case Stmt.Reset(body, onSuspend, onResume, onReturn) => onReturn.map { blocklit => tailResumptive(k, blocklit.body) }.getOrElse(tailResumptive(k, body.body))
+      case Stmt.Reset(body, onSuspend, onResume, onReturn) => false
       case Stmt.Shift(prompt, body) => false
       case Stmt.Resume(k2, body) => k2.id == k // what if k is free in body?
       case Stmt.Hole() => true
@@ -258,7 +259,11 @@ object Inline {
     case Stmt.Alloc(id, init, region, body) => Stmt.Alloc(id, init, region, removeTailResumption(k, body))
     case Stmt.Var(id, init, capture, body) => Stmt.Var(id, init, capture, removeTailResumption(k, body))
     // case Stmt.Reset(body, onSuspend, onResume, onReturn) => Stmt.Reset(removeTailResumption(k, body))
-    case Stmt.Reset(_, _, _, _) => ???
+    // case Stmt.Reset(body, suspend, resume, Some(ret)) =>
+    //   Stmt.Reset(body, resume, suspend, Some(removeTailResumption(k, ret)))
+    // case Stmt.Reset(body, suspend, resume, ret) =>
+    //   Stmt.Reset(removeTailResumption(k, body), suspend, resume, ret)
+    case Stmt.Reset(body, suspend, resume, ret) => stmt
     case Stmt.Resume(k2, body) if k2.id == k => body
 
     case Stmt.Resume(k, body) => stmt
diff --git a/effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala b/effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala
index 1f7847c77..2658ad93b 100644
--- a/effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala
+++ b/effekt/shared/src/main/scala/effekt/core/PrettyPrinter.scala
@@ -186,7 +186,7 @@ object PrettyPrinter extends ParenPrettyPrinter {
       "if" <+> parens(toDoc(cond)) <+> block(toDoc(thn)) <+> "else" <+> block(toDoc(els))
 
     case Reset(body, onSuspend, onResume, onReturn) =>
-      "reset" <+> toDoc(body) <+> "on Suspend" <+> onSuspend.map { toDoc }.getOrElse("{}") <+> "on Resume" <+> onResume.map { toDoc }.getOrElse("{}") <+> "on Return" <+> onReturn.map { toDoc }.getOrElse("{}")
+      "reset" <+> toDoc(body) <+> "on suspend" <+> onSuspend.map { toDoc }.getOrElse("{}") <+> "on resume" <+> onResume.map { toDoc }.getOrElse("{}") <+> "on return" <+> onReturn.map { toDoc }.getOrElse("{}")
 
     case Shift(prompt, body) =>
       "shift" <> parens(toDoc(prompt)) <+> toDoc(body)
diff --git a/effekt/shared/src/main/scala/effekt/core/Reachable.scala b/effekt/shared/src/main/scala/effekt/core/Reachable.scala
index 719cf4d28..590554d3d 100644
--- a/effekt/shared/src/main/scala/effekt/core/Reachable.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Reachable.scala
@@ -88,7 +88,11 @@ class Reachable(
       process(body)
     case Stmt.Get(id, capt, tpe) => process(id)
     case Stmt.Put(id, tpe, value) => process(id); process(value)
-    case Stmt.Reset(body, onSuspend, onResume, onReturn) => process(body); onSuspend.foreach { process }; onResume.foreach { process }; onReturn.foreach { process }
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) =>
+      process(body)
+      onSuspend.foreach { process }
+      onResume.foreach { process }
+      onReturn.foreach { process }
     case Stmt.Shift(prompt, body) => process(prompt); process(body)
     case Stmt.Resume(k, body) => process(k); process(body)
     case Stmt.Region(body) => process(body)
diff --git a/effekt/shared/src/main/scala/effekt/core/Tree.scala b/effekt/shared/src/main/scala/effekt/core/Tree.scala
index cfbfe02e5..b48379ff9 100644
--- a/effekt/shared/src/main/scala/effekt/core/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Tree.scala
@@ -497,8 +497,6 @@ case class Operation(name: Id, tparams: List[Id], cparams: List[Id], vparams: Li
   val capt = body.capt -- cparams.toSet
 }
 
-case class FinalizerClause(vp: Option[ValueParam], body: Stmt) extends Tree
-
 
 object Tree {
 

From 996a17f90879a74178dd870b831d186e34cb2e6d Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 3 Dec 2024 15:26:01 +0100
Subject: [PATCH 18/25] change tests to account for 'finally' being a keyword
 now

---
 examples/neg/unresolved_type.effekt    |  6 +++---
 examples/pos/finalizerSemantics.check  |  3 +++
 examples/pos/finalizerSemantics.effekt | 16 +++++++++-------
 3 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/examples/neg/unresolved_type.effekt b/examples/neg/unresolved_type.effekt
index ceb0c7ef6..d008fb859 100644
--- a/examples/neg/unresolved_type.effekt
+++ b/examples/neg/unresolved_type.effekt
@@ -1,10 +1,10 @@
 interface Defer {
-    def defer[A, B] { prog: () => A } { finally: A => B }: B
+    def defer[A, B] { prog: () => A } { fin: A => B }: B
 }
 
 def impl = new Defer {
-    def defer { prog: () => A } { finally: A => B }: B = { // ERROR Could not resolve type A
+    def defer { prog: () => A } { fin: A => B }: B = { // ERROR Could not resolve type A
         val res = prog()
-        finally(res)
+        fin(res)
     }
 }
diff --git a/examples/pos/finalizerSemantics.check b/examples/pos/finalizerSemantics.check
index 90c85d962..faad4b6c0 100644
--- a/examples/pos/finalizerSemantics.check
+++ b/examples/pos/finalizerSemantics.check
@@ -1,5 +1,8 @@
 suspending inner
+Eff
+Eff
 resuming inner
 returning inner
+Eff
 returning outer
 87
diff --git a/examples/pos/finalizerSemantics.effekt b/examples/pos/finalizerSemantics.effekt
index ade67b90c..6937fe0fd 100644
--- a/examples/pos/finalizerSemantics.effekt
+++ b/examples/pos/finalizerSemantics.effekt
@@ -5,20 +5,22 @@ def main() = {
     try {
       try {
         do Eff(); 42
-      } suspend {
+      } on suspend {
         println("suspending inner")
-      } resume {
+        do Eff()
+      } on resume {
         _ => println("resuming inner")
-    } return { x =>
+    } on return { x =>
         println("returning inner")
+        do Eff()
         x * 2
       }
-    } with Eff { () => resume(()) }
-    suspend {
+    } with Eff { () => println("Eff"); resume(()) }
+    on suspend {
       println("suspending outer")
-    } resume {
+    } on resume {
       _ => println("resuming outer")
-    } return { x =>
+    } on return { x =>
       println("returning outer")
       x + 3
     }

From e8f88af28163ab2fb24889933a6272b2c300f1a2 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Tue, 3 Dec 2024 15:28:12 +0100
Subject: [PATCH 19/25] account for effect operations in finalizer clauses

---
 libraries/js/effekt_runtime.js | 56 +++++++++++++++++++++++++++++++---
 1 file changed, 51 insertions(+), 5 deletions(-)

diff --git a/libraries/js/effekt_runtime.js b/libraries/js/effekt_runtime.js
index 021dcee90..cfc89bc39 100644
--- a/libraries/js/effekt_runtime.js
+++ b/libraries/js/effekt_runtime.js
@@ -1,3 +1,4 @@
+// const $effekt = {}
 // Common Runtime
 // --------------
 function Cell(init, region) {
@@ -121,10 +122,11 @@ function SHIFT(p, body, ks, k, cont) {
 
   // package the prompt itself
   cont = { stack: meta.stack, prompt: meta.prompt, backup: meta.arena.backup(), onSuspend: meta.onSuspend, onSuspendData: meta.onSuspendData, onResume: meta.onResume, rest: cont }
-   meta = meta.rest
+  meta = meta.rest
 
   const k1 = meta.stack
-  meta.stack = null
+  // TODO why is this needed?
+  // meta.stack = null
   return body(cont, meta, k1)
 }
 
@@ -138,8 +140,8 @@ function RESUME(cont, c, b, ks, k) {
   while (!!toRewind) {
     if (toRewind.onResume && b) {
       return toRewind.onResume(toRewind.onSuspendData, meta, (x, ks) => {
-        // TODO what about ks here?
-        meta = { stack: toRewind.stack, prompt: toRewind.prompt, arena: toRewind.backup(), onSuspend: toRewind.onSuspend, onSuspendData: toRewind.onSuspendData, onResume: toRewind.onResume, rest: meta }
+        // push stack back onto the meta-stack before resuming later
+        meta = { stack: toRewind.stack, prompt: toRewind.prompt, arena: toRewind.backup(), onSuspend: toRewind.onSuspend, onSuspendData: toRewind.onSuspendData, onResume: toRewind.onResume, rest: ks }
         return RESUME(toRewind.rest, c, true, meta, meta.stack)
       })
     }
@@ -149,7 +151,8 @@ function RESUME(cont, c, b, ks, k) {
   }
 
   const k1 = meta.stack // TODO instead copy meta here, like elsewhere?
-  meta.stack = null
+  // TODO why is this needed?
+  // meta.stack = null
   return () => c(meta, k1)
 }
 
@@ -233,3 +236,46 @@ $effekt.run = RUN
  * If a runtime is available, use `$effekt.run`, instead.
  */
 $effekt.runToplevel = RUN_TOPLEVEL
+
+/*
+function main_94(ks_1463, k_1130) {
+  return RESET((p_93, ks_1467, k_1134) => {
+    const Eff_3 = {
+      Eff_4: (ks_1468, k_1135) =>
+        SHIFT(p_93, (k_1136, ks_1469, k_1137) => {
+          function resume_84(a_88, ks_1470, k_1138) {
+            return RESUME(k_1136, (ks_1471, k_1139) =>
+              () => k_1139(a_88, ks_1471), false, ks_1470, k_1138);
+          }
+          const _285 = console.log("Eff");
+          return resume_84($effekt.unit, ks_1469, k_1137);
+        }, ks_1468, k_1135)
+    };
+    return RESET((p_94, ks_1475, k_1143) =>
+      Eff_3.Eff_4(ks_1475, (_289, ks_1476) => () => k_1143(42, ks_1476)), (ks_1472, k_1140) => {
+      const _286 = console.log("suspending inner");
+      return Eff_3.Eff_4(ks_1472, k_1140);
+    }, (_287, ks_1473, k_1141) => {
+      const v_r_655 = console.log("resuming inner");
+      return () => k_1141(v_r_655, ks_1473);
+    }, (x_217, ks_1474, k_1142) => {
+      const _288 = console.log("returning inner");
+      return () => k_1142((x_217 * (2)), ks_1474);
+    }, ks_1467, k_1134);
+  }, (ks_1464, k_1131) => {
+    const v_r_653 = console.log("suspending outer");
+    return () => k_1131(v_r_653, ks_1464);
+  }, (_283, ks_1465, k_1132) => {
+    const v_r_654 = console.log("resuming outer");
+    return () => k_1132(v_r_654, ks_1465);
+  }, (x_216, ks_1466, k_1133) => {
+    const _284 = console.log("returning outer");
+    return () => k_1133((x_216 + (3)), ks_1466);
+  }, ks_1463, (x_218, ks_1477) => {
+    const v_r_656 = console.log(('' + x_218));
+    return () => k_1130($effekt.unit, ks_1477);
+  });
+}
+
+RUN_TOPLEVEL(main_94)
+*/

From 3d995580f9e77207f71b8033e4191fe5253e4b48 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 12 Dec 2024 10:26:08 +0100
Subject: [PATCH 20/25] resolve conflicts

---
 .../src/main/scala/effekt/core/Inline.scala   |  1 -
 .../main/scala/effekt/core/Recursive.scala    |  6 +-
 .../scala/effekt/core/StaticArguments.scala   |  8 +--
 .../effekt/generator/js/TransformerCps.scala  |  3 -
 .../effekt/generator/llvm/PrettyPrinter.scala |  4 +-
 .../effekt/generator/llvm/Transformer.scala   | 56 ++++++++-----------
 6 files changed, 32 insertions(+), 46 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/core/Inline.scala b/effekt/shared/src/main/scala/effekt/core/Inline.scala
index 34a1c413a..4f57316e6 100644
--- a/effekt/shared/src/main/scala/effekt/core/Inline.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Inline.scala
@@ -98,7 +98,6 @@ object Inline {
 
   def blockDefFor(id: Id)(using ctx: InlineContext): Option[Block] =
     ctx.defs.get(id) map {
-      // TODO rewriting here leads to a stack overflow in one test, why?
       case Definition.Def(id, block) => rewrite(block)
       case Definition.Let(id, _, binding) => INTERNAL_ERROR("Should not happen")
     }
diff --git a/effekt/shared/src/main/scala/effekt/core/Recursive.scala b/effekt/shared/src/main/scala/effekt/core/Recursive.scala
index 1e197c89a..bae8b9ad8 100644
--- a/effekt/shared/src/main/scala/effekt/core/Recursive.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Recursive.scala
@@ -81,7 +81,11 @@ class Recursive(
       process(body)
     case Stmt.Get(id, capt, tpe) => ()
     case Stmt.Put(id, tpe, value) => process(value)
-    case Stmt.Reset(body) => process(body)
+    case Stmt.Reset(body, suspend, resume, ret) =>
+      process(body)
+      suspend.foreach { process }
+      resume.foreach { process }
+      ret.foreach { process }
     case Stmt.Shift(prompt, body) => process(prompt); process(body)
     case Stmt.Resume(k, body) => process(k); process(body)
     case Stmt.Region(body) => process(body)
diff --git a/effekt/shared/src/main/scala/effekt/core/StaticArguments.scala b/effekt/shared/src/main/scala/effekt/core/StaticArguments.scala
index 4aabbf42d..fe1888fbd 100644
--- a/effekt/shared/src/main/scala/effekt/core/StaticArguments.scala
+++ b/effekt/shared/src/main/scala/effekt/core/StaticArguments.scala
@@ -137,11 +137,9 @@ object StaticArguments {
     case Stmt.Invoke(b, method, methodTpe, targs, vargs, bargs) =>
       invoke(rewrite(b), method, methodTpe, targs, vargs.map(rewrite), bargs.map(rewrite))
 
-    case Stmt.Reset(body) =>
-      rewrite(body) match {
-        case b => Stmt.Reset(b)
-      }
-
+    case Stmt.Reset(body, suspend, resume, ret) =>
+      reset(rewrite(body), suspend.map { rewrite }, resume.map { rewrite }, ret.map { rewrite })
+    
     // congruences
     case Stmt.Return(expr) => Return(rewrite(expr))
     case Stmt.Val(id, tpe, binding, body) => valDef(id, tpe, rewrite(binding), rewrite(body))
diff --git a/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala b/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
index 48b6a02a9..87bedac96 100644
--- a/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
+++ b/effekt/shared/src/main/scala/effekt/generator/js/TransformerCps.scala
@@ -264,9 +264,6 @@ object TransformerCps extends Transformer {
     case cps.Stmt.Resume(r, b, ks2, k2) =>
       pure(js.Return(js.Call(RESUME, nameRef(r), toJS(b), js.RawLiteral("false"), toJS(ks2), toJS(k2))))
 
-    case cps.Stmt.Resume(r, b, ks2, k2) =>
-      pure(js.Return(js.Call(RESUME, nameRef(r), toJS(b), toJS(ks2), toJS(k2))))
-
     case cps.Stmt.Hole() =>
       pure(js.Return($effekt.call("hole")))
   }
diff --git a/effekt/shared/src/main/scala/effekt/generator/llvm/PrettyPrinter.scala b/effekt/shared/src/main/scala/effekt/generator/llvm/PrettyPrinter.scala
index 5e42c1525..a166d46a0 100644
--- a/effekt/shared/src/main/scala/effekt/generator/llvm/PrettyPrinter.scala
+++ b/effekt/shared/src/main/scala/effekt/generator/llvm/PrettyPrinter.scala
@@ -72,12 +72,12 @@ ${indentedLines(instructions.map(show).mkString("\n"))}
       C.abort(s"tail call to non-void function returning: $tpe")
 
     case Load(result, tpe, LocalReference(PointerType(), name)) =>
-      s"${localName(result)} = load ${show(tpe)}, ${show(LocalReference(PointerType(), name))}"
+      s"${localName(result)} = load ${show(tpe)}, ${show(LocalReference(PointerType(), name))}, !noalias !2"
     case Load(_, _, operand) => C.abort(s"WIP: loading anything but local references not yet implemented: $operand")
 
     // TODO [jfrech, 2022-07-26] Why does `Load` explicitly check for a local reference and `Store` does not?
     case Store(address, value) =>
-      s"store ${show(value)}, ${show(address)}"
+      s"store ${show(value)}, ${show(address)}, !noalias !2"
 
     case GetElementPtr(result, tpe, ptr @ LocalReference(_, name), i :: is) =>
       s"${localName(result)} = getelementptr ${show(tpe)}, ${show(ptr)}, i64 $i" + is.map(", i32 " + _).mkString
diff --git a/effekt/shared/src/main/scala/effekt/generator/llvm/Transformer.scala b/effekt/shared/src/main/scala/effekt/generator/llvm/Transformer.scala
index d57ab7f25..5cb66a27b 100644
--- a/effekt/shared/src/main/scala/effekt/generator/llvm/Transformer.scala
+++ b/effekt/shared/src/main/scala/effekt/generator/llvm/Transformer.scala
@@ -217,8 +217,7 @@ object Transformer {
         emit(Call(name, Ccc(), referenceType, newReference, List(getStack())))
 
         shareValues(environment, freeVariables(rest));
-        pushEnvironmentOnto(getStack(), environment);
-        pushReturnAddressOnto(getStack(), returnAddressName, sharer, eraser);
+        pushFrameOnto(getStack(), environment, returnAddressName, sharer, eraser);
 
         transform(rest)
 
@@ -262,6 +261,7 @@ object Transformer {
         val parameters = frame.parameters.map { case machine.Variable(name, tpe) => Parameter(transform(tpe), name) }
         defineLabel(returnAddressName, parameters) {
           emit(Comment(s"pushFrame / return address, ${frameEnvironment.length} free variables"))
+          emit(Call("", Ccc(), VoidType(), ConstantGlobal("assumeFrameHeaderWasPopped"), List(getStack())))
           popEnvironmentFrom(getStack(), frameEnvironment);
           // eraseValues(frameEnvironment, frameEnvironment) (unnecessary)
           eraseValues(frame.parameters, freeVariables(frame.body))
@@ -273,8 +273,7 @@ object Transformer {
         val eraser = getEraser(frameEnvironment, StackFrameEraser)
 
         shareValues(frameEnvironment, freeVariables(rest));
-        pushEnvironmentOnto(getStack(), frameEnvironment);
-        pushReturnAddressOnto(getStack(), returnAddressName, sharer, eraser);
+        pushFrameOnto(getStack(), frameEnvironment, returnAddressName, sharer, eraser);
 
         transform(rest)
 
@@ -318,8 +317,7 @@ object Transformer {
 
         shareValues(frameEnvironment, freeVariables(rest));
 
-        pushEnvironmentOnto(getStack(), frameEnvironment);
-        pushReturnAddressOnto(getStack(), returnAddressName, sharer, eraser);
+        pushFrameOnto(getStack(), frameEnvironment, returnAddressName, sharer, eraser);
 
         transform(rest)
 
@@ -582,15 +580,24 @@ object Transformer {
     }
   }
 
-  def pushEnvironmentOnto(stack: Operand, environment: machine.Environment)(using ModuleContext, FunctionContext, BlockContext): Unit = {
-    if (environment.isEmpty) {
-      ()
-    } else {
-      val stackPointer = LocalReference(stackPointerType, freshName("stackPointer"));
-      val size = ConstantInt(environmentSize(environment));
-      emit(Call(stackPointer.name, Ccc(), stackPointer.tpe, stackAllocate, List(stack, size)));
-      storeEnvironmentAt(stackPointer, environment);
-    }
+  def pushFrameOnto(stack: Operand, environment: machine.Environment, returnAddressName: String, sharer: Operand, eraser: Operand)(using ModuleContext, FunctionContext, BlockContext) = {
+    val stackPointer = LocalReference(stackPointerType, freshName("stackPointer"));
+    val size = ConstantInt(environmentSize(environment) + 24);
+    emit(Call(stackPointer.name, Ccc(), stackPointer.tpe, stackAllocate, List(stack, size)));
+
+    val frameType = StructureType(List(environmentType(environment), frameHeaderType));
+    storeEnvironmentAt(stackPointer, environment);
+
+    val returnAddressPointer = LocalReference(PointerType(), freshName("returnAddress_pointer"));
+    emit(GetElementPtr(returnAddressPointer.name, frameType, stackPointer, List(0, 1, 0)));
+    val sharerPointer = LocalReference(PointerType(), freshName("sharer_pointer"));
+    emit(GetElementPtr(sharerPointer.name, frameType, stackPointer, List(0, 1, 1)));
+    val eraserPointer = LocalReference(PointerType(), freshName("eraser_pointer"));
+    emit(GetElementPtr(eraserPointer.name, frameType, stackPointer, List(0, 1, 2)));
+
+    emit(Store(returnAddressPointer, ConstantGlobal(returnAddressName)));
+    emit(Store(sharerPointer, sharer));
+    emit(Store(eraserPointer, eraser));
   }
 
   def popEnvironmentFrom(stack: Operand, environment: machine.Environment)(using ModuleContext, FunctionContext, BlockContext): Unit = {
@@ -671,25 +678,6 @@ object Transformer {
     }.map(emit)
   }
 
-  def pushReturnAddressOnto(stack: Operand, returnAddressName: String, sharer: Operand, eraser: Operand)(using ModuleContext, FunctionContext, BlockContext): Unit = {
-
-    val stackPointer = LocalReference(stackPointerType, freshName("stackPointer"));
-    // TODO properly find size
-    val size = ConstantInt(24);
-    emit(Call(stackPointer.name, Ccc(), stackPointer.tpe, stackAllocate, List(stack, size)));
-
-    val returnAddressPointer = LocalReference(PointerType(), freshName("returnAddress_pointer"));
-    emit(GetElementPtr(returnAddressPointer.name, frameHeaderType, stackPointer, List(0, 0)));
-    val sharerPointer = LocalReference(PointerType(), freshName("sharer_pointer"));
-    emit(GetElementPtr(sharerPointer.name, frameHeaderType, stackPointer, List(0, 1)));
-    val eraserPointer = LocalReference(PointerType(), freshName("eraser_pointer"));
-    emit(GetElementPtr(eraserPointer.name, frameHeaderType, stackPointer, List(0, 2)));
-
-    emit(Store(returnAddressPointer, ConstantGlobal(returnAddressName)));
-    emit(Store(sharerPointer, sharer));
-    emit(Store(eraserPointer, eraser));
-  }
-
   def popReturnAddressFrom(stack: Operand, returnAddressName: String)(using ModuleContext, FunctionContext, BlockContext): Unit = {
 
     val stackPointer = LocalReference(stackPointerType, freshName("stackPointer"));

From b5b10e9445361fb06457b501da73348772b257e4 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 19 Dec 2024 14:35:18 +0100
Subject: [PATCH 21/25] add missing calls in free variable computation

---
 .../src/main/scala/effekt/core/Inline.scala   | 21 +++++++------------
 .../src/main/scala/effekt/cps/Tree.scala      |  2 +-
 libraries/js/effekt_runtime.js                |  1 -
 3 files changed, 9 insertions(+), 15 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/core/Inline.scala b/effekt/shared/src/main/scala/effekt/core/Inline.scala
index 4f57316e6..6f22f0fd9 100644
--- a/effekt/shared/src/main/scala/effekt/core/Inline.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Inline.scala
@@ -131,7 +131,6 @@ object Inline {
       invoke(rewrite(b), method, methodTpe, targs, vargs.map(rewrite), bargs.map(rewrite))
 
     case Stmt.Reset(body, onSuspend, onResume, onReturn) =>
-      // TODO figure out inlining rules for new clauses
       // conjecture: we cannot inline the body of a reset clause, since even if the prompt is unused, we still need to
       // account for on suspend and resume clauses when a shift to another prompt occurs.
       Stmt.Reset(rewrite(body), onSuspend.map { rewrite }, onResume.map { rewrite }, onReturn.map { rewrite })
@@ -143,9 +142,9 @@ object Inline {
     case Stmt.Match(scrutinee, clauses, default) =>
       patternMatch(rewrite(scrutinee), clauses.map { case (id, value) => id -> rewrite(value) }, default.map(rewrite))
     case Stmt.Alloc(id, init, region, body) => Alloc(id, rewrite(init), region, rewrite(body))
-    // case Stmt.Shift(prompt, b @ BlockLit(tparams, cparams, vparams, List(k), body)) if tailResumptive(k.id, body) =>
-    //   C.inlineCount.next()
-    //   rewrite(removeTailResumption(k.id, body))
+    case Stmt.Shift(prompt, b @ BlockLit(tparams, cparams, vparams, List(k), body)) if tailResumptive(k.id, body) =>
+      C.inlineCount.next()
+      rewrite(removeTailResumption(k.id, body))
 
     case Stmt.Shift(prompt, body) => Shift(prompt, rewrite(body))
 
@@ -237,9 +236,7 @@ object Inline {
       case Stmt.Var(id, init, capture, body) => tailResumptive(k, body) && !freeInExpr(init)
       case Stmt.Get(id, annotatedCapt, annotatedTpe) => false
       case Stmt.Put(id, annotatedCapt, value) => false
-      // case Stmt.Reset(BlockLit(tparams, cparams, vparams, bparams, body)) => tailResumptive(k, body) // is this correct?
-      // case Stmt.Reset(body, onSuspend, onResume, onReturn) => onReturn.map { blocklit => tailResumptive(k, blocklit.body) }.getOrElse(tailResumptive(k, body.body))
-      case Stmt.Reset(body, onSuspend, onResume, onReturn) => false
+      case Stmt.Reset(body, onSuspend, onResume, onReturn) => onReturn.map { blocklit => tailResumptive(k, blocklit.body) }.getOrElse(tailResumptive(k, body.body))
       case Stmt.Shift(prompt, body) => false
       case Stmt.Resume(k2, body) => k2.id == k // what if k is free in body?
       case Stmt.Hole() => true
@@ -257,12 +254,10 @@ object Inline {
     case Stmt.Region(_) => ???
     case Stmt.Alloc(id, init, region, body) => Stmt.Alloc(id, init, region, removeTailResumption(k, body))
     case Stmt.Var(id, init, capture, body) => Stmt.Var(id, init, capture, removeTailResumption(k, body))
-    // case Stmt.Reset(body, onSuspend, onResume, onReturn) => Stmt.Reset(removeTailResumption(k, body))
-    // case Stmt.Reset(body, suspend, resume, Some(ret)) =>
-    //   Stmt.Reset(body, resume, suspend, Some(removeTailResumption(k, ret)))
-    // case Stmt.Reset(body, suspend, resume, ret) =>
-    //   Stmt.Reset(removeTailResumption(k, body), suspend, resume, ret)
-    case Stmt.Reset(body, suspend, resume, ret) => stmt
+    case Stmt.Reset(body, suspend, resume, Some(ret)) =>
+      Stmt.Reset(body, resume, suspend, Some(removeTailResumption(k, ret)))
+    case Stmt.Reset(body, suspend, resume, None) =>
+      Stmt.Reset(removeTailResumption(k, body), suspend, resume, None)
     case Stmt.Resume(k2, body) if k2.id == k => body
 
     case Stmt.Resume(k, body) => stmt
diff --git a/effekt/shared/src/main/scala/effekt/cps/Tree.scala b/effekt/shared/src/main/scala/effekt/cps/Tree.scala
index cd0ba63f6..3cfb7bdff 100644
--- a/effekt/shared/src/main/scala/effekt/cps/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/cps/Tree.scala
@@ -220,7 +220,7 @@ object Variables {
     case Stmt.Get(ref, id, body) => block(ref) ++ (free(body) -- value(id))
     case Stmt.Put(ref, value, body) => block(ref) ++ free(value) ++ free(body)
 
-    case Stmt.Reset(prog, onSuspend, onResume, onReturn, ks, k) => free(prog) ++ all(onSuspend, free) ++ all(onResume, free) ++ all(onReturn, free)
+    case Stmt.Reset(prog, onSuspend, onResume, onReturn, ks, k) => free(prog) ++ all(onSuspend, free) ++ all(onResume, free) ++ all(onReturn, free) ++ free(ks) ++ free(k)
     case Stmt.Shift(prompt, body, ks, k) => block(prompt) ++ free(body) ++ free(ks) ++ free(k)
     case Stmt.Resume(r, body, ks, k) => block(r) ++ free(body) ++ free(ks) ++ free(k)
     case Stmt.Hole() => empty
diff --git a/libraries/js/effekt_runtime.js b/libraries/js/effekt_runtime.js
index 98ab66476..f2b945d9b 100644
--- a/libraries/js/effekt_runtime.js
+++ b/libraries/js/effekt_runtime.js
@@ -1,4 +1,3 @@
-const $effekt = {}
 // Common Runtime
 // --------------
 function Cell(init, region) {

From 06e95d9e73ff96f50a630dbeb61c846e854a5f32 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 19 Dec 2024 16:02:54 +0100
Subject: [PATCH 22/25] fix unwinding and rewinding when effect operations are
 involved

---
 libraries/js/effekt_runtime.js | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/libraries/js/effekt_runtime.js b/libraries/js/effekt_runtime.js
index f2b945d9b..f3af4aacc 100644
--- a/libraries/js/effekt_runtime.js
+++ b/libraries/js/effekt_runtime.js
@@ -101,18 +101,17 @@ function SHIFT(p, body, ks, k, cont) {
 
   // TODO avoid constructing this object
   let meta = { stack: k, prompt: ks.prompt, arena: ks.arena, onSuspend: ks.onSuspend, onSuspendData: ks.onSuspendData, onResume: ks.onResume, rest: ks.rest }
-  // let cont = null
 
   while (!!meta && meta.prompt !== p) {
     cont = { stack: meta.stack, prompt: meta.prompt, backup: meta.arena.backup(), onSuspend: meta.onSuspend, onSuspendData: meta.onSuspendData, onResume: meta.onResume, rest: cont }
-    if (meta.onSuspend) {
+    if (!!meta.onSuspend) {
       return meta.onSuspend(meta.rest, (x, ks) => {
         // TODO what about ks here? It is just ignored -- doesn't seem right
         // this will probably become a problem once a resumptive effect operation is called in onSuspend
 
         // just change onSuspendData to retain the value returned by onSuspend
         const contt = { ...cont, onSuspendData: x }
-        return SHIFT(p, body, meta.rest, meta.rest.stack, contt)
+        return SHIFT(p, body, ks, meta.rest.stack, contt)
       })
     }
     meta = meta.rest
@@ -137,11 +136,9 @@ function RESUME(cont, c, b, ks, k) {
   let meta = { stack: k, prompt: ks.prompt, arena: ks.arena, onSuspend: ks.onSuspend, onSuspendData: ks.onSuspendData, onResume: ks.onResume, rest: ks.rest }
   let toRewind = cont
   while (!!toRewind) {
-    if (toRewind.onResume && b) {
+    if (!!toRewind.onResume && b) {
       return toRewind.onResume(toRewind.onSuspendData, meta, (x, ks) => {
-        // push stack back onto the meta-stack before resuming later
-        meta = { stack: toRewind.stack, prompt: toRewind.prompt, arena: toRewind.backup(), onSuspend: toRewind.onSuspend, onSuspendData: toRewind.onSuspendData, onResume: toRewind.onResume, rest: ks }
-        return RESUME(toRewind.rest, c, true, meta, meta.stack)
+        return RESUME(toRewind, c, false, ks, meta.stack)
       })
     }
     b = true

From b2bfebc82f96201226858e93f25e9d4f5502ae87 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 19 Dec 2024 16:05:54 +0100
Subject: [PATCH 23/25] do not inline tail resumptive shifts

---
 effekt/shared/src/main/scala/effekt/core/Inline.scala      | 7 ++++---
 .../src/main/scala/effekt/core/StaticArguments.scala       | 2 +-
 effekt/shared/src/main/scala/effekt/core/Tree.scala        | 6 ------
 effekt/shared/src/main/scala/effekt/core/Type.scala        | 2 +-
 4 files changed, 6 insertions(+), 11 deletions(-)

diff --git a/effekt/shared/src/main/scala/effekt/core/Inline.scala b/effekt/shared/src/main/scala/effekt/core/Inline.scala
index 6f22f0fd9..d838f3a38 100644
--- a/effekt/shared/src/main/scala/effekt/core/Inline.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Inline.scala
@@ -142,9 +142,10 @@ object Inline {
     case Stmt.Match(scrutinee, clauses, default) =>
       patternMatch(rewrite(scrutinee), clauses.map { case (id, value) => id -> rewrite(value) }, default.map(rewrite))
     case Stmt.Alloc(id, init, region, body) => Alloc(id, rewrite(init), region, rewrite(body))
-    case Stmt.Shift(prompt, b @ BlockLit(tparams, cparams, vparams, List(k), body)) if tailResumptive(k.id, body) =>
-      C.inlineCount.next()
-      rewrite(removeTailResumption(k.id, body))
+    // Note: We cannot inline tail resumptive shifts, otherwise and the suspend and resume clauses are not executed
+    // case Stmt.Shift(prompt, b @ BlockLit(tparams, cparams, vparams, List(k), body)) if tailResumptive(k.id, body) =>
+    //   C.inlineCount.next()
+    //   rewrite(removeTailResumption(k.id, body))
 
     case Stmt.Shift(prompt, body) => Shift(prompt, rewrite(body))
 
diff --git a/effekt/shared/src/main/scala/effekt/core/StaticArguments.scala b/effekt/shared/src/main/scala/effekt/core/StaticArguments.scala
index fe1888fbd..f60406849 100644
--- a/effekt/shared/src/main/scala/effekt/core/StaticArguments.scala
+++ b/effekt/shared/src/main/scala/effekt/core/StaticArguments.scala
@@ -138,7 +138,7 @@ object StaticArguments {
       invoke(rewrite(b), method, methodTpe, targs, vargs.map(rewrite), bargs.map(rewrite))
 
     case Stmt.Reset(body, suspend, resume, ret) =>
-      reset(rewrite(body), suspend.map { rewrite }, resume.map { rewrite }, ret.map { rewrite })
+      Stmt.Reset(rewrite(body), suspend.map { rewrite }, resume.map { rewrite }, ret.map { rewrite })
     
     // congruences
     case Stmt.Return(expr) => Return(rewrite(expr))
diff --git a/effekt/shared/src/main/scala/effekt/core/Tree.scala b/effekt/shared/src/main/scala/effekt/core/Tree.scala
index c2822159c..cadf6260f 100644
--- a/effekt/shared/src/main/scala/effekt/core/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Tree.scala
@@ -395,12 +395,6 @@ object normal {
       case other => Invoke(callee, method, methodTpe, targs, vargs, bargs)
     }
 
-  def reset(body: BlockLit, onSuspend: Option[BlockLit], onResume: Option[BlockLit], onReturn: Option[BlockLit]): Stmt = body match {
-    //    case BlockLit(tparams, cparams, vparams, List(prompt),
-    //      Stmt.Shift(prompt2, body) if prompt.id == prompt2.id => ???
-    case other => Stmt.Reset(body, onSuspend, onResume, onSuspend)
-  }
-
   def make(tpe: ValueType.Data, tag: Id, vargs: List[Pure]): Pure =
     Pure.Make(tpe, tag, vargs)
 
diff --git a/effekt/shared/src/main/scala/effekt/core/Type.scala b/effekt/shared/src/main/scala/effekt/core/Type.scala
index 733c86e5d..2a7e28c27 100644
--- a/effekt/shared/src/main/scala/effekt/core/Type.scala
+++ b/effekt/shared/src/main/scala/effekt/core/Type.scala
@@ -236,7 +236,7 @@ object Type {
     case Stmt.Var(id, init, cap, body) => body.capt -- Set(cap)
     case Stmt.Get(id, capt, tpe) => capt
     case Stmt.Put(id, capt, value) => capt
-    case Stmt.Reset(body, onSuspend, onResume, onReturn) => body.capt
+    case Stmt.Reset(body, onSuspend, onResume, onReturn) => body.capt ++ onSuspend.toSet.flatMap(_.capt) ++ onResume.toSet.flatMap(_.capt) ++ onReturn.toSet.flatMap(_.capt)
     case Stmt.Shift(prompt, body) => prompt.capt ++ body.capt
     case Stmt.Resume(k, body) => k.capt ++ body.capt
     case Stmt.Region(body) => body.capt

From 770829c5985bfbd52f38518578d9b1339f7c7999 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 19 Dec 2024 16:06:21 +0100
Subject: [PATCH 24/25] add effect op call in new clauses

---
 examples/pos/finalizerSemantics.effekt | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/examples/pos/finalizerSemantics.effekt b/examples/pos/finalizerSemantics.effekt
index 6937fe0fd..c2bec4de9 100644
--- a/examples/pos/finalizerSemantics.effekt
+++ b/examples/pos/finalizerSemantics.effekt
@@ -4,12 +4,14 @@ def main() = {
   val x = 
     try {
       try {
-        do Eff(); 42
+        do Eff()
+        42
       } on suspend {
         println("suspending inner")
         do Eff()
-      } on resume {
-        _ => println("resuming inner")
+      } on resume { _ =>
+        println("resuming inner")
+        do Eff()
     } on return { x =>
         println("returning inner")
         do Eff()

From 9dd5638a198c6a15fd8c7d97289f4c38e0e43ba2 Mon Sep 17 00:00:00 2001
From: dvdvgt <david.voigt@mailbox.org>
Date: Thu, 19 Dec 2024 16:07:36 +0100
Subject: [PATCH 25/25] update check file

---
 examples/pos/finalizerSemantics.check | 1 +
 1 file changed, 1 insertion(+)

diff --git a/examples/pos/finalizerSemantics.check b/examples/pos/finalizerSemantics.check
index faad4b6c0..c04ffd326 100644
--- a/examples/pos/finalizerSemantics.check
+++ b/examples/pos/finalizerSemantics.check
@@ -2,6 +2,7 @@ suspending inner
 Eff
 Eff
 resuming inner
+Eff
 returning inner
 Eff
 returning outer