Skip to content

Commit

Permalink
Fix all compile errors
Browse files Browse the repository at this point in the history
  • Loading branch information
@tgeng
tgeng committed Oct 6, 2024
1 parent 76be3cf commit c081b71
Show file tree
Hide file tree
Showing 7 changed files with 112 additions and 96 deletions.
8 changes: 6 additions & 2 deletions src/main/scala/com/github/tgeng/archon/core/ir/term.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -384,6 +384,10 @@ enum VTerm(val sourceInfo: SourceInfo) extends SourceInfoOwner[VTerm]:
case LevelType(strictUpperBound) => LevelType(strictUpperBound)
case Level(literal, maxOperands) => Level(literal, maxOperands)
case Auto() => Auto()
case EffectInstanceType(effect, handlerConstraint) =>
EffectInstanceType(effect, handlerConstraint)
case EffectInstance(effect, handlerConstraint, handlerKey) =>
EffectInstance(effect, handlerConstraint, handlerKey)

def visitWith[C, R](visitor: Visitor[C, R])(using ctx: C)(using Σ: Signature): R =
visitor.visitVTerm(this)
Expand Down Expand Up @@ -460,8 +464,8 @@ object VTerm:
Set(div),
)

def EffectsLiteral(handlerKeys: Set[VTerm])(using sourceInfo: SourceInfo): Effects =
Effects(handlerKeys, SeqMap.empty)
def EffectsLiteral(effectInstances: Set[VTerm])(using sourceInfo: SourceInfo): Effects =
Effects(effectInstances, SeqMap.empty)

def EffectsUnion(effects: VTerm*): Effects =
Effects(Set.empty, SeqMap(effects.map(_ -> false)*))
Expand Down
1 change: 1 addition & 0 deletions src/main/scala/com/github/tgeng/archon/core/ir/typing.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -946,6 +946,7 @@ private def getEffectsContinuationUsage
inferType(effectInstance)._1 match
case EffectInstanceType(_, handlerConstraint) =>
UsageLiteral(handlerConstraint.continuationUsage)
case _ => throw IllegalStateException("type error")
}
val usages = operands.keySet.map(getEffectsContinuationUsage)
UsageJoin(Set(UsageLiteral(U1)) ++ usages ++ literalUsages)
Expand Down
4 changes: 0 additions & 4 deletions src/main/scala/com/github/tgeng/archon/core/ir/typingContext.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,6 @@ enum Constraint:
case EffSubsumption(context: Context, sub: VTerm, sup: VTerm)
case LevelSubsumption(context: Context, sub: VTerm, sup: VTerm)
case UsageSubsumption(context: Context, sub: VTerm, sup: VTerm)
case EqDecidabilitySubsumption(context: Context, sub: VTerm, sup: VTerm)
case HandlerTypeSubsumption(context: Context, sub: VTerm, sup: VTerm)

enum UnsolvedMetaVariableConstraint:
case UmcNothing
Expand Down Expand Up @@ -554,8 +552,6 @@ class TypingContext
case Constraint.EffSubsumption(_, sub, sup) => visitVTerm(sub) ++ visitVTerm(sup)
case Constraint.LevelSubsumption(_, sub, sup) => visitVTerm(sub) ++ visitVTerm(sup)
case Constraint.UsageSubsumption(_, sub, sup) => visitVTerm(sub) ++ visitVTerm(sup)
case Constraint.EqDecidabilitySubsumption(_, sub, sup) => visitVTerm(sub) ++ visitVTerm(sup)
case Constraint.HandlerTypeSubsumption(_, sub, sup) => visitVTerm(sub) ++ visitVTerm(sup)

@throws(classOf[IrError])
private def solveConstraints(constraints: Set[Constraint])(using Σ: Signature): Set[Constraint] =
Expand Down
71 changes: 50 additions & 21 deletions src/main/scala/com/github/tgeng/archon/core/ir/visitor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,24 +29,26 @@ trait TermVisitor[C, R]:
)

def visitVTerm(tm: VTerm)(using ctx: C)(using Σ: Signature): R = tm match
case ty: Type => visitType(ty)
case top: Top => visitTop(top)
case v: Var => visitVar(v)
case collapse: Collapse => visitCollapse(collapse)
case u: U => visitU(u)
case thunk: Thunk => visitThunk(thunk)
case dataType: DataType => visitDataType(dataType)
case con: Con => visitCon(con)
case usageType: UsageType => visitUsageType(usageType)
case usageLiteral: UsageLiteral => visitUsageLiteral(usageLiteral)
case usageProd: UsageProd => visitUsageProd(usageProd)
case usageSum: UsageSum => visitUsageSum(usageSum)
case usageJoin: UsageJoin => visitUsageJoin(usageJoin)
case effectsType: EffectsType => visitEffectsType(effectsType)
case effects: Effects => visitEffects(effects)
case levelType: LevelType => visitLevelType(levelType)
case level: Level => visitLevel(level)
case auto: Auto => visitAuto(auto)
case ty: Type => visitType(ty)
case top: Top => visitTop(top)
case v: Var => visitVar(v)
case collapse: Collapse => visitCollapse(collapse)
case u: U => visitU(u)
case thunk: Thunk => visitThunk(thunk)
case dataType: DataType => visitDataType(dataType)
case con: Con => visitCon(con)
case usageType: UsageType => visitUsageType(usageType)
case usageLiteral: UsageLiteral => visitUsageLiteral(usageLiteral)
case usageProd: UsageProd => visitUsageProd(usageProd)
case usageSum: UsageSum => visitUsageSum(usageSum)
case usageJoin: UsageJoin => visitUsageJoin(usageJoin)
case effectsType: EffectsType => visitEffectsType(effectsType)
case effects: Effects => visitEffects(effects)
case levelType: LevelType => visitLevelType(levelType)
case level: Level => visitLevel(level)
case effectInstanceType: EffectInstanceType => visitEffectInstanceType(effectInstanceType)
case effectInstance: EffectInstance => visitEffectInstance(effectInstance)
case auto: Auto => visitAuto(auto)

def visitType(ty: Type)(using ctx: C)(using Σ: Signature): R =
visitVTerm(ty.upperBound)
Expand Down Expand Up @@ -114,6 +116,16 @@ trait TermVisitor[C, R]:
}.toSeq*,
)

def visitEffectInstanceType
(instanceType: EffectInstanceType)
(using ctx: C)
(using Σ: Signature)
: R =
visitEff(instanceType.effect)

def visitEffectInstance(instance: VTerm.EffectInstance)(using ctx: C)(using Σ: Signature): R =
visitEff(instance.effect)

def visitAuto(auto: Auto)(using ctx: C)(using Σ: Signature): R = combine()

def visitHole(using ctx: C)(using Σ: Signature): R = combine()
Expand Down Expand Up @@ -569,6 +581,9 @@ trait Transformer[C]:
case levelType: LevelType => transformLevelType(levelType)
case level: Level => transformLevel(level)
case auto: Auto => transformAuto(auto)
case effectInstanceType: VTerm.EffectInstanceType =>
transformEffectInstanceType(effectInstanceType)
case effectInstance: VTerm.EffectInstance => transformEffectInstance(effectInstance)

def transformType(ty: Type)(using ctx: C)(using Σ: Signature): VTerm =
Type(transformVTerm(ty.upperBound))(using ty.sourceInfo)
Expand Down Expand Up @@ -634,6 +649,23 @@ trait Transformer[C]:
level.maxOperands.map((k, v) => (transformVTerm(k), v)),
)(using level.sourceInfo)

def transformEffectInstanceType
(instanceType: EffectInstanceType)
(using ctx: C)
(using Σ: Signature)
: VTerm =
EffectInstanceType(
transformEff(instanceType.effect),
instanceType.handlerConstraint,
)

def transformEffectInstance(instance: EffectInstance)(using ctx: C)(using Σ: Signature): VTerm =
EffectInstance(
transformEff(instance.effect),
instance.handlerConstraint,
instance.handlerKey,
)

def transformAuto(auto: Auto)(using ctx: C)(using Σ: Signature): VTerm = auto

def transformHole(using ctx: C)(using Σ: Signature): CTerm = Hole
Expand Down Expand Up @@ -777,9 +809,6 @@ trait Transformer[C]:
def transformEff(eff: (QualifiedName, Arguments))(using ctx: C)(using Σ: Signature): Eff =
(transformQualifiedName(eff._1), eff._2.map(transformVTerm))

def transformBigLevel(layer: Nat)(using ctx: C)(using Σ: Signature): Nat =
layer

def transformQualifiedName(qn: QualifiedName)(using ctx: C)(using Σ: Signature): QualifiedName =
qn

Expand Down
2 changes: 1 addition & 1 deletion src/test/scala/com/github/tgeng/archon/core/ir/testing/tterm/tTerm.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ enum TTerm(val sourceInfo: SourceInfo):
extends TTerm(SourceInfo.merge(arg.sourceInfo, bodyType.sourceInfo))
case THandler
(
eff: TTerm,
eff: (QualifiedName, Seq[TTerm]),
otherEffects: TTerm,
outputEffects: TTerm,
outputUsage: TTerm,
Expand Down
111 changes: 54 additions & 57 deletions src/test/scala/com/github/tgeng/archon/core/ir/testing/tterm/translation.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ enum GlobalNameInfo:
case GData(qn: QualifiedName)
case GDataValue(n: Name)
case GRecord(qn: QualifiedName)
case GEffect(qn: QualifiedName)

case class TranslationContext
(
Expand Down Expand Up @@ -115,7 +114,6 @@ extension (tTerm: TTerm)
case Right(GData(qn)) => Return(DataType(qn, Nil))
case Right(GDataValue(n)) => Return(Con(n, Nil))
case Right(GRecord(qn)) => RecordType(qn, Nil)
case Right(GEffect(qn)) => Return(EffectsLiteral(Set((qn, Nil))))
case TDef(qn) => Def(qn)
case TForce(t) =>
translate(t) { case Seq(t) =>
Expand Down Expand Up @@ -160,7 +158,6 @@ extension (tTerm: TTerm)
case Right(GData(qn)) => Return(DataType(qn, args))
case Right(GDataValue(n)) => Return(Con(n, args))
case Right(GRecord(qn)) => RecordType(qn, args)
case Right(GEffect(qn)) => Return(EffectsLiteral(Set((qn, args))))
case _ => redex(c.toCTerm, translatedElims)
case _ => redex(c.toCTerm, translatedElims)
case TFunctionType(arg, bodyType, effects) =>
Expand All @@ -173,7 +170,7 @@ extension (tTerm: TTerm)
)
}
case THandler(
eff,
(qn, tArgs),
otherEffects,
outputEffects,
outputUsage,
Expand All @@ -187,58 +184,58 @@ extension (tTerm: TTerm)
input,
inputBinding,
) =>
translate(
eff,
otherEffects,
outputEffects,
outputUsage,
outputTy,
parameter,
parameterBinding.ty,
parameterBinding.usage,
inputBinding.ty,
inputBinding.usage,
) {
case Seq(
eff,
otherEffects,
outputEffects,
outputUsage,
outputTy,
parameter,
parameterTy,
parameterUsage,
inputTy,
inputUsage,
) =>
Handler(
eff,
otherEffects,
outputEffects,
outputUsage,
outputTy,
parameter,
Binding(parameterTy, parameterUsage)(Name.Normal(parameterBinding.name)),
parameterDisposer.map(_.toCTerm),
parameterReplicator.map(_.toCTerm),
transform.toCTerm,
handlers
.map:
case (qn, THandlerImpl(h, body, boundNames)) =>
qn -> HandlerImpl(
h,
body.toCTerm(using
summon[TranslationContext].bindLocal(parameterBinding.name +: boundNames*),
),
F(Auto(), Auto(), u1),
h.handlerType match
case HandlerType.Simple => None
case HandlerType.Complex => Some(Auto()),
)(boundNames.map(n => Name.Normal(n)))
.to(SeqMap),
input.toCTerm,
Binding(inputTy, inputUsage)(Name.Normal(inputBinding.name)),
)
translate(tArgs*) { case tArgs =>
translate(
otherEffects,
outputEffects,
outputUsage,
outputTy,
parameter,
parameterBinding.ty,
parameterBinding.usage,
inputBinding.ty,
inputBinding.usage,
) {
case Seq(
otherEffects,
outputEffects,
outputUsage,
outputTy,
parameter,
parameterTy,
parameterUsage,
inputTy,
inputUsage,
) =>
Handler(
(qn, tArgs.toList),
otherEffects,
outputEffects,
outputUsage,
outputTy,
parameter,
Binding(parameterTy, parameterUsage)(Name.Normal(parameterBinding.name)),
parameterDisposer.map(_.toCTerm),
parameterReplicator.map(_.toCTerm),
transform.toCTerm,
handlers
.map:
case (qn, THandlerImpl(h, body, boundNames)) =>
qn -> HandlerImpl(
h,
body.toCTerm(using
summon[TranslationContext].bindLocal(parameterBinding.name +: boundNames*),
),
F(Auto(), Auto(), u1),
h.handlerType match
case HandlerType.Simple => None
case HandlerType.Complex => Some(Auto()),
)(boundNames.map(n => Name.Normal(n)))
.to(SeqMap),
input.toCTerm,
Binding(inputTy, inputUsage)(Name.Normal(inputBinding.name)),
)
}
}

def translate
Expand Down Expand Up @@ -278,7 +275,7 @@ extension (tp: TPattern)
case Left(index) => Pattern.PVar(index)
case Right(GData(qn)) => Pattern.PDataType(qn, Nil)
case Right(GDataValue(n)) => Pattern.PConstructor(n, Nil)
case Right(GRecord(_)) | Right(GEffect(_)) | Right(GDef(_)) =>
case Right(GRecord(_)) | Right(GDef(_)) =>
throw UnresolvedSymbol(name)
case TpXConstructor(forced, name, args) =>
val argPatterns = args.map(_.toPattern).toList
Expand Down
11 changes: 0 additions & 11 deletions src/test/scala/com/github/tgeng/archon/core/ir/typing/BasicTypeCheckSpec.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ import com.github.tgeng.archon.common.Ref.given
import com.github.tgeng.archon.core.common.{n, qn}
import com.github.tgeng.archon.core.ir.*
import com.github.tgeng.archon.core.ir.CTerm.*
import com.github.tgeng.archon.core.ir.EqDecidability.{EqDecidable, EqUnknown}
import com.github.tgeng.archon.core.ir.HandlerType.*
import com.github.tgeng.archon.core.ir.Usage.*
import com.github.tgeng.archon.core.ir.VTerm.*
Expand Down Expand Up @@ -78,16 +77,6 @@ class BasicTypeCheckSpec extends AnyFreeSpec:
assertNotVType(UsageLiteral(U1), UsageType(Some(UsageLiteral(U0))))
assertNotVType(LevelLiteral(1), UsageType())

"check eq decidability literals" in:
assertVType(EqDecidabilityLiteral(EqDecidable), EqDecidabilityType())
assertVType(EqDecidabilityLiteral(EqUnknown), EqDecidabilityType())
assertNotVType(LevelLiteral(1), EqDecidabilityType())

"check handler type literals" in:
assertVType(HandlerTypeLiteral(Simple), HandlerTypeType())
assertVType(HandlerTypeLiteral(Complex), HandlerTypeType())
assertNotVType(LevelLiteral(1), HandlerTypeType())

"check vtype types" in:
assertVType(UsageType(), Type(UsageType()))
assertVType(UsageType(), Type(Top(LevelLiteral(0))))
Expand Down

0 comments on commit c081b71

Please sign in to comment.