Skip to content

Commit 897e4b5

Browse files
Subtract block parameter captures in extern defs (#1023)
This fixes #448 by subtracting the block param captures, so the following becomes OK: ``` extern def ifJS{ thn: => R }{ els: => R}: R = js { thn() } default { els() } ``` Note that the implementor of the extern is in charge of properly calling the block parameters with the correct calling convention.
1 parent 03525a0 commit 897e4b5

File tree

5 files changed

+26
-4
lines changed

5 files changed

+26
-4
lines changed

effekt/shared/src/main/scala/effekt/Typer.scala

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -868,7 +868,14 @@ object Typer extends Phase[NameResolved, Typechecked] {
868868
sym.vparams foreach Context.bind
869869
sym.bparams foreach Context.bind
870870

871-
flowingInto(Context.lookupCapture(sym)) {
871+
val functionCapture = Context.lookupCapture(sym)
872+
val inferredCapture = Context.freshCaptVar(CaptUnificationVar.ExternDefRegion(d))
873+
874+
875+
flowsIntoWithout(inferredCapture, functionCapture) {
876+
sym.bparams.map(_.capture)
877+
}
878+
flowingInto(inferredCapture) {
872879

873880
// Note: Externs are always annotated with a type
874881
val expectedReturnType = d.symbol.annotatedType.get.result
@@ -879,7 +886,6 @@ object Typer extends Phase[NameResolved, Typechecked] {
879886
checkStmt(body, Some(expectedReturnType))
880887
case u: source.ExternBody.Unsupported => u
881888
}
882-
883889
}
884890

885891
Result((), Pure)

effekt/shared/src/main/scala/effekt/symbols/symbols.scala

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -385,6 +385,7 @@ object CaptUnificationVar {
385385
case class RegionRegion(handler: source.Region) extends Role
386386
case class VarRegion(definition: source.VarDef) extends Role
387387
case class FunctionRegion(fun: source.FunDef) extends Role
388+
case class ExternDefRegion(fun: source.ExternDef) extends Role
388389
case class BlockRegion(fun: source.DefDef) extends Role
389390
case class AnonymousFunctionRegion(fun: source.BlockLiteral) extends Role
390391
case class InferredBox(box: source.Box) extends Role
Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[error] examples/neg/effekt_implemented_extern.effekt:4:8: Used captures {io} are not in the allowed set {}
1+
[error] examples/neg/effekt_implemented_extern.effekt:4:8: Not allowed {io}
22
js { test() }
3-
^^^^^^
3+
^^^^^^

examples/pos/ifbackend.check

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Hallo

examples/pos/ifbackend.effekt

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
extern pure def ifJS[R]{ thn: => R }{ els: => R}: R =
2+
js { thn() }
3+
default { els() }
4+
5+
extern pure def jsOnly(): String =
6+
js """ "Hallo" """
7+
8+
def main() = {
9+
ifJS{
10+
println(jsOnly())
11+
}{
12+
println("Hallo")
13+
}
14+
}

0 commit comments

Comments
 (0)