Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 5242–5261

coreWorkCharge

Full file
5242def coreWorkCharge =
5243  (lambda unrestricted amount : (family ModelWord32) .
5244    (lambda unrestricted budget : (family NormalizationBudget) .
5245      (lambda unrestricted continuation : (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult)) .
5246        (eliminate
5247          NormalizationChargeResult
5248          (lambda unrestricted current : (family NormalizationChargeResult) .
5249            (family CoreWorkResult))
5250          (Compiler.NormalizationBudget/chargeNormalizationBudget amount budget)
5251          (branch NormalizationCharged remaining . (continuation remaining))
5252          (branch
5253            NormalizationChargeExhausted
5254            unchanged
5255            rejected
5256            .
5257            (constructor CoreWorkResult CoreWorkExhausted unchanged))
5258          (branch
5259            NormalizationChargeInvalid
5260            .
5261            (constructor CoreWorkResult CoreWorkExhausted budget))))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.