(* This code extends 'mini_prelude'. *)

Dtype
  [(["a"],"times",
    [("Twice",[Tapp [Tvar "a"] "times"; Tapp [Tvar "a"] "times"]);
     ("Once",[Tvar "a"])])]

Dtype
  [(["a"],"digit",
    [("Two",[Tapp [Tvar "a"] "times"; Tapp [Tvar "a"] "times"]);
     ("One",[Tapp [Tvar "a"] "times"]); ("Zero",[])])]

Dtype
  [(["a"],"queue",
    [("Deep",
      [Tapp [Tvar "a"] "digit"; Tapp [Tvar "a"] "queue";
       Tapp [Tvar "a"] "digit"]);
     ("Shallow",[Tapp [Tvar "a"] "digit"])])]

Dlet (Pvar "empty") (Con "Shallow" [Con "Zero" []])

Dlet (Pvar "is_empty")
  (Fun "v8"
     (Mat (Var "v8")
        [(Pcon "Shallow" [Pvar "v4"],
          Mat (Var "v4")
            [(Pcon "Zero" [],Val (Lit (Bool T)));
             (Pcon "One" [Pvar "v1"],Val (Lit (Bool F)));
             (Pcon "Two" [Pvar "v3"; Pvar "v2"],Val (Lit (Bool F)))]);
         (Pcon "Deep" [Pvar "v7"; Pvar "v6"; Pvar "v5"],
          Val (Lit (Bool F)))]))

Dletrec
  [("snoc","x",
    Fun "x1"
      (Mat (Var "x")
         [(Pcon "Shallow" [Pvar "v4"],
           Mat (Var "v4")
             [(Pcon "Zero" [],Con "Shallow" [Con "One" [Var "x1"]]);
              (Pcon "One" [Pvar "v1"],
               Con "Deep"
                 [Con "Two" [Var "v1"; Var "x1"]; Var "empty";
                  Con "Zero" []]);
              (Pcon "Two" [Pvar "v3"; Pvar "v2"],Raise Bind_error)]);
          (Pcon "Deep" [Pvar "v10"; Pvar "v9"; Pvar "v8"],
           Mat (Var "v8")
             [(Pcon "Zero" [],
               Con "Deep" [Var "v10"; Var "v9"; Con "One" [Var "x1"]]);
              (Pcon "One" [Pvar "v5"],
               Con "Deep"
                 [Var "v10";
                  App Opapp (App Opapp (Var "snoc") (Var "v9"))
                    (Con "Twice" [Var "v5"; Var "x1"]); Con "Zero" []]);
              (Pcon "Two" [Pvar "v7"; Pvar "v6"],Raise Bind_error)])]))]

Dlet (Pvar "head")
  (Fun "x"
     (Mat (Var "x")
        [(Pcon "Shallow" [Pvar "v4"],
          Mat (Var "v4")
            [(Pcon "Zero" [],Raise Bind_error);
             (Pcon "One" [Pvar "v1"],Var "v1");
             (Pcon "Two" [Pvar "v3"; Pvar "v2"],Raise Bind_error)]);
         (Pcon "Deep" [Pvar "v10"; Pvar "v9"; Pvar "v8"],
          Mat (Var "v10")
            [(Pcon "Zero" [],Raise Bind_error);
             (Pcon "One" [Pvar "v5"],Var "v5");
             (Pcon "Two" [Pvar "v7"; Pvar "v6"],Var "v7")])]))

Dletrec
  [("tail","x",
    Mat (Var "x")
      [(Pcon "Shallow" [Pvar "v4"],
        Mat (Var "v4")
          [(Pcon "Zero" [],Raise Bind_error);
           (Pcon "One" [Pvar "v1"],Var "empty");
           (Pcon "Two" [Pvar "v3"; Pvar "v2"],Raise Bind_error)]);
       (Pcon "Deep" [Pvar "v13"; Pvar "v12"; Pvar "v11"],
        Mat (Var "v13")
          [(Pcon "Zero" [],Raise Bind_error);
           (Pcon "One" [Pvar "v8"],
            If (App Opapp (Var "is_empty") (Var "v12"))
              (Con "Shallow" [Var "v11"])
              (Mat (App Opapp (Var "head") (Var "v12"))
                 [(Pcon "Once" [Pvar "v5"],Raise Bind_error);
                  (Pcon "Twice" [Pvar "v7"; Pvar "v6"],
                   Con "Deep"
                     [Con "Two" [Var "v7"; Var "v6"];
                      App Opapp (Var "tail") (Var "v12");
                      Var "v11"])]));
           (Pcon "Two" [Pvar "v10"; Pvar "v9"],
            Con "Deep"
              [Con "One" [Var "v9"]; Var "v12"; Var "v11"])])])]