Local work: the leaf reads `leafAt`; branches apply the caller's arithmetic.
437def nativeCombineLocal =
438 (lambda unrestricted placement : (family NativeCombinePlacement) .
439 (lambda unrestricted leafAt : Nat .
440 (lambda unrestricted apply : (pi unrestricted out : Nat . (pi unrestricted left : Nat . (pi unrestricted right : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) .
441 (lambda unrestricted operation : (family OrderedCombineOperation (family RegionTransferIdentity)) .
442 (eliminate
443 OrderedCombineOperation
444 (lambda unrestricted current : (family OrderedCombineOperation (family RegionTransferIdentity)) .
445 (pi unrestricted tail : (family NativePhysicalCommands) .
446 (family NativePhysicalCommands)))
447 operation
448 (branch
449 CombineReadLeaf
450 destination
451 .
452 (nativeCombineCopy placement leafAt (nativeCombineAddress placement destination)))
453 (branch
454 CombineCopy
455 source
456 destination
457 .
458 (nativeCombineCopy
459 placement
460 (nativeCombineAddress placement source)
461 (nativeCombineAddress placement destination)))
462 (branch
463 CombineApply
464 left
465 right
466 destination
467 .
468 (apply
469 (nativeCombineAddress placement destination)
470 (nativeCombineAddress placement left)
471 (nativeCombineAddress placement right)))
472 (branch
473 CombinePrepare
474 source
475 identity
476 .
477 (nativeCombineCopy
478 placement
479 (nativeCombineAddress placement source)
480 (framePayloadAt (nativeCombineFrame placement identity))))
481 (branch
482 CombineConsume
483 identity
484 destination
485 .
486 (lambda unrestricted tail : (family NativePhysicalCommands) .
487 (let unrestricted frame =
488 (nativeCombineFrame placement identity)
489 in
490 (nativeFrameConsume
491 frame
492 (nativeCombineCopy
493 placement
494 (framePayloadAt frame)
495 (nativeCombineAddress placement destination)
496 (nativeFrameAdvance
497 frame
498 (constructor NativeFrameTerminal NativeFrameConsumeComplete)
499 0
500 tail)))))))))))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.