diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/elaboration.scala b/src/main/scala/com/github/tgeng/archon/core/ir/elaboration.scala index 67cbff1..a61ef1a 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/elaboration.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/elaboration.scala @@ -7,12 +7,14 @@ import com.github.tgeng.archon.core.ir.CTerm.* import com.github.tgeng.archon.core.ir.CaseTree.* import com.github.tgeng.archon.core.ir.CoPattern.* import com.github.tgeng.archon.core.ir.Declaration.* +import com.github.tgeng.archon.core.ir.DeclarationPart.* import com.github.tgeng.archon.core.ir.IrError.* import com.github.tgeng.archon.core.ir.Pattern.* import com.github.tgeng.archon.core.ir.PreDeclaration.* import com.github.tgeng.archon.core.ir.SourceInfo.* import com.github.tgeng.archon.core.ir.UnificationResult.* import com.github.tgeng.archon.core.ir.VTerm.* +import com.github.tgeng.archon.core.ir.unifyAll import scala.collection.immutable.SeqMap import scala.collection.mutable @@ -55,8 +57,6 @@ def elaborate enum DeclarationPart: case HEAD, BODY -import com.github.tgeng.archon.core.ir.DeclarationPart.* import com.github.tgeng.archon.core.ir.unifyAll - @throws(classOf[IrError]) def sortPreDeclarations (declarations: Seq[PreDeclaration]) @@ -192,17 +192,15 @@ private def elaborateDataHead case _ => throw NotDataTypeType(ty) val (tIndices, level) = elaborateTy(preData.ty) - // level and eqDecidability should not depend on index arguments + // level should not depend on index arguments val strengthenedLevel = try level.strengthen(tIndices.size, 0) catch case e: StrengthenException => throw DataLevelCannotDependOnIndexArgument(preData) - val data = checkData( - Data( - preData.qn, - Γ.zip(Iterator.continually(Variance.INVARIANT)) ++ tParamTys, - tIndices, - strengthenedLevel, - ), + val data = Data( + preData.qn, + Γ.zip(Iterator.continually(Variance.INVARIANT)) ++ tParamTys, + tIndices, + strengthenedLevel, ) Σ.addDeclaration(data) @@ -216,12 +214,12 @@ private def elaborateDataBody @throws(classOf[IrError]) def elaborateTy - (ty: CTerm) + (ty: CTerm, level: VTerm) (using Γ: Context) (using Signature) (using TypingContext) : (Telescope, /* constructor tArgs */ List[VTerm]) = - checkIsCType(ty).normalized(None) match + checkIsCType(ty, Some(level)).normalized(None) match // Here and below we do not care the declared effect types because data type constructors // are always total. Declaring non-total signature is not necessary (nor desirable) but // acceptable. @@ -234,23 +232,25 @@ private def elaborateDataBody (Nil, args.drop(data.context.size)) case F(t, _, _) => throw ExpectDataType(t, Some(data.qn)) case FunctionType(binding, bodyTy, _, _) => - val (telescope, level) = elaborateTy(bodyTy)(using Γ :+ binding) - (binding :: telescope, level) + val (telescope, args) = elaborateTy(bodyTy, level.weakened)(using Γ :+ binding) + (binding :: telescope, args) case _ => throw NotDataTypeType(ty) // number of index arguments given Context = data.context.map(_._1) ctx.trace(s"elaborating data body ${preData.qn}"): - preData.constructors.foldLeft[Signature](Σ) { case (_Σ, constructor) => - given Signature = _Σ - ctx.trace(s"elaborating constructor ${constructor.name}"): - val ty = constructor.ty - val (paramTys, tArgs) = elaborateTy(ty) - val con = - checkDataConstructor(preData.qn, Constructor(constructor.name, paramTys, tArgs)) - _Σ.addConstructor(preData.qn, con) - } + preData.constructors + .foldLeft[Signature](Σ) { case (_Σ, constructor) => + given Signature = _Σ + ctx.trace(s"elaborating constructor ${constructor.name}"): + val ty = constructor.ty + val (paramTys, tArgs) = elaborateTy(ty, data.level) + val con = + checkDataConstructor(preData.qn, Constructor(constructor.name, paramTys, tArgs)) + _Σ.addConstructor(preData.qn, con) + } + .replaceDeclaration(checkData(data)) @throws(classOf[IrError]) private def elaborateRecordHead @@ -280,7 +280,7 @@ private def elaborateRecordHead ), ) case t => throw ExpectCType(t) - Σ.addDeclaration(checkRecord(r)) + Σ.addDeclaration(r) @throws(classOf[IrError]) private def elaborateRecordBody @@ -297,13 +297,16 @@ private def elaborateRecordBody record.selfBinding.name, ) + val level = record.level.weakened // weakened for self ctx.trace(s"elaborating record body ${preRecord.qn}"): - preRecord.fields.foldLeft[Signature](Σ) { case (_Σ, field) => - ctx.trace(s"elaborating field ${field.name}"): - val ty = checkIsCType(field.ty).normalized(None) - val f = checkRecordField(preRecord.qn, Field(field.name, ty)) - _Σ.addField(preRecord.qn, f) - } + preRecord.fields + .foldLeft[Signature](Σ) { case (_Σ, field) => + ctx.trace(s"elaborating field ${field.name}"): + val ty = checkIsCType(field.ty, Some(level)).normalized(None) + val f = checkRecordField(preRecord.qn, Field(field.name, ty)) + _Σ.addField(preRecord.qn, f) + } + .replaceDeclaration(checkRecord(record)) @throws(classOf[IrError]) private def elaborateDefHead @@ -323,7 +326,7 @@ private def elaborateDefHead given Context = newEContext.map(_._1) val ty = checkIsCType(definition.ty).normalized(None) val d: Definition = Definition(definition.qn, newEContext, ty) - Σ.addDeclaration(checkDef(d)) + Σ.addDeclaration(d) @throws(classOf[IrError]) private def elaborateDefBody @@ -690,7 +693,6 @@ private def elaborateDefBody val ρ2t = ρ2.toTermSubstitutor given ΓSplit: Context = _Γ1 ++ Δ.subst(ρ.toTermSubstitutor) ++ _Γ2.subst(ρ1t) - ctx.debug(ΓSplit) val newProblem = subst(problem, ρ2t) if newProblem.isEmpty then @@ -785,12 +787,12 @@ private def elaborateDefBody }, ) _Σ.addCaseTree(preDefinition.qn, _Q) - // We didn't solve the meta-variables inside the definition type until now because we want to - // have the call-site context ready before solving them. Delay solving during body elaboration - // works as long as lambda definitions are APPENDED after the call-site declaration. This is - // because our topological sort preserves original order of definitions when possible. Hence, - // the call-site function body would be elaborated before the lambda body. - _Σ.replaceDeclaration(definition.copy(ty = ctx.solveTerm(definition.ty))) + // We didn't solve the meta-variables inside the definition type until now because we want to + // have the call-site context ready before solving them. Delay solving during body elaboration + // works as long as lambda definitions are APPENDED after the call-site declaration. This is + // because our topological sort preserves original order of definitions when possible. Hence, + // the call-site function body would be elaborated before the lambda body. + .replaceDeclaration(checkDef(definition)) @throws(classOf[IrError]) private def elaborateEffectHead @@ -808,7 +810,7 @@ private def elaborateEffectHead case Return(continuationUsage, _) => continuationUsage case c => throw ExpectReturnAValue(c) val e: Effect = Effect(effect.qn, Γ2, continuationUsage) - Σ.addDeclaration(checkEffect(e)) + Σ.addDeclaration(e) @throws(classOf[IrError]) private def elaborateEffectBody @@ -831,20 +833,21 @@ private def elaborateEffectBody // Here and below we do not care the declared effect types because data type constructors // are always total. Declaring non-total signature is not necessary (nor desirable) but // acceptable. - case F(ty, _, usage) => - (Nil, ty, usage) + case F(ty, _, usage) => (Nil, ty, usage.normalized) case FunctionType(binding, bodyTy, _, _) => val (telescope, level, usage) = elaborateTy(bodyTy)(using Γ :+ binding) (binding :: telescope, level, usage) case _ => throw ExpectFType(ty) - preEffect.operations.foldLeft[Signature](Σ) { case (_Σ, operation) => - given Signature = _Σ - ctx.trace(s"elaborating operation ${operation.name}"): - val (paramTys, resultTy, usage) = elaborateTy(operation.ty) - val o = Operation(operation.name, paramTys, resultTy, usage) - _Σ.addOperation(effect.qn, checkOperation(effect.qn, o)) - } + preEffect.operations + .foldLeft[Signature](Σ) { case (_Σ, operation) => + given Signature = _Σ + ctx.trace(s"elaborating operation ${operation.name}"): + val (paramTys, resultTy, usage) = elaborateTy(operation.ty) + val o = Operation(operation.name, paramTys, resultTy, usage) + _Σ.addOperation(effect.qn, checkOperation(effect.qn, o)) + } + .replaceDeclaration(checkEffect(effect)) @throws(classOf[IrError]) private def elaborateTTelescope diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/signature.scala b/src/main/scala/com/github/tgeng/archon/core/ir/signature.scala index d3ddab6..3df7d69 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/signature.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/signature.scala @@ -26,7 +26,7 @@ enum Declaration: ( qn: QualifiedName, context: TContext, - /* binding: + context + tIndexTys */ + /* binding += context */ level: VTerm, selfBinding: Binding[VTerm], ) @@ -56,11 +56,11 @@ case class Constructor tArgs: Arguments = Nil, /* binding += context + paramTys */ ) -case class Field(name: Name, /* + tParamTys + 1 for self */ ty: CTerm) +case class Field(name: Name, /* binding += context + 1 for self */ ty: CTerm) case class Clause ( - // contains def.context + // contains def.context + elaborated variables from lhs co-patterns context: Context, lhs: List[CoPattern], /* bindings += clause.context */ rhs: CTerm, /* bindings += clause.context */ diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/signatureTyping.scala b/src/main/scala/com/github/tgeng/archon/core/ir/signatureTyping.scala index 27b6912..d95f7f4 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/signatureTyping.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/signatureTyping.scala @@ -1,7 +1,6 @@ package com.github.tgeng.archon.core.ir import com.github.tgeng.archon.common.* -import com.github.tgeng.archon.common.IndentPolicy.* import com.github.tgeng.archon.core.common.* import com.github.tgeng.archon.core.ir import com.github.tgeng.archon.core.ir.CTerm.* @@ -18,13 +17,12 @@ def checkData(data: Data)(using Σ: Signature)(using ctx: TypingContext): Data = given Context = IndexedSeq() ctx.trace(s"checking data signature ${data.qn}"): val tParamsTysTelescope = - ctx.solveTerm(checkParameterTyDeclarations(data.context.map(_._1).toTelescope)) + ctx.solveTerm(data.context.map(_._1).toTelescope) { given tParamTys: Context = Context.fromTelescope(tParamsTysTelescope) - val tIndexTys = - ctx.solveTerm(checkParameterTyDeclarations(data.tIndexTys)) + val tIndexTys = ctx.solveTerm(data.tIndexTys) checkTParamsAreUnrestricted((tParamTys ++ tIndexTys).toTelescope) - val level = ctx.solveTerm(checkLevel(data.level)) + val level = ctx.solveTerm(data.level) Data(data.qn, tParamTys.zip(data.context.map(_._2)), tIndexTys, level) } @@ -39,7 +37,7 @@ def checkDataConstructor case Some(data) => given Γ: Context = data.context.map(_._1) ctx.trace(s"checking data constructor $qn.${con.name}"): - val paramTys = ctx.solveTerm(checkParameterTyDeclarations(con.paramTys, Some(data.level))) + val paramTys = ctx.solveTerm(con.paramTys) val tArgsContext = Γ ++ paramTys val tArgs = checkTypes(con.tArgs, data.tIndexTys.weaken(con.paramTys.size, 0))(using tArgsContext) @@ -54,7 +52,7 @@ def checkRecord(record: Record)(using Σ: Signature)(using ctx: TypingContext): given Context = IndexedSeq() ctx.trace(s"checking record signature ${record.qn}"): val tParams = record.context.map(_._1) - val tParamTysTelescope = ctx.solveTerm(checkParameterTyDeclarations(tParams.toList)) + val tParamTysTelescope = ctx.solveTerm(tParams.toList) { given tParamTys: Context = Context.fromTelescope(tParamTysTelescope) checkTParamsAreUnrestricted(tParamTysTelescope) @@ -81,7 +79,7 @@ def checkRecordField given Context = record.context.map(_._1).toIndexedSeq :+ record.selfBinding ctx.trace(s"checking record field $qn.${field.name}"): - val ty = ctx.solveTerm(checkIsCType(field.ty, Some(record.level.weakened))) + val ty = ctx.solveTerm(field.ty) val violatingVars = // 1 is to offset self binding. VarianceChecker.visitCTerm(field.ty)(using record.context, Variance.COVARIANT, 1) @@ -210,24 +208,15 @@ private object VarianceChecker extends Visitor[(TContext, Variance, Nat), Seq[Va @throws(classOf[IrError]) def checkDef(definition: Definition)(using Signature)(using ctx: TypingContext): Definition = - // TODO[P0]: do escape analysis here. Make sure to automatically derive it for null escape status - given Context = definition.context.map(_._1) - ctx.trace(s"checking def signature ${definition.qn}"): - val ty = checkIsCType(definition.ty) - Definition(definition.qn, definition.context, ty) + definition.copy(ty = ctx.solveTerm(definition.ty)(using definition.context.map(_._1))) @throws(classOf[IrError]) def checkEffect(effect: Effect)(using Signature)(using ctx: TypingContext): Effect = given Context = Context.empty ctx.trace(s"checking effect signature ${effect.qn}"): - val telescope = ctx.solveTerm(checkParameterTyDeclarations(effect.context.toTelescope)) - checkTParamsAreUnrestricted(telescope) - - { - given Γ: Context = Context.fromTelescope(telescope) - val continuationUsage = ctx.solveTerm(checkType(effect.continuationUsage, UsageType())) - Effect(effect.qn, Γ, continuationUsage) - } + given Γ: Context = Context.fromTelescope(effect.context.toTelescope) + val continuationUsage = ctx.solveTerm(effect.continuationUsage) + Effect(effect.qn, Γ, continuationUsage) @throws(classOf[IrError]) def checkOperation @@ -241,12 +230,11 @@ def checkOperation given Γ: Context = effect.context ctx.trace(s"checking effect operation $qn.${operation.name}"): - val paramTys = ctx.solveTerm(checkParameterTyDeclarations(operation.paramTys)) + val paramTys = ctx.solveTerm(operation.paramTys) { given Context = Γ ++ paramTys - val resultTy = ctx.solveTerm(checkIsType(operation.resultTy)) - val resultUsage = - ctx.solveTerm(checkType(operation.resultUsage, UsageType(None))) + val resultTy = ctx.solveTerm(operation.resultTy) + val resultUsage = ctx.solveTerm(operation.resultUsage) Operation( operation.name, paramTys, @@ -270,16 +258,3 @@ private def checkTParamsAreUnrestricted ExpectUnrestrictedTypeParameterBinding(binding), ) checkTParamsAreUnrestricted(rest)(using Γ :+ binding) - -@throws(classOf[IrError]) -private def checkParameterTyDeclarations - (tParamTys: Telescope, levelBound: Option[VTerm] = None) - (using Γ: Context) - (using Σ: Signature) - (using TypingContext) - : Telescope = tParamTys match - case Nil => Nil - case binding :: rest => - val ty = checkIsType(binding.ty, levelBound) - val usage = checkType(binding.usage, UsageType(None)) - Binding(ty, usage)(binding.name) :: checkParameterTyDeclarations(rest)(using Γ :+ binding) 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 4fef6c7..1387672 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 @@ -298,7 +298,7 @@ enum VTerm(val sourceInfo: SourceInfo) extends SourceInfoOwner[VTerm]: case Con(name: Name, args: Arguments = Nil)(using sourceInfo: SourceInfo) extends VTerm(sourceInfo) - // Note, `upper` here is in the sense of typing subsumption, not the usage lattice. This is the + // Note, `upper` here is in the sense of typing subsumption, not the usage lattice. This is, the // lower bound in the usage lattice. Hence Option.None is used to represent unbounded case, as the // lattice is not bounded below. Note that the semantic of this `upperBound` is different from // `continuationUsage`. diff --git a/src/main/scala/com/github/tgeng/archon/core/ir/typingContext.scala b/src/main/scala/com/github/tgeng/archon/core/ir/typingContext.scala index 8f58a8b..cd9937c 100644 --- a/src/main/scala/com/github/tgeng/archon/core/ir/typingContext.scala +++ b/src/main/scala/com/github/tgeng/archon/core/ir/typingContext.scala @@ -638,7 +638,7 @@ class TypingContext if enableDebugging then val indent = "│ " * traceLevel + " " println( - indent + ANSI_CYAN + stringify(t) + " = " + verbosePPrinter + indent + ANSI_CYAN + "[DEBUG] " + stringify(t) + " = " + verbosePPrinter .apply(t) .toString .replace("\n", "\n" + indent) + ANSI_RESET,