(* If you would like, write how many hours you spent on this homework:

  XXX

*)

let rec forall gen prop n = 
  if n <= 0 then None else
     let x = gen () in 
     if prop x then forall gen prop (n - 1) else Some x

let gen_pair (f : unit -> 'a) (g : unit -> 'b) : (unit -> ('a * 'b)) = 
    fun _ -> 
        let x = f () in 
        let y = g () in 
        (x, y)

type 's pq_ops = { 
    empty : 's;
    push : 's -> string -> int -> 's;
    peek : 's -> (string * int) option;
    size : 's -> int;
    pop : 's -> 's;
    increment : 's -> 's;
}

(* ** Q1 ** *)

(* *** PROPERTIES GO HERE ***

Property 1: If we push onto the empty queue, then peek, we get the thing we pushed with the same priority. 
------
forall x : string, forall i : int, 
    peek (push empty x i) = Some (x, i)

Property 2: When we push two elements onto a queue, and then take the size,
this gives the same result as reversing the pushes.
-----
forall q : queue, forall x : string, forall y : string, forall i : int, forall j : int,
    size (push (push q x i) y j) = 
    size (push (push q y j) x i)


Your properties below:




*)


(* ** Q2 ** *)

let prop1 (ops : 's pq_ops) (x : string) (i : int) : bool = 
  ops.peek (ops.push ops.empty x i) = Some (x, i)

let prop2 (ops : 's pq_ops) (q : 's) (x : string) (y : string) (i : int) (j : int) : bool =
  ops.size (ops.push (ops.push q x i) y j)
  =
  ops.size (ops.push (ops.push q y j) x i)

(* Your properties below: *)


(* ** Q3 ** *)
type instruction = | Push of string * int | Pop | Increment
let gen_ins () : instruction list = failwith "TODO"

let rec mk_queue (ops : 's pq_ops) (xs : instruction list) : 's = failwith "TODO"

let gen_string () : string = failwith "TODO"

let gen_priority () : int = failwith "TODO"

(* ** Q4 ** *)
let prop1_test (ops : 's pq_ops) () : (string * int) option =
  forall (gen_pair gen_string gen_priority) (fun (x, i) -> prop1 ops x i) 32

let prop2_test (ops : 's pq_ops) () : (instruction list * (string * (string * (int * int)))) option =
  forall (gen_pair gen_ins (gen_pair gen_string (gen_pair gen_string (gen_pair gen_priority gen_priority))))
             (fun (xs, (x, (y, (i, j)))) -> 
              prop2 ops (mk_queue ops xs) x y i j
             ) 32

(* Your prop3_test, prop4_test, ... below: *)

(* *** Q5 *** *)
type my_q = | TODO  (* Replace with your chosen type! *)
let my_q_ops : my_q pq_ops = {
  empty = TODO;
  push = (fun _ _ -> failwith "TODO");
  peek = (fun _ -> failwith "TODO");
  size = (fun _ -> failwith "TODO");
  pop = (fun _ -> failwith "TODO");
  increment = (fun _ -> failwith "TODO");
}

(* *** Q6 *** *)
let my_q_correct () : bool = 
  prop1_test my_q_ops () = None && 
  prop2_test my_q_ops () = None  
  (* TODO: Add in your tests here! *)

(* *** Q7 *** *)

(*** Q7.1:

- Correct trace (Y/N):
- Corrected observation, if incorrect trace (write N/A if correct trace): 

***)


(*** Q7.2:

- Correct trace (Y/N):
- Corrected observation, if incorrect trace (write N/A if correct trace): 

***)

(*** Q7.3:

- Correct trace (Y/N):
- Corrected observation, if incorrect trace (write N/A if correct trace): 

***)

(*** Q7.4:

- Correct trace (Y/N):
- Corrected observation, if incorrect trace (write N/A if correct trace): 

***)