(* This code extends 'mini_prelude'. *)

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

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

Dtype
  [(["a"],"tree",
    [("Node",[Tnum; Tapp [Tvar "a"] "tree"; Tapp [Tvar "a"] "tree"]);
     ("Leaf",[Tvar "a"])])]

Dlet (Pvar "size")
  (Fun "v5"
     (Mat (Var "v5")
        [(Pcon "Leaf" [Pvar "v1"],Val (Lit (IntLit 1)));
         (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],Var "v4")]))

Dlet (Pvar "link")
  (Fun "v1"
     (Fun "v2"
        (Con "Node"
           [App (Opn Plus) (App Opapp (Var "size") (Var "v1"))
              (App Opapp (Var "size") (Var "v2")); Var "v1";
            Var "v2"])))

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

Dletrec
  [("cons_tree","v4",
    Fun "v5"
      (Mat (Var "v5")
         [(Pcon "Nil" [],
           Con "Cons" [Con "One" [Var "v4"]; Con "Nil" []]);
          (Pcon "Cons" [Pvar "v3"; Pvar "v2"],
           Mat (Var "v3")
             [(Pcon "Zero" [],
               Con "Cons" [Con "One" [Var "v4"]; Var "v2"]);
              (Pcon "One" [Pvar "v1"],
               Con "Cons"
                 [Con "Zero" [];
                  App Opapp
                    (App Opapp (Var "cons_tree")
                       (App Opapp (App Opapp (Var "link") (Var "v4"))
                          (Var "v1"))) (Var "v2")])])]))]

Dletrec
  [("uncons_tree","x",
    Mat (Var "x")
      [(Pcon "Nil" [],Raise Bind_error);
       (Pcon "Cons" [Pvar "v11"; Pvar "v10"],
        Mat (Var "v11")
          [(Pcon "Zero" [],
            Mat (App Opapp (Var "uncons_tree") (Var "v10"))
              [(Pcon "Pair" [Pvar "v6"; Pvar "v5"],
                Mat (Var "v6")
                  [(Pcon "Leaf" [Pvar "v1"],Raise Bind_error);
                   (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
                    Con "Pair"
                      [Var "v3";
                       Con "Cons"
                         [Con "One" [Var "v2"]; Var "v5"]])])]);
           (Pcon "One" [Pvar "v9"],
            Mat (Var "v10")
              [(Pcon "Nil" [],Con "Pair" [Var "v9"; Con "Nil" []]);
               (Pcon "Cons" [Pvar "v8"; Pvar "v7"],
                Con "Pair"
                  [Var "v9";
                   Con "Cons"
                     [Con "Zero" [];
                      Con "Cons" [Var "v8"; Var "v7"]]])])])])]

Dlet (Pvar "cons")
  (Fun "v2"
     (Fun "v1"
        (App Opapp (App Opapp (Var "cons_tree") (Con "Leaf" [Var "v2"]))
           (Var "v1"))))

Dlet (Pvar "head")
  (Fun "v7"
     (Mat (App Opapp (Var "uncons_tree") (Var "v7"))
        [(Pcon "Pair" [Pvar "v6"; Pvar "v5"],
          Mat (Var "v6")
            [(Pcon "Leaf" [Pvar "v1"],Var "v1");
             (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
              Raise Bind_error)])]))

