(* This code extends 'mini_prelude'. *)

datatype ('a) status = 
    Finished of ('a) list 
  | Appending of int * ('a) list * ('a) list 
  | Reversing of int * ('a) list * ('a) list * ('a) list * ('a) list 
  | Idle ;

val exec = 
  (fn v22 => 
    (case v22 of 
        Idle => Idle 
      | (Reversing (v13, v12, v11, v10, v9)) => 
          (case v12 of 
              Nil => 
                (case v10 of 
                    Nil => (Reversing (v13, Nil, v11, Nil, v9)) 
                  | (Cons (v4, v3)) => 
                      (case v3 of 
                          Nil => (Appending (v13, v11, (Cons (v4, v9)))) 
                        | (Cons (v2, v1)) => (Reversing (v13, Nil, v11, (Cons (v4, (Cons (v2, v1)))), v9)))) 
            | (Cons (v8, v7)) => 
                (case v10 of 
                    Nil => (Reversing (v13, (Cons (v8, v7)), v11, Nil, v9)) 
                  | (Cons (v6, v5)) => (Reversing ((v13 + 1), v7, (Cons (v8, v11)), v5, (Cons (v6, v9)))))) 
      | (Appending (v20, v19, v18)) => 
          (if (v20 <= 0) 
          then 
            (case v19 of 
                Nil => (Finished (v18)) 
              | (Cons (v15, v14)) => (Finished (v18))) 
          else 
            (case v19 of 
                Nil => (Appending (v20, Nil, v18)) 
              | (Cons (v17, v16)) => (Appending ((v20 - 1), v16, (Cons (v17, v18)))))) 
      | (Finished (v21)) => (Finished (v21)))) ;

val invalidate = 
  (fn v12 => 
    (case v12 of 
        Idle => Idle 
      | (Reversing (v5, v4, v3, v2, v1)) => (Reversing (
          let val k = (v5 - 1) 
          in 
            (if (k < 0) 
            then 0 
            else k) 
          end , v4, v3, v2, v1)) 
      | (Appending (v10, v9, v8)) => 
          (if (v10 <= 0) 
          then 
            (case v8 of 
                Nil => (Appending (0, v9, Nil)) 
              | (Cons (v7, v6)) => (Finished (v6))) 
          else (Appending ((v10 - 1), v9, v8))) 
      | (Finished (v11)) => (Finished (v11)))) ;

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

val exec2 = 
  (fn v15 => 
    (case v15 of 
        (Queue (v14, v13, v12, v11, v10)) => 
          (case (exec (exec v12)) of 
              Idle => (Queue (v14, v13, Idle, v11, v10)) 
            | (Reversing (v5, v4, v3, v2, v1)) => (Queue (v14, v13, (Reversing (v5, v4, v3, v2, v1)), v11, v10)) 
            | (Appending (v8, v7, v6)) => (Queue (v14, v13, (Appending (v8, v7, v6)), v11, v10)) 
            | (Finished (v9)) => (Queue (v14, v9, Idle, v11, v10))))) ;

val check = 
  (fn v7 => 
    (case v7 of 
        (Queue (v6, v5, v4, v3, v2)) => 
          (if (v3 <= v6) 
          then (exec2 (Queue (v6, v5, v4, v3, v2))) 
          else 
            let val v1 = (Reversing (0, v5, Nil, v2, Nil)) 
            in (exec2 (Queue ((v6 + v3), v5, v1, 0, Nil))) 
            end ))) ;

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

val is_empty = 
  (fn v1 => 
    (fn v2 => 
      (fn v3 => 
        (fn v4 => 
          (fn v5 => (v1 = 0)))))) ;

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 v6 of 
              Nil => (raise Bind) 
            | (Cons (v2, v1)) => v2))) ;

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