val depth (#p: Type0) (x: tree' p) : nat
val depth (#p: Type0) (x: tree' p) : nat
let rec depth (#p:Type0) (x:tree' p) : nat =
  match x with
  | Leaf _ -> 0
  | Node _ lxs -> 1 + children_depth lxs
and children_depth (#p:Type0) (lxs:children' p) : nat  =
  match lxs with
  | (_,x) :: lxs -> max (depth x) (children_depth lxs)
  | [] -> 0
module MiTLS.Pkg.Tree
open MiTLS

open MiTLS.Mem
open MiTLS.Pkg
open MiTLS.Idx

/// We use subtrees to specify KDF usages. We hope we can erase
/// them when modelling is off!
///
/// This module is generic, and could be made parametric in its index
/// package. The TLS-specific details are filled-in in KeySchedule.

type t = pkg ii

noeq noextract
type tree' (par_ideal:Type0) =
  | Leaf: package:t{Pkg?.ideal package ==> par_ideal} -> tree' par_ideal
  | Node: node:t{Pkg?.ideal node ==> par_ideal} -> children: children' (Pkg?.ideal node) -> tree' par_ideal
and children' (par_ideal:Type0) = list (label * tree' par_ideal)

// would prefer to use Map.t, but positivity check fails

inline_for_extraction
let max x y = if x <= y then y else x

// induction on n-ary trees requires explicit termination
/
prims.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Idx.fst.checked FStar.Pervasives.fsti.checked
MiTLS.Pkg.Tree.fst
x: MiTLS.Pkg.Tree.tree' p -> Prims.nat
MiTLS.Pkg.Tree.tree' MiTLS.Pkg.Tree.t Prims.l_imp MiTLS.Pkg.__proj__Pkg__item__ideal MiTLS.Idx.ii Prims.list FStar.Pervasives.Native.tuple2 MiTLS.Idx.label Prims.op_Addition MiTLS.Pkg.Tree.children_depth Prims.nat
let rec depth (#p: Type0) (x: tree' p) : nat =
  
match x with
| Leaf _ -> 0
| Node _ lxs -> 1 + children_depth lxs