(* This code extends 'mini_prelude'. *)

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

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

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

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

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

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

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