(* This code extends 'mini_prelude'. *)

datatype ('a) heap = 
    Tree of int * 'a * ('a) heap * ('a) heap 
  | Empty ;

val rank = 
  (fn v5 => 
    (case v5 of 
        Empty => 0 
      | (Tree (v4, v3, v2, v1)) => v4)) ;

val make_node = 
  (fn v3 => 
    (fn v1 => 
      (fn v2 => 
        (if ((rank v1) > (rank v2)) 
        then (Tree (((rank v2) + 1), v3, v1, v2)) 
        else (Tree (((rank v1) + 1), v3, v2, v1)))))) ;

val empty = Empty ;

val is_empty = 
  (fn v5 => 
    (case v5 of 
        Empty => true 
      | (Tree (v4, v3, v2, v1)) => false)) ;

fun merge v13 = 
  (fn v14 => 
    (fn v15 => 
      (fn v16 => 
        (case v15 of 
            Empty => 
              (case v16 of 
                  Empty => Empty 
                | (Tree (v4, v3, v2, v1)) => (Tree (v4, v3, v2, v1))) 
          | (Tree (v12, v11, v10, v9)) => 
              (case v16 of 
                  Empty => (Tree (v12, v11, v10, v9)) 
                | (Tree (v8, v7, v6, v5)) => 
                    (if ((v14 (v13 v11)) (v13 v7)) 
                    then (((make_node v11) v10) ((((merge v13) v14) v9) (Tree (v8, v7, v6, v5)))) 
                    else (((make_node v7) v6) ((((merge v13) v14) (Tree (v12, v11, v10, v9))) v5)))))))) ;

val insert = 
  (fn v1 => 
    (fn v3 => 
      (fn v4 => 
        (fn v2 => ((((merge v1) v3) (Tree (1, v4, Empty, Empty))) v2))))) ;

val find_min = 
  (fn x1 => 
    (case x1 of 
        Empty => (raise Bind) 
      | (Tree (v4, v3, v2, v1)) => v3)) ;

val delete_min = 
  (fn x1 => 
    (fn x2 => 
      (fn x3 => 
        (case x3 of 
            Empty => (raise Bind) 
          | (Tree (v4, v3, v2, v1)) => ((((merge x1) x2) v2) v1))))) ;