[EscapeAnalysis] Check effIns escape

Also fix a bug in usage checking during constructor split.
tgeng · Nov 10, 2024 · e401c24 · e401c24
1 parent 60f4dc8
commit e401c24
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 25 deletions.
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
@@ -55,8 +55,7 @@ def elaborate
 enum DeclarationPart:
   case HEAD, BODY
 
-import com.github.tgeng.archon.core.ir.DeclarationPart.*
-import com.github.tgeng.archon.core.ir.unifyAll
+import com.github.tgeng.archon.core.ir.DeclarationPart.* import com.github.tgeng.archon.core.ir.unifyAll
 
 @throws(classOf[IrError])
 def sortPreDeclarations
@@ -655,7 +654,16 @@ private def elaborateDefBody
                       given Signature = _Σ
                       // in context _Γ1
                       val tArgs = binding.ty.asInstanceOf[DataType].args
-                      val Δ = constructor.paramTys.substLowers(tArgs*)
+                      val xUsage = binding.usage
+                      val Δ: Telescope = constructor.paramTys
+                        .substLowers(tArgs*)
+                        .zipWithIndex
+                        .map((binding, i) =>
+                          // Here we need to multiply the component usage by the usage of X at the split
+                          binding.copy(usage = UsageProd(xUsage.weaken(i, 0), binding.usage))(
+                            binding.name,
+                          ),
+                        )
 
                       // in context _Γ1 ⊎ Δ
                       val cTArgs = constructor.tArgs.map(

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
@@ -1,6 +1,5 @@
 package com.github.tgeng.archon.core.ir
 
-import com.github.tgeng.archon.common.Nat
 import com.github.tgeng.archon.core.common.*
 import com.github.tgeng.archon.core.ir.*
 
@@ -93,5 +92,7 @@ enum IrError(val Γ: Context, e: Throwable | Null = null) extends Exception(e):
   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(Γ)
+  case ExpectEffectInstanceTypeSubsumption(sub: VTerm, sup: VTerm)(using Γ: Context)
+    extends IrError(Γ)
+  case EscapedEffectInstanceCausesNdet(handler: CTerm.Handler)(using Γ: Context) extends IrError(Γ)
   override def getMessage: String = verbosePPrinter.apply(this).plainText
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
@@ -411,7 +411,6 @@ def inferType
             case (e @ ETerm(uncheckedArg)) :: uncheckedRest =>
               // Note that this `cty` is created by `inferType` so it's already checked.
               cty match
-                // TODO[P0]: honor escape status here and use it for escape analysis
                 case FunctionType(binding, bodyTy, effects, _) =>
                   val arg = checkType(uncheckedArg, binding.ty)
                   val (rest, cty) =
@@ -669,31 +668,13 @@ def checkHandler
   (using Σ: Signature)
   (using ctx: TypingContext)
   : (CTerm, CTerm) =
-  // TODO[P0]: do escape analysis of the effect instance variable and if it escapes, otherEffects
-  //  should contain ndet.
   val eff = checkEff(h.eff)
   val operations = Σ.getOperations(eff._1).map(op => (eff._1 / op.name, eff._2, op)).toSet
   val expectedOperationNames = operations.map(_._1)
   val actualOperationNames = h.handlers.keySet
   if expectedOperationNames != actualOperationNames then
     throw HandlerOperationsMismatch(h, expectedOperationNames, actualOperationNames)
   val otherEffects = checkType(h.otherEffects, EffectsType()).normalized
-  val handlerEffects = checkType(h.handlerEffects, EffectsType()).normalized
-  val outputEffects = EffectsUnion(otherEffects, handlerEffects).normalized
-  val outputUsage = checkType(h.outputUsage, UsageType()).normalized
-  val outputTy = checkIsType(h.outputTy)
-  outputType match
-    case None =>
-    case Some(outputType) =>
-      ctx.checkSolved(
-        checkIsSubtype(F(outputTy, outputEffects, outputUsage), outputType),
-        NotCSubtype(F(outputTy, outputEffects, outputUsage), outputType),
-      )
-  val parameterTy = checkIsType(h.parameterBinding.ty)
-  // parameter binding usage dictates how much resources the handler needs when consuming the parameter
-  val parameterBindingUsage = checkType(h.parameterBinding.usage, UsageType())
-  val parameterBinding = Binding(parameterTy, parameterBindingUsage)(h.parameterBinding.name)
-  val parameter = checkType(h.parameter, parameterTy)
   val inputTy = checkIsType(h.inputBinding.ty)
   // Unlike parameter, input is a computation and hence only executed linearly. The input binding usage is simply a
   // requirement on the final return type of the input computation.
@@ -717,7 +698,34 @@ def checkHandler
       inputEffects,
       inputBindingUsage.weakened, /* for effect instance */
     ),
-  )
+  )(using inputΓ)
+  val effInsDbNumber = Γ.size
+  val effInsEscapeStatus =
+    computeEscapeStatuses(h.input, Set(effInsDbNumber))(using inputΓ)(effInsDbNumber)
+  effInsEscapeStatus match
+    // If effect instance does not escape, there is no need to check anything.
+    case EscapeStatus.EsLocal =>
+    case _ =>
+      ctx.checkSolved(
+        checkEffectSubsumption(EffectsLiteral(Set(ndet)), otherEffects),
+        EscapedEffectInstanceCausesNdet(h),
+      )
+  val handlerEffects = checkType(h.handlerEffects, EffectsType()).normalized
+  val outputEffects = EffectsUnion(otherEffects, handlerEffects).normalized
+  val outputUsage = checkType(h.outputUsage, UsageType()).normalized
+  val outputTy = checkIsType(h.outputTy)
+  outputType match
+    case None =>
+    case Some(outputType) =>
+      ctx.checkSolved(
+        checkIsSubtype(F(outputTy, outputEffects, outputUsage), outputType),
+        NotCSubtype(F(outputTy, outputEffects, outputUsage), outputType),
+      )
+  val parameterTy = checkIsType(h.parameterBinding.ty)
+  // parameter binding usage dictates how much resources the handler needs when consuming the parameter
+  val parameterBindingUsage = checkType(h.parameterBinding.usage, UsageType())
+  val parameterBinding = Binding(parameterTy, parameterBindingUsage)(h.parameterBinding.name)
+  val parameter = checkType(h.parameter, parameterTy)
   val inputEffectsContinuationUsage = getEffectsContinuationUsage(inputEffects)
   val parameterDisposer = h.parameterDisposer match
     case Some(parameterDisposer) =>