Plan, check and project the reduce-and-replicate protocol for `rounds`
repetitions under an admitted numerical contract; the caller emits it with
nativeProtocolCommands and the callbacks above.
788def planNativeCombineRounds =
789 (lambda unrestricted placement : (family NativeCombinePlacement) .
790 (lambda unrestricted required : (family NumericalContract) .
791 (lambda unrestricted participants : Nat .
792 (lambda unrestricted members : (family CombineCoverage) .
793 (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
794 (lambda unrestricted rounds : Nat .
795 (stdResultBind
796 (family OrderedCombineFailure)
797 (family
798 GlobalProtocol
799 (family OrderedCombineOperation (family RegionTransferIdentity))
800 (family RegionTransferIdentity)
801 (family ProtocolNoDecision))
802 (family
803 ParticipantProtocol
804 (family OrderedCombineOperation (family RegionTransferIdentity))
805 (family RegionTransferIdentity)
806 (family ProtocolNoDecision))
807 (planNumericalCombineAndReplicate
808 (family RegionTransferIdentity)
809 required
810 required
811 participants
812 members
813 baseAnchor
814 nativeCombineBinding
815 (nativeCombineLocalAdmitted placement)
816 (nativeCombineTransferAdmitted placement)
817 (nativeCombineTree (nativeCombinePlacementContext placement))
818 nativeCombineEnd)
819 (lambda unrestricted global : (family GlobalProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
820 (eliminate
821 StdResult
822 (lambda unrestricted result : (family StdResult (family ProtocolFailure) (family ParticipantProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision))) .
823 (family
824 StdResult
825 (family OrderedCombineFailure)
826 (family
827 ParticipantProtocol
828 (family OrderedCombineOperation (family RegionTransferIdentity))
829 (family RegionTransferIdentity)
830 (family ProtocolNoDecision))))
831 (planParticipantProtocol
832 (family OrderedCombineOperation (family RegionTransferIdentity))
833 (family RegionTransferIdentity)
834 (family ProtocolNoDecision)
835 participants
836 (nativeCombineRole (nativeCombinePlacementContext placement))
837 (nativeCombineLocalAdmitted placement)
838 (nativeCombineTransferAdmitted placement)
839 (protocolNoDecision (family RegionTransferIdentity))
840 (protocolRepeat
841 (family OrderedCombineOperation (family RegionTransferIdentity))
842 (family RegionTransferIdentity)
843 (family ProtocolNoDecision)
844 rounds
845 global
846 nativeCombineEnd))
847 (branch
848 StdFailure
849 failure
850 .
851 (constructor
852 StdResult
853 StdFailure
854 (family OrderedCombineFailure)
855 (family
856 ParticipantProtocol
857 (family OrderedCombineOperation (family RegionTransferIdentity))
858 (family RegionTransferIdentity)
859 (family ProtocolNoDecision))
860 (constructor OrderedCombineFailure CombineProtocolRefused failure)))
861 (branch
862 StdSuccess
863 projected
864 .
865 (constructor
866 StdResult
867 StdSuccess
868 (family OrderedCombineFailure)
869 (family
870 ParticipantProtocol
871 (family OrderedCombineOperation (family RegionTransferIdentity))
872 (family RegionTransferIdentity)
873 (family ProtocolNoDecision))
874 projected)))))))))))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.