Source/Packages

Compiler.Planning.VA

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

590 lines101 declarations22.4 KiBSHA-256 1df69a11644a

def · lines 422–460

vaPrepareReservation

Full file
422def vaPrepareReservation =
423  (lambda unrestricted eventIndex : Nat .
424    (lambda unrestricted size : ByteCount .
425      (lambda unrestricted allocator : (family VAAllocator) .
426        (eliminate
427          VAAllocator
428          (lambda unrestricted current : (family VAAllocator) . (family VAPrepareResult))
429          allocator
430          (branch
431            VAAllocatorValue
432            inputNext
433            .
434            (eliminate
435              VAResult
436              (lambda unrestricted result : (family VAResult) . (family VAPrepareResult))
437              (vaTake size allocator)
438              (branch
439                VASucceeded
440                allocation
441                .
442                (constructor
443                  VAPrepareResult
444                  VAPrepared
445                  (constructor
446                    VAPendingReservation
447                    VAPendingReservationValue
448                    eventIndex
449                    allocator
450                    allocation)
451                  (vaTelemetrySucceededFor eventIndex inputNext size allocation)))
452              (branch
453                VAFailed
454                error
455                .
456                (constructor
457                  VAPrepareResult
458                  VAPrepareFailed
459                  error
460                  (vaTelemetryFailed eventIndex inputNext size error)))))))))

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.