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

Module bool.
  Module Impl_bool.
    Definition Self : Ty.t := Ty.path "bool".
    
    (*
        pub fn then_some<T>(self, t: T) -> Option<T> {
            if self { Some(t) } else { None }
        }
    *)
    Definition then_some (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self; t ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let t := M.alloc (| t |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use self in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| t |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_then_some : M.IsAssociatedFunction Self "then_some" then_some.
    
    (*
        pub fn then<T, F: FnOnce() -> T>(self, f: F) -> Option<T> {
            if self { Some(f()) } else { None }
        }
    *)
    Definition then_ (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T; F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use self in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| f |); Value.Tuple [] ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_then_ : M.IsAssociatedFunction Self "then_" then_.
  End Impl_bool.
End bool.
