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

(* StructRecord
  {
    name := "Book";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("author", Ty.apply (Ty.path "&") [] [ Ty.path "str" ]);
        ("title", Ty.apply (Ty.path "&") [] [ Ty.path "str" ]);
        ("year", Ty.path "u32")
      ];
  } *)

Module Impl_core_clone_Clone_for_scoping_rules_borrowing_mutablity_Book.
  Definition Self : Ty.t := Ty.path "scoping_rules_borrowing_mutablity::Book".
  
  (* Clone *)
  Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    Value.DeclaredButUndefined,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            Value.DeclaredButUndefined,
                            [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                          |)))
                    ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_scoping_rules_borrowing_mutablity_Book.

Module Impl_core_marker_Copy_for_scoping_rules_borrowing_mutablity_Book.
  Definition Self : Ty.t := Ty.path "scoping_rules_borrowing_mutablity::Book".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_scoping_rules_borrowing_mutablity_Book.

(*
fn borrow_book(book: &Book) {
    println!(
        "I immutably borrowed {} - {} edition",
        book.title, book.year
    );
}
*)
Definition borrow_book (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ book ] =>
    ltac:(M.monadic
      (let book := M.alloc (| book |) 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 "I immutably borrowed " |);
                            M.read (| Value.String " - " |);
                            M.read (| Value.String " edition
" |)
                          ]
                      |);
                      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 "str" ] ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| book |),
                                  "scoping_rules_borrowing_mutablity::Book",
                                  "title"
                                |)
                              ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "u32" ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| book |),
                                  "scoping_rules_borrowing_mutablity::Book",
                                  "year"
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_borrow_book :
  M.IsFunction "scoping_rules_borrowing_mutablity::borrow_book" borrow_book.

(*
fn new_edition(book: &mut Book) {
    book.year = 2014;
    println!("I mutably borrowed {} - {} edition", book.title, book.year);
}
*)
Definition new_edition (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ book ] =>
    ltac:(M.monadic
      (let book := M.alloc (| book |) in
      M.read (|
        let~ _ :=
          M.write (|
            M.SubPointer.get_struct_record_field (|
              M.read (| book |),
              "scoping_rules_borrowing_mutablity::Book",
              "year"
            |),
            Value.Integer IntegerKind.U32 2014
          |) 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 "I mutably borrowed " |);
                            M.read (| Value.String " - " |);
                            M.read (| Value.String " edition
" |)
                          ]
                      |);
                      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 "str" ] ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| book |),
                                  "scoping_rules_borrowing_mutablity::Book",
                                  "title"
                                |)
                              ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "u32" ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| book |),
                                  "scoping_rules_borrowing_mutablity::Book",
                                  "year"
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_new_edition :
  M.IsFunction "scoping_rules_borrowing_mutablity::new_edition" new_edition.

(*
fn main() {
    // Create an immutable Book named `immutabook`
    let immutabook = Book {
        // string literals have type `&'static str`
        author: "Douglas Hofstadter",
        title: "Gödel, Escher, Bach",
        year: 1979,
    };

    // Create a mutable copy of `immutabook` and call it `mutabook`
    let mut mutabook = immutabook;

    // Immutably borrow an immutable object
    borrow_book(&immutabook);

    // Immutably borrow a mutable object
    borrow_book(&mutabook);

    // Borrow a mutable object as mutable
    new_edition(&mut mutabook);

    // Error! Cannot borrow an immutable object as mutable
    //new_edition(&mut immutabook);
    // FIXME ^ Comment out this line
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ immutabook :=
          M.alloc (|
            Value.StructRecord
              "scoping_rules_borrowing_mutablity::Book"
              [
                ("author", M.read (| Value.String "Douglas Hofstadter" |));
                ("title",
                  M.read (| Value.String ("G" ++ (String.String "246" "del, Escher, Bach")) |));
                ("year", Value.Integer IntegerKind.U32 1979)
              ]
          |) in
        let~ mutabook := M.copy (| immutabook |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_borrowing_mutablity::borrow_book", [] |),
              [ immutabook ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_borrowing_mutablity::borrow_book", [] |),
              [ mutabook ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "scoping_rules_borrowing_mutablity::new_edition", [] |),
              [ mutabook ]
            |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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