ferrite_session/internal/session/
end.rs

1use std::future::Future;
2
3use crate::internal::{
4  base::{
5    unsafe_create_session,
6    unsafe_run_session,
7    Context,
8    ContextLens,
9    Empty,
10    EmptyContext,
11    PartialSession,
12    Protocol,
13    Session,
14  },
15  protocol::End,
16};
17
18/*
19
20         cleaner() :: ()
21   ===============================
22     terminate_async (cleaner) :: · ⊢ 1
23
24   Create a unit protocol (1) out of nothing.
25*/
26
27pub fn terminate_async<C, Func, Fut>(cleaner: Func) -> PartialSession<C, End>
28where
29  C: EmptyContext,
30  Func: FnOnce() -> Fut + Send + 'static,
31  Fut: Future<Output = ()> + Send,
32{
33  unsafe_create_session::<C, End, _, _>(move |_, sender| async move {
34    cleaner().await;
35
36    sender.send(()).unwrap();
37  })
38}
39
40pub fn terminate<C>() -> PartialSession<C, End>
41where
42  C: EmptyContext,
43{
44  terminate_async(|| async {})
45}
46
47pub fn terminate_nil() -> Session<End>
48{
49  terminate()
50}
51
52/*
53         cont :: Δ ⊢ P
54   ===========================
55     wait_async (cont) :: 1, Δ ⊢ P
56
57   Wait for a given input protocol to terminate, then continue as P.
58*/
59
60pub fn wait<N, C, A>(
61  _: N,
62  cont: PartialSession<N::Target, A>,
63) -> PartialSession<C, A>
64where
65  C: Context,
66  A: Protocol,
67  N: ContextLens<C, End, Empty>,
68{
69  unsafe_create_session(move |ctx1, sender| async move {
70    let (endpoint, ctx2) = N::extract_source(ctx1);
71
72    let receiver = endpoint.get_applied();
73
74    let ctx3 = N::insert_target((), ctx2);
75
76    receiver.recv().await.unwrap();
77
78    unsafe_run_session(cont, ctx3, sender).await;
79  })
80}
ferrite_session/internal/session/end.rs

ferrite_session/internal/session/
end.rs
