(* This code extends 'mini_prelude'. *)

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

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

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

val checkf = 
  (fn v5 => 
    (case v5 of 
        (Queue (v4, v3)) => 
          (case v4 of 
              Nil => (Queue ((REVERSE v3), Nil)) 
            | (Cons (v2, v1)) => (Queue ((Cons (v2, v1)), v3))))) ;

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

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

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