module Runtime.NativePeerTree

import Representation.ParticipantTree
import Runtime.NativePeerEndpoint
import Data.Bytes
import Std.Foundation
import Std.List
import Std.Natural

-- 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.
def nativePeerTreeEdges =
  (lambda unrestricted fanout : Nat .
    (lambda unrestricted count : Nat .
      (lambda unrestricted role : Nat .
        (lambda unrestricted address : (pi unrestricted child : Nat . Bytes) .
          (let unrestricted node =
            (participantTreeNode fanout count role)
            in
            (let unrestricted children =
              (stdListMap
                (family ParticipantTreeNode)
                (family NativePeerEdge)
                (lambda unrestricted child : (family ParticipantTreeNode) .
                  (constructor
                    NativePeerEdge
                    NativePeerEdgeOf
                    (participantTreeRoleOf child)
                    (address (participantTreeRoleOf child))))
                (participantTreeChildren fanout node))
              in
              (nat-eliminate
                (lambda unrestricted root : Nat . (family StdList (family NativePeerEdge)))
                (constructor
                  StdList
                  StdListCons
                  (family NativePeerEdge)
                  (constructor
                    NativePeerEdge
                    NativePeerEdgeOf
                    (participantTreeParentOf node)
                    (address role))
                  children)
                (lambda unrestricted predecessor : Nat .
                  (lambda unrestricted ignored : (family StdList (family NativePeerEdge)) .
                    children))
                (participantTreeIsRoot node))))))))

-- The connection slot to this role's parent (its first edge).
def nativePeerTreeParentConnection : Nat =
  (nativePeerEdgeConnectionSlot 0)

-- A tree is admitted for this role when the hierarchy admits it and its
-- edges are admitted endpoints (distinct ascending peers, IPv4 addresses).
def nativePeerTreeAdmitted =
  (lambda unrestricted fanout : Nat .
    (lambda unrestricted count : Nat .
      (lambda unrestricted role : Nat .
        (lambda unrestricted address : (pi unrestricted child : Nat . Bytes) .
          (naturalAnd
            (participantTreeAdmitted fanout count role)
            (nativePeerEdgesAdmitted role (nativePeerTreeEdges fanout count role address)))))))

-- The role's edges with addresses listed in the hierarchy's edge order
-- (parent first unless root, then children in role order): the form a
-- caller that compiles each role's own addresses supplies.
def nativePeerTreeEdgesListed =
  (lambda unrestricted fanout : Nat .
    (lambda unrestricted owners : Nat .
      (lambda unrestricted role : Nat .
        (lambda unrestricted addresses : (family StdList Bytes) .
          (stdListFold
            (family NativePeerEdge)
            (pi unrestricted index : Nat . (family StdList (family NativePeerEdge)))
            (lambda unrestricted edge : (family NativePeerEdge) .
              (lambda unrestricted next : (pi unrestricted index : Nat . (family StdList (family NativePeerEdge))) .
                (lambda unrestricted index : Nat .
                  (constructor
                    StdList
                    StdListCons
                    (family NativePeerEdge)
                    (constructor
                      NativePeerEdge
                      NativePeerEdgeOf
                      (nativePeerEdgePeerOf edge)
                      (stdListHeadOr Bytes b"" (stdListDrop Bytes index addresses)))
                    (next (succ index))))))
            (lambda unrestricted index : Nat .
              (constructor StdList StdListEmpty (family NativePeerEdge)))
            (nativePeerTreeEdges fanout owners role (lambda unrestricted child : Nat . b""))
            0)))))

def nativePeerTreeListedAdmitted =
  (lambda unrestricted fanout : Nat .
    (lambda unrestricted owners : Nat .
      (lambda unrestricted role : Nat .
        (lambda unrestricted addresses : (family StdList Bytes) .
          (naturalAnd
            (participantTreeAdmitted fanout owners role)
            (naturalAnd
              (naturalEqual
                (stdListLength Bytes addresses)
                (stdListLength
                  (family NativePeerEdge)
                  (nativePeerTreeEdges fanout owners role (lambda unrestricted child : Nat . b""))))
              (nativePeerEdgesAdmitted
                role
                (nativePeerTreeEdgesListed fanout owners role addresses))))))))