(* This code extends 'mini_prelude'. *)

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

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

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

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

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

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

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