Dlet (Pvar "tail")
  (Fun "v4"
     (Let "v3" (App Opapp (Var "uncons_tree") (Var "v4"))
        (Mat (Var "v3")
           [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v1")])))

Dletrec
  [("lookup_tree","x1",
    Fun "x2"
      (Mat (Var "x2")
         [(Pcon "Leaf" [Pvar "v1"],
           If (App (Opb Leq) (Var "x1") (Val (Lit (IntLit 0))))
             (Var "v1") (Raise Bind_error));
          (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
           If
             (App (Opb Lt) (Var "x1")
                (App (Opn Divide) (Var "v4") (Val (Lit (IntLit 2)))))
             (App Opapp (App Opapp (Var "lookup_tree") (Var "x1"))
                (Var "v3"))
             (App Opapp
                (App Opapp (Var "lookup_tree")
                   (Let "k"
                      (App (Opn Minus) (Var "x1")
                         (App (Opn Divide) (Var "v4")
                            (Val (Lit (IntLit 2)))))
                      (If
                         (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0))))
                         (Val (Lit (IntLit 0))) (Var "k"))))
                (Var "v2")))]))]

Dletrec
  [("update_tree","x1",
    Fun "x2"
      (Fun "x3"
         (Mat (Var "x3")
            [(Pcon "Leaf" [Pvar "v1"],
              If (App (Opb Leq) (Var "x1") (Val (Lit (IntLit 0))))
                (Con "Leaf" [Var "x2"]) (Raise Bind_error));
             (Pcon "Node" [Pvar "v4"; Pvar "v3"; Pvar "v2"],
              If
                (App (Opb Lt) (Var "x1")
                   (App (Opn Divide) (Var "v4") (Val (Lit (IntLit 2)))))
                (Con "Node"
                   [Var "v4";
                    App Opapp
                      (App Opapp
                         (App Opapp (Var "update_tree") (Var "x1"))
                         (Var "x2")) (Var "v3"); Var "v2"])
                (Con "Node"
                   [Var "v4"; Var "v3";
                    App Opapp
                      (App Opapp
                         (App Opapp (Var "update_tree")
                            (Let "k"
                               (App (Opn Minus) (Var "x1")
                                  (App (Opn Divide) (Var "v4")
                                     (Val (Lit (IntLit 2)))))
                               (If
                                  (App (Opb Lt) (Var "k")
                                     (Val (Lit (IntLit 0))))
                                  (Val (Lit (IntLit 0))) (Var "k"))))
                         (Var "x2")) (Var "v2")]))])))]

Dletrec
  [("lookup","x",
    Fun "x1"
      (Mat (Var "x1")
         [(Pcon "Nil" [],Raise Bind_error);
          (Pcon "Cons" [Pvar "v3"; Pvar "v2"],
           Mat (Var "v3")
             [(Pcon "Zero" [],
               App Opapp (App Opapp (Var "lookup") (Var "x"))
                 (Var "v2"));
              (Pcon "One" [Pvar "v1"],
               If
                 (App (Opb Lt) (Var "x")
                    (App Opapp (Var "size") (Var "v1")))
                 (App Opapp (App Opapp (Var "lookup_tree") (Var "x"))
                    (Var "v1"))
                 (App Opapp
                    (App Opapp (Var "lookup")
                       (Let "k"
                          (App (Opn Minus) (Var "x")
                             (App Opapp (Var "size") (Var "v1")))
                          (If
                             (App (Opb Lt) (Var "k")
                                (Val (Lit (IntLit 0))))
                             (Val (Lit (IntLit 0))) (Var "k"))))
                    (Var "v2")))])]))]

Dletrec
  [("update","x",
    Fun "x1"
      (Fun "x2"
         (Mat (Var "x2")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v3"; Pvar "v2"],
              Mat (Var "v3")
                [(Pcon "Zero" [],
                  Con "Cons"
                    [Con "Zero" [];
                     App Opapp
                       (App Opapp (App Opapp (Var "update") (Var "x"))
                          (Var "x1")) (Var "v2")]);
                 (Pcon "One" [Pvar "v1"],
                  If
                    (App (Opb Lt) (Var "x")
                       (App Opapp (Var "size") (Var "v1")))
                    (Con "Cons"
                       [Con "One"
                          [App Opapp
                             (App Opapp
                                (App Opapp (Var "update_tree")
                                   (Var "x")) (Var "x1")) (Var "v1")];
                        Var "v2"])
                    (Con "Cons"
                       [Con "One" [Var "v1"];
                        App Opapp
                          (App Opapp
                             (App Opapp (Var "update")
                                (Let "k"
                                   (App (Opn Minus) (Var "x")
                                      (App Opapp (Var "size")
                                         (Var "v1")))
                                   (If
                                      (App (Opb Lt) (Var "k")
                                         (Val (Lit (IntLit 0))))
                                      (Val (Lit (IntLit 0)))
                                      (Var "k")))) (Var "x1"))
                          (Var "v2")]))])])))]