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

(* StructTuple
  {
    name := "LoopA";
    const_params := [];
    ty_params := [];
    fields := [];
  } *)

Module Impl_mutual_loop_LoopA.
  Definition Self : Ty.t := Ty.path "mutual_loop::LoopA".
  
  (*
      pub(crate) fn new() -> Self {
          LoopA {}
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] => ltac:(M.monadic (Value.StructTuple "mutual_loop::LoopA" []))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      pub(crate) fn start_loop(&self) -> LoopB {
          LoopB::start_loop()
      }
  *)
  Definition start_loop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "mutual_loop::LoopB", "start_loop", [] |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_start_loop : M.IsAssociatedFunction Self "start_loop" start_loop.
End Impl_mutual_loop_LoopA.

(*
Enum LoopB
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Item";
        item := StructRecord [ ("ident", Ty.path "mutual_loop::LoopA") ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_mutual_loop_LoopB.
  Definition Self : Ty.t := Ty.path "mutual_loop::LoopB".
  
  (*
      pub(crate) fn start_loop() -> Self {
          LoopB::Item {
              ident: LoopA::new(),
          }
      }
  *)
  Definition start_loop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "mutual_loop::LoopB::Item"
          [
            ("ident",
              M.call_closure (|
                M.get_associated_function (| Ty.path "mutual_loop::LoopA", "new", [] |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_start_loop : M.IsAssociatedFunction Self "start_loop" start_loop.
End Impl_mutual_loop_LoopB.

(*
pub fn start_loop() {
    // The following code would bypass the compiler and crash the `rustc` thread
    let la = LoopA::new();
    let lb = la.start_loop();
}
*)
Definition start_loop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ la :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "mutual_loop::LoopA", "new", [] |),
              []
            |)
          |) in
        let~ lb :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "mutual_loop::LoopA", "start_loop", [] |),
              [ la ]
            |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_start_loop : M.IsFunction "mutual_loop::start_loop" start_loop.
