433def nativePhysicalImageCommandRecordForFormat =
434 (lambda unrestricted format : (family NativePhysicalImageFormat) .
435 (lambda unrestricted tag : Byte .
436 (lambda unrestricted binding : (family NativePhysicalResultBinding) .
437 (lambda unrestricted operands : Bytes .
438 (lambda unrestricted payload : Bytes .
439 (lambda unrestricted auxiliary : Bytes .
440 (lambda unrestricted errorIdentity : Bytes .
441 (nat-eliminate
442 (lambda unrestricted current : Nat . (family NativePhysicalEncodedCommandResult))
443 (constructor
444 NativePhysicalEncodedCommandResult
445 NativePhysicalCommandEncodingFailed
446 (constructor
447 NativePhysicalImageErrorCode
448 NativePhysicalImageCommandErrorIdentityEmpty))
449 (lambda unrestricted errorPredecessor : Nat .
450 (lambda unrestricted ignoredError : (family NativePhysicalEncodedCommandResult) .
451 (eliminate
452 NativeTelemetryCounterResult
453 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
454 (family NativePhysicalEncodedCommandResult))
455 (nativeTelemetryCounterFromNatural (bytes-length payload))
456 (branch
457 NativeTelemetryCounterSucceeded
458 payloadExtent
459 .
460 (eliminate
461 NativeTelemetryCounterResult
462 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
463 (family NativePhysicalEncodedCommandResult))
464 (nativeTelemetryCounterFromNatural (bytes-length auxiliary))
465 (branch
466 NativeTelemetryCounterSucceeded
467 auxiliaryExtent
468 .
469 (eliminate
470 NativeTelemetryCounterResult
471 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
472 (family NativePhysicalEncodedCommandResult))
473 (nativeTelemetryCounterFromNatural (bytes-length errorIdentity))
474 (branch
475 NativeTelemetryCounterSucceeded
476 errorExtent
477 .
478 (eliminate
479 NativeTelemetryCounterResult
480 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
481 (family NativePhysicalEncodedCommandResult))
482 (nativeTelemetryCounterFromNatural
483 (nativePhysicalImageRecordExtentFor format
484 (naturalAdd nativePhysicalImageCommandFixedBytes
485 (naturalAdd (bytes-length payload)
486 (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity))))))
487 (branch
488 NativeTelemetryCounterSucceeded
489 recordExtent
490 .
491 (eliminate
492 NativePhysicalImageResultDescriptor
493 (lambda unrestricted current : (family NativePhysicalImageResultDescriptor) .
494 (family NativePhysicalEncodedCommandResult))
495 (nativePhysicalImageResultDescriptor binding)
496 (branch
497 NativePhysicalImageResultDescriptorValue
498 resultKind
499 resultSlot
500 .
501 (constructor
502 NativePhysicalEncodedCommandResult
503 NativePhysicalCommandEncoded
504 (constructor
505 NativePhysicalEncodedCommand
506 NativePhysicalEncodedCommandValue
507 (bytes-append
508 (nativePhysicalImageWord64Bytes
509 (nativePhysicalImageWord64 tag))
510 (bytes-append
511 (nativePhysicalImageWord64Bytes recordExtent)
512 (bytes-append
513 (nativePhysicalImageWord64Bytes resultKind)
514 (bytes-append
515 (nativePhysicalImageWord64Bytes resultSlot)
516 (bytes-append
517 (nativePhysicalImageWord64Bytes payloadExtent)
518 (bytes-append
519 (nativePhysicalImageWord64Bytes auxiliaryExtent)
520 (bytes-append
521 (nativePhysicalImageWord64Bytes errorExtent)
522 (bytes-append
523 (nativePhysicalImageWord64Bytes
524 nativePhysicalImageZeroWord64)
525 (bytes-append
526 operands
527 (bytes-append
528 payload
529 (bytes-append auxiliary (bytes-append errorIdentity
530 (nativePhysicalImageZeroPad
531 (nativePhysicalImageRecordPaddingFor format
532 (naturalAdd nativePhysicalImageCommandFixedBytes
533 (naturalAdd (bytes-length payload)
534 (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity))))))))))))))))))
535 (bytes-length payload)
536 (bytes-length auxiliary)
537 (bytes-length errorIdentity))))))
538 (branch
539 NativeTelemetryCounterFailed
540 counterError
541 naturalValue
542 .
543 (constructor
544 NativePhysicalEncodedCommandResult
545 NativePhysicalCommandEncodingFailed
546 (constructor
547 NativePhysicalImageErrorCode
548 NativePhysicalImageExtentOverflow)))))
549 (branch
550 NativeTelemetryCounterFailed
551 counterError
552 naturalValue
553 .
554 (constructor
555 NativePhysicalEncodedCommandResult
556 NativePhysicalCommandEncodingFailed
557 (constructor
558 NativePhysicalImageErrorCode
559 NativePhysicalImageExtentOverflow)))))
560 (branch
561 NativeTelemetryCounterFailed
562 counterError
563 naturalValue
564 .
565 (constructor
566 NativePhysicalEncodedCommandResult
567 NativePhysicalCommandEncodingFailed
568 (constructor
569 NativePhysicalImageErrorCode
570 NativePhysicalImageExtentOverflow)))))
571 (branch
572 NativeTelemetryCounterFailed
573 counterError
574 naturalValue
575 .
576 (constructor
577 NativePhysicalEncodedCommandResult
578 NativePhysicalCommandEncodingFailed
579 (constructor
580 NativePhysicalImageErrorCode
581 NativePhysicalImageExtentOverflow))))))
582 (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.