Skip to content

Commit

Permalink
First work for BlockType Wildcards
Browse files Browse the repository at this point in the history
  • Loading branch information
MattisKra committed Jun 12, 2023
1 parent 373776d commit 52c6ca2
Show file tree
Hide file tree
Showing 15 changed files with 163 additions and 38 deletions.
3 changes: 2 additions & 1 deletion effekt/shared/src/main/scala/effekt/Namer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -569,13 +569,14 @@ object Namer extends Phase[Parsed, NameResolved] {
case source.BoxedType(tpe, capt) =>
BoxedType(resolve(tpe), resolve(capt))
case source.ValueTypeWildcard =>
symbols.ValueTypeRef(ValueTypeWildcard())
ValueTypeRef(ValueTypeWildcard())
}

def resolve(tpe: source.BlockType)(using Context): BlockType = resolvingType(tpe) {
case t: source.FunctionType => resolve(t)
case t: source.BlockTypeTree => t.eff
case t: source.BlockTypeRef => resolve(t)
case source.BlockTypeWildcard => BlockTypeRef(BlockTypeWildcard())
}

def resolve(funTpe: source.FunctionType)(using Context): FunctionType = resolvingType(funTpe) {
Expand Down
3 changes: 2 additions & 1 deletion effekt/shared/src/main/scala/effekt/Parser.scala
Original file line number Diff line number Diff line change
Expand Up @@ -526,7 +526,8 @@ class EffektParsers(positions: Positions) extends EffektLexers(positions) {
lazy val captureSet: P[CaptureSet] = `{` ~> manySep(idRef, `,`) <~ `}` ^^ CaptureSet.apply

lazy val blockType: P[BlockType] =
( (`(` ~> manySep(valueType, `,`) <~ `)`) ~ many(blockTypeParam) ~ (`=>` ~/> primValueType) ~ maybeEffects ^^ FunctionType.apply
( literal("_") ^^^ source.BlockTypeWildcard
| (`(` ~> manySep(valueType, `,`) <~ `)`) ~ many(blockTypeParam) ~ (`=>` ~/> primValueType) ~ maybeEffects ^^ FunctionType.apply
| some(blockTypeParam) ~ (`=>` ~/> primValueType) ~ maybeEffects ^^ { case tpes ~ ret ~ eff => FunctionType(Nil, tpes, ret, eff) }
| primValueType ~ (`=>` ~/> primValueType) ~ maybeEffects ^^ { case t ~ ret ~ eff => FunctionType(List(t), Nil, ret, eff) }
| (valueType <~ guard(`/`)) !!! "Effects not allowed here. Maybe you mean to use a function type `() => T / E`?"
Expand Down
27 changes: 18 additions & 9 deletions effekt/shared/src/main/scala/effekt/Typer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,11 @@ package typer
/**
* In this file we fully qualify source types, but use symbols directly
*/
import effekt.context.{ Annotation, Annotations, Context, ContextOps }
import effekt.context.{Annotation, Annotations, Context, ContextOps}
import effekt.context.assertions.*
import effekt.source.{ AnyPattern, Def, IgnorePattern, MatchPattern, ModuleDecl, Stmt, TagPattern, Term, Tree, resolve, symbol }
import effekt.source.{AnyPattern, Def, IgnorePattern, MatchPattern, ModuleDecl, Stmt, TagPattern, Term, Tree, resolve, symbol}
import effekt.symbols.*
import effekt.symbols.BlockType.BlockTypeRef
import effekt.symbols.builtins.*
import effekt.symbols.kinds.*
import effekt.util.messages.*
Expand Down Expand Up @@ -72,7 +73,8 @@ object Typer extends Phase[NameResolved, Typechecked] {
// to allow mutually recursive defs
tree.defs.foreach { d => precheckDef(d) }
tree.defs.foreach { d =>
val Result(_, effs) = synthDef(d)
println("\n" + d + "\n")
val Result(_, effs) = synthDef(d) // This causes the problem for BlockTypeWildcards
val unhandled = effs.toEffects
if (unhandled.nonEmpty)
Context.at(d) {
Expand Down Expand Up @@ -173,7 +175,7 @@ object Typer extends Phase[NameResolved, Typechecked] {
// (3) add effect to used effects
Result(tpe, effs ++ ConcreteEffects(List(effect)))

case c @ source.Call(t: source.IdTarget, targs, vargs, bargs) =>
case c @ source.Call(t: source.IdTarget, targs, vargs, bargs) => // this path is taken
checkOverloadedFunctionCall(c, t.id, targs map { _.resolve }, vargs, bargs, expected)

case c @ source.Call(source.ExprTarget(e), targs, vargs, bargs) =>
Expand Down Expand Up @@ -527,6 +529,7 @@ object Typer extends Phase[NameResolved, Typechecked] {
//<editor-fold desc="statements and definitions">

def checkStmt(stmt: Stmt, expected: Option[ValueType])(using Context, Captures): Result[ValueType] =
println(expected)
checkAgainst(stmt, expected) {
case source.DefStmt(b, rest) =>
val Result(t, effBinding) = Context in { precheckDef(b); synthDef(b) }
Expand Down Expand Up @@ -617,13 +620,15 @@ object Typer extends Phase[NameResolved, Typechecked] {
case x: CaptUnificationVar => List(x)
case _ => Nil
}
val Result(funTpe, unhandledEffects) = Context.withUnificationScope(captVars) {

val Result(funTpe, unhandledEffects) = Context.withUnificationScope(captVars) {
sym.vparams foreach Context.bind
sym.bparams foreach Context.bind

val inferredCapture = Context.freshCaptVar(CaptUnificationVar.FunctionRegion(d))



Context.withRegion(selfRegion) {
(sym.annotatedType: @unchecked) match {
case Some(annotated) =>
Expand Down Expand Up @@ -653,8 +658,10 @@ object Typer extends Phase[NameResolved, Typechecked] {
given Captures = inferredCapture

// all effects are handled by the function itself (since they are inferred)
val (Result(tpe, effs), caps) = Context.bindingAllCapabilities(d) {
Context in { checkStmt(body, None) }
val (Result(tpe, effs), caps) = Context.bindingAllCapabilities(d) { // This causes the error
Context in {
checkStmt(body, None)
}
}

// We do no longer use the order annotated on the function, but always the canonical ordering.
Expand Down Expand Up @@ -1231,7 +1238,8 @@ object Typer extends Phase[NameResolved, Typechecked] {
// TODO currently the return type cannot refer to the annotated effects, so we can make up capabilities
// in the future namer needs to annotate the function with the capture parameters it introduced.
capt = effects.canonical.map { tpe => CaptureParam(tpe.name) }
} yield toType(ret, effects, capt)
}
yield toType(ret, effects, capt)
}
//</editor-fold>

Expand Down Expand Up @@ -1373,7 +1381,8 @@ trait TyperOps extends ContextOps { self: Context =>
annotations.get(Annotations.BlockType, s)
.map {
case f: FunctionType => unification(f) // here we apply the substitutions known so far.
case tpe => abort(pretty"Expected function type, but got ${tpe}.")
case tpe =>
abort(pretty"Expected function type, but got ${tpe}.")
}
.orElse(functionTypeOption(s))
.getOrElse {
Expand Down
6 changes: 5 additions & 1 deletion effekt/shared/src/main/scala/effekt/core/Transformer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import effekt.context.{Annotations, Context, ContextOps}
import effekt.symbols.*
import effekt.symbols.builtins.*
import effekt.context.assertions.*
import effekt.source.BlockType.BlockTypeWildcard
import effekt.source.{MatchPattern, Term}
import effekt.typer.Substitutions

Expand Down Expand Up @@ -176,6 +177,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
case v: source.Var =>
val sym = v.definition
Context.blockTypeOf(sym) match {
case BlockTypeRef(x : BlockTypeWildcard) => Context.panic("Wildcard in unexpected place")
case _: BlockType.FunctionType => transformAsControlBlock(tree)
case _: BlockType.InterfaceType => transformAsObject(tree)
}
Expand Down Expand Up @@ -216,6 +218,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
val sym = v.definition
val tpe = Context.blockTypeOf(sym)
tpe match {
case BlockTypeRef(x : BlockTypeWildcard) => Context.abort("Wildcard in unexpected place")
case BlockType.FunctionType(tparams, cparams, vparamtps, bparamtps, restpe, effects) =>
// if this block argument expects to be called using PureApp or DirectApp, make sure it is
// by wrapping it in a BlockLit
Expand Down Expand Up @@ -460,7 +463,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
case InterfaceType(i: Interface, targs) => member match {
// For operations, we substitute the first type parameters by concrete type args.
case Operation(name, tparams, vparams, resultType, effects, _) =>
val substitution = Substitutions((tparams zip targs).toMap, Map.empty)
val substitution = Substitutions((tparams zip targs).toMap, Map.empty, Map.empty)
val remainingTypeParams = tparams.drop(targs.size)
val bparams = Nil
// TODO this is exactly like in [[Typer.toType]] -- TODO repeated here:
Expand Down Expand Up @@ -522,6 +525,7 @@ object Transformer extends Phase[Typechecked, CoreTransformed] {
}

def transform(tpe: BlockType)(using Context): core.BlockType = tpe match {
case BlockTypeRef(x : BlockTypeWildcard) => Context.panic("Wildcard in unexpected place")
case BlockType.FunctionType(tparams, cparams, vparams, bparams, result, effects) =>

val capabilityTypes = effects.canonical.map(transform)
Expand Down
1 change: 1 addition & 0 deletions effekt/shared/src/main/scala/effekt/source/Tree.scala
Original file line number Diff line number Diff line change
Expand Up @@ -485,6 +485,7 @@ enum BlockType extends Type {
case BlockTypeTree(eff: symbols.BlockType)
case FunctionType(vparams: List[ValueType], bparams: List[(Option[IdDef], BlockType)], result: ValueType, effects: Effects)
case BlockTypeRef(id: IdRef, args: List[ValueType]) extends BlockType, Reference
case BlockTypeWildcard
}

export BlockType.*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ object TypePrinter extends ParenPrettyPrinter {
}

def toDoc(tpe: BlockType): Doc = tpe match {
case BlockTypeRef(x) => toDoc(LocalName("Wildcard")) // Improve
case FunctionType(tparams, cparams, vparams, bparams, result, effects) =>
val tps = if (tparams.isEmpty) emptyDoc else typeParams(tparams)
val ps: Doc = (vparams, bparams) match {
Expand Down
1 change: 1 addition & 0 deletions effekt/shared/src/main/scala/effekt/symbols/kinds.scala
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ package object kinds {
}

def wellformed(tpe: BlockType)(using Context): Unit = tpe match {
case BlockTypeRef(x) => // Is this right?
case b: FunctionType => wellformed(b)
case c: InterfaceType => wellformed(c)
}
Expand Down
13 changes: 13 additions & 0 deletions effekt/shared/src/main/scala/effekt/symbols/symbols.scala
Original file line number Diff line number Diff line change
Expand Up @@ -204,6 +204,19 @@ enum TypeVar(val name: Name) extends ValueTypeSymbol {
}
export TypeVar.*

enum BlockTypeVar(val name: Name) extends BlockTypeSymbol {
/**
* Introduced when instantiating type schemes
*
* Should neither occur in source programs, nor in inferred types
*/
case BlockUnificationVar(underlying: TypeVar.TypeParam, call: source.Tree) extends BlockTypeVar(underlying.name)


case BlockTypeWildcard() extends BlockTypeVar(NoName)
}
export BlockTypeVar.*

case class TypeAlias(name: Name, tparams: List[TypeParam], tpe: ValueType) extends ValueTypeSymbol

/**
Expand Down
2 changes: 2 additions & 0 deletions effekt/shared/src/main/scala/effekt/symbols/types.scala
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,8 @@ enum BlockType extends Type {
)

case InterfaceType(typeConstructor: BlockTypeConstructor, args: List[ValueType])

case BlockTypeRef(bvar: BlockTypeVar)
}
export BlockType.*

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,7 @@ private def isConcreteValueType(tpe: TypeVar): Boolean = tpe match {
}

private def isConcreteBlockType(tpe: BlockType): Boolean = tpe match {
case BlockTypeRef(x) => false // Is this right?
case FunctionType(tparams, cparams, vparams, bparams, result, effects) =>
vparams.forall(isConcreteValueType) && bparams.forall(isConcreteBlockType) && isConcreteValueType(result) && isConcreteEffects(effects)
case InterfaceType(tpe, args) => args.forall(isConcreteValueType)
Expand Down
59 changes: 51 additions & 8 deletions effekt/shared/src/main/scala/effekt/typer/Constraints.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@ package effekt
package typer

import effekt.symbols.*
import effekt.util.messages.{ ErrorReporter, ErrorMessageReifier }
import effekt.symbols.BlockTypeVar.BlockUnificationVar
import effekt.util.messages.{ErrorMessageReifier, ErrorReporter}
import effekt.util.foreachAborting

// Auxiliary Definitions
Expand Down Expand Up @@ -100,11 +101,15 @@ class Constraints(
*/
private var valueTypeSubstitution: Map[Node, ValueType] = Map.empty,

private var blockTypeSubstitution: Map[Node, BlockType] = Map.empty,

/**
* A map from a member in the equivalence class to the class' representative
*/
private var classes: Map[UnificationVar, Node] = Map.empty,

private var blockClasses : Map[BlockUnificationVar, Node] = Map.empty,

/**
* Concrete bounds for each unification variable
*/
Expand All @@ -128,9 +133,10 @@ class Constraints(
* The currently known substitutions
*/
def subst: Substitutions =
val types = classes.flatMap[TypeVar, ValueType] { case (k, v) => valueTypeSubstitution.get(v).map { k -> _ } }
val values = classes.flatMap[TypeVar, ValueType] { case (k, v) => valueTypeSubstitution.get(v).map { k -> _ } }
val blocks = blockClasses.flatMap[BlockTypeVar, BlockType] { case (k, v) => blockTypeSubstitution.get(v).map { k -> _ } }
val captures = captSubstitution.asInstanceOf[Map[CaptVar, Captures]]
Substitutions(types, captures)
Substitutions(values, blocks, captures)

/**
* Should only be called on unification variables where we do not know any types, yet
Expand Down Expand Up @@ -164,7 +170,7 @@ class Constraints(
* Retreive the potentially known type of [[x]]
*/
def typeOf(x: UnificationVar): Option[ValueType] =
typeOf(getNode(x))
valueTypeOf(getNode(x))

/**
* Learn that unification variable [[x]] needs to be compatible with [[y]]. If there already is
Expand All @@ -174,7 +180,7 @@ class Constraints(

def learnType(x: Node, tpe: ValueType): Unit = {
// tpe should not be a reference to a unification variable
typeOf(x) foreach { otherTpe => merge(tpe, otherTpe) }
valueTypeOf(x) foreach { otherTpe => merge(tpe, otherTpe) }
valueTypeSubstitution = valueTypeSubstitution.updated(x, tpe)
updateSubstitution()
}
Expand All @@ -183,7 +189,7 @@ class Constraints(
// Already connected
if (x == y) return ()

(typeOf(x), typeOf(y)) match {
(valueTypeOf(x), valueTypeOf(y)) match {
case (Some(typeOfX), Some(typeOfY)) => merge(typeOfX, typeOfY)
case (Some(typeOfX), None) => learnType(y, typeOfX)
case (None, Some(typeOfY)) => learnType(x, typeOfY)
Expand All @@ -200,6 +206,36 @@ class Constraints(
}
}

def learn(x: BlockUnificationVar, y: BlockType)(merge: (BlockType, BlockType) => Unit): Unit = {

def learnType(x: Node, tpe: BlockType): Unit = {
// tpe should not be a reference to a unification variable
blockTypeOf(x) foreach { otherTpe => merge(tpe, otherTpe) }
blockTypeSubstitution = blockTypeSubstitution.updated(x, tpe)
updateSubstitution()
}

def connectNodes(x: Node, y: Node): Unit = {
// Already connected
if (x == y) return ()

(blockTypeOf(x), blockTypeOf(y)) match {
case (Some(typeOfX), Some(typeOfY)) => merge(typeOfX, typeOfY)
case (Some(typeOfX), None) => learnType(y, typeOfX)
case (None, Some(typeOfY)) => learnType(x, typeOfY)
case (None, None) => ()
}

// create mapping to representative
blockClasses = blockClasses.view.mapValues { node => if (node == x) y else node }.toMap
}

y match {
case BlockTypeRef(y: BlockUnificationVar) => connectNodes(getNode(x), getNode(y))
case tpe => learnType(getNode(x), tpe)
}
}

/**
* Marks [[xs]] as pending inactive and solves them, if they do not have active bounds.
*/
Expand Down Expand Up @@ -252,7 +288,7 @@ class Constraints(
})


override def clone(): Constraints = new Constraints(valueTypeSubstitution, classes, captureConstraints, captSubstitution, pendingInactive)
override def clone(): Constraints = new Constraints(valueTypeSubstitution, blockTypeSubstitution, classes, blockClasses, captureConstraints, captSubstitution, pendingInactive)

def dumpTypeConstraints() =
println("\n--- Type Constraints ---")
Expand Down Expand Up @@ -466,8 +502,15 @@ class Constraints(
private def getNode(x: UnificationVar): Node =
classes.getOrElse(x, { val rep = new Node; classes += (x -> rep); rep })

private def typeOf(n: Node): Option[ValueType] =
private def getNode(x: BlockUnificationVar): Node =
blockClasses.getOrElse(x, { val rep = new Node; blockClasses += (x -> rep); rep })

private def valueTypeOf(n: Node): Option[ValueType] =
valueTypeSubstitution.get(n)

private def blockTypeOf(n: Node): Option[BlockType] =
blockTypeSubstitution.get(n)


//</editor-fold>
}
Loading

0 comments on commit 52c6ca2

Please sign in to comment.