The ordered sum over a bounded-fan-out hierarchy
(Representation.ParticipantTree): a node's value is its own leaf followed
by each child's subtree value in role order, combined left-deep at the node:
S(p) = ((l_p + S(c1)) + S(c2)) + ...
Every transfer is between a node and one of its children, so reduction and
replication run over the hierarchy's edges and no participant combines
more than fanout + 1 values. With fan-out count - 1 it is the chain at 0.
719def nativeCombineHierarchy =
720 (lambda unrestricted fanout : Nat .
721 (lambda unrestricted count : Nat .
722 (let unrestricted subtree =
723 (nat-eliminate
724 (lambda unrestricted fuel : Nat .
725 (pi unrestricted node : (family ParticipantTreeNode) . (family OrderedCombineTree)))
726 (lambda unrestricted node : (family ParticipantTreeNode) .
727 (constructor OrderedCombineTree OrderedCombineLeaf (participantTreeRoleOf node)))
728 (lambda unrestricted fuel : Nat .
729 (lambda unrestricted below : (pi unrestricted node : (family ParticipantTreeNode) . (family OrderedCombineTree)) .
730 (lambda unrestricted node : (family ParticipantTreeNode) .
731 (let unrestricted role =
732 (participantTreeRoleOf node)
733 in
734 (stdListFold
735 (family ParticipantTreeNode)
736 (pi unrestricted acc : (family OrderedCombineTree) .
737 (family OrderedCombineTree))
738 (lambda unrestricted child : (family ParticipantTreeNode) .
739 (lambda unrestricted next : (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree)) .
740 (lambda unrestricted acc : (family OrderedCombineTree) .
741 (next
742 (constructor
743 OrderedCombineTree
744 OrderedCombineBranch
745 role
746 acc
747 (below child))))))
748 (lambda unrestricted acc : (family OrderedCombineTree) . acc)
749 (participantTreeChildren fanout node)
750 (constructor OrderedCombineTree OrderedCombineLeaf role))))))
751 (participantTreeFuel fanout count))
752 in
753 (subtree (participantTreeRoot count)))))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.