From 20345abe0a2f66dd04995d013c8c8f2dac4605a4 Mon Sep 17 00:00:00 2001 From: Tianyu Geng Date: Sun, 6 Oct 2024 14:49:52 -0700 Subject: [PATCH] fix test --- .../com/github/tgeng/archon/core/ir/builtins.scala | 6 +++--- .../com/github/tgeng/archon/core/ir/conversion.scala | 2 +- .../com/github/tgeng/archon/core/ir/irError.scala | 11 +---------- .../com/github/tgeng/archon/core/ir/reduction.scala | 10 +++++----- .../com/github/tgeng/archon/core/ir/subtyping.scala | 9 +++++++-- .../scala/com/github/tgeng/archon/core/ir/term.scala | 10 +++++----- .../com/github/tgeng/archon/core/ir/typing.scala | 9 ++++++--- .../com/github/tgeng/archon/core/ir/usages.scala | 2 +- .../com/github/tgeng/archon/core/ir/visitor.scala | 8 ++++---- .../record_stream/translation_output.scala | 2 +- 10 files changed, 34 insertions(+), 35 deletions(-) diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/builtins.scala b/src/main/scala/com/github/tgeng/archon/core/ir/builtins.scala index bf80aeb..05e0c3f 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/builtins.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/builtins.scala @@ -113,6 +113,7 @@ object Builtins: val EffectsRetainSimpleLinearQn: QualifiedName = BuiltinEffects / "retainSimpleLinear" val TotalQn: QualifiedName = BuiltinEffects / "total" val DivQn: QualifiedName = BuiltinEffects / "div" + val NdetQn: QualifiedName = BuiltinEffects / "ndet" val MaybeDivQn: QualifiedName = BuiltinEffects / "mdiv" val BuiltinLevel: QualifiedName = Builtin / "level" @@ -134,9 +135,8 @@ object Builtins: throw new IllegalArgumentException(s"Conflicting definitions: $conflictingDefs") elaborateAll(builtins)(using Context.empty)(using SimpleSignature()) - import CTerm.* - import PreDeclaration.* - import Usage.* +import CTerm.* +import PreDeclaration.* import Usage.* import VTerm.* private def binding(name: Name, ty: VTerm, usage: VTerm = uAny): Binding[CTerm] = diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/conversion.scala b/src/main/scala/com/github/tgeng/archon/core/ir/conversion.scala index 618993e..0648675 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/conversion.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/conversion.scala @@ -284,7 +284,7 @@ def checkIsConvertible op2 @ OperationCall(effInstance2, name2, args2), ) if name1 == name2 => val effConstraint = checkIsConvertible(effInstance1, effInstance2, Some(EffectsType())) - val (qn, tArgs) = inferType(effInstance1)._1 match + val (qn, tArgs) = inferType(effInstance1)._2 match case EffectInstanceType(eff, _) => eff case _ => throw ComplexOperationCall(op2) val operation = Σ.getOperation(qn, name1) diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/irError.scala b/src/main/scala/com/github/tgeng/archon/core/ir/irError.scala index 77d8850..e335757 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/irError.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/irError.scala @@ -49,7 +49,6 @@ enum IrError(val Γ: Context, e: Throwable | Null = null) extends Exception(e): case MissingDefinition(qn: QualifiedName) extends IrError(Context.empty) case MissingField(name: Name, qn: QualifiedName) extends IrError(Context.empty) case MissingFieldsInCoPattern(clause: PreClause)(using Γ: Context) extends IrError(Γ) - case MissingOperation(name: Name, qn: QualifiedName) extends IrError(Context.empty) case MissingUserCoPattern(clause: PreClause)(using Γ: Context) extends IrError(Γ) case NonEmptyType(ty: VTerm, source: PreClause)(using Γ: Context) extends IrError(Γ) case NotCConvertible(sub: CTerm, sup: CTerm, ty: Option[CTerm])(using Γ: Context) @@ -60,12 +59,6 @@ enum IrError(val Γ: Context, e: Throwable | Null = null) extends Exception(e): case NotDataTypeType(tm: CTerm)(using Γ: Context) extends IrError(Γ) case NotLevelType(tm: VTerm)(using Γ: Context) extends IrError(Γ) case NotEffectSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ) - case NotEqDecidabilitySubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ) - case NotHandlerTypeSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ) - case NotEqDecidableDueToConstructor - (qn: QualifiedName, conName: Name, badComponentIndex: Nat) - (using Γ: Context) extends IrError(Γ) - case NotEqDecidableType(ty: VTerm)(using Γ: Context) extends IrError(Γ) case NotLevelSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ) case NotTypeError(tm: VTerm)(using Γ: Context) extends IrError(Γ) case NotUsageSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ) @@ -94,13 +87,11 @@ enum IrError(val Γ: Context, e: Throwable | Null = null) extends Exception(e): (using Γ: Context) extends IrError(Γ, cause) case DataLevelCannotDependOnIndexArgument(preData: PreDeclaration.PreData)(using Γ: Context) extends IrError(Γ) - case DataEqDecidabilityCannotDependOnIndexArgument - (preData: PreDeclaration.PreData) - (using Γ: Context) extends IrError(Γ) case DuplicatedDeclaration(qn: QualifiedName) extends IrError(Context.empty) case UnableToFindUsageMeetDuringUnification(lowerBounds: Set[VTerm])(using Γ: Context) extends IrError(Γ) case InternalIrError(message: String)(using Γ: Context) extends IrError(Γ) case ComplexOperationCall(call: CTerm.OperationCall)(using Γ: Context) extends IrError(Γ) case ExpectEffectInstance(badEffInstance: VTerm)(using Γ: Context) extends IrError(Γ) + case ExpectEffectInstanceTypeSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context) extends IrError(Γ) override def getMessage: String = verbosePPrinter.apply(this).plainText diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/reduction.scala b/src/main/scala/com/github/tgeng/archon/core/ir/reduction.scala index ce3809c..bc658cd 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/reduction.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/reduction.scala @@ -557,9 +557,9 @@ extension (v: VTerm) operands.map((k, v) => dfs(k.normalized, retainSimpleLinearOnly || v)).toSeq val newLiterals = (literalsAndOperands.flatMap { case (l, _) => l } ++ literal) .filter(effInstance => - val (qn, args) = inferType(effInstance)._1 match + val (qn, args) = inferType(effInstance)._2 match case EffectInstanceType(eff, _) => eff - case _ => throw IllegalStateException("bad type") + case t => throw IllegalStateException(s"Expect EffectInstanceType but got $t") if retainSimpleLinearOnly then { val effect = Σ.getEffect(qn) effect.continuationUsage @@ -634,9 +634,9 @@ given Reducible[CTerm] with (using signature: Signature) (using TypingContext) : CTerm = - // TODO[P0]: if the reduced term contains `Continuation` or `HandlerKey`, then throw away the - // reduced term and simply return t as it is. This is needed because `Continuation` is too hard - // to be lowered. + // TODO[P1]: if the reduced term contains `Continuation` or `EffectInstance`, then throw away + // the reduced term and simply return t as it is. This is needed because `Continuation` is too + // hard to be lowered. StackMachine(mutable.ArrayBuffer()).run(t).withSourceInfo(t.sourceInfo) object Reducible: diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/subtyping.scala b/src/main/scala/com/github/tgeng/archon/core/ir/subtyping.scala index 188d5bc..22663ec 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/subtyping.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/subtyping.scala @@ -6,7 +6,6 @@ import com.github.tgeng.archon.common.WrapPolicy.* import com.github.tgeng.archon.core.common.* import com.github.tgeng.archon.core.ir.CTerm.* import com.github.tgeng.archon.core.ir.Declaration.* -import com.github.tgeng.archon.core.ir.HandlerType.{Complex, Simple} import com.github.tgeng.archon.core.ir.IrError.* import com.github.tgeng.archon.core.ir.PrettyPrinter.pprint import com.github.tgeng.archon.core.ir.ResolvedMetaVariable.* @@ -28,7 +27,6 @@ def checkIsSubtype (using ctx: TypingContext) : Set[Constraint] = debugSubsumption("checkIsSubtype", sub, sup): check2(sub, sup): - // TODO[P0]: add logic for EffectInstanceType case (sub, sup) if sub == sup => Set.empty case (sub: VTerm, u @ RUnsolved(_, _, constraint, _, _)) => ctx.adaptForMetaVariable(u, sub): @@ -96,6 +94,13 @@ def checkIsSubtype case _ => throw NotVSubtype(sub, sup) case (LevelType(ub1), LevelType(ub2)) => if ub1 <= ub2 then Set.empty else throw NotVSubtype(sub, sup) + case ( + EffectInstanceType((qn1, args1), handlerConstraint1), + EffectInstanceType((qn2, args2), handlerConstraint2), + ) => + if handlerConstraint1 > handlerConstraint2 || qn1 != qn2 then + throw ExpectEffectInstanceTypeSubsumption(sub, sup) + else checkAreConvertible(args1, args2, Σ.getEffect(qn1).context.toList) case _ => checkIsConvertible(sub, sup, None) /** Preconditions: sub and sup are both types diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/term.scala b/src/main/scala/com/github/tgeng/archon/core/ir/term.scala index 1f2a6fa..ef3fca3 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/term.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/term.scala @@ -327,14 +327,12 @@ enum VTerm(val sourceInfo: SourceInfo) extends SourceInfoOwner[VTerm]: (literal: LevelOrder, maxOperands: SeqMap[VTerm, /* level offset */ Nat]) (using sourceInfo: SourceInfo) extends VTerm(sourceInfo) - // TODO[P0]: rename to EffectInstanceType case EffectInstanceType - (effect: Eff, handlerConstraint: HandlerConstraint) + (eff: Eff, handlerConstraint: HandlerConstraint) (using sourceInfo: SourceInfo) extends VTerm(sourceInfo) - // TODO[P0]: rename to EffectInstance case EffectInstance - (effect: Eff, handlerConstraint: HandlerConstraint, handlerKey: HandlerKey = HandlerKey()) + (eff: Eff, handlerConstraint: HandlerConstraint, handlerKey: HandlerKey = HandlerKey()) extends VTerm(SourceInfo.SiEmpty) /** Automatically derived term, aka, `_` in Agda-like languages. During type checking, this is @@ -455,7 +453,9 @@ object VTerm: val uAny: VTerm = VTerm.UsageLiteral(Usage.UAny) val div: EffectInstance = EffectInstance((Builtins.DivQn, Nil), HandlerConstraint(Usage.U0, HandlerType.Simple)) - val globalKeys: Set[EffectInstance] = Set(div) + val ndet: EffectInstance = + EffectInstance((Builtins.NdetQn, Nil), HandlerConstraint(Usage.U1, HandlerType.Simple)) + val globalKeys: Set[EffectInstance] = Set(div, ndet) /** Marker of a computation that surely diverges. Computation with this effect will not be * executed by the type checker. diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/typing.scala b/src/main/scala/com/github/tgeng/archon/core/ir/typing.scala index b4fbfa0..fa6aa79 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/typing.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/typing.scala @@ -179,7 +179,9 @@ def inferType case EffectInstanceType(eff, handlerConstraint) => val newTm = EffectInstanceType(checkEff(eff), handlerConstraint) (newTm, Type(newTm)) - case EffectInstance(_, _, _) => ??? + case t @ EffectInstance(eff, handlerConstraint, _) => + // There is no need to check eff because EffectInstance is only created by reduction. + (t, EffectInstanceType(eff, handlerConstraint)) case LevelType(strictUpperBound) => (LevelType(strictUpperBound), Type(LevelType(strictUpperBound))) case Level(literal, maxOperands) => @@ -440,7 +442,7 @@ def inferType val args = checkTypes(uncheckedArgs, record.context.map(_._1).toList) (RecordType(qn, args, effects), CType(tm, Total())) case OperationCall(effInstance, name, uncheckedArgs) => - val (qn, uncheckedTArgs) = inferType(effInstance)._1 match + val (qn, uncheckedTArgs) = inferType(effInstance)._2 match case EffectInstanceType(eff, _) => eff case _ => throw IllegalStateException( @@ -511,6 +513,7 @@ def checkType (using Σ: Signature) (using ctx: TypingContext) : CTerm = debugCheckType(tm, ty): + // TODO[P0]: using something of effect instance type but not as an effect instance should yield ndet effect. tm match case Force(v) => val checkedV = checkType(v, U(ty)) @@ -943,7 +946,7 @@ private def getEffectsContinuationUsage val usage = ctx.withMetaResolved(effects.normalized): case Effects(effectInstances, operands) => val literalUsages = effectInstances.map { effectInstance => - inferType(effectInstance)._1 match + inferType(effectInstance)._2 match case EffectInstanceType(_, handlerConstraint) => UsageLiteral(handlerConstraint.continuationUsage) case _ => throw IllegalStateException("type error") diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/usages.scala b/src/main/scala/com/github/tgeng/archon/core/ir/usages.scala index 082affa..2b298a8 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/usages.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/usages.scala @@ -194,7 +194,7 @@ def collectUsages collectArgsUsages(args, record.context.map(_._1).toList) + collectUsages(effects, Some(EffectsType())) case OperationCall(effectInstance, name, args) => - val (qn, tArgs) = inferType(effectInstance)._1 match + val (qn, tArgs) = inferType(effectInstance)._2 match case EffectInstanceType(eff, _) => eff case _ => throw IllegalStateException( diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/visitor.scala b/src/main/scala/com/github/tgeng/archon/core/ir/visitor.scala index 44ead43..e6fae59 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/visitor.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/visitor.scala @@ -121,10 +121,10 @@ trait TermVisitor[C, R]: (using ctx: C) (using Σ: Signature) : R = - visitEff(instanceType.effect) + visitEff(instanceType.eff) def visitEffectInstance(instance: VTerm.EffectInstance)(using ctx: C)(using Σ: Signature): R = - visitEff(instance.effect) + visitEff(instance.eff) def visitAuto(auto: Auto)(using ctx: C)(using Σ: Signature): R = combine() @@ -655,13 +655,13 @@ trait Transformer[C]: (using Σ: Signature) : VTerm = EffectInstanceType( - transformEff(instanceType.effect), + transformEff(instanceType.eff), instanceType.handlerConstraint, ) def transformEffectInstance(instance: EffectInstance)(using ctx: C)(using Σ: Signature): VTerm = EffectInstance( - transformEff(instance.effect), + transformEff(instance.eff), instance.handlerConstraint, instance.handlerKey, ) diff --git a/src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/record_stream/translation_output.scala b/src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/record_stream/translation_output.scala index 9063fa9..208dc86 100644 --- a/src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/record_stream/translation_output.scala +++ b/src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/record_stream/translation_output.scala @@ -48,7 +48,7 @@ List( bodyTy = RecordType( qn = qn"test.CStream", args = List(), - effects = Effects(literal = Set(), unionOperands = SeqMap()) @ "ε" + effects = Effects(handlerKeys = Set(), unionOperands = SeqMap()) @ "ε" ) @ "CStream", effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total") @ "ε") @ "ε" ) @ "Eq Nat m (head self) -> CStream",