AlphaGitHub
Source/Packages

Compiler.Planning.Liveness

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

1,458 lines160 declarations54.8 KiBSHA-256 5734e8062a86
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 276–288

retainLifetimeThrough

Full file
Remote reads retain the existing allocation through transport completion. Extending an earlier bound is monotone: a transfer cannot accidentally shorten an activation's already-established local lifetime.
276def retainLifetimeThrough =
277  (lambda unrestricted remoteLastRead : (family ModelWord32) .
278    (lambda unrestricted lifetime : (family Lifetime) .
279      (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . (family Lifetime))
280        lifetime
281        (branch LifetimeValue tensor firstUse lastUse bytes alignment .
282          (nat-eliminate
283            (lambda unrestricted flag : Nat . (family Lifetime))
284            lifetime
285            (lambda unrestricted previous : Nat .
286              (lambda unrestricted ignored : (family Lifetime) .
287                (constructor Lifetime LifetimeValue tensor firstUse remoteLastRead bytes alignment)))
288            (naturalLess (modelWord32ToNatural lastUse) (modelWord32ToNatural remoteLastRead)))))))

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.