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

Module move_resource.
  (* Trait *)
  Module MoveStructType.
    Definition module_identifier
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_trait_method (|
              "alloc::borrow::ToOwned",
              Ty.path "move_core_types::identifier::IdentStr",
              [],
              "to_owned",
              []
            |),
            [
              M.read (|
                M.get_constant (| "move_core_types::move_resource::MoveStructType::MODULE_NAME" |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_module_identifier :
      M.IsProvidedMethod
        "move_core_types::move_resource::MoveStructType"
        "module_identifier"
        module_identifier.
    Definition struct_identifier
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_trait_method (|
              "alloc::borrow::ToOwned",
              Ty.path "move_core_types::identifier::IdentStr",
              [],
              "to_owned",
              []
            |),
            [
              M.read (|
                M.get_constant (| "move_core_types::move_resource::MoveStructType::STRUCT_NAME" |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_struct_identifier :
      M.IsProvidedMethod
        "move_core_types::move_resource::MoveStructType"
        "struct_identifier"
        struct_identifier.
    Definition type_params
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.path "move_core_types::language_storage::TypeTag";
                  Ty.path "alloc::alloc::Global"
                ],
              "new",
              []
            |),
            []
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_type_params :
      M.IsProvidedMethod "move_core_types::move_resource::MoveStructType" "type_params" type_params.
    Definition struct_tag (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "move_core_types::language_storage::StructTag"
            [
              ("address",
                M.read (|
                  M.get_constant (| "move_core_types::move_resource::MoveStructType::ADDRESS" |)
                |));
              ("name",
                M.call_closure (|
                  M.get_trait_method (|
                    "move_core_types::move_resource::MoveStructType",
                    Self,
                    [],
                    "struct_identifier",
                    []
                  |),
                  []
                |));
              ("module",
                M.call_closure (|
                  M.get_trait_method (|
                    "move_core_types::move_resource::MoveStructType",
                    Self,
                    [],
                    "module_identifier",
                    []
                  |),
                  []
                |));
              ("type_params",
                M.call_closure (|
                  M.get_trait_method (|
                    "move_core_types::move_resource::MoveStructType",
                    Self,
                    [],
                    "type_params",
                    []
                  |),
                  []
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_struct_tag :
      M.IsProvidedMethod "move_core_types::move_resource::MoveStructType" "struct_tag" struct_tag.
  End MoveStructType.
  
  (* Trait *)
  Module MoveResource.
    Definition resource_path
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::language_storage::StructTag",
              "access_vector",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "move_core_types::move_resource::MoveStructType",
                    Self,
                    [],
                    "struct_tag",
                    []
                  |),
                  []
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_resource_path :
      M.IsProvidedMethod
        "move_core_types::move_resource::MoveResource"
        "resource_path"
        resource_path.
  End MoveResource.
End move_resource.
