(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

(*
fn print_one<'a>(x: &'a i32) {
    println!("`print_one`: x is {}", x);
}
*)
Definition print_one (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ x ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      M.read (|
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (| Value.String "`print_one`: x is " |);
                            M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.apply (Ty.path "&") [] [ Ty.path "i32" ] ]
                              |),
                              [ x ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_print_one : M.IsFunction "scoping_rules_lifetimes_functions::print_one" print_one.

(*
fn add_one<'a>(x: &'a mut i32) {
    *x += 1;
}
*)
Definition add_one (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ x ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      M.read (|
        let~ _ :=
          let β := M.read (| x |) in
          M.write (| β, BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.I32 1 |) |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_add_one : M.IsFunction "scoping_rules_lifetimes_functions::add_one" add_one.

(*
fn print_multi<'a, 'b>(x: &'a i32, y: &'b i32) {
    println!("`print_multi`: x is {}, y is {}", x, y);
}
*)
Definition print_multi (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ x; y ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      let y := M.alloc (| y |) in
      M.read (|
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (| Value.String "`print_multi`: x is " |);
                            M.read (| Value.String ", y is " |);
                            M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.apply (Ty.path "&") [] [ Ty.path "i32" ] ]
                              |),
                              [ x ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.apply (Ty.path "&") [] [ Ty.path "i32" ] ]
                              |),
                              [ y ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_print_multi :
  M.IsFunction "scoping_rules_lifetimes_functions::print_multi" print_multi.

(*
fn pass_x<'a, 'b>(x: &'a i32, _: &'b i32) -> &'a i32 {
    x
}
*)
Definition pass_x (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ x; β1 ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      let β1 := M.alloc (| β1 |) in
      M.match_operator (| β1, [ fun γ => ltac:(M.monadic (M.read (| x |))) ] |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_pass_x : M.IsFunction "scoping_rules_lifetimes_functions::pass_x" pass_x.

(*
fn main() {
    let x = 7;
    let y = 9;

    print_one(&x);
    print_multi(&x, &y);

    let z = pass_x(&x, &y);
    print_one(z);

    let mut t = 3;
    add_one(&mut t);
    print_one(&t);
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ x := M.alloc (| Value.Integer IntegerKind.I32 7 |) in
        let~ y := M.alloc (| Value.Integer IntegerKind.I32 9 |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_lifetimes_functions::print_one", [] |),
              [ x ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_lifetimes_functions::print_multi", [] |),
              [ x; y ]
            |)
          |) in
        let~ z :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_lifetimes_functions::pass_x", [] |),
              [ x; y ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_lifetimes_functions::print_one", [] |),
              [ M.read (| z |) ]
            |)
          |) in
        let~ t := M.alloc (| Value.Integer IntegerKind.I32 3 |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_lifetimes_functions::add_one", [] |),
              [ t ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_lifetimes_functions::print_one", [] |),
              [ t ]
            |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_main : M.IsFunction "scoping_rules_lifetimes_functions::main" main.
