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

(*
fn main() {
    // This is our data to process.
    // We will calculate the sum of all digits via a threaded  map-reduce algorithm.
    // Each whitespace separated chunk will be handled in a different thread.
    //
    // TODO: see what happens to the output if you insert spaces!
    let data = "86967897737416471853297327050364959
11861322575564723963297542624962850
70856234701860851907960690014725639
38397966707106094172783238747669219
52380795257888236525459303330302837
58495327135744041048897885734297812
69920216438980873548808413720956532
16278424637452589860345374828574668";

    // Make a vector to hold the child-threads which we will spawn.
    let mut children = vec![];

    /*************************************************************************
     * "Map" phase
     *
     * Divide our data into segments, and apply initial processing
     ************************************************************************/

    // split our data into segments for individual calculation
    // each chunk will be a reference (&str) into the actual data
    let chunked_data = data.split_whitespace();

    // Iterate over the data segments.
    // .enumerate() adds the current loop index to whatever is iterated
    // the resulting tuple "(index, element)" is then immediately
    // "destructured" into two variables, "i" and "data_segment" with a
    // "destructuring assignment"
    for (i, data_segment) in chunked_data.enumerate() {
        println!("data segment {} is \"{}\"", i, data_segment);

        // Process each data segment in a separate thread
        //
        // spawn() returns a handle to the new thread,
        // which we MUST keep to access the returned value
        //
        // 'move || -> u32' is syntax for a closure that:
        // * takes no arguments ('||')
        // * takes ownership of its captured variables ('move') and
        // * returns an unsigned 32-bit integer ('-> u32')
        //
        // Rust is smart enough to infer the '-> u32' from
        // the closure itself so we could have left that out.
        //
        // TODO: try removing the 'move' and see what happens
        children.push(thread::spawn(move || -> u32 {
            // Calculate the intermediate sum of this segment:
            let result = data_segment
                // iterate over the characters of our segment..
                .chars()
                // .. convert text-characters to their number value..
                .map(|c| c.to_digit(10).expect("should be a digit"))
                // .. and sum the resulting iterator of numbers
                .sum();

            // println! locks stdout, so no text-interleaving occurs
            println!("processed segment {}, result={}", i, result);

            // "return" not needed, because Rust is an "expression language", the
            // last evaluated expression in each block is automatically its value.
            result
        }));
    }

    /*************************************************************************
     * "Reduce" phase
     *
     * Collect our intermediate results, and combine them into a final result
     ************************************************************************/

    // combine each thread's intermediate results into a single final sum.
    //
    // we use the "turbofish" ::<> to provide sum() with a type hint.
    //
    // TODO: try without the turbofish, by instead explicitly
    // specifying the type of final_result
    let final_result = children.into_iter().map(|c| c.join().unwrap()).sum::<u32>();

    println!("Final sum result: {}", final_result);
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ data :=
          M.copy (|
            Value.String
              "86967897737416471853297327050364959
11861322575564723963297542624962850
70856234701860851907960690014725639
38397966707106094172783238747669219
52380795257888236525459303330302837
58495327135744041048897885734297812
69920216438980873548808413720956532
16278424637452589860345374828574668"
          |) in
        let~ children :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply (Ty.path "std::thread::JoinHandle") [] [ Ty.path "u32" ];
                    Ty.path "alloc::alloc::Global"
                  ],
                "new",
                []
              |),
              []
            |)
          |) in
        let~ chunked_data :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "str", "split_whitespace", [] |),
              [ M.read (| data |) ]
            |)
          |) in
        let~ _ :=
          M.use
            (M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::IntoIterator",
                    Ty.apply
                      (Ty.path "core::iter::adapters::enumerate::Enumerate")
                      []
                      [ Ty.path "core::str::iter::SplitWhitespace" ],
                    [],
                    "into_iter",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.path "core::str::iter::SplitWhitespace",
                        [],
                        "enumerate",
                        []
                      |),
                      [ M.read (| chunked_data |) ]
                    |)
                  ]
                |)
              |),
              [
                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::iter::adapters::enumerate::Enumerate")
                                    []
                                    [ Ty.path "core::str::iter::SplitWhitespace" ],
                                  [],
                                  "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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                  let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                  let i := M.copy (| γ1_0 |) in
                                  let data_segment := M.copy (| γ1_1 |) 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_v1",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (| Value.String "data segment " |);
                                                      M.read (| Value.String " is """ |);
                                                      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 "usize" ]
                                                        |),
                                                        [ i ]
                                                      |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_display",
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [ Ty.path "str" ]
                                                          ]
                                                        |),
                                                        [ data_segment ]
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "std::thread::JoinHandle")
                                                []
                                                [ Ty.path "u32" ];
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "push",
                                          []
                                        |),
                                        [
                                          children;
                                          M.call_closure (|
                                            M.get_function (|
                                              "std::thread::spawn",
                                              [
                                                Ty.function [ Ty.tuple [] ] (Ty.path "u32");
                                                Ty.path "u32"
                                              ]
                                            |),
                                            [
                                              M.closure
                                                (fun γ =>
                                                  ltac:(M.monadic
                                                    match γ with
                                                    | [ α0 ] =>
                                                      ltac:(M.monadic
                                                        (M.match_operator (|
                                                          M.alloc (| α0 |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.read (|
                                                                  let~ result :=
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::iter::traits::iterator::Iterator",
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::iter::adapters::map::Map")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "core::str::iter::Chars";
                                                                              Ty.function
                                                                                [
                                                                                  Ty.tuple
                                                                                    [ Ty.path "char"
                                                                                    ]
                                                                                ]
                                                                                (Ty.path "u32")
                                                                            ],
                                                                          [],
                                                                          "sum",
                                                                          [ Ty.path "u32" ]
                                                                        |),
                                                                        [
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::iter::traits::iterator::Iterator",
                                                                              Ty.path
                                                                                "core::str::iter::Chars",
                                                                              [],
                                                                              "map",
                                                                              [
                                                                                Ty.path "u32";
                                                                                Ty.function
                                                                                  [
                                                                                    Ty.tuple
                                                                                      [
                                                                                        Ty.path
                                                                                          "char"
                                                                                      ]
                                                                                  ]
                                                                                  (Ty.path "u32")
                                                                              ]
                                                                            |),
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.path "str",
                                                                                  "chars",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (|
                                                                                    data_segment
                                                                                  |)
                                                                                ]
                                                                              |);
                                                                              M.closure
                                                                                (fun γ =>
                                                                                  ltac:(M.monadic
                                                                                    match γ with
                                                                                    | [ α0 ] =>
                                                                                      ltac:(M.monadic
                                                                                        (M.match_operator (|
                                                                                          M.alloc (|
                                                                                            α0
                                                                                          |),
                                                                                          [
                                                                                            fun γ =>
                                                                                              ltac:(M.monadic
                                                                                                (let
                                                                                                      c :=
                                                                                                  M.copy (|
                                                                                                    γ
                                                                                                  |) in
                                                                                                M.call_closure (|
                                                                                                  M.get_associated_function (|
                                                                                                    Ty.apply
                                                                                                      (Ty.path
                                                                                                        "core::option::Option")
                                                                                                      []
                                                                                                      [
                                                                                                        Ty.path
                                                                                                          "u32"
                                                                                                      ],
                                                                                                    "expect",
                                                                                                    []
                                                                                                  |),
                                                                                                  [
                                                                                                    M.call_closure (|
                                                                                                      M.get_associated_function (|
                                                                                                        Ty.path
                                                                                                          "char",
                                                                                                        "to_digit",
                                                                                                        []
                                                                                                      |),
                                                                                                      [
                                                                                                        M.read (|
                                                                                                          c
                                                                                                        |);
                                                                                                        Value.Integer
                                                                                                          IntegerKind.U32
                                                                                                          10
                                                                                                      ]
                                                                                                    |);
                                                                                                    M.read (|
                                                                                                      Value.String
                                                                                                        "should be a digit"
                                                                                                    |)
                                                                                                  ]
                                                                                                |)))
                                                                                          ]
                                                                                        |)))
                                                                                    | _ =>
                                                                                      M.impossible
                                                                                        "wrong number of arguments"
                                                                                    end))
                                                                            ]
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |) 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_v1",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.alloc (|
                                                                                  Value.Array
                                                                                    [
                                                                                      M.read (|
                                                                                        Value.String
                                                                                          "processed segment "
                                                                                      |);
                                                                                      M.read (|
                                                                                        Value.String
                                                                                          ", result="
                                                                                      |);
                                                                                      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
                                                                                              "usize"
                                                                                          ]
                                                                                        |),
                                                                                        [ i ]
                                                                                      |);
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.path
                                                                                            "core::fmt::rt::Argument",
                                                                                          "new_display",
                                                                                          [
                                                                                            Ty.path
                                                                                              "u32"
                                                                                          ]
                                                                                        |),
                                                                                        [ result ]
                                                                                      |)
                                                                                    ]
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |) in
                                                                  result
                                                                |)))
                                                          ]
                                                        |)))
                                                    | _ => M.impossible "wrong number of arguments"
                                                    end))
                                            ]
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                    |)))
              ]
            |)) in
        let~ final_result :=
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::iter::adapters::map::Map")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::into_iter::IntoIter")
                      []
                      [
                        Ty.apply (Ty.path "std::thread::JoinHandle") [] [ Ty.path "u32" ];
                        Ty.path "alloc::alloc::Global"
                      ];
                    Ty.function
                      [
                        Ty.tuple
                          [ Ty.apply (Ty.path "std::thread::JoinHandle") [] [ Ty.path "u32" ] ]
                      ]
                      (Ty.path "u32")
                  ],
                [],
                "sum",
                [ Ty.path "u32" ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Ty.apply
                      (Ty.path "alloc::vec::into_iter::IntoIter")
                      []
                      [
                        Ty.apply (Ty.path "std::thread::JoinHandle") [] [ Ty.path "u32" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "map",
                    [
                      Ty.path "u32";
                      Ty.function
                        [
                          Ty.tuple
                            [ Ty.apply (Ty.path "std::thread::JoinHandle") [] [ Ty.path "u32" ] ]
                        ]
                        (Ty.path "u32")
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply (Ty.path "std::thread::JoinHandle") [] [ Ty.path "u32" ];
                            Ty.path "alloc::alloc::Global"
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [ M.read (| children |) ]
                    |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let c := M.copy (| γ |) in
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "u32";
                                              Ty.apply
                                                (Ty.path "alloc::boxed::Box")
                                                []
                                                [
                                                  Ty.dyn
                                                    [
                                                      ("core::any::Any::Trait", []);
                                                      ("core::marker::Send::AutoTrait", [])
                                                    ];
                                                  Ty.path "alloc::alloc::Global"
                                                ]
                                            ],
                                          "unwrap",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "std::thread::JoinHandle")
                                                []
                                                [ Ty.path "u32" ],
                                              "join",
                                              []
                                            |),
                                            [ M.read (| c |) ]
                                          |)
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |)
              ]
            |)
          |) 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_v1", [] |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (| Value.String "Final sum result: " |);
                            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" ]
                              |),
                              [ final_result ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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