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

Module handler.
  Module register.
    Axiom EvmHandler :
      forall (EXT DB : Ty.t),
      (Ty.apply (Ty.path "revm::handler::register::EvmHandler") [] [ EXT; DB ]) =
        (Ty.apply
          (Ty.path "revm::handler::Handler")
          []
          [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ]).
    
    Axiom HandleRegister :
      forall (EXT DB : Ty.t),
      (Ty.apply (Ty.path "revm::handler::register::HandleRegister") [] [ EXT; DB ]) =
        (Ty.function
          [
            Ty.apply
              (Ty.path "&mut")
              []
              [
                Ty.apply
                  (Ty.path "revm::handler::Handler")
                  []
                  [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ]
              ]
          ]
          (Ty.tuple [])).
    
    Axiom HandleRegisterBox :
      forall (EXT DB : Ty.t),
      (Ty.apply (Ty.path "revm::handler::register::HandleRegisterBox") [] [ EXT; DB ]) =
        (Ty.apply
          (Ty.path "alloc::boxed::Box")
          []
          [
            Ty.dyn
              [
                ("existential predicate with variables", []);
                ("existential predicate with variables", [])
              ];
            Ty.path "alloc::alloc::Global"
          ]).
    
    (*
    Enum HandleRegisters
    {
      const_params := [];
      ty_params := [ "EXT"; "DB" ];
      variants :=
        [
          {
            name := "Plain";
            item :=
              StructTuple
                [
                  Ty.function
                    [
                      Ty.apply
                        (Ty.path "&mut")
                        []
                        [
                          Ty.apply
                            (Ty.path "revm::handler::Handler")
                            []
                            [ Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ]; EXT; DB ]
                        ]
                    ]
                    (Ty.tuple [])
                ];
            discriminant := None;
          };
          {
            name := "Box";
            item :=
              StructTuple
                [
                  Ty.apply
                    (Ty.path "alloc::boxed::Box")
                    []
                    [
                      Ty.dyn
                        [
                          ("existential predicate with variables", []);
                          ("existential predicate with variables", [])
                        ];
                      Ty.path "alloc::alloc::Global"
                    ]
                ];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_revm_handler_register_HandleRegisters_EXT_DB.
      Definition Self (EXT DB : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm::handler::register::HandleRegisters") [] [ EXT; DB ].
      
      (*
          pub fn register(&self, handler: &mut EvmHandler<'_, EXT, DB>) {
              match self {
                  HandleRegisters::Plain(f) => f(handler),
                  HandleRegisters::Box(f) => f(handler),
              }
          }
      *)
      Definition register
          (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; handler ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let handler := M.alloc (| handler |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm::handler::register::HandleRegisters::Plain",
                          0
                        |) in
                      let f := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (| M.read (| M.read (| f |) |), [ M.read (| handler |) ] |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm::handler::register::HandleRegisters::Box",
                          0
                        |) in
                      let f := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::function::Fn",
                            Ty.apply
                              (Ty.path "alloc::boxed::Box")
                              []
                              [
                                Ty.dyn
                                  [
                                    ("existential predicate with variables", []);
                                    ("existential predicate with variables", [])
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&mut")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "revm::handler::Handler")
                                        []
                                        [
                                          Ty.apply (Ty.path "revm::evm::Evm") [] [ EXT; DB ];
                                          EXT;
                                          DB
                                        ]
                                    ]
                                ]
                            ],
                            "call",
                            []
                          |),
                          [ M.read (| f |); Value.Tuple [ M.read (| handler |) ] ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_register :
        forall (EXT DB : Ty.t),
        M.IsAssociatedFunction (Self EXT DB) "register" (register EXT DB).
    End Impl_revm_handler_register_HandleRegisters_EXT_DB.
  End register.
End handler.
