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

(*
fn multiply<'a>(first: &'a i32, second: &'a i32) -> i32 {
    first * second
}
*)
Definition multiply (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ first; second ] =>
    ltac:(M.monadic
      (let first := M.alloc (| first |) in
      let second := M.alloc (| second |) in
      M.call_closure (|
        M.get_trait_method (|
          "core::ops::arith::Mul",
          Ty.apply (Ty.path "&") [] [ Ty.path "i32" ],
          [ Ty.apply (Ty.path "&") [] [ Ty.path "i32" ] ],
          "mul",
          []
        |),
        [ M.read (| first |); M.read (| second |) ]
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_multiply : M.IsFunction "scoping_rules_lifetimes_coercion::multiply" multiply.

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

Axiom Function_choose_first :
  M.IsFunction "scoping_rules_lifetimes_coercion::choose_first" choose_first.

(*
fn main() {
    let first = 2; // Longer lifetime

    {
        let second = 3; // Shorter lifetime

        println!("The product is {}", multiply(&first, &second));
        println!("{} is the first", choose_first(&first, &second));
    };
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ first := M.alloc (| Value.Integer IntegerKind.I32 2 |) in
        let~ _ :=
          let~ second := M.alloc (| Value.Integer IntegerKind.I32 3 |) in
          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 "The product 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.path "i32" ]
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "scoping_rules_lifetimes_coercion::multiply",
                                        []
                                      |),
                                      [ first; second ]
                                    |)
                                  |)
                                ]
                              |)
                            ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |) in
          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 "" |);
                              M.read (| Value.String " is the first
" |)
                            ]
                        |);
                        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" ] ]
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "scoping_rules_lifetimes_coercion::choose_first",
                                        []
                                      |),
                                      [ first; second ]
                                    |)
                                  |)
                                ]
                              |)
                            ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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