(* This code extends 'mini_prelude'. *)

datatype ('a) queue = 
    Queue of ('a) list * ('a) list * ('a) list ;

val empty = (Queue (Nil, Nil, Nil)) ;

val is_empty = 
  (fn v6 => 
    (case v6 of 
        (Queue (v5, v4, v3)) => 
          (case v5 of 
              Nil => true 
            | (Cons (v2, v1)) => false))) ;

fun rotate x = 
  (case x of 
      (Queue (v9, v8, v7)) => 
        (case v9 of 
            Nil => 
              (case v8 of 
                  Nil => (raise Bind) 
                | (Cons (v2, v1)) => (Cons (v2, v7))) 
          | (Cons (v6, v5)) => 
              (case v8 of 
                  Nil => (raise Bind) 
                | (Cons (v4, v3)) => (Cons (v6, (rotate (Queue (v5, v3, (Cons (v4, v7)))))))))) ;

val exec = 
  (fn v7 => 
    (case v7 of 
        (Queue (v6, v5, v4)) => 
          (case v4 of 
              Nil => 
                let val v1 = (rotate (Queue (v6, v5, Nil))) 
                in (Queue (v1, Nil, v1)) 
                end 
            | (Cons (v3, v2)) => (Queue (v6, v5, v2))))) ;

val snoc = 
  (fn v4 => 
    (fn v5 => 
      (case v4 of 
          (Queue (v3, v2, v1)) => (exec (Queue (v3, (Cons (v5, v2)), v1)))))) ;

val head = 
  (fn x => 
    (case x of 
        (Queue (v5, v4, v3)) => 
          (case v5 of 
              Nil => (raise Bind) 
            | (Cons (v2, v1)) => v2))) ;

val tail = 
  (fn x => 
    (case x of 
        (Queue (v5, v4, v3)) => 
          (case v5 of 
              Nil => (raise Bind) 
            | (Cons (v2, v1)) => (exec (Queue (v1, v4, v3)))))) ;