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

(*
fn is_divisible_by(lhs: u32, rhs: u32) -> bool {
    // Corner case, early return
    if rhs == 0 {
        return false;
    }

    // This is an expression, the `return` keyword is not necessary here
    lhs % rhs == 0
}
*)
Definition is_divisible_by (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ lhs; rhs ] =>
    ltac:(M.monadic
      (let lhs := M.alloc (| lhs |) in
      let rhs := M.alloc (| rhs |) 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 (|
                            BinOp.eq (| M.read (| rhs |), Value.Integer IntegerKind.U32 0 |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              BinOp.eq (|
                BinOp.Wrap.rem (| M.read (| lhs |), M.read (| rhs |) |),
                Value.Integer IntegerKind.U32 0
              |)
            |)
          |)))
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_is_divisible_by : M.IsFunction "functions::is_divisible_by" is_divisible_by.

(*
fn fizzbuzz(n: u32) -> () {
    if is_divisible_by(n, 15) {
        println!("fizzbuzz");
    } else if is_divisible_by(n, 3) {
        println!("fizz");
    } else if is_divisible_by(n, 5) {
        println!("buzz");
    } else {
        println!("{}", n);
    }
}
*)
Definition fizzbuzz (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ n ] =>
    ltac:(M.monadic
      (let n := M.alloc (| n |) in
      M.read (|
        M.match_operator (|
          M.alloc (| Value.Tuple [] |),
          [
            fun γ =>
              ltac:(M.monadic
                (let γ :=
                  M.use
                    (M.alloc (|
                      M.call_closure (|
                        M.get_function (| "functions::is_divisible_by", [] |),
                        [ M.read (| n |); Value.Integer IntegerKind.U32 15 ]
                      |)
                    |)) in
                let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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 "fizzbuzz
" |) ] |) ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                M.alloc (| Value.Tuple [] |)));
            fun γ =>
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "functions::is_divisible_by", [] |),
                                [ M.read (| n |); Value.Integer IntegerKind.U32 3 ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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 "fizz
" |) ]
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      M.call_closure (|
                                        M.get_function (| "functions::is_divisible_by", [] |),
                                        [ M.read (| n |); Value.Integer IntegerKind.U32 5 ]
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) 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 "buzz
" |) ]
                                              |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (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_v1",
                                              []
                                            |),
                                            [
                                              M.alloc (|
                                                Value.Array
                                                  [
                                                    M.read (| Value.String "" |);
                                                    M.read (| Value.String "
" |)
                                                  ]
                                              |);
                                              M.alloc (|
                                                Value.Array
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "core::fmt::rt::Argument",
                                                        "new_display",
                                                        [ Ty.path "u32" ]
                                                      |),
                                                      [ n ]
                                                    |)
                                                  ]
                                              |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |) in
                                M.alloc (| Value.Tuple [] |)))
                          ]
                        |)))
                  ]
                |)))
          ]
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_fizzbuzz : M.IsFunction "functions::fizzbuzz" fizzbuzz.

(*
fn fizzbuzz_to(n: u32) {
    for n in 1..=n {
        fizzbuzz(n);
    }
}
*)
Definition fizzbuzz_to (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ n ] =>
    ltac:(M.monadic
      (let n := M.alloc (| n |) in
      M.read (|
        M.use
          (M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::collect::IntoIterator",
                  Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "u32" ],
                  [],
                  "into_iter",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "u32" ],
                      "new",
                      []
                    |),
                    [ Value.Integer IntegerKind.U32 1; M.read (| n |) ]
                  |)
                ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let iter := M.copy (| γ |) in
                  M.loop (|
                    ltac:(M.monadic
                      (let~ _ :=
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeInclusive")
                                  []
                                  [ Ty.path "u32" ],
                                [],
                                "next",
                                []
                              |),
                              [ iter ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let n := M.copy (| γ0_0 |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "functions::fizzbuzz", [] |),
                                      [ M.read (| n |) ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)))
                  |)))
            ]
          |))
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_fizzbuzz_to : M.IsFunction "functions::fizzbuzz_to" fizzbuzz_to.

(*
fn main() {
    // We can use this function here, and define it somewhere later
    fizzbuzz_to(100);
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "functions::fizzbuzz_to", [] |),
              [ Value.Integer IntegerKind.U32 100 ]
            |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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