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 310–336

lifetimeError

Full file
310def lifetimeError =
311  (lambda unrestricted lifetime : (family Lifetime) .
312    (eliminate
313      Lifetime
314      (lambda unrestricted current : (family Lifetime) . (family LivenessErrorCode))
315      lifetime
316      (branch
317        LifetimeValue
318        tensor
319        firstUse
320        lastUse
321        bytes
322        alignment
323        .
324        (nat-eliminate
325          (lambda unrestricted intervalInvalid : Nat . (family LivenessErrorCode))
326          (nat-eliminate
327            (lambda unrestricted bytesAreZero : Nat . (family LivenessErrorCode))
328            (constructor LivenessErrorCode LifetimeAlignmentInvalid)
329            (lambda unrestricted predecessor : Nat .
330              (lambda unrestricted induction : (family LivenessErrorCode) .
331                (constructor LivenessErrorCode LifetimeBytesZero)))
332            (modelWord64IsZero (stdByteCountValue bytes)))
333          (lambda unrestricted predecessor : Nat .
334            (lambda unrestricted induction : (family LivenessErrorCode) .
335              (constructor LivenessErrorCode LifetimeIntervalInvalid)))
336          (nat-less-than (modelWord32ToNatural lastUse) (modelWord32ToNatural firstUse))))))

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.