module ParticipantTreeLaws

import Representation.ParticipantTree
import Std.Foundation
import Std.List
import Std.Natural

-- Hand-computed hierarchies (checked against an independent model of the
-- same splitting rule). Each law is decided by normalization.
-- Seven roles, fan-out two: 0 -> {1, 4}; 1 -> {2, 3}; 4 -> {5, 6}.
def binaryRootChildren :
  (equal
    (family StdList Nat)
    (stdListMap
      (family ParticipantTreeNode)
      Nat
      participantTreeRoleOf
      (participantTreeChildren 2 (participantTreeNode 2 7 0)))
    (constructor
      StdList
      StdListCons
      Nat
      1
      (constructor StdList StdListCons Nat 4 (constructor StdList StdListEmpty Nat)))) =
  (refl
    (family StdList Nat)
    (constructor
      StdList
      StdListCons
      Nat
      1
      (constructor StdList StdListCons Nat 4 (constructor StdList StdListEmpty Nat))))

def binaryNodeThreeParent : (equal Nat (participantTreeParentOf (participantTreeNode 2 7 3)) 1) =
  (refl Nat 1)

def binaryNodeThreeDepth : (equal Nat (participantTreeDepthOf (participantTreeNode 2 7 3)) 2) =
  (refl Nat 2)

def binaryNodeOneSize : (equal Nat (participantTreeSizeOf (participantTreeNode 2 7 1)) 3) =
  (refl Nat 3)

def binaryHeight : (equal Nat (participantTreeHeight 2 7) 2) =
  (refl Nat 2)

-- Ten roles, fan-out four: the nine descendants split 3, 2, 2, 2.
def quaternarySecondChildSize : (equal Nat (participantTreeChildSize 4 10 1) 2) =
  (refl Nat 2)

def quaternaryFirstChildSize : (equal Nat (participantTreeChildSize 4 10 0) 3) =
  (refl Nat 3)

def quaternaryNodeFiveParent :
  (equal Nat (participantTreeParentOf (participantTreeNode 4 10 5)) 4) =
  (refl Nat 4)

def quaternaryNodeNineParent :
  (equal Nat (participantTreeParentOf (participantTreeNode 4 10 9)) 8) =
  (refl Nat 8)

-- Children tile the node's range: the start after the last child is the end.
def quaternaryTiling : (equal Nat (participantTreeChildStart 4 0 10 4) 10) =
  (refl Nat 10)

-- Fan-out one is a chain.
def chainParent : (equal Nat (participantTreeParentOf (participantTreeNode 1 4 3)) 2) =
  (refl Nat 2)

def chainHeight : (equal Nat (participantTreeHeight 1 4) 3) =
  (refl Nat 3)

-- The PRD's fleet design point: 200,000 roles with fan-out 64 need three
-- edge levels (64^2 < 200,000 <= 64^3). The root's 199,999 descendants split
-- into 63 subtrees of 3,125 and one of 3,124; no padding roles exist.
def fleetHeight : (equal Nat (participantTreeHeight 64 200000) 3) =
  (refl Nat 3)

def fleetRootChildren : (equal Nat (participantTreeChildCount 64 200000) 64) =
  (refl Nat 64)

def fleetFirstSubtree : (equal Nat (participantTreeChildSize 64 200000 0) 3125) =
  (refl Nat 3125)

def fleetLastSubtree : (equal Nat (participantTreeChildSize 64 200000 63) 3124) =
  (refl Nat 3124)

def fleetLastRoleParent :
  (equal Nat (participantTreeParentOf (participantTreeNode 64 200000 199999)) 199952) =
  (refl Nat 199952)

def fleetLastRoleDepth :
  (equal Nat (participantTreeDepthOf (participantTreeNode 64 200000 199999)) 3) =
  (refl Nat 3)

def fleetMiddleRoleParent :
  (equal Nat (participantTreeParentOf (participantTreeNode 64 200000 100000)) 99953) =
  (refl Nat 99953)

def roleOutsideRefused : (equal Nat (participantTreeAdmitted 64 200000 200000) 0) =
  (refl Nat 0)

-- Ancestors, root first: role 3 of the seven-role binary tree descends 0, 1.
def binaryAncestors :
  (equal
    (family StdList Nat)
    (stdListMap
      (family ParticipantTreeNode)
      Nat
      participantTreeRoleOf
      (participantTreeAncestors 2 7 3))
    (constructor
      StdList
      StdListCons
      Nat
      0
      (constructor StdList StdListCons Nat 1 (constructor StdList StdListEmpty Nat)))) =
  (refl
    (family StdList Nat)
    (constructor
      StdList
      StdListCons
      Nat
      0
      (constructor StdList StdListCons Nat 1 (constructor StdList StdListEmpty Nat))))

def rootHasNoAncestors :
  (equal Nat (stdListLength (family ParticipantTreeNode) (participantTreeAncestors 2 7 0)) 0) =
  (refl Nat 0)

def fleetAncestorCount :
  (equal
    Nat
    (stdListLength (family ParticipantTreeNode) (participantTreeAncestors 64 200000 199999))
    3) =
  (refl Nat 3)

def main : Nat =
  0