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

(*
fn division(dividend: i32, divisor: i32) -> i32 {
    if divisor == 0 {
        // Division by zero triggers a panic
        panic!("division by zero");
    } else {
        dividend / divisor
    }
}
*)
Definition division (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ dividend; divisor ] =>
    ltac:(M.monadic
      (let dividend := M.alloc (| dividend |) in
      let divisor := M.alloc (| divisor |) in
      M.read (|
        M.match_operator (|
          M.alloc (| Value.Tuple [] |),
          [
            fun γ =>
              ltac:(M.monadic
                (let γ :=
                  M.use
                    (M.alloc (|
                      BinOp.eq (| M.read (| divisor |), Value.Integer IntegerKind.I32 0 |)
                    |)) in
                let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                M.alloc (|
                  M.never_to_any (|
                    M.call_closure (|
                      M.get_function (|
                        "std::panicking::begin_panic",
                        [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                      |),
                      [ M.read (| Value.String "division by zero" |) ]
                    |)
                  |)
                |)));
            fun γ =>
              ltac:(M.monadic
                (M.alloc (| BinOp.Wrap.div (| M.read (| dividend |), M.read (| divisor |) |) |)))
          ]
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_division : M.IsFunction "panic::division" division.

(*
fn main() {
    // Heap allocated integer
    let _x = Box::new(0i32);

    // This operation will trigger a task failure
    division(3, 0);

    println!("This point won't be reached!");

    // `_x` should get destroyed at this point
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ _x :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.path "i32"; Ty.path "alloc::alloc::Global" ],
                "new",
                []
              |),
              [ Value.Integer IntegerKind.I32 0 ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "panic::division", [] |),
              [ Value.Integer IntegerKind.I32 3; Value.Integer IntegerKind.I32 0 ]
            |)
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [
                      M.alloc (|
                        Value.Array [ M.read (| Value.String "This point won't be reached!
" |) ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_main : M.IsFunction "panic::main" main.
