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

Module asserting.
  (* StructTuple
    {
      name := "TryCaptureWithoutDebug";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  (* Trait *)
  (* Empty module 'TryCaptureGeneric' *)
  
  Module Impl_core_asserting_TryCaptureGeneric_E_core_asserting_TryCaptureWithoutDebug_for_ref__core_asserting_Wrapper_ref__E.
    Definition Self (E : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "&")
        []
        [ Ty.apply (Ty.path "core::asserting::Wrapper") [] [ Ty.apply (Ty.path "&") [] [ E ] ] ].
    
    (*     fn try_capture(&self, _: &mut Capture<E, TryCaptureWithoutDebug>) {} *)
    Definition try_capture (E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self E in
      match ε, τ, α with
      | [], [], [ self; β1 ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (| β1, [ fun γ => ltac:(M.monadic (Value.Tuple [])) ] |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (E : Ty.t),
      M.IsTraitInstance
        "core::asserting::TryCaptureGeneric"
        (Self E)
        (* Trait polymorphic types *)
        [ (* E *) E; (* M *) Ty.path "core::asserting::TryCaptureWithoutDebug" ]
        (* Instance *) [ ("try_capture", InstanceField.Method (try_capture E)) ].
  End Impl_core_asserting_TryCaptureGeneric_E_core_asserting_TryCaptureWithoutDebug_for_ref__core_asserting_Wrapper_ref__E.
  
  Module Impl_core_fmt_Debug_for_core_asserting_Capture_E_core_asserting_TryCaptureWithoutDebug.
    Definition Self (E : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "core::asserting::Capture")
        []
        [ E; Ty.path "core::asserting::TryCaptureWithoutDebug" ].
    
    (*
        fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), core::fmt::Error> {
            f.write_str("N/A")
        }
    *)
    Definition fmt (E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self E in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [ M.read (| f |); M.read (| Value.String "N/A" |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (E : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self E)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt E)) ].
  End Impl_core_fmt_Debug_for_core_asserting_Capture_E_core_asserting_TryCaptureWithoutDebug.
  
  (* StructTuple
    {
      name := "TryCaptureWithDebug";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  (* Trait *)
  (* Empty module 'TryCapturePrintable' *)
  
  Module Impl_core_asserting_TryCapturePrintable_where_core_asserting_Printable_E_E_core_asserting_TryCaptureWithDebug_for_core_asserting_Wrapper_ref__E.
    Definition Self (E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::asserting::Wrapper") [] [ Ty.apply (Ty.path "&") [] [ E ] ].
    
    (*
        fn try_capture(&self, to: &mut Capture<E, TryCaptureWithDebug>) {
            to.elem = Some( *self.0);
        }
    *)
    Definition try_capture (E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self E in
      match ε, τ, α with
      | [], [], [ self; to ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let to := M.alloc (| to |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| to |),
                  "core::asserting::Capture",
                  "elem"
                |),
                Value.StructTuple
                  "core::option::Option::Some"
                  [
                    M.read (|
                      M.read (|
                        M.SubPointer.get_struct_tuple_field (|
                          M.read (| self |),
                          "core::asserting::Wrapper",
                          0
                        |)
                      |)
                    |)
                  ]
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (E : Ty.t),
      M.IsTraitInstance
        "core::asserting::TryCapturePrintable"
        (Self E)
        (* Trait polymorphic types *)
        [ (* E *) E; (* M *) Ty.path "core::asserting::TryCaptureWithDebug" ]
        (* Instance *) [ ("try_capture", InstanceField.Method (try_capture E)) ].
  End Impl_core_asserting_TryCapturePrintable_where_core_asserting_Printable_E_E_core_asserting_TryCaptureWithDebug_for_core_asserting_Wrapper_ref__E.
  
  Module Impl_core_fmt_Debug_where_core_asserting_Printable_E_for_core_asserting_Capture_E_core_asserting_TryCaptureWithDebug.
    Definition Self (E : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "core::asserting::Capture")
        []
        [ E; Ty.path "core::asserting::TryCaptureWithDebug" ].
    
    (*
        fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), core::fmt::Error> {
            match self.elem {
                None => f.write_str("N/A"),
                Some(ref value) => Debug::fmt(value, f),
            }
        }
    *)
    Definition fmt (E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self E in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::asserting::Capture",
                "elem"
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "N/A" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let value := M.alloc (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::fmt::Debug", E, [], "fmt", [] |),
                        [ M.read (| value |); M.read (| f |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (E : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self E)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt E)) ].
  End Impl_core_fmt_Debug_where_core_asserting_Printable_E_for_core_asserting_Capture_E_core_asserting_TryCaptureWithDebug.
  
  (* StructRecord
    {
      name := "Capture";
      const_params := [];
      ty_params := [ "E"; "M_" ];
      fields :=
        [
          ("elem", Ty.apply (Ty.path "core::option::Option") [] [ E ]);
          ("phantom", Ty.apply (Ty.path "core::marker::PhantomData") [] [ M_ ])
        ];
    } *)
  
  Module Impl_core_asserting_Capture_M__T.
    Definition Self (M_ T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::asserting::Capture") [] [ M_; T ].
    
    (*
        pub const fn new() -> Self {
            Self { elem: None, phantom: PhantomData }
        }
    *)
    Definition new (M_ T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self M_ T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "core::asserting::Capture"
            [
              ("elem", Value.StructTuple "core::option::Option::None" []);
              ("phantom", Value.StructTuple "core::marker::PhantomData" [])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new :
      forall (M_ T : Ty.t),
      M.IsAssociatedFunction (Self M_ T) "new" (new M_ T).
  End Impl_core_asserting_Capture_M__T.
  
  (* StructTuple
    {
      name := "Wrapper";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ T ];
    } *)
  
  (* Trait *)
  (* Empty module 'Printable' *)
  
  Module Impl_core_asserting_Printable_where_core_marker_Copy_T_where_core_fmt_Debug_T_for_T.
    Definition Self (T : Ty.t) : Ty.t := T.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::asserting::Printable"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_asserting_Printable_where_core_marker_Copy_T_where_core_fmt_Debug_T_for_T.
End asserting.
