Raw (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Gen

type key = Eqtype.Equality.sort

type 'elt tree =

| Leaf
| Node of 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t

val tree_rect : 
  'a2 ->
  ('a1 tree -> 'a2 -> key -> 'a1 -> 'a1 tree -> 'a2 -> Int.Z_as_Int.t -> 'a2) ->
  'a1 tree ->
  'a2

val tree_rec : 
  'a2 ->
  ('a1 tree -> 'a2 -> key -> 'a1 -> 'a1 tree -> 'a2 -> Int.Z_as_Int.t -> 'a2) ->
  'a1 tree ->
  'a2

val height : 'a1 tree -> Int.Z_as_Int.t

val cardinal : 'a1 tree -> Datatypes.nat

val empty : 'a1 tree

val is_empty : 'a1 tree -> bool

val mem : Eqtype.Equality.sort -> 'a1 tree -> bool

val find : Eqtype.Equality.sort -> 'a1 tree -> 'a1 option

val create : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree

val assert_false : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree

val bal : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree

val add : key -> 'a1 -> 'a1 tree -> 'a1 tree

val remove_min : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree * (key * 'a1)

val merge : 'a1 tree -> 'a1 tree -> 'a1 tree

val remove : Eqtype.Equality.sort -> 'a1 tree -> 'a1 tree

val join : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree

type 'elt triple = {

t_left : 'elt tree;
t_opt : 'elt option;
t_right : 'elt tree;

}

val t_left : 'a1 triple -> 'a1 tree

val t_opt : 'a1 triple -> 'a1 option

val t_right : 'a1 triple -> 'a1 tree

val split : Eqtype.Equality.sort -> 'a1 tree -> 'a1 triple

val concat : 'a1 tree -> 'a1 tree -> 'a1 tree

val elements_aux : (key * 'a1) list -> 'a1 tree -> (key * 'a1) list

val elements : 'a1 tree -> (key * 'a1) list

val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 tree -> 'a2 -> 'a2

type 'elt enumeration =

| End
| More of key * 'elt * 'elt tree * 'elt enumeration

val enumeration_rect : 
  'a2 ->
  (key -> 'a1 -> 'a1 tree -> 'a1 enumeration -> 'a2 -> 'a2) ->
  'a1 enumeration ->
  'a2

val enumeration_rec : 
  'a2 ->
  (key -> 'a1 -> 'a1 tree -> 'a1 enumeration -> 'a2 -> 'a2) ->
  'a1 enumeration ->
  'a2

val cons : 'a1 tree -> 'a1 enumeration -> 'a1 enumeration

val equal_more : 
  ('a1 -> 'a1 -> bool) ->
  Eqtype.Equality.sort ->
  'a1 ->
  ('a1 enumeration -> bool) ->
  'a1 enumeration ->
  bool

val equal_cont : 
  ('a1 -> 'a1 -> bool) ->
  'a1 tree ->
  ('a1 enumeration -> bool) ->
  'a1 enumeration ->
  bool

val equal_end : 'a1 enumeration -> bool

val equal : ('a1 -> 'a1 -> bool) -> 'a1 tree -> 'a1 tree -> bool

val map : ('a1 -> 'a2) -> 'a1 tree -> 'a2 tree

val mapi : (key -> 'a1 -> 'a2) -> 'a1 tree -> 'a2 tree

val map_option : (key -> 'a1 -> 'a2 option) -> 'a1 tree -> 'a2 tree

val map2_opt : 
  (key -> 'a1 -> 'a2 option -> 'a3 option) ->
  ('a1 tree -> 'a3 tree) ->
  ('a2 tree -> 'a3 tree) ->
  'a1 tree ->
  'a2 tree ->
  'a3 tree

val map2 : 
  ('a1 option -> 'a2 option -> 'a3 option) ->
  'a1 tree ->
  'a2 tree ->
  'a3 tree

module Proofs : sig ... end