A participant's edges in a bounded-fan-out hierarchy
(Representation.ParticipantTree). Every non-root role has exactly one
parent, so the edge (parent(c), c) is named by c and its address is
`address c`. A role's edges are its parent (a lower role: this role
connects) followed by its children in role order (higher roles: this role
listens), which is the ascending order Runtime.NativePeerEndpoint requires.
A participant holds at most fanout + 1 edges and never the membership of
the whole hierarchy: its control state is bounded by the fan-out.
18def nativePeerTreeEdges =
19 (lambda unrestricted fanout : Nat .
20 (lambda unrestricted count : Nat .
21 (lambda unrestricted role : Nat .
22 (lambda unrestricted address : (pi unrestricted child : Nat . Bytes) .
23 (let unrestricted node =
24 (participantTreeNode fanout count role)
25 in
26 (let unrestricted children =
27 (stdListMap
28 (family ParticipantTreeNode)
29 (family NativePeerEdge)
30 (lambda unrestricted child : (family ParticipantTreeNode) .
31 (constructor
32 NativePeerEdge
33 NativePeerEdgeOf
34 (participantTreeRoleOf child)
35 (address (participantTreeRoleOf child))))
36 (participantTreeChildren fanout node))
37 in
38 (nat-eliminate
39 (lambda unrestricted root : Nat . (family StdList (family NativePeerEdge)))
40 (constructor
41 StdList
42 StdListCons
43 (family NativePeerEdge)
44 (constructor
45 NativePeerEdge
46 NativePeerEdgeOf
47 (participantTreeParentOf node)
48 (address role))
49 children)
50 (lambda unrestricted predecessor : Nat .
51 (lambda unrestricted ignored : (family StdList (family NativePeerEdge)) .
52 children))
53 (participantTreeIsRoot node))))))))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.