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 476–498

placementRangeValid

Full file
476def placementRangeValid =
477  (lambda unrestricted arenaBytes : ByteCount .
478    (lambda unrestricted placement : (family Placement) .
479      (eliminate
480        Placement
481        (lambda unrestricted current : (family Placement) . Nat)
482        placement
483        (branch
484          PlacementValue
485          lifetime
486          offset
487          capacity
488          .
489          (eliminate
490            ModelWord64CheckedResult
491            (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat)
492            (modelWord64AddChecked (stdByteCountValue offset) (stdByteCountValue capacity))
493            (branch
494              ModelWord64CheckedSucceeded
495              end
496              .
497              (word64LessThanOrEqual end (stdByteCountValue arenaBytes)))
498            (branch ModelWord64CheckedFailed error . zero))))))

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.