(* This code extends 'mini_prelude'. *)

Dtype
  [(["a"],"queue",
    [("Queue",
      [Tapp [Tvar "a"] "list"; Tnum; Tapp [Tvar "a"] "list"; Tnum;
       Tapp [Tvar "a"] "list"])])]

Dlet (Pvar "empty")
  (Con "Queue"
     [Con "Nil" []; Val (Lit (IntLit 0)); Con "Nil" [];
      Val (Lit (IntLit 0)); Con "Nil" []])

Dlet (Pvar "is_empty")
  (Fun "v6"
     (Mat (Var "v6")
        [(Pcon "Queue"
            [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
          App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0))))]))

Dlet (Pvar "checkw")
  (Fun "v8"
     (Mat (Var "v8")
        [(Pcon "Queue"
            [Pvar "v7"; Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"],
          Mat (Var "v7")
            [(Pcon "Nil" [],
              Con "Queue"
                [Var "v5"; Var "v6"; Var "v5"; Var "v4"; Var "v3"]);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
              Con "Queue"
                [Con "Cons" [Var "v2"; Var "v1"]; Var "v6"; Var "v5";
                 Var "v4"; Var "v3"])])]))

Dlet (Pvar "check")
  (Fun "v6"
     (Mat (Var "v6")
        [(Pcon "Queue"
            [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
          If (App (Opb Leq) (Var "v2") (Var "v4"))
            (App Opapp (Var "checkw")
               (Con "Queue"
                  [Var "v5"; Var "v4"; Var "v3"; Var "v2"; Var "v1"]))
            (App Opapp (Var "checkw")
               (Con "Queue"
                  [Var "v3"; App (Opn Plus) (Var "v4") (Var "v2");
                   App Opapp (App Opapp (Var "APPEND") (Var "v3"))
                     (App Opapp (Var "REVERSE") (Var "v1"));
                   Val (Lit (IntLit 0)); Con "Nil" []])))]))

Dlet (Pvar "snoc")
  (Fun "v6"
     (Fun "v7"
        (Mat (Var "v6")
           [(Pcon "Queue"
               [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
             App Opapp (Var "check")
               (Con "Queue"
                  [Var "v5"; Var "v4"; Var "v3";
                   App (Opn Plus) (Var "v2") (Val (Lit (IntLit 1)));
                   Con "Cons" [Var "v7"; Var "v1"]]))])))

Dlet (Pvar "head")
  (Fun "x"
     (Mat (Var "x")
        [(Pcon "Queue"
            [Pvar "v7"; Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"],
          Mat (Var "v7")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")])]))

Dlet (Pvar "tail")
  (Fun "x"
     (Mat (Var "x")
        [(Pcon "Queue"
            [Pvar "v7"; Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"],
          Mat (Var "v7")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
              App Opapp (Var "check")
                (Con "Queue"
                   [Var "v1";
                    Let "k"
                      (App (Opn Minus) (Var "v6")
                         (Val (Lit (IntLit 1))))
                      (If
                         (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                         (Val (Lit (IntLit 0))) (Var "k"));
                    App Opapp (Var "TL") (Var "v5"); Var "v4";
                    Var "v3"]))])]))