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

Module context.
  (* StructRecord
    {
      name := "Context";
      const_params := [];
      ty_params := [ "EXT"; "DB" ];
      fields :=
        [
          ("evm", Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ]);
          ("external", EXT)
        ];
    } *)
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_EXT_where_revm_primitives_db_Database_DB_where_core_clone_Clone_DB_where_core_clone_Clone_associated_type_for_revm_context_Context_EXT_DB.
    Definition Self (EXT DB : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ].
    
    (*
        fn clone(&self) -> Self {
            Self {
                evm: self.evm.clone(),
                external: self.external.clone(),
            }
        }
    *)
    Definition clone (EXT DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self EXT DB in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "revm::context::Context"
            [
              ("evm",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::Context",
                      "evm"
                    |)
                  ]
                |));
              ("external",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", EXT, [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::Context",
                      "external"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (EXT DB : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self EXT DB)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone EXT DB)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_EXT_where_revm_primitives_db_Database_DB_where_core_clone_Clone_DB_where_core_clone_Clone_associated_type_for_revm_context_Context_EXT_DB.
  
  Module Impl_core_default_Default_for_revm_context_Context_Tuple__revm_db_emptydb_EmptyDBTyped_core_convert_Infallible.
    Definition Self : Ty.t :=
      Ty.apply
        (Ty.path "revm::context::Context")
        []
        [
          Ty.tuple [];
          Ty.apply
            (Ty.path "revm::db::emptydb::EmptyDBTyped")
            []
            [ Ty.path "core::convert::Infallible" ]
        ].
    
    (*
        fn default() -> Self {
            Self::new_empty()
        }
    *)
    Definition default (ε : 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 "revm::context::Context")
                []
                [
                  Ty.tuple [];
                  Ty.apply
                    (Ty.path "revm::db::emptydb::EmptyDBTyped")
                    []
                    [ Ty.path "core::convert::Infallible" ]
                ],
              "new_empty",
              []
            |),
            []
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::default::Default"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method default) ].
  End Impl_core_default_Default_for_revm_context_Context_Tuple__revm_db_emptydb_EmptyDBTyped_core_convert_Infallible.
  
  Module Impl_revm_context_Context_Tuple__revm_db_emptydb_EmptyDBTyped_core_convert_Infallible.
    Definition Self : Ty.t :=
      Ty.apply
        (Ty.path "revm::context::Context")
        []
        [
          Ty.tuple [];
          Ty.apply
            (Ty.path "revm::db::emptydb::EmptyDBTyped")
            []
            [ Ty.path "core::convert::Infallible" ]
        ].
    
    (*
        pub fn new_empty() -> Context<(), EmptyDB> {
            Context {
                evm: EvmContext::new(EmptyDB::new()),
                external: (),
            }
        }
    *)
    Definition new_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm::context::Context"
            [
              ("evm",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "revm::context::evm_context::EvmContext")
                      []
                      [
                        Ty.apply
                          (Ty.path "revm::db::emptydb::EmptyDBTyped")
                          []
                          [ Ty.path "core::convert::Infallible" ]
                      ],
                    "new",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "revm::db::emptydb::EmptyDBTyped")
                          []
                          [ Ty.path "core::convert::Infallible" ],
                        "new",
                        []
                      |),
                      []
                    |)
                  ]
                |));
              ("external", Value.Tuple [])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_empty : M.IsAssociatedFunction Self "new_empty" new_empty.
  End Impl_revm_context_Context_Tuple__revm_db_emptydb_EmptyDBTyped_core_convert_Infallible.
  
  Module Impl_revm_context_Context_Tuple__DB.
    Definition Self (DB : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "revm::context::Context") [] [ Ty.tuple []; DB ].
    
    (*
        pub fn new_with_db(db: DB) -> Context<(), DB> {
            Context {
                evm: EvmContext::new_with_env(db, Box::default()),
                external: (),
            }
        }
    *)
    Definition new_with_db (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self DB in
      match ε, τ, α with
      | [], [], [ db ] =>
        ltac:(M.monadic
          (let db := M.alloc (| db |) in
          Value.StructRecord
            "revm::context::Context"
            [
              ("evm",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "revm::context::evm_context::EvmContext") [] [ DB ],
                    "new_with_env",
                    []
                  |),
                  [
                    M.read (| db |);
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |)
                  ]
                |));
              ("external", Value.Tuple [])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_with_db :
      forall (DB : Ty.t),
      M.IsAssociatedFunction (Self DB) "new_with_db" (new_with_db DB).
  End Impl_revm_context_Context_Tuple__DB.
  
  Module Impl_revm_context_Context_EXT_DB.
    Definition Self (EXT DB : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ].
    
    (*
        pub fn new(evm: EvmContext<DB>, external: EXT) -> Context<EXT, DB> {
            Context { evm, external }
        }
    *)
    Definition new (EXT DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self EXT DB in
      match ε, τ, α with
      | [], [], [ evm; external ] =>
        ltac:(M.monadic
          (let evm := M.alloc (| evm |) in
          let external := M.alloc (| external |) in
          Value.StructRecord
            "revm::context::Context"
            [ ("evm", M.read (| evm |)); ("external", M.read (| external |)) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "new" (new EXT DB).
  End Impl_revm_context_Context_EXT_DB.
  
  (* StructRecord
    {
      name := "ContextWithHandlerCfg";
      const_params := [];
      ty_params := [ "EXT"; "DB" ];
      fields :=
        [
          ("context", Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ]);
          ("cfg", Ty.path "revm_primitives::env::handler_cfg::HandlerCfg")
        ];
    } *)
  
  Module Impl_revm_context_ContextWithHandlerCfg_EXT_DB.
    Definition Self (EXT DB : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "revm::context::ContextWithHandlerCfg") [] [ EXT; DB ].
    
    (*
        pub fn new(context: Context<EXT, DB>, cfg: HandlerCfg) -> Self {
            Self { cfg, context }
        }
    *)
    Definition new (EXT DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self EXT DB in
      match ε, τ, α with
      | [], [], [ context; cfg ] =>
        ltac:(M.monadic
          (let context := M.alloc (| context |) in
          let cfg := M.alloc (| cfg |) in
          Value.StructRecord
            "revm::context::ContextWithHandlerCfg"
            [ ("cfg", M.read (| cfg |)); ("context", M.read (| context |)) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new :
      forall (EXT DB : Ty.t),
      M.IsAssociatedFunction (Self EXT DB) "new" (new EXT DB).
  End Impl_revm_context_ContextWithHandlerCfg_EXT_DB.
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_EXT_where_revm_primitives_db_Database_DB_where_core_clone_Clone_DB_where_core_clone_Clone_associated_type_for_revm_context_ContextWithHandlerCfg_EXT_DB.
    Definition Self (EXT DB : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "revm::context::ContextWithHandlerCfg") [] [ EXT; DB ].
    
    (*
        fn clone(&self) -> Self {
            Self {
                context: self.context.clone(),
                cfg: self.cfg,
            }
        }
    *)
    Definition clone (EXT DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self EXT DB in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "revm::context::ContextWithHandlerCfg"
            [
              ("context",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::context::ContextWithHandlerCfg",
                      "context"
                    |)
                  ]
                |));
              ("cfg",
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::context::ContextWithHandlerCfg",
                    "cfg"
                  |)
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (EXT DB : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self EXT DB)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone EXT DB)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_EXT_where_revm_primitives_db_Database_DB_where_core_clone_Clone_DB_where_core_clone_Clone_associated_type_for_revm_context_ContextWithHandlerCfg_EXT_DB.
End context.
