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

(*
fn call(number: &str) -> &str {
    match number {
        "798-1364" => {
            "We're sorry, the call cannot be completed as dialed. 
            Please hang up and try again."
        }
        "645-7689" => {
            "Hello, this is Mr. Awesome's Pizza. My name is Fred.
            What can I get for you today?"
        }
        _ => "Hi! Who is this again?",
    }
}
*)
Definition call (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ number ] =>
    ltac:(M.monadic
      (let number := M.alloc (| number |) in
      M.read (|
        M.match_operator (|
          number,
          [
            fun γ =>
              ltac:(M.monadic
                (let _ :=
                  M.is_constant_or_break_match (| M.read (| γ |), Value.String "798-1364" |) in
                M.alloc (|
                  M.read (|
                    Value.String
                      "We're sorry, the call cannot be completed as dialed. 
            Please hang up and try again."
                  |)
                |)));
            fun γ =>
              ltac:(M.monadic
                (let _ :=
                  M.is_constant_or_break_match (| M.read (| γ |), Value.String "645-7689" |) in
                M.alloc (|
                  M.read (|
                    Value.String
                      "Hello, this is Mr. Awesome's Pizza. My name is Fred.
            What can I get for you today?"
                  |)
                |)));
            fun γ =>
              ltac:(M.monadic (M.alloc (| M.read (| Value.String "Hi! Who is this again?" |) |)))
          ]
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_call : M.IsFunction "hash_map::call" call.

(*
fn main() {
    let mut contacts = HashMap::new();

    contacts.insert("Daniel", "798-1364");
    contacts.insert("Ashley", "645-7689");
    contacts.insert("Katie", "435-8291");
    contacts.insert("Robert", "956-1745");

    // Takes a reference and returns Option<&V>
    match contacts.get(&"Daniel") {
        Some(&number) => println!("Calling Daniel: {}", call(number)),
        _ => println!("Don't have Daniel's number."),
    }

    // `HashMap::insert()` returns `None`
    // if the inserted value is new, `Some(value)` otherwise
    contacts.insert("Daniel", "164-6743");

    match contacts.get(&"Ashley") {
        Some(&number) => println!("Calling Ashley: {}", call(number)),
        _ => println!("Don't have Ashley's number."),
    }

    contacts.remove(&"Ashley");

    // `HashMap::iter()` returns an iterator that yields
    // (&'a key, &'a value) pairs in arbitrary order.
    for (contact, &number) in contacts.iter() {
        println!("Calling {}: {}", contact, call(number));
    }
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ contacts :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.path "std::hash::random::RandomState"
                  ],
                "new",
                []
              |),
              []
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.path "std::hash::random::RandomState"
                  ],
                "insert",
                []
              |),
              [ contacts; M.read (| Value.String "Daniel" |); M.read (| Value.String "798-1364" |) ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.path "std::hash::random::RandomState"
                  ],
                "insert",
                []
              |),
              [ contacts; M.read (| Value.String "Ashley" |); M.read (| Value.String "645-7689" |) ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.path "std::hash::random::RandomState"
                  ],
                "insert",
                []
              |),
              [ contacts; M.read (| Value.String "Katie" |); M.read (| Value.String "435-8291" |) ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.path "std::hash::random::RandomState"
                  ],
                "insert",
                []
              |),
              [ contacts; M.read (| Value.String "Robert" |); M.read (| Value.String "956-1745" |) ]
            |)
          |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "std::collections::hash::map::HashMap")
                    []
                    [
                      Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                      Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                      Ty.path "std::hash::random::RandomState"
                    ],
                  "get",
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                |),
                [ contacts; Value.String "Daniel" ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                  let γ0_0 := M.read (| γ0_0 |) in
                  let number := M.copy (| γ0_0 |) in
                  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 "Calling Daniel: " |);
                                    M.read (| Value.String "
" |)
                                  ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (| "hash_map::call", [] |),
                                            [ M.read (| number |) ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ =>
                ltac:(M.monadic
                  (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 "Don't have Daniel's number.
" |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.path "std::hash::random::RandomState"
                  ],
                "insert",
                []
              |),
              [ contacts; M.read (| Value.String "Daniel" |); M.read (| Value.String "164-6743" |) ]
            |)
          |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "std::collections::hash::map::HashMap")
                    []
                    [
                      Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                      Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                      Ty.path "std::hash::random::RandomState"
                    ],
                  "get",
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                |),
                [ contacts; Value.String "Ashley" ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                  let γ0_0 := M.read (| γ0_0 |) in
                  let number := M.copy (| γ0_0 |) in
                  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 "Calling Ashley: " |);
                                    M.read (| Value.String "
" |)
                                  ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (| "hash_map::call", [] |),
                                            [ M.read (| number |) ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ =>
                ltac:(M.monadic
                  (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 "Don't have Ashley's number.
" |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                    Ty.path "std::hash::random::RandomState"
                  ],
                "remove",
                [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
              |),
              [ contacts; Value.String "Ashley" ]
            |)
          |) in
        M.use
          (M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::collect::IntoIterator",
                  Ty.apply
                    (Ty.path "std::collections::hash::map::Iter")
                    []
                    [
                      Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                      Ty.apply (Ty.path "&") [] [ Ty.path "str" ]
                    ],
                  [],
                  "into_iter",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                          Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      "iter",
                      []
                    |),
                    [ contacts ]
                  |)
                ]
              |)
            |),
            [
              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 "std::collections::hash::map::Iter")
                                  []
                                  [
                                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ]
                                  ],
                                [],
                                "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 contact := M.copy (| γ1_0 |) in
                                let γ1_1 := M.read (| γ1_1 |) in
                                let number := 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 "Calling " |);
                                                    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.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [ Ty.path "str" ]
                                                            ]
                                                        ]
                                                      |),
                                                      [ contact ]
                                                    |);
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "core::fmt::rt::Argument",
                                                        "new_display",
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [ Ty.path "str" ]
                                                        ]
                                                      |),
                                                      [
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "hash_map::call",
                                                              []
                                                            |),
                                                            [ M.read (| number |) ]
                                                          |)
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                              |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |) in
                                M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)))
                  |)))
            ]
          |))
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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