Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7698–7717

coreWorkChargeBytes

Full file
Natural folds and beta substitution share the meter. Primitive byte payload costs and generic family induction still need separate accounting.
7698def coreWorkChargeBytes =
7699  (lambda unrestricted payload : Bytes .
7700    (lambda unrestricted budget : (family NormalizationBudget) .
7701      (lambda unrestricted continue : (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult)) .
7702        (eliminate
7703          NormalizationChargeResult
7704          (lambda unrestricted result : (family NormalizationChargeResult) .
7705            (family CoreWorkResult))
7706          (chargeNormalizationBytes payload budget)
7707          (branch NormalizationCharged remaining . (continue remaining))
7708          (branch
7709            NormalizationChargeExhausted
7710            remaining
7711            amount
7712            .
7713            (constructor CoreWorkResult CoreWorkExhausted remaining))
7714          (branch
7715            NormalizationChargeInvalid
7716            .
7717            (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.