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

(*
fn main() {
    let mut a: HashSet<i32> = vec![1i32, 2, 3].into_iter().collect();
    let mut b: HashSet<i32> = vec![2i32, 3, 4].into_iter().collect();

    assert!(a.insert(4));
    assert!(a.contains(&4));

    // `HashSet::insert()` returns false if
    // there was a value already present.
    // assert!(b.insert(4), "Value 4 is already in set B!");
    // FIXME ^ Comment out this line

    b.insert(5);

    // If a collection's element type implements `Debug`,
    // then the collection implements `Debug`.
    // It usually prints its elements in the format `[elem1, elem2, ...]`
    println!("A: {:?}", a);
    println!("B: {:?}", b);

    // Print [1, 2, 3, 4, 5] in arbitrary order
    println!("Union: {:?}", a.union(&b).collect::<Vec<&i32>>());

    // This should print [1]
    println!("Difference: {:?}", a.difference(&b).collect::<Vec<&i32>>());

    // Print [2, 3, 4] in arbitrary order.
    println!(
        "Intersection: {:?}",
        a.intersection(&b).collect::<Vec<&i32>>()
    );

    // Print [1, 5]
    println!(
        "Symmetric Difference: {:?}",
        a.symmetric_difference(&b).collect::<Vec<&i32>>()
    );
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ a :=
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "alloc::vec::into_iter::IntoIter")
                  []
                  [ Ty.path "i32"; Ty.path "alloc::alloc::Global" ],
                [],
                "collect",
                [
                  Ty.apply
                    (Ty.path "std::collections::hash::set::HashSet")
                    []
                    [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ]
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::IntoIterator",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "i32"; Ty.path "alloc::alloc::Global" ],
                    [],
                    "into_iter",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "i32" ],
                        "into_vec",
                        [ Ty.path "alloc::alloc::Global" ]
                      |),
                      [
                        M.read (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::boxed::Box")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 3 ]
                                    [ Ty.path "i32" ];
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "new",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [
                                    Value.Integer IntegerKind.I32 1;
                                    Value.Integer IntegerKind.I32 2;
                                    Value.Integer IntegerKind.I32 3
                                  ]
                              |)
                            ]
                          |)
                        |)
                      ]
                    |)
                  ]
                |)
              ]
            |)
          |) in
        let~ b :=
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "alloc::vec::into_iter::IntoIter")
                  []
                  [ Ty.path "i32"; Ty.path "alloc::alloc::Global" ],
                [],
                "collect",
                [
                  Ty.apply
                    (Ty.path "std::collections::hash::set::HashSet")
                    []
                    [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ]
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::IntoIterator",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "i32"; Ty.path "alloc::alloc::Global" ],
                    [],
                    "into_iter",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "i32" ],
                        "into_vec",
                        [ Ty.path "alloc::alloc::Global" ]
                      |),
                      [
                        M.read (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::boxed::Box")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 3 ]
                                    [ Ty.path "i32" ];
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "new",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [
                                    Value.Integer IntegerKind.I32 2;
                                    Value.Integer IntegerKind.I32 3;
                                    Value.Integer IntegerKind.I32 4
                                  ]
                              |)
                            ]
                          |)
                        |)
                      ]
                    |)
                  ]
                |)
              ]
            |)
          |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        UnOp.not (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "std::collections::hash::set::HashSet")
                                []
                                [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ],
                              "insert",
                              []
                            |),
                            [ a; Value.Integer IntegerKind.I32 4 ]
                          |)
                        |)
                      |)) 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 (| "core::panicking::panic", [] |),
                        [ M.read (| Value.String "assertion failed: a.insert(4)" |) ]
                      |)
                    |)
                  |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        UnOp.not (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "std::collections::hash::set::HashSet")
                                []
                                [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ],
                              "contains",
                              [ Ty.path "i32" ]
                            |),
                            [ a; M.alloc (| Value.Integer IntegerKind.I32 4 |) ]
                          |)
                        |)
                      |)) 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 (| "core::panicking::panic", [] |),
                        [ M.read (| Value.String "assertion failed: a.contains(&4)" |) ]
                      |)
                    |)
                  |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "std::collections::hash::set::HashSet")
                  []
                  [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ],
                "insert",
                []
              |),
              [ b; Value.Integer IntegerKind.I32 5 ]
            |)
          |) 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 "A: " |); M.read (| Value.String "
" |) ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_debug",
                                [
                                  Ty.apply
                                    (Ty.path "std::collections::hash::set::HashSet")
                                    []
                                    [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ]
                                ]
                              |),
                              [ a ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) 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 "B: " |); M.read (| Value.String "
" |) ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_debug",
                                [
                                  Ty.apply
                                    (Ty.path "std::collections::hash::set::HashSet")
                                    []
                                    [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ]
                                ]
                              |),
                              [ b ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) 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 "Union: " |); M.read (| Value.String "
" |) ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_debug",
                                [
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.apply (Ty.path "&") [] [ Ty.path "i32" ];
                                      Ty.path "alloc::alloc::Global"
                                    ]
                                ]
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "std::collections::hash::set::Union")
                                        []
                                        [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ],
                                      [],
                                      "collect",
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.apply (Ty.path "&") [] [ Ty.path "i32" ];
                                            Ty.path "alloc::alloc::Global"
                                          ]
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "std::collections::hash::set::HashSet")
                                            []
                                            [
                                              Ty.path "i32";
                                              Ty.path "std::hash::random::RandomState"
                                            ],
                                          "union",
                                          []
                                        |),
                                        [ a; b ]
                                      |)
                                    ]
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) 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 "Difference: " |); M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_debug",
                                [
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.apply (Ty.path "&") [] [ Ty.path "i32" ];
                                      Ty.path "alloc::alloc::Global"
                                    ]
                                ]
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "std::collections::hash::set::Difference")
                                        []
                                        [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ],
                                      [],
                                      "collect",
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.apply (Ty.path "&") [] [ Ty.path "i32" ];
                                            Ty.path "alloc::alloc::Global"
                                          ]
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "std::collections::hash::set::HashSet")
                                            []
                                            [
                                              Ty.path "i32";
                                              Ty.path "std::hash::random::RandomState"
                                            ],
                                          "difference",
                                          []
                                        |),
                                        [ a; b ]
                                      |)
                                    ]
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) 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 "Intersection: " |);
                            M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_debug",
                                [
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.apply (Ty.path "&") [] [ Ty.path "i32" ];
                                      Ty.path "alloc::alloc::Global"
                                    ]
                                ]
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "std::collections::hash::set::Intersection")
                                        []
                                        [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ],
                                      [],
                                      "collect",
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.apply (Ty.path "&") [] [ Ty.path "i32" ];
                                            Ty.path "alloc::alloc::Global"
                                          ]
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "std::collections::hash::set::HashSet")
                                            []
                                            [
                                              Ty.path "i32";
                                              Ty.path "std::hash::random::RandomState"
                                            ],
                                          "intersection",
                                          []
                                        |),
                                        [ a; b ]
                                      |)
                                    ]
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) 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 "Symmetric Difference: " |);
                            M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_debug",
                                [
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.apply (Ty.path "&") [] [ Ty.path "i32" ];
                                      Ty.path "alloc::alloc::Global"
                                    ]
                                ]
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "std::collections::hash::set::SymmetricDifference")
                                        []
                                        [ Ty.path "i32"; Ty.path "std::hash::random::RandomState" ],
                                      [],
                                      "collect",
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.apply (Ty.path "&") [] [ Ty.path "i32" ];
                                            Ty.path "alloc::alloc::Global"
                                          ]
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "std::collections::hash::set::HashSet")
                                            []
                                            [
                                              Ty.path "i32";
                                              Ty.path "std::hash::random::RandomState"
                                            ],
                                          "symmetric_difference",
                                          []
                                        |),
                                        [ a; b ]
                                      |)
                                    ]
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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