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

Module resolver.
  (* Trait *)
  Module LinkageResolver.
    Definition link_context
        (Self : Ty.t)
        (ε : 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.get_constant (| "move_core_types::account_address::ZERO" |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_link_context :
      M.IsProvidedMethod "move_core_types::resolver::LinkageResolver" "link_context" link_context.
    Definition relocate (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; module_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let module_id := M.alloc (| module_id |) in
          Value.StructTuple
            "core::result::Result::Ok"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.path "move_core_types::language_storage::ModuleId",
                  [],
                  "clone",
                  []
                |),
                [ M.read (| module_id |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_relocate :
      M.IsProvidedMethod "move_core_types::resolver::LinkageResolver" "relocate" relocate.
    Definition defining_module
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; module_id; _struct ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let module_id := M.alloc (| module_id |) in
          let _struct := M.alloc (| _struct |) in
          Value.StructTuple
            "core::result::Result::Ok"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.path "move_core_types::language_storage::ModuleId",
                  [],
                  "clone",
                  []
                |),
                [ M.read (| module_id |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_defining_module :
      M.IsProvidedMethod
        "move_core_types::resolver::LinkageResolver"
        "defining_module"
        defining_module.
  End LinkageResolver.
  
  (* Trait *)
  (* Empty module 'ModuleResolver' *)
  
  (* Trait *)
  (* Empty module 'ResourceResolver' *)
  
  (* Trait *)
  (* Empty module 'MoveResolver' *)
  
  Module Impl_move_core_types_resolver_MoveResolver_where_core_fmt_Debug_E_where_move_core_types_resolver_LinkageResolver_T_where_move_core_types_resolver_ModuleResolver_T_where_move_core_types_resolver_ResourceResolver_T_where_core_marker_Sized_T_for_T.
    Definition Self (E T : Ty.t) : Ty.t := T.
    
    (*     type Err = E; *)
    Definition _Err (E T : Ty.t) : Ty.t := E.
    
    Axiom Implements :
      forall (E T : Ty.t),
      M.IsTraitInstance
        "move_core_types::resolver::MoveResolver"
        (Self E T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("Err", InstanceField.Ty (_Err E T)) ].
  End Impl_move_core_types_resolver_MoveResolver_where_core_fmt_Debug_E_where_move_core_types_resolver_LinkageResolver_T_where_move_core_types_resolver_ModuleResolver_T_where_move_core_types_resolver_ResourceResolver_T_where_core_marker_Sized_T_for_T.
  
  Module Impl_move_core_types_resolver_ResourceResolver_where_move_core_types_resolver_ResourceResolver_T_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*     type Error = T::Error; *)
    Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
    
    (*
        fn get_resource(
            &self,
            address: &AccountAddress,
            tag: &StructTag,
        ) -> Result<Option<Vec<u8>>, Self::Error> {
            ( **self).get_resource(address, tag)
        }
    *)
    Definition get_resource (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; address; tag ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let address := M.alloc (| address |) in
          let tag := M.alloc (| tag |) in
          M.call_closure (|
            M.get_trait_method (|
              "move_core_types::resolver::ResourceResolver",
              T,
              [],
              "get_resource",
              []
            |),
            [ M.read (| M.read (| self |) |); M.read (| address |); M.read (| tag |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "move_core_types::resolver::ResourceResolver"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Error", InstanceField.Ty (_Error T));
          ("get_resource", InstanceField.Method (get_resource T))
        ].
  End Impl_move_core_types_resolver_ResourceResolver_where_move_core_types_resolver_ResourceResolver_T_where_core_marker_Sized_T_for_ref__T.
  
  Module Impl_move_core_types_resolver_ModuleResolver_where_move_core_types_resolver_ModuleResolver_T_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*     type Error = T::Error; *)
    Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
    
    (*
        fn get_module(&self, module_id: &ModuleId) -> Result<Option<Vec<u8>>, Self::Error> {
            ( **self).get_module(module_id)
        }
    *)
    Definition get_module (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; module_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let module_id := M.alloc (| module_id |) in
          M.call_closure (|
            M.get_trait_method (|
              "move_core_types::resolver::ModuleResolver",
              T,
              [],
              "get_module",
              []
            |),
            [ M.read (| M.read (| self |) |); M.read (| module_id |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "move_core_types::resolver::ModuleResolver"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Error", InstanceField.Ty (_Error T));
          ("get_module", InstanceField.Method (get_module T))
        ].
  End Impl_move_core_types_resolver_ModuleResolver_where_move_core_types_resolver_ModuleResolver_T_where_core_marker_Sized_T_for_ref__T.
  
  Module Impl_move_core_types_resolver_ModuleResolver_where_move_core_types_resolver_ModuleResolver_T_where_core_marker_Sized_T_for_alloc_sync_Arc_T_alloc_alloc_Global.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "alloc::sync::Arc") [] [ T; Ty.path "alloc::alloc::Global" ].
    
    (*     type Error = T::Error; *)
    Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
    
    (*
        fn get_module(&self, module_id: &ModuleId) -> Result<Option<Vec<u8>>, Self::Error> {
            ( **self).get_module(module_id)
        }
    *)
    Definition get_module (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; module_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let module_id := M.alloc (| module_id |) in
          M.call_closure (|
            M.get_trait_method (|
              "move_core_types::resolver::ModuleResolver",
              T,
              [],
              "get_module",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "alloc::sync::Arc") [] [ T; Ty.path "alloc::alloc::Global" ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.read (| module_id |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "move_core_types::resolver::ModuleResolver"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Error", InstanceField.Ty (_Error T));
          ("get_module", InstanceField.Method (get_module T))
        ].
  End Impl_move_core_types_resolver_ModuleResolver_where_move_core_types_resolver_ModuleResolver_T_where_core_marker_Sized_T_for_alloc_sync_Arc_T_alloc_alloc_Global.
  
  Module Impl_move_core_types_resolver_LinkageResolver_where_move_core_types_resolver_LinkageResolver_T_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*     type Error = T::Error; *)
    Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
    
    (*
        fn link_context(&self) -> AccountAddress {
            ( **self).link_context()
        }
    *)
    Definition link_context (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "move_core_types::resolver::LinkageResolver",
              T,
              [],
              "link_context",
              []
            |),
            [ M.read (| M.read (| self |) |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn relocate(&self, module_id: &ModuleId) -> Result<ModuleId, Self::Error> {
            ( **self).relocate(module_id)
        }
    *)
    Definition relocate (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; module_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let module_id := M.alloc (| module_id |) in
          M.call_closure (|
            M.get_trait_method (|
              "move_core_types::resolver::LinkageResolver",
              T,
              [],
              "relocate",
              []
            |),
            [ M.read (| M.read (| self |) |); M.read (| module_id |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn defining_module(
            &self,
            module_id: &ModuleId,
            struct_: &IdentStr,
        ) -> Result<ModuleId, Self::Error> {
            ( **self).defining_module(module_id, struct_)
        }
    *)
    Definition defining_module
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; module_id; struct_ ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let module_id := M.alloc (| module_id |) in
          let struct_ := M.alloc (| struct_ |) in
          M.call_closure (|
            M.get_trait_method (|
              "move_core_types::resolver::LinkageResolver",
              T,
              [],
              "defining_module",
              []
            |),
            [ M.read (| M.read (| self |) |); M.read (| module_id |); M.read (| struct_ |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "move_core_types::resolver::LinkageResolver"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Error", InstanceField.Ty (_Error T));
          ("link_context", InstanceField.Method (link_context T));
          ("relocate", InstanceField.Method (relocate T));
          ("defining_module", InstanceField.Method (defining_module T))
        ].
  End Impl_move_core_types_resolver_LinkageResolver_where_move_core_types_resolver_LinkageResolver_T_where_core_marker_Sized_T_for_ref__T.
End resolver.
