AlphaGitHub
Source/Packages

Compiler.Planning.Resources

packages/compiler/planning/src/Compiler/Planning/Resources.alpha

636 lines34 declarations25.9 KiBSHA-256 773ccd6b9504
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 610–636

resourceLeaseFromLifetime

Full file
Lifetimes use inclusive last-use events. Leases are half-open: retain bytes through lastUse, including any extension made by the transfer planner. The lifetime owner is U32, so adding one here fits the resource event word.
610def resourceLeaseFromLifetime =
611  (lambda unrestricted identity : Bytes .
612    (lambda unrestricted endpoint : Nat .
613      (lambda unrestricted domain : Nat .
614        (lambda unrestricted lifetime : (family Lifetime) .
615          (eliminate
616            Lifetime
617            (lambda unrestricted current : (family Lifetime) . (family ResourceLease))
618            lifetime
619            (branch
620              LifetimeValue
621              tensor
622              first
623              last
624              bytes
625              alignment
626              .
627              (constructor
628                ResourceLease
629                ResourceLeaseOf
630                identity
631                endpoint
632                domain
633                (constructor ResourceUnit ResourceMemoryBytes)
634                (modelWord64Natural (stdByteCountValue bytes))
635                (modelWord32ToNatural first)
636                (naturalAdd (modelWord32ToNatural last) 1))))))))

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.