(* This code extends 'mini_prelude'. *)

datatype ('a) times = 
    Twice of ('a) times * ('a) times 
  | Once of 'a ;

datatype ('a) digit = 
    Two of ('a) times * ('a) times 
  | One of ('a) times 
  | Zero ;

datatype ('a) queue = 
    Deep of ('a) digit * ('a) queue * ('a) digit 
  | Shallow of ('a) digit ;

val empty = (Shallow (Zero)) ;

val is_empty = 
  (fn v8 => 
    (case v8 of 
        (Shallow (v4)) => 
          (case v4 of 
              Zero => true 
            | (One (v1)) => false 
            | (Two (v3, v2)) => false) 
      | (Deep (v7, v6, v5)) => false)) ;

fun snoc x = 
  (fn x1 => 
    (case x of 
        (Shallow (v4)) => 
          (case v4 of 
              Zero => (Shallow ((One (x1)))) 
            | (One (v1)) => (Deep ((Two (v1, x1)), empty, Zero)) 
            | (Two (v3, v2)) => (raise Bind)) 
      | (Deep (v10, v9, v8)) => 
          (case v8 of 
              Zero => (Deep (v10, v9, (One (x1)))) 
            | (One (v5)) => (Deep (v10, ((snoc v9) (Twice (v5, x1))), Zero)) 
            | (Two (v7, v6)) => (raise Bind)))) ;

val head = 
  (fn x => 
    (case x of 
        (Shallow (v4)) => 
          (case v4 of 
              Zero => (raise Bind) 
            | (One (v1)) => v1 
            | (Two (v3, v2)) => (raise Bind)) 
      | (Deep (v10, v9, v8)) => 
          (case v10 of 
              Zero => (raise Bind) 
            | (One (v5)) => v5 
            | (Two (v7, v6)) => v7))) ;

fun tail x = 
  (case x of 
      (Shallow (v4)) => 
        (case v4 of 
            Zero => (raise Bind) 
          | (One (v1)) => empty 
          | (Two (v3, v2)) => (raise Bind)) 
    | (Deep (v13, v12, v11)) => 
        (case v13 of 
            Zero => (raise Bind) 
          | (One (v8)) => 
              (if (is_empty v12) 
              then (Shallow (v11)) 
              else 
                (case (head v12) of 
                    (Once (v5)) => (raise Bind) 
                  | (Twice (v7, v6)) => (Deep ((Two (v7, v6)), (tail v12), v11)))) 
          | (Two (v10, v9)) => (Deep ((One (v9)), v12, v11)))) ;