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

use std::future::Future;

use crate::internal::{
  base::{
    unsafe_create_session,
    unsafe_run_session,
    Context,
    ContextLens,
    Empty,
    EmptyContext,
    PartialSession,
    Protocol,
    Session,
  },
  protocol::End,
};

/*

         cleaner() :: ()
   ===============================
     terminate_async (cleaner) :: · ⊢ 1

   Create a unit protocol (1) out of nothing.
*/

pub fn terminate_async<C, Func, Fut>(cleaner: Func) -> PartialSession<C, End>
where
  C: EmptyContext,
  Func: FnOnce() -> Fut + Send + 'static,
  Fut: Future<Output = ()> + Send,
{
  unsafe_create_session::<C, End, _, _>(move |_, sender| async move {
    cleaner().await;

    sender.send(()).unwrap();
  })
}

pub fn terminate<C>() -> PartialSession<C, End>
where
  C: EmptyContext,
{
  terminate_async(|| async {})
}

pub fn terminate_nil() -> Session<End>
{
  terminate()
}

/*
         cont :: Δ ⊢ P
   ===========================
     wait_async (cont) :: 1, Δ ⊢ P

   Wait for a given input protocol to terminate, then continue as P.
*/

pub fn wait<N, C, A>(
  _: N,
  cont: PartialSession<N::Target, A>,
) -> PartialSession<C, A>
where
  C: Context,
  A: Protocol,
  N: ContextLens<C, End, Empty>,
{
  unsafe_create_session(move |ctx1, sender| async move {
    let (endpoint, ctx2) = N::extract_source(ctx1);

    let receiver = endpoint.get_applied();

    let ctx3 = N::insert_target((), ctx2);

    receiver.recv().await.unwrap();

    unsafe_run_session(cont, ctx3, sender).await;
  })
}