1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181

use std::time::Duration;

use ferrite_session::prelude::*;
use tokio::time::sleep;

pub struct MushroomSoup {}

pub struct TomatoSoup {}

pub struct BeefSteak {}

pub struct PorkChop {}

define_choice! {
  SoupMenu ;
  MushroomMenu: SendValue < MushroomSoup, End >,
  TomatoMenu: SendValue < TomatoSoup, End >,
}

define_choice! {
  MainMenu ;
  BeefMenu: SendValue < BeefSteak, End >,
  PorkMenu: SendValue < PorkChop, End >,
}

pub fn restaurant_session() -> Session<End>
{
  let soup_of_the_day: Session<InternalChoice<SoupMenu>> = offer_case(
    MushroomMenuLabel,
    step(async move {
      send_value(
        {
          println!("[Soup] Spending 3 seconds to prepare mushroom soup");

          sleep(Duration::from_secs(2)).await;

          println!("[Soup] Finished preparing mushroom soup");

          MushroomSoup {}
        },
        terminate_async(|| async {
          println!("[Soup] Served mushroom soup. Terminating soup protocol");
        }),
      )
    }),
  );

  let main_dish: Session<ExternalChoice<MainMenu>> = offer_choice! {
    BeefMenu => {
      println!("[MainCourse] Customer chose to eat beef steak");

      step(async move {
        println!("[MainCourse] Spending 7 seconds to prepare beef steak");
        sleep(Duration::from_secs(7)).await;

        send_value(BeefSteak{},
          terminate_async (|| async {
            println!("[MainCourse] Served beef steak. Terminating main course protocol");
          }))
      })
    }
    PorkMenu => {
      println!("[MainCourse] Customer chose to eat pork chop");

      println!("[MainCourse] Spending 5 seconds to prepare pork chop");
      sleep(Duration::from_secs(5)).await;

      send_value (PorkChop{},
        terminate_async (|| async {
          println!("[MainCourse] Served pork chop. Terminating main course protocol");
        }) )
    }
  };

  let menu: Session<
    SendChannel<InternalChoice<SoupMenu>, ExternalChoice<MainMenu>>,
  > = include_session(soup_of_the_day, |chan| {
    send_channel_from(chan, partial_session(main_dish))
  });

  let diner: Session<
    ReceiveChannel<
      SendChannel<InternalChoice<SoupMenu>, ExternalChoice<MainMenu>>,
      End,
    >,
  > = receive_channel(|menu_chan| {
    receive_channel_from(menu_chan, |soup_chan| {
      case! { soup_chan ;
          MushroomMenu => {
            println!("[Diner] Restaurant offers mushroom soup today");

            receive_value_from ( soup_chan, move |_mushroom_soup| {
              println!("[Diner] Received mushroom soup. Spending 2 seconds drinking it");

              step(async move {
                sleep(Duration::from_secs(2)).await;
                println!("[Diner] Finished drinking mushroom soup");

                println!("[Diner] Choosing pork chop for main");

                wait(soup_chan,
                  step(async move {
                    println!("[Diner] Soup protocol terminated");

                    choose! ( menu_chan, PorkMenu,
                      receive_value_from ( menu_chan, move |_pork_chop| {
                        println!("[Diner] Received pork chop. Spending 5 seconds eating it");

                        step(async move {
                          sleep(Duration::from_secs(5)).await;
                          println!("[Diner] Finished eating pork chop");

                          wait( menu_chan,
                            step(async move {
                              println!("[Diner] Main course protocol terminated");

                              terminate_async (|| async {
                                println!("[Diner] Spending 4 seconds in washroom");
                                sleep(Duration::from_secs(4)).await;
                                println!("[Diner] Leaving restaurant");
                              })
                            }))
                        })
                      })
                    )
                  }))
              })
            })
          }
          TomatoMenu => {
            println!("[Diner] Restaurant offers tomato soup today");

            receive_value_from( soup_chan, move |_tomato_soup| {
              println!("[Diner] Received tomato soup. Spending 1 second drinking it");

              step(async move {
                sleep(Duration::from_secs(1)).await;

                println!("[Diner] finished drinking tomato soup");
                println!("[Diner] Choosing beef steak for main");

                wait ( soup_chan, {
                  println!("[Diner] Soup protocol terminated");

                  choose! ( menu_chan, BeefMenu,
                    receive_value_from( menu_chan, move |_beef_steak| {
                      println!("[Diner] Received beef steak. Spending 6 seconds eating it");

                      step(async move {
                        sleep(Duration::from_secs(6)).await;
                        println!("[Diner] Finished eating beef steak.");

                        wait ( menu_chan,
                          step(async move {
                            println!("[Diner] Main course protocol terminated");

                            terminate_async (|| async {
                              println!("[Diner] Spending 3 seconds in washroom");
                              sleep(Duration::from_secs(3)).await;
                              println!("[Diner] Leaving restaurant");
                            })
                          }))
                      })
                    }))
                })
              })
            })
          }
      }
    })
  });

  apply_channel(diner, menu)
}

#[tokio::main]

pub async fn main()
{
  run_session(restaurant_session()).await;
}