diff --git a/build.sbt b/build.sbt index b60051a..83d2cbd 100644 --- a/build.sbt +++ b/build.sbt @@ -1,14 +1,14 @@ Global / onChangedBuildSource := ReloadOnSourceChanges ThisBuild / version := "0.1.0-SNAPSHOT" -ThisBuild / scalaVersion := "3.4.2" +ThisBuild / scalaVersion := "3.5.1" lazy val root = (project in file(".")) .settings( name := "archon", scalacOptions ++= Seq( "-Yexplicit-nulls", - "-Ykind-projector", + "-Xkind-projector", "-Xfatal-warnings", "-feature", "-deprecation", @@ -17,10 +17,10 @@ lazy val root = (project in file(".")) "-indent", ), libraryDependencies ++= Seq( - "org.scalatest" %% "scalatest" % "3.2.18" % "test", + "org.scalatest" %% "scalatest" % "3.2.19" % "test", "com.lihaoyi" %% "pprint" % "0.9.0", - "com.lihaoyi" %% "fastparse" % "3.1.0", - "com.lihaoyi" %% "os-lib" % "0.10.2", + "com.lihaoyi" %% "fastparse" % "3.1.1", + "com.lihaoyi" %% "os-lib" % "0.10.7", "org.scala-lang.modules" %% "scala-collection-contrib" % "0.3.0", ), Compile / unmanagedJars += { 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 05e0c3f..b3446cd 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 @@ -2,7 +2,11 @@ package com.github.tgeng.archon.core.ir import com.github.tgeng.archon.core.common.* import com.github.tgeng.archon.core.common.QualifiedName.* +import com.github.tgeng.archon.core.ir.CTerm.* import com.github.tgeng.archon.core.ir.Declaration.* +import com.github.tgeng.archon.core.ir.PreDeclaration.* +import com.github.tgeng.archon.core.ir.Usage.* +import com.github.tgeng.archon.core.ir.VTerm.* import scala.collection.immutable.SeqMap @@ -135,10 +139,6 @@ object Builtins: throw new IllegalArgumentException(s"Conflicting definitions: $conflictingDefs") elaborateAll(builtins)(using Context.empty)(using SimpleSignature()) -import CTerm.* -import PreDeclaration.* import Usage.* - import VTerm.* - private def binding(name: Name, ty: VTerm, usage: VTerm = uAny): Binding[CTerm] = Binding(Return(ty, uAny), Return(usage, uAny))(name) 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 22663ec..d63606b 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 @@ -131,15 +131,15 @@ def checkIsSubtype case ((_: ResolvedMetaVariable, Nil), _) | (_, (_: ResolvedMetaVariable, Nil)) => Set(Constraint.CSubType(Γ, sub, sup)) case (CType(upperBound1, eff1), CType(upperBound2, eff2)) => - val effConstraint = checkEffSubsumption(eff1, eff2) + val effConstraint = checkEffectSubsumption(eff1, eff2) val upperBoundConstraint = checkIsSubtype(upperBound1, upperBound2) effConstraint ++ upperBoundConstraint case (ty: IType, CTop(level2, eff2)) => val levelConstraint = checkLevelSubsumption(inferLevel(sub), level2) - val effConstraint = checkEffSubsumption(ty.effects, eff2) + val effConstraint = checkEffectSubsumption(ty.effects, eff2) levelConstraint ++ effConstraint case (F(vTy1, eff1, u1), F(vTy2, eff2, u2)) => - val effConstraint = checkEffSubsumption(eff1, eff2) + val effConstraint = checkEffectSubsumption(eff1, eff2) val usageConstraint = checkUsageSubsumption(u1, u2) val tyConstraint = checkIsSubtype(vTy1, vTy2) effConstraint ++ usageConstraint ++ tyConstraint @@ -147,7 +147,7 @@ def checkIsSubtype FunctionType(binding1, bodyTy1, eff1), FunctionType(binding2, bodyTy2, eff2), ) => - val effConstraint = checkEffSubsumption(eff1, eff2) + val effConstraint = checkEffectSubsumption(eff1, eff2) val tyConstraint = ctx.solve(checkIsSubtype(binding2.ty, binding1.ty)) val usageConstraint = ctx.solve(checkUsageSubsumption(binding2.usage, binding1.usage)) val bodyConstraint = @@ -177,7 +177,7 @@ def checkIsSubtype case None => throw MissingDeclaration(qn1) case Some(record) => val args = ArrayBuffer[VTerm]() - val effConstraint = checkEffSubsumption(eff1, eff2) + val effConstraint = checkEffectSubsumption(eff1, eff2) val argConstraint = args1 .zip(args2) .zip(record.context) @@ -449,6 +449,8 @@ def checkUsageSubsumption ) Set.empty case _ => Set(Constraint.UsageSubsumption(Γ, sub, rawSup)) + case (_: VTerm, r: ResolvedMetaVariable) => + throw IllegalStateException(s"Expected unsolved usage meta var but got $r") case (_: ResolvedMetaVariable, sup: VTerm) => Set(Constraint.UsageSubsumption(Γ, rawSub, sup)) case (_: ResolvedMetaVariable, _: ResolvedMetaVariable) => @@ -464,12 +466,12 @@ def checkUsageSubsumption else checkUsageSubsumption(solvedSub, solvedSup) @throws(classOf[IrError]) -private def checkEffSubsumption +private def checkEffectSubsumption (rawSub: VTerm, rawSup: VTerm) (using Γ: Context) (using Σ: Signature) (using ctx: TypingContext) - : Set[Constraint] = debugSubsumption("checkEffSubsumption", rawSub, rawSup): + : Set[Constraint] = debugSubsumption("checkEffectSubsumption", rawSub, rawSup): check2(rawSub, rawSup): case (sub, sup) if sub == sup => Set.empty // Handle the special case that the right hand side simply contains the left hand side as an operand. @@ -501,6 +503,8 @@ private def checkEffSubsumption case _ => throw IllegalStateException("type error") ctx.updateConstraint(u, UmcEffSubsumption(newLowerBound)) Set.empty + case (_: VTerm, r: ResolvedMetaVariable) => + throw IllegalStateException(s"Expected unsolved effect meta var but got $r") // If upper bound is total, the meta variable can only take total as the value. case ( u @ RUnsolved(_, _, UmcEffSubsumption(_), _, _), @@ -549,7 +553,7 @@ private def checkEffSubsumption val solvedSub = ctx.solveTerm(sub) val solvedSup = ctx.solveTerm(sup) if solvedSub == sub && solvedSup == sup then throw NotEffectSubsumption(sub, sup) - else checkEffSubsumption(solvedSub, solvedSup) + else checkEffectSubsumption(solvedSub, solvedSup) // If spurious operands are all stuck computation, it's possible for sub to be if all of these stuck computation // ends up being assigned values that are part of sup // Also, if sup contains stuck computation, it's possible for sup to end up including arbitrary effects and hence @@ -561,7 +565,7 @@ private def checkEffSubsumption val solvedSub = ctx.solveTerm(sub) val solvedSup = ctx.solveTerm(sup) if solvedSub == sub && solvedSup == sup then throw NotEffectSubsumption(sub, sup) - else checkEffSubsumption(solvedSub, solvedSup) + else checkEffectSubsumption(solvedSub, solvedSup) /** Checks if l1 is smaller than l2. */ @@ -605,6 +609,8 @@ private def checkLevelSubsumption val solvedSup = ctx.solveTerm(sup) if solvedSub == sub && solvedSup == sup then throw NotLevelSubsumption(sub, sup) else checkLevelSubsumption(solvedSub, solvedSup) + case (_: VTerm, r: ResolvedMetaVariable) => + throw IllegalStateException(s"Expected unsolved level meta var but got $r") // Handle the special case that the right hand side simply contains the left hand side as an operand. case (RUnsolved(_, _, _, tm, _), Level(_, operands)) if operands.contains(Collapse(tm)) => Set.empty 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 ef3fca3..141bcf3 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 @@ -193,8 +193,6 @@ object LevelOrder: // 256 is arbitrary but it should be enough for any practical purpose val upperBound: LevelOrder = LevelOrder(256, 0) -extension (o: LevelOrder) infix def suc(n: Nat): LevelOrder = LevelOrder(o.m, o.n + n) - sealed trait UsageCompound(val distinctOperands: Set[VTerm]) /** @param body 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 fa6aa79..dc77cbc 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 @@ -846,7 +846,7 @@ def checkHandler ExpectU1Effect(qn), ) ctx.checkSolved( - checkEffSubsumption( + checkEffectSubsumption( bodyTy.asInstanceOf[F].effects, EffectsRetainSimpleLinear(implOutputEffects), ), 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 f949703..8f58a8b 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 @@ -301,7 +301,7 @@ class TypingContext case UmcNothing => Set.empty case UmcCSubtype(lowerBounds) => lowerBounds.map(checkIsSubtype(_, value)).flatten case UmcVSubtype(lowerBounds) => lowerBounds.map(checkIsSubtype(_, Collapse(value))).flatten - case UmcEffSubsumption(lowerBound) => checkEffSubsumption(lowerBound, Collapse(value)) + case UmcEffSubsumption(lowerBound) => checkEffectSubsumption(lowerBound, Collapse(value)) case UmcLevelSubsumption(lowerBound) => checkLevelSubsumption(lowerBound, Collapse(value)) case UmcUsageSubsumption(lowerBounds, upperBound) => lowerBounds.flatMap(lb => checkUsageSubsumption(Collapse(value), lb)) ++ @@ -567,7 +567,7 @@ class TypingContext case Constraint.CSubType(context, sub, sup) => checkIsSubtype(sub, sup)(using context) case Constraint.EffSubsumption(context, sub, sup) => - checkEffSubsumption(sub, sup)(using context) + checkEffectSubsumption(sub, sup)(using context) case Constraint.LevelSubsumption(context, sub, sup) => checkLevelSubsumption(sub, sup)(using context) case Constraint.UsageSubsumption(context, sub, sup) => 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 2b298a8..831f0b4 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 @@ -94,6 +94,8 @@ def collectUsages case LevelType(_) => Usages.zero case Level(_, maxOperands) => maxOperands.keys.map(collectUsages(_, Some(LevelType()))).fold(Usages.zero)(_ + _) + case EffectInstanceType(eff, _) => collectEffUsages(eff) + case EffectInstance(eff, _, _) => collectEffUsages(eff) case Auto() => throw IllegalStateException("All auto should have been replaced by meta variables.")