(* This code extends 'mini_prelude'. *)

datatype color = 
    Black 
  | Red ;

datatype ('a) tree = 
    Tree of color * ('a) tree * 'a * ('a) tree 
  | Empty ;

val empty = Empty ;

fun member v5 = 
  (fn v6 => 
    (fn v7 => 
      (case v7 of 
          Empty => false 
        | (Tree (v4, v3, v2, v1)) => 
            (if ((v5 v6) v2) 
            then (((member v5) v6) v3) 
            else 
              (if ((v5 v2) v6) 
              then (((member v5) v6) v1) 
              else true))))) ;

datatype ('a) option = 
    Some of 'a 
  | None ;

val balance_left_left = 
  (fn v11 => 
    (fn v9 => 
      (fn v10 => 
        (case v11 of 
            Empty => None 
          | (Tree (v8, v7, v6, v5)) => 
              (case v8 of 
                  Red => 
                    (case v7 of 
                        Empty => None 
                      | (Tree (v4, v3, v2, v1)) => 
                          (case v4 of 
                              Red => (Some ((Tree (Red, (Tree (Black, v3, v2, v1)), v6, (Tree (Black, v5, v9, v10)))))) 
                            | Black => None)) 
                | Black => None))))) ;

val balance_left_right = 
  (fn v11 => 
    (fn v9 => 
      (fn v10 => 
        (case v11 of 
            Empty => None 
          | (Tree (v8, v7, v6, v5)) => 
              (case v8 of 
                  Red => 
                    (case v5 of 
                        Empty => None 
                      | (Tree (v4, v3, v2, v1)) => 
                          (case v4 of 
                              Red => (Some ((Tree (Red, (Tree (Black, v7, v6, v3)), v2, (Tree (Black, v1, v9, v10)))))) 
                            | Black => None)) 
                | Black => None))))) ;

val balance_right_left = 
  (fn v11 => 
    (fn v9 => 
      (fn v10 => 
        (case v10 of 
            Empty => None 
          | (Tree (v8, v7, v6, v5)) => 
              (case v8 of 
                  Red => 
                    (case v7 of 
                        Empty => None 
                      | (Tree (v4, v3, v2, v1)) => 
                          (case v4 of 
                              Red => (Some ((Tree (Red, (Tree (Black, v11, v9, v3)), v2, (Tree (Black, v1, v6, v5)))))) 
                            | Black => None)) 
                | Black => None))))) ;

val balance_right_right = 
  (fn v11 => 
    (fn v9 => 
      (fn v10 => 
        (case v10 of 
            Empty => None 
          | (Tree (v8, v7, v6, v5)) => 
              (case v8 of 
                  Red => 
                    (case v5 of 
                        Empty => None 
                      | (Tree (v4, v3, v2, v1)) => 
                          (case v4 of 
                              Red => (Some ((Tree (Red, (Tree (Black, v11, v9, v7)), v6, (Tree (Black, v3, v2, v1)))))) 
                            | Black => None)) 
                | Black => None))))) ;

val balance' = 
  (fn v7 => 
    (fn v5 => 
      (fn v8 => 
        (fn v6 => 
          (if (v7 = Black) 
          then 
            (case (((balance_left_left v5) v8) v6) of 
                None => 
                  (case (((balance_left_right v5) v8) v6) of 
                      None => 
                        (case (((balance_right_left v5) v8) v6) of 
                            None => 
                              (case (((balance_right_right v5) v8) v6) of 
                              None => (Tree (Black, v5, v8, v6)) 
                              | (Some (v1)) => v1) 
                          | (Some (v2)) => v2) 
                    | (Some (v3)) => v3) 
              | (Some (v4)) => v4) 
          else (Tree (v7, v5, v8, v6))))))) ;

fun ins v5 = 
  (fn v6 => 
    (fn v7 => 
      (case v7 of 
          Empty => (Tree (Red, Empty, v6, Empty)) 
        | (Tree (v4, v3, v2, v1)) => 
            (if ((v5 v6) v2) 
            then ((((balance' v4) (((ins v5) v6) v3)) v2) v1) 
            else 
              (if ((v5 v2) v6) 
              then ((((balance' v4) v3) v2) (((ins v5) v6) v1)) 
              else (Tree (v4, v3, v2, v1))))))) ;

val insert = 
  (fn v5 => 
    (fn v7 => 
      (fn v6 => 
        (case (((ins v5) v7) v6) of 
            Empty => (raise Bind) 
          | (Tree (v4, v3, v2, v1)) => (Tree (Black, v3, v2, v1)))))) ;