(* This code extends 'mini_prelude'. *)

Dtype
  [(["a"],"status",
    [("Finished",[Tapp [Tvar "a"] "list"]);
     ("Appending",
      [Tnum; Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "list"]);
     ("Reversing",
      [Tnum; Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "list";
       Tapp [Tvar "a"] "list"; Tapp [Tvar "a"] "list"]); ("Idle",[])])]

Dlet (Pvar "exec")
  (Fun "v22"
     (Mat (Var "v22")
        [(Pcon "Idle" [],Con "Idle" []);
         (Pcon "Reversing"
            [Pvar "v13"; Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"],
          Mat (Var "v12")
            [(Pcon "Nil" [],
              Mat (Var "v10")
                [(Pcon "Nil" [],
                  Con "Reversing"
                    [Var "v13"; Con "Nil" []; Var "v11"; Con "Nil" [];
                     Var "v9"]);
                 (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
                  Mat (Var "v3")
                    [(Pcon "Nil" [],
                      Con "Appending"
                        [Var "v13"; Var "v11";
                         Con "Cons" [Var "v4"; Var "v9"]]);
                     (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                      Con "Reversing"
                        [Var "v13"; Con "Nil" []; Var "v11";
                         Con "Cons"
                           [Var "v4"; Con "Cons" [Var "v2"; Var "v1"]];
                         Var "v9"])])]);
             (Pcon "Cons" [Pvar "v8"; Pvar "v7"],
              Mat (Var "v10")
                [(Pcon "Nil" [],
                  Con "Reversing"
                    [Var "v13"; Con "Cons" [Var "v8"; Var "v7"];
                     Var "v11"; Con "Nil" []; Var "v9"]);
                 (Pcon "Cons" [Pvar "v6"; Pvar "v5"],
                  Con "Reversing"
                    [App (Opn Plus) (Var "v13") (Val (Lit (IntLit 1)));
                     Var "v7"; Con "Cons" [Var "v8"; Var "v11"];
                     Var "v5"; Con "Cons" [Var "v6"; Var "v9"]])])]);
         (Pcon "Appending" [Pvar "v20"; Pvar "v19"; Pvar "v18"],
          If (App (Opb Leq) (Var "v20") (Val (Lit (IntLit 0))))
            (Mat (Var "v19")
               [(Pcon "Nil" [],Con "Finished" [Var "v18"]);
                (Pcon "Cons" [Pvar "v15"; Pvar "v14"],
                 Con "Finished" [Var "v18"])])
            (Mat (Var "v19")
               [(Pcon "Nil" [],
                 Con "Appending" [Var "v20"; Con "Nil" []; Var "v18"]);
                (Pcon "Cons" [Pvar "v17"; Pvar "v16"],
                 Con "Appending"
                   [App (Opn Minus) (Var "v20") (Val (Lit (IntLit 1)));
                    Var "v16"; Con "Cons" [Var "v17"; Var "v18"]])]));
         (Pcon "Finished" [Pvar "v21"],Con "Finished" [Var "v21"])]))

Dlet (Pvar "invalidate")
  (Fun "v12"
     (Mat (Var "v12")
        [(Pcon "Idle" [],Con "Idle" []);
         (Pcon "Reversing"
            [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
          Con "Reversing"
            [Let "k" (App (Opn Minus) (Var "v5") (Val (Lit (IntLit 1))))
               (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                  (Val (Lit (IntLit 0))) (Var "k")); Var "v4"; Var "v3";
             Var "v2"; Var "v1"]);
         (Pcon "Appending" [Pvar "v10"; Pvar "v9"; Pvar "v8"],
          If (App (Opb Leq) (Var "v10") (Val (Lit (IntLit 0))))
            (Mat (Var "v8")
               [(Pcon "Nil" [],
                 Con "Appending"
                   [Val (Lit (IntLit 0)); Var "v9"; Con "Nil" []]);
                (Pcon "Cons" [Pvar "v7"; Pvar "v6"],
                 Con "Finished" [Var "v6"])])
            (Con "Appending"
               [App (Opn Minus) (Var "v10") (Val (Lit (IntLit 1)));
                Var "v9"; Var "v8"]));
         (Pcon "Finished" [Pvar "v11"],Con "Finished" [Var "v11"])]))

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

Dlet (Pvar "exec2")
  (Fun "v15"
     (Mat (Var "v15")
        [(Pcon "Queue"
            [Pvar "v14"; Pvar "v13"; Pvar "v12"; Pvar "v11";
             Pvar "v10"],
          Mat
            (App Opapp (Var "exec")
               (App Opapp (Var "exec") (Var "v12")))
            [(Pcon "Idle" [],
              Con "Queue"
                [Var "v14"; Var "v13"; Con "Idle" []; Var "v11";
                 Var "v10"]);
             (Pcon "Reversing"
                [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
              Con "Queue"
                [Var "v14"; Var "v13";
                 Con "Reversing"
                   [Var "v5"; Var "v4"; Var "v3"; Var "v2"; Var "v1"];
                 Var "v11"; Var "v10"]);
             (Pcon "Appending" [Pvar "v8"; Pvar "v7"; Pvar "v6"],
              Con "Queue"
                [Var "v14"; Var "v13";
                 Con "Appending" [Var "v8"; Var "v7"; Var "v6"];
                 Var "v11"; Var "v10"]);
             (Pcon "Finished" [Pvar "v9"],
              Con "Queue"
                [Var "v14"; Var "v9"; Con "Idle" []; Var "v11";
                 Var "v10"])])]))

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

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

Dlet (Pvar "is_empty")
  (Fun "v1"
     (Fun "v2"
        (Fun "v3"
           (Fun "v4"
              (Fun "v5"
                 (App Equality (Var "v1") (Val (Lit (IntLit 0)))))))))

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 "v6")
            [(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 "v6")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
              App Opapp (Var "check")
                (Con "Queue"
                   [Let "k"
                      (App (Opn Minus) (Var "v7")
                         (Val (Lit (IntLit 1))))
                      (If
                         (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                         (Val (Lit (IntLit 0))) (Var "k")); Var "v1";
                    App Opapp (Var "invalidate") (Var "v5"); Var "v4";
                    Var "v3"]))])]))