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

Module dummy.
  (* StructTuple
    {
      name := "DummyMeter";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  Module Impl_move_bytecode_verifier_meter_Meter_for_move_bytecode_verifier_meter_dummy_DummyMeter.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier_meter::dummy::DummyMeter".
    
    (*     fn enter_scope(&mut self, _name: &str, _scope: Scope) {} *)
    Definition enter_scope (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; _name; _scope ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let _name := M.alloc (| _name |) in
          let _scope := M.alloc (| _scope |) in
          Value.Tuple []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn transfer(&mut self, _from: Scope, _to: Scope, _factor: f32) -> PartialVMResult<()> {
            Ok(())
        }
    *)
    Definition transfer (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; _from; _to; _factor ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let _from := M.alloc (| _from |) in
          let _to := M.alloc (| _to |) in
          let _factor := M.alloc (| _factor |) in
          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn add(&mut self, _scope: Scope, _units: u128) -> PartialVMResult<()> {
            Ok(())
        }
    *)
    Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; _scope; _units ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let _scope := M.alloc (| _scope |) in
          let _units := M.alloc (| _units |) in
          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "move_bytecode_verifier_meter::Meter"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("enter_scope", InstanceField.Method enter_scope);
          ("transfer", InstanceField.Method transfer);
          ("add", InstanceField.Method add)
        ].
  End Impl_move_bytecode_verifier_meter_Meter_for_move_bytecode_verifier_meter_dummy_DummyMeter.
End dummy.
