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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions effekt/shared/src/main/scala/effekt/Typer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -314,7 +314,7 @@ object Typer extends Phase[NameResolved, Typechecked] {
val allImplicit = capabilities.forall { c => !(explicitCapabilities contains c) }
val used = effs.exists(e => e == effect)

if (allImplicit && !used)
if (allImplicit && !used && effect.name.name != "codepos")
Context.warning(pp"Handling effect ${effect}, which seems not to be used by the program.")
}

Expand Down Expand Up @@ -1511,7 +1511,7 @@ object Typer extends Phase[NameResolved, Typechecked] {

// We add return effects last to have more information at this point to
// concretize the effect.
effs = effs ++ Effects(retEffs)
effs = effs ++ Effects(retEffs.filterNot { p => p.name.name == "codepos" })

// annotate call node with inferred type arguments
Context.annotateTypeArgs(call, typeArgs)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import effekt.source.SpannedOps._
object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {

val phaseName = "explicit-capabilities"
val shouldForward = scala.util.DynamicVariable[Boolean](false)

def run(input: Typechecked)(using C: Context) =
val rewritten = C.timed(phaseName, input.source.name) { rewrite(input.tree) }
Expand All @@ -33,12 +34,38 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
case f @ FunDef(id, tps, vps, bps, ret, cpt, body, doc, span) =>
val capabilities = Context.annotation(Annotations.BoundCapabilities, f)
val capParams = capabilities.map(definitionFor)
f.copy(bparams = (bps.unspan ++ capParams).spanned(bps.span), body = rewrite(body))
shouldForward.withValue(shouldForward.value || capParams.exists { p => p.id.name == "codepos" }) {
f.copy(bparams = (bps.unspan ++ capParams).spanned(bps.span), body = rewrite(body))
}
case extDef @ ExternDef(capture, id, tparams, vparams, bparams, ret, bodies, doc, span) =>
val rewrittenBodies = bodies.map { rewrite }
extDef.copy(bodies = rewrittenBodies)
}

def codeposImplFor(span: Span, p: TrackedParam.BlockParam)(using Context): Term = {
val from = span.source.offsetToPosition(span.from)
val to = span.source.offsetToPosition(span.to)
val pos = s"${span.source.name}:${from.line}:${from.column}-${to.line}:${to.column}"
val sp = span.synthesized
val (ifce, op, tpe) = p.tpe match {
case Some(tpe @ BlockType.InterfaceType(ifce @ BlockTypeConstructor.Interface(name, Nil, List(op), decl), Nil)) =>
(ifce, op, tpe)
case _ => Context.abort("Could not find codepos interface with compatible type")
}
// now, synthesize an object that always returns the current position
val idIfce = IdRef(Nil, "codepos", sp)
Context.annotate(Annotations.Symbol, idIfce, ifce)
val idOp = IdRef(Nil, op.name.name, sp)
Context.annotate(Annotations.Symbol, idOp, op)
val impl = Implementation(TypeRef(idIfce, Many(Nil, sp), sp),
List(OpClause(idOp,
Nil, Nil, Nil, Some(Effectful(ValueTypeTree(builtins.TString, sp), source.Effects(Nil, sp), sp)),
Stmt.Return(Term.Literal(pos, builtins.TString, sp), sp),
IdDef("resume", sp), sp)), sp)
Context.annotate(Annotations.InferredBlockType, impl, tpe)
New(impl, sp)
}

override def expr(using Context) = {

// an effect call -- translate to method call on the inferred capability
Expand All @@ -53,7 +80,11 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
val others = Context.annotation(Annotations.CapabilityArguments, c)

// the remaining capabilities are provided as arguments
val capabilityArgs = others.map(referenceToCapability)
val capabilityArgs = others.map{
case p if p.name.name == "codepos" && !shouldForward.value =>
codeposImplFor(span, p)
case p => referenceToCapability(p)
}

val typeArguments = Context.annotation(Annotations.TypeArguments, c)
val typeArgs = typeArguments.map { e => ValueTypeTree(e, Span.missing) }
Expand All @@ -70,7 +101,11 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
val blockArgs = bargs.map { a => rewrite(a) }

val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
val capabilityArgs = capabilities.map(referenceToCapability)
val capabilityArgs = capabilities.map{
case p if p.name.name == "codepos" && !shouldForward.value =>
codeposImplFor(span, p)
case p => referenceToCapability(p)
}

val typeArguments = Context.annotation(Annotations.TypeArguments, c)
val typeArgs = typeArguments.map { e => ValueTypeTree(e, Span.missing) }
Expand All @@ -85,18 +120,26 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
val blockArgs = bargs.map { a => rewrite(a) }

val capabilities = Context.annotation(Annotations.CapabilityArguments, c)
val capabilityArgs = capabilities.map(referenceToCapability)
val capabilityArgs = capabilities.map{
case p if p.name.name == "codepos" && !shouldForward.value =>
codeposImplFor(span, p)
case p =>
referenceToCapability(p)
}

val typeArguments = Context.annotation(Annotations.TypeArguments, c)
val typeArgs = typeArguments.map { e => ValueTypeTree(e, Span.missing) }

Call(receiver, typeArgs, valueArgs, blockArgs ++ capabilityArgs, span)

case h @ TryHandle(prog, handlers, span) =>
val body = rewrite(prog)

val capabilities = Context.annotation(Annotations.BoundCapabilities, h)

val body = shouldForward.withValue(shouldForward.value || capabilities.exists { p => p.name.name == "codepos" }) {
rewrite(prog)
}


assert(capabilities.size == handlers.size)

// here we use the invariant that the order of capabilities is the same as the order of handlers
Expand Down Expand Up @@ -127,7 +170,10 @@ object ExplicitCapabilities extends Phase[Typechecked, Typechecked], Rewrite {
case b @ source.BlockLiteral(tps, vps, bps, body, span) =>
val capabilities = Context.annotation(Annotations.BoundCapabilities, b)
val capParams = capabilities.map(definitionFor)
source.BlockLiteral(tps, vps, bps ++ capParams, rewrite(body), span)

shouldForward.withValue(shouldForward.value || capabilities.exists { p => p.name.name == "codepos" }) {
source.BlockLiteral(tps, vps, bps ++ capParams, rewrite(body), span)
}
}

override def rewrite(body: ExternBody)(using context.Context): ExternBody =
Expand Down
11 changes: 9 additions & 2 deletions effekt/shared/src/main/scala/effekt/typer/CapabilityScope.scala
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,15 @@ case object GlobalCapabilityScope extends CapabilityScope {
def parent: CapabilityScope = sys error "No parent"
// If we try to find a capability for an effect that is known to be unhandled (that is no outer scope could
// potentially handle it, then we raise an error.
def capabilityFor(tpe: symbols.InterfaceType)(using C: Context): symbols.BlockParam =
C.abort(pretty"Effect ${tpe} is not allowed in this context.")
def capabilityFor(tpe: symbols.InterfaceType)(using C: Context): symbols.BlockParam = {
if (tpe.typeConstructor.name.name == "codepos") {
symbols.BlockParam(symbols.Name.local("codepos"), Some(tpe),
symbols.Resource(symbols.Name.local("codepos")), decl = source.NoSource)
} else {
C.abort(pretty"Effect ${tpe} is not allowed in this context.")
}
}

def relevantInScopeFor(tpe: symbols.InterfaceType)(using C: Context): Set[symbols.InterfaceType] = Set.empty
}

Expand Down
6 changes: 6 additions & 0 deletions examples/pos/codepos.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
examples/pos/codepos.effekt:13:3-13:17
examples/pos/codepos.effekt:14:3-14:17
examples/pos/codepos.effekt:15:3-15:22
examples/pos/codepos.effekt:15:3-15:22
X
examples/pos/codepos.effekt:10:3-10:9
18 changes: 18 additions & 0 deletions examples/pos/codepos.effekt
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
def printCodepos(): Unit / codepos = {
println(do codepos())
}

def printCodeposTwice(): Unit / codepos = {
printCodepos()
printCodepos()
}
def atHere{ body: => Unit / codepos }: Unit = {
body()
}
def main() = {
printCodepos()
printCodepos()
printCodeposTwice()
try { printCodepos() } with codepos { () => resume("X") }
atHere{ printCodepos() }
}
6 changes: 5 additions & 1 deletion libraries/common/effekt.effekt
Original file line number Diff line number Diff line change
Expand Up @@ -832,4 +832,8 @@ effect write(s: String): Unit

effect splice[A](x: A): Unit


// Code positions
// ==============
//
/// Allows to get the code position of the callsite of the current function
effect codepos(): String
Loading