(* This code extends 'mini_prelude'. *)

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

Dlet (Pvar "empty")
  (Con "Queue" [Con "Nil" []; Con "Nil" []; Con "Nil" []])

Dlet (Pvar "is_empty")
  (Fun "v6"
     (Mat (Var "v6")
        [(Pcon "Queue" [Pvar "v5"; Pvar "v4"; Pvar "v3"],
          Mat (Var "v5")
            [(Pcon "Nil" [],Val (Lit (Bool T)));
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
              Val (Lit (Bool F)))])]))

Dletrec
  [("rotate","x",
    Mat (Var "x")
      [(Pcon "Queue" [Pvar "v9"; Pvar "v8"; Pvar "v7"],
        Mat (Var "v9")
          [(Pcon "Nil" [],
            Mat (Var "v8")
              [(Pcon "Nil" [],Raise Bind_error);
               (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                Con "Cons" [Var "v2"; Var "v7"])]);
           (Pcon "Cons" [Pvar "v6"; Pvar "v5"],
            Mat (Var "v8")
              [(Pcon "Nil" [],Raise Bind_error);
               (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
                Con "Cons"
                  [Var "v6";
                   App Opapp (Var "rotate")
                     (Con "Queue"
                        [Var "v5"; Var "v3";
                         Con "Cons" [Var "v4"; Var "v7"]])])])])])]

Dlet (Pvar "exec")
  (Fun "v7"
     (Mat (Var "v7")
        [(Pcon "Queue" [Pvar "v6"; Pvar "v5"; Pvar "v4"],
          Mat (Var "v4")
            [(Pcon "Nil" [],
              Let "v1"
                (App Opapp (Var "rotate")
                   (Con "Queue" [Var "v6"; Var "v5"; Con "Nil" []]))
                (Con "Queue" [Var "v1"; Con "Nil" []; Var "v1"]));
             (Pcon "Cons" [Pvar "v3"; Pvar "v2"],
              Con "Queue" [Var "v6"; Var "v5"; Var "v2"])])]))

Dlet (Pvar "snoc")
  (Fun "v4"
     (Fun "v5"
        (Mat (Var "v4")
           [(Pcon "Queue" [Pvar "v3"; Pvar "v2"; Pvar "v1"],
             App Opapp (Var "exec")
               (Con "Queue"
                  [Var "v3"; Con "Cons" [Var "v5"; Var "v2"];
                   Var "v1"]))])))

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

Dlet (Pvar "tail")
  (Fun "x"
     (Mat (Var "x")
        [(Pcon "Queue" [Pvar "v5"; Pvar "v4"; Pvar "v3"],
          Mat (Var "v5")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
              App Opapp (Var "exec")
                (Con "Queue" [Var "v1"; Var "v4"; Var "v3"]))])]))