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

(*
pub fn add(a: i32, b: i32) -> i32 {
    a + b
}
*)
Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ a; b ] =>
    ltac:(M.monadic
      (let a := M.alloc (| a |) in
      let b := M.alloc (| b |) in
      BinOp.Wrap.add (| M.read (| a |), M.read (| b |) |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_add : M.IsFunction "unit_testing::add" add.

(*
fn bad_add(a: i32, b: i32) -> i32 {
    a - b
}
*)
Definition bad_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ a; b ] =>
    ltac:(M.monadic
      (let a := M.alloc (| a |) in
      let b := M.alloc (| b |) in
      BinOp.Wrap.sub (| M.read (| a |), M.read (| b |) |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_bad_add : M.IsFunction "unit_testing::bad_add" bad_add.

Module tests.
  (*
      fn test_add() {
          assert_eq!(add(1, 2), 3);
      }
  *)
  Definition test_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (|
                Value.Tuple
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "unit_testing::add", [] |),
                        [ Value.Integer IntegerKind.I32 1; Value.Integer IntegerKind.I32 2 ]
                      |)
                    |);
                    M.alloc (| Value.Integer IntegerKind.I32 3 |)
                  ]
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let left_val := M.copy (| γ0_0 |) in
                    let right_val := M.copy (| γ0_1 |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    BinOp.eq (|
                                      M.read (| M.read (| left_val |) |),
                                      M.read (| M.read (| right_val |) |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ kind :=
                                    M.alloc (|
                                      Value.StructTuple "core::panicking::AssertKind::Eq" []
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::panicking::assert_failed",
                                        [ Ty.path "i32"; Ty.path "i32" ]
                                      |),
                                      [
                                        M.read (| kind |);
                                        M.read (| left_val |);
                                        M.read (| right_val |);
                                        Value.StructTuple "core::option::Option::None" []
                                      ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |)))
              ]
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_test_add : M.IsFunction "unit_testing::tests::test_add'1" test_add.
  
  (*
      fn test_bad_add() {
          // This assert would fire and test will fail.
          // Please note, that private functions can be tested too!
          assert_eq!(bad_add(1, 2), 3);
      }
  *)
  Definition test_bad_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (|
                Value.Tuple
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "unit_testing::bad_add", [] |),
                        [ Value.Integer IntegerKind.I32 1; Value.Integer IntegerKind.I32 2 ]
                      |)
                    |);
                    M.alloc (| Value.Integer IntegerKind.I32 3 |)
                  ]
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let left_val := M.copy (| γ0_0 |) in
                    let right_val := M.copy (| γ0_1 |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    BinOp.eq (|
                                      M.read (| M.read (| left_val |) |),
                                      M.read (| M.read (| right_val |) |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ kind :=
                                    M.alloc (|
                                      Value.StructTuple "core::panicking::AssertKind::Eq" []
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::panicking::assert_failed",
                                        [ Ty.path "i32"; Ty.path "i32" ]
                                      |),
                                      [
                                        M.read (| kind |);
                                        M.read (| left_val |);
                                        M.read (| right_val |);
                                        Value.StructTuple "core::option::Option::None" []
                                      ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |)))
              ]
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_test_bad_add : M.IsFunction "unit_testing::tests::test_bad_add'1" test_bad_add.
End tests.
