497def nativePhysicalImageCommandRecordForFormat =
498 (lambda unrestricted format : (family NativePhysicalImageFormat) .
499 (lambda unrestricted tag : Byte .
500 (lambda unrestricted binding : (family NativePhysicalResultBinding) .
501 (lambda unrestricted operands : Bytes .
502 (lambda unrestricted payload : Bytes .
503 (lambda unrestricted auxiliary : Bytes .
504 (lambda unrestricted errorIdentity : Bytes .
505 (nat-eliminate
506 (lambda unrestricted current : Nat . (family NativePhysicalEncodedCommandResult))
507 (constructor
508 NativePhysicalEncodedCommandResult
509 NativePhysicalCommandEncodingFailed
510 (constructor
511 NativePhysicalImageErrorCode
512 NativePhysicalImageCommandErrorIdentityEmpty))
513 (lambda unrestricted errorPredecessor : Nat .
514 (lambda unrestricted ignoredError : (family NativePhysicalEncodedCommandResult) .
515 (eliminate
516 NativeTelemetryCounterResult
517 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
518 (family NativePhysicalEncodedCommandResult))
519 (nativeTelemetryCounterFromNatural (bytes-length payload))
520 (branch
521 NativeTelemetryCounterSucceeded
522 payloadExtent
523 .
524 (eliminate
525 NativeTelemetryCounterResult
526 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
527 (family NativePhysicalEncodedCommandResult))
528 (nativeTelemetryCounterFromNatural (bytes-length auxiliary))
529 (branch
530 NativeTelemetryCounterSucceeded
531 auxiliaryExtent
532 .
533 (eliminate
534 NativeTelemetryCounterResult
535 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
536 (family NativePhysicalEncodedCommandResult))
537 (nativeTelemetryCounterFromNatural (bytes-length errorIdentity))
538 (branch
539 NativeTelemetryCounterSucceeded
540 errorExtent
541 .
542 (eliminate
543 NativeTelemetryCounterResult
544 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
545 (family NativePhysicalEncodedCommandResult))
546 (nativeTelemetryCounterFromNatural
547 (nativePhysicalImageRecordExtentFor format
548 (naturalAdd
549 (naturalSaturatingSubtract nativePhysicalImageCommandFixedBytes
550 (nativePhysicalImageOmittedOperandBytes format operands))
551 (naturalAdd (bytes-length payload)
552 (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity))))))
553 (branch
554 NativeTelemetryCounterSucceeded
555 recordExtent
556 .
557 (eliminate
558 NativePhysicalImageResultDescriptor
559 (lambda unrestricted current : (family NativePhysicalImageResultDescriptor) .
560 (family NativePhysicalEncodedCommandResult))
561 (nativePhysicalImageResultDescriptor binding)
562 (branch
563 NativePhysicalImageResultDescriptorValue
564 resultKind
565 resultSlot
566 .
567 (constructor
568 NativePhysicalEncodedCommandResult
569 NativePhysicalCommandEncoded
570 (constructor
571 NativePhysicalEncodedCommand
572 NativePhysicalEncodedCommandValue
573 (bytes-append
574 (nativePhysicalImageWord64Bytes
575 (nativePhysicalImageWord64 tag))
576 (bytes-append
577 (nativePhysicalImageWord64Bytes recordExtent)
578 (bytes-append
579 (nativePhysicalImageWord64Bytes resultKind)
580 (bytes-append
581 (nativePhysicalImageWord64Bytes resultSlot)
582 (bytes-append
583 (nativePhysicalImageWord64Bytes payloadExtent)
584 (bytes-append
585 (nativePhysicalImageWord64Bytes auxiliaryExtent)
586 (bytes-append
587 (nativePhysicalImageWord64Bytes errorExtent)
588 (bytes-append
589 (nativePhysicalImageWord64Bytes
590 (nativePhysicalImageWord64
591 (nat-to-byte (nativePhysicalImageOmittedOperandBytes format operands))))
592 (bytes-append
593 (nativePhysicalImageStoredOperands format operands)
594 (bytes-append
595 payload
596 (bytes-append auxiliary (bytes-append errorIdentity
597 (nativePhysicalImageZeroPad
598 (nativePhysicalImageRecordPaddingFor format
599 (naturalAdd
600 (naturalSaturatingSubtract nativePhysicalImageCommandFixedBytes
601 (nativePhysicalImageOmittedOperandBytes format operands))
602 (naturalAdd (bytes-length payload)
603 (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity))))))))))))))))))
604 (bytes-length payload)
605 (bytes-length auxiliary)
606 (bytes-length errorIdentity))))))
607 (branch
608 NativeTelemetryCounterFailed
609 counterError
610 naturalValue
611 .
612 (constructor
613 NativePhysicalEncodedCommandResult
614 NativePhysicalCommandEncodingFailed
615 (constructor
616 NativePhysicalImageErrorCode
617 NativePhysicalImageExtentOverflow)))))
618 (branch
619 NativeTelemetryCounterFailed
620 counterError
621 naturalValue
622 .
623 (constructor
624 NativePhysicalEncodedCommandResult
625 NativePhysicalCommandEncodingFailed
626 (constructor
627 NativePhysicalImageErrorCode
628 NativePhysicalImageExtentOverflow)))))
629 (branch
630 NativeTelemetryCounterFailed
631 counterError
632 naturalValue
633 .
634 (constructor
635 NativePhysicalEncodedCommandResult
636 NativePhysicalCommandEncodingFailed
637 (constructor
638 NativePhysicalImageErrorCode
639 NativePhysicalImageExtentOverflow)))))
640 (branch
641 NativeTelemetryCounterFailed
642 counterError
643 naturalValue
644 .
645 (constructor
646 NativePhysicalEncodedCommandResult
647 NativePhysicalCommandEncodingFailed
648 (constructor
649 NativePhysicalImageErrorCode
650 NativePhysicalImageExtentOverflow))))))
651 (bytes-length errorIdentity)))))))))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.