(* This code extends 'mini_prelude'. *)

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

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

val is_empty = 
  (fn v6 => 
    (case v6 of 
        (Queue (v5, v4, v3, v2, v1)) => (v4 <= 0))) ;

val checkw = 
  (fn v8 => 
    (case v8 of 
        (Queue (v7, v6, v5, v4, v3)) => 
          (case v7 of 
              Nil => (Queue (v5, v6, v5, v4, v3)) 
            | (Cons (v2, v1)) => (Queue ((Cons (v2, v1)), v6, v5, v4, v3))))) ;

val check = 
  (fn v6 => 
    (case v6 of 
        (Queue (v5, v4, v3, v2, v1)) => 
          (if (v2 <= v4) 
          then (checkw (Queue (v5, v4, v3, v2, v1))) 
          else (checkw (Queue (v3, (v4 + v2), ((APPEND v3) (REVERSE v1)), 0, Nil)))))) ;

val snoc = 
  (fn v6 => 
    (fn v7 => 
      (case v6 of 
          (Queue (v5, v4, v3, v2, v1)) => (check (Queue (v5, v4, v3, (v2 + 1), (Cons (v7, v1)))))))) ;

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

val tail = 
  (fn x => 
    (case x of 
        (Queue (v7, v6, v5, v4, v3)) => 
          (case v7 of 
              Nil => (raise Bind) 
            | (Cons (v2, v1)) => (check (Queue (v1, 
                let val k = (v6 - 1) 
                in 
                  (if (k < 0) 
                  then 0 
                  else k) 
                end , (TL v5), v4, v3)))))) ;