(* If you would like, please write here how many hours you spent on the assignment: 
  XXXX
*)

type entry = 
  { key : int; value : string }

type bst = 
  | Leaf
  | Node of bst * entry * bst

(**** Q1 ****)

(* Q1.1 *)
let rec has_key (t : bst) (k : int) = failwith "TODO"

(* Q1.2 *)
let rec has_entry (t : bst) (e : entry) : bool = failwith "TODO"

(* Q1.3 *)
let rec sorted (t : bst) : bool = failwith "TODO"


(**** Q2 ****)
let rec gen_bst (n : int) : unit -> bst = failwith "TODO"

(**** Q3 ****)
(* Q3.1 *)
let rec lookup (t : bst) (k : int) : string option = failwith "TODO"

(* Q3.2 *)
let p1 () : (bst * int) option = failwith "TODO"


(* Q3.3 *)

(* This property is false, so it should return a counter-example. *)
let p2 () : (bst * entry) option = failwith "TODO"

(* Briefly explain below why this counter-example breaks the property:

    TODO

*)
let p2_counter_example () : (bst * entry) = 
  failwith "TODO"


(* Q3.4 *)

(* Why is (P2') true? 

  TODO 

*)
let p2' () : (bst * entry) option = failwith "TODO"

(**** Q4 ****)
(* Q4.1 *)

let rec lookup_sorted (t : bst) (k : int) : string option = failwith "TODO"

(* Q4.2 *)
let p3 () : (bst * int) option = failwith "TODO"

(* Q4.3 *)
let rec gen_sorted (n : int) : unit -> bst = failwith "TODO"

(* Q4.4 *)
let gen_sorted_property () : bst option = failwith "TODO"

(* Q4.5 *)
let p3_gen_sorted () : (bst * int) option = failwith "TODO"

(* Q4.6 *)
let p4 () : (bst * int) = failwith "TODO"


(**** Q5 ****)
(* Q5.1 *)
let rec remove (k : int) (t : bst) : bst = failwith "TODO"

(* Q5.2 *)

(* Write your logical specification of remove below: 

    forall k1 : key, k2 : key, t : bst. 
      .... TODO .....

*)

(* Q5.3 *)
let p_remove () : (int * int * bst) option = failwith "TODO"

(* TODO: 
  - Is your property true or false?
  - If true, explain why. If false, give a counter-example you found using PBT. 
    ... TODO ...

*)