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

Module cell.
  Module once.
    (* StructRecord
      {
        name := "OnceCell";
        const_params := [];
        ty_params := [ "T" ];
        fields :=
          [
            ("inner",
              Ty.apply
                (Ty.path "core::cell::UnsafeCell")
                []
                [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ])
          ];
      } *)
    
    Module Impl_core_cell_once_OnceCell_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ].
      
      (*
          pub const fn new() -> OnceCell<T> {
              OnceCell { inner: UnsafeCell::new(None) }
          }
      *)
      Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "core::cell::once::OnceCell"
              [
                ("inner",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::cell::UnsafeCell")
                        []
                        [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                      "new",
                      []
                    |),
                    [ Value.StructTuple "core::option::Option::None" [] ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "new" (new T).
      
      (*
          pub fn get(&self) -> Option<&T> {
              // SAFETY: Safe due to `inner`'s invariant
              unsafe { &*self.inner.get() }.as_ref()
          }
      *)
      Definition get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::option::Option") [] [ T ],
                "as_ref",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::cell::UnsafeCell")
                      []
                      [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                    "get",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::cell::once::OnceCell",
                      "inner"
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get" (get T).
      
      (*
          pub fn get_mut(&mut self) -> Option<&mut T> {
              self.inner.get_mut().as_mut()
          }
      *)
      Definition get_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::option::Option") [] [ T ],
                "as_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::cell::UnsafeCell")
                      []
                      [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                    "get_mut",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::cell::once::OnceCell",
                      "inner"
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_mut" (get_mut T).
      
      (*
          pub fn set(&self, value: T) -> Result<(), T> {
              match self.try_insert(value) {
                  Ok(_) => Ok(()),
                  Err((_, value)) => Err(value),
              }
          }
      *)
      Definition set (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let value := M.alloc (| value |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                      "try_insert",
                      []
                    |),
                    [ M.read (| self |); M.read (| value |) ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Err",
                          0
                        |) in
                      let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                      let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                      let value := M.copy (| γ1_1 |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Err" [ M.read (| value |) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_set :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "set" (set T).
      
      (*
          pub fn try_insert(&self, value: T) -> Result<&T, (&T, T)> {
              if let Some(old) = self.get() {
                  return Err((old, value));
              }
      
              // SAFETY: This is the only place where we set the slot, no races
              // due to reentrancy/concurrency are possible, and we've
              // checked that slot is currently `None`, so this write
              // maintains the `inner`'s invariant.
              let slot = unsafe { &mut *self.inner.get() };
              Ok(slot.insert(value))
          }
      *)
      Definition try_insert (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let value := M.alloc (| value |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                                    "get",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let old := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [ Value.Tuple [ M.read (| old |); M.read (| value |) ] ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ slot :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::cell::UnsafeCell")
                            []
                            [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                          "get",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::cell::once::OnceCell",
                            "inner"
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::option::Option") [] [ T ],
                            "insert",
                            []
                          |),
                          [ M.read (| slot |); M.read (| value |) ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_try_insert :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "try_insert" (try_insert T).
      
      (*
          pub fn get_or_init<F>(&self, f: F) -> &T
          where
              F: FnOnce() -> T,
          {
              match self.get_or_try_init(|| Ok::<T, !>(f())) {
                  Ok(val) => val,
              }
          }
      *)
      Definition get_or_init (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ 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 (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                      "get_or_try_init",
                      [
                        Ty.function
                          [ Ty.tuple [] ]
                          (Ty.apply (Ty.path "core::result::Result") [] [ T; Ty.path "never" ]);
                        Ty.path "never"
                      ]
                    |),
                    [
                      M.read (| self |);
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (Value.StructTuple
                                          "core::result::Result::Ok"
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnOnce",
                                                F,
                                                [ Ty.tuple [] ],
                                                "call_once",
                                                []
                                              |),
                                              [ M.read (| f |); Value.Tuple [] ]
                                            |)
                                          ]))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let val := M.copy (| γ0_0 |) in
                      M.alloc (| M.read (| val |) |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_or_init :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_or_init" (get_or_init T).
      
      (*
          pub fn get_mut_or_init<F>(&mut self, f: F) -> &mut T
          where
              F: FnOnce() -> T,
          {
              match self.get_mut_or_try_init(|| Ok::<T, !>(f())) {
                  Ok(val) => val,
              }
          }
      *)
      Definition get_mut_or_init
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ 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 (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                      "get_mut_or_try_init",
                      [
                        Ty.function
                          [ Ty.tuple [] ]
                          (Ty.apply (Ty.path "core::result::Result") [] [ T; Ty.path "never" ]);
                        Ty.path "never"
                      ]
                    |),
                    [
                      M.read (| self |);
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (Value.StructTuple
                                          "core::result::Result::Ok"
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnOnce",
                                                F,
                                                [ Ty.tuple [] ],
                                                "call_once",
                                                []
                                              |),
                                              [ M.read (| f |); Value.Tuple [] ]
                                            |)
                                          ]))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let val := M.copy (| γ0_0 |) in
                      M.alloc (| M.read (| val |) |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_mut_or_init :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_mut_or_init" (get_mut_or_init T).
      
      (*
          pub fn get_or_try_init<F, E>(&self, f: F) -> Result<&T, E>
          where
              F: FnOnce() -> Result<T, E>,
          {
              if let Some(val) = self.get() {
                  return Ok(val);
              }
              self.try_init(f)
          }
      *)
      Definition get_or_try_init
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F; E ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                                    "get",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Ok"
                                      [ M.read (| val |) ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                        "try_init",
                        [ F; E ]
                      |),
                      [ M.read (| self |); M.read (| f |) ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_or_try_init :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_or_try_init" (get_or_try_init T).
      
      (*
          pub fn get_mut_or_try_init<F, E>(&mut self, f: F) -> Result<&mut T, E>
          where
              F: FnOnce() -> Result<T, E>,
          {
              if self.get().is_none() {
                  self.try_init(f)?;
              }
              Ok(self.get_mut().unwrap())
          }
      *)
      Definition get_mut_or_try_init
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F; E ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.apply (Ty.path "&") [] [ T ] ],
                                      "is_none",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::cell::once::OnceCell")
                                              []
                                              [ T ],
                                            "get",
                                            []
                                          |),
                                          [ M.read (| self |) ]
                                        |)
                                      |)
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::try_trait::Try",
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [ Ty.apply (Ty.path "&") [] [ T ]; E ],
                                      [],
                                      "branch",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                                          "try_init",
                                          [ F; E ]
                                        |),
                                        [ M.read (| self |); M.read (| f |) ]
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Break",
                                          0
                                        |) in
                                      let residual := M.copy (| γ0_0 |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::FromResidual",
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [ Ty.apply (Ty.path "&mut") [] [ T ]; E ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [ Ty.path "core::convert::Infallible"; E ]
                                                  ],
                                                  "from_residual",
                                                  []
                                                |),
                                                [ M.read (| residual |) ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Continue",
                                          0
                                        |) in
                                      let val := M.copy (| γ0_0 |) in
                                      val))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                            "unwrap",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                                "get_mut",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_mut_or_try_init :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_mut_or_try_init" (get_mut_or_try_init T).
      
      (*
          fn try_init<F, E>(&self, f: F) -> Result<&T, E>
          where
              F: FnOnce() -> Result<T, E>,
          {
              let val = f()?;
              // Note that *some* forms of reentrant initialization might lead to
              // UB (see `reentrant_init` test). I believe that just removing this
              // `panic`, while keeping `try_insert` would be sound, but it seems
              // better to panic, rather than to silently use an old value.
              if let Ok(val) = self.try_insert(val) { Ok(val) } else { panic!("reentrant init") }
          }
      *)
      Definition try_init (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F; E ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ val :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              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
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [ Ty.apply (Ty.path "&") [] [ T ]; E ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              []
                                              [ Ty.path "core::convert::Infallible"; E ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |) in
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                                  "try_insert",
                                  []
                                |),
                                [ M.read (| self |); M.read (| val |) ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::result::Result::Ok",
                              0
                            |) in
                          let val := M.copy (| γ0_0 |) in
                          M.alloc (|
                            Value.StructTuple "core::result::Result::Ok" [ M.read (| val |) ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.never_to_any (|
                              M.call_closure (|
                                M.get_function (| "core::panicking::panic_fmt", [] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::Arguments",
                                      "new_const",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        Value.Array [ M.read (| Value.String "reentrant init" |) ]
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |)
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_try_init :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "try_init" (try_init T).
      
      (*
          pub const fn into_inner(self) -> Option<T> {
              // Because `into_inner` takes `self` by value, the compiler statically verifies
              // that it is not currently borrowed. So it is safe to move out `Option<T>`.
              self.inner.into_inner()
          }
      *)
      Definition into_inner (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::cell::UnsafeCell")
                  []
                  [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                "into_inner",
                []
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::cell::once::OnceCell",
                    "inner"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_into_inner :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).
      
      (*
          pub fn take(&mut self) -> Option<T> {
              mem::take(self).into_inner()
          }
      *)
      Definition take (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                "into_inner",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (|
                    "core::mem::take",
                    [ Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ] ]
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_take :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "take" (take T).
    End Impl_core_cell_once_OnceCell_T.
    
    Module Impl_core_default_Default_for_core_cell_once_OnceCell_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ].
      
      (*
          fn default() -> Self {
              Self::new()
          }
      *)
      Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                "new",
                []
              |),
              []
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::default::Default"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    End Impl_core_default_Default_for_core_cell_once_OnceCell_T.
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_cell_once_OnceCell_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              let mut d = f.debug_tuple("OnceCell");
              match self.get() {
                  Some(v) => d.field(v),
                  None => d.field(&format_args!("<uninit>")),
              };
              d.finish()
          }
      *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              let~ d :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::Formatter",
                      "debug_tuple",
                      []
                    |),
                    [ M.read (| f |); M.read (| Value.String "OnceCell" |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                        "get",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let v := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::builders::DebugTuple",
                              "field",
                              []
                            |),
                            [ d; M.read (| v |) ]
                          |)
                        |)));
                    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::builders::DebugTuple",
                              "field",
                              []
                            |),
                            [
                              d;
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::Arguments",
                                    "new_const",
                                    []
                                  |),
                                  [
                                    M.alloc (|
                                      Value.Array [ M.read (| Value.String "<uninit>" |) ]
                                    |)
                                  ]
                                |)
                              |)
                            ]
                          |)
                        |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugTuple",
                    "finish",
                    []
                  |),
                  [ d ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_cell_once_OnceCell_T.
    
    Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_cell_once_OnceCell_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ].
      
      (*
          fn clone(&self) -> OnceCell<T> {
              let res = OnceCell::new();
              if let Some(value) = self.get() {
                  match res.set(value.clone()) {
                      Ok(()) => (),
                      Err(_) => unreachable!(),
                  }
              }
              res
          }
      *)
      Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ res :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                      "new",
                      []
                    |),
                    []
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                                "get",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |) in
                        let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let value := M.copy (| γ0_0 |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                                "set",
                                []
                              |),
                              [
                                res;
                                M.call_closure (|
                                  M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                                  [ M.read (| value |) ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::result::Result::Ok",
                                    0
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::result::Result::Err",
                                    0
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic", [] |),
                                      [
                                        M.read (|
                                          Value.String "internal error: entered unreachable code"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)))
                          ]
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              res
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
    End Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_cell_once_OnceCell_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_for_core_cell_once_OnceCell_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ].
      
      (*
          fn eq(&self, other: &Self) -> bool {
              self.get() == other.get()
          }
      *)
      Definition eq (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
                [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ]
                ],
                "eq",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                      "get",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |);
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ],
                      "get",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method (eq T)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_for_core_cell_once_OnceCell_T.
    
    Module Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_core_cell_once_OnceCell_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_core_cell_once_OnceCell_T.
    
    Module Impl_core_convert_From_T_for_core_cell_once_OnceCell_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ].
      
      (*
          fn from(value: T) -> Self {
              OnceCell { inner: UnsafeCell::new(Some(value)) }
          }
      *)
      Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ value ] =>
          ltac:(M.monadic
            (let value := M.alloc (| value |) in
            Value.StructRecord
              "core::cell::once::OnceCell"
              [
                ("inner",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::cell::UnsafeCell")
                        []
                        [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                      "new",
                      []
                    |),
                    [ Value.StructTuple "core::option::Option::Some" [ M.read (| value |) ] ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) T ]
          (* Instance *) [ ("from", InstanceField.Method (from T)) ].
    End Impl_core_convert_From_T_for_core_cell_once_OnceCell_T.
    
    Module Impl_core_marker_Sync_for_core_cell_once_OnceCell_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::once::OnceCell") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::marker::Sync"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Sync_for_core_cell_once_OnceCell_T.
  End once.
End cell.
