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

use async_std::task;
use async_macros::join;
use std::future::{ Future };
use async_std::sync::{ channel };

use crate::protocol::{ SendValue };

use crate::base::{
  Protocol,
  Context,
  ContextLens,
  PartialSession,
  unsafe_run_session,
  unsafe_create_session,
};

pub fn send_value
  < T, C, A >
  ( val : T,
    cont : PartialSession < C, A >
  ) ->
    PartialSession <
      C,
      SendValue < T, A >
    >
where
  T : Send + 'static,
  A : Protocol,
  C : Context
{
  unsafe_create_session (
    move | ctx, sender1 | async move {
      let (sender2, receiver2) = channel(1);

      let child1 = task::spawn(async move {
        sender1.send(
          SendValue
            ( val,
              receiver2
            ) ).await;
      });

      let child2 = task::spawn(async move {
        unsafe_run_session
          ( cont, ctx, sender2
          ).await;
      });

      join!(child1, child2).await;
    })
}

/*
        cont_builder(x) :: Q, Δ ⊢ P    x :: T
    ================================================
      receive_value_from(cont_builder) :: T ∧ Q, Δ ⊢ P
 */
pub fn receive_value_from
  < N, C, T, A, B, Fut >
  ( _ : N,
    cont : impl
      FnOnce ( T ) -> Fut
      + Send + 'static
  ) ->
    PartialSession < C, B >
where
  A : Protocol,
  B : Protocol,
  C : Context,
  T : Send + 'static,
  Fut :
    Future <
      Output =
        PartialSession <
          N :: Target,
          B
        >
    > + Send,
  N :
    ContextLens <
      C,
      SendValue < T, A >,
      A
    >
{
  unsafe_create_session (
    move | ctx1, sender | async move {
      let (receiver1, ctx2) =
        N :: extract_source ( ctx1 );

      let SendValue ( val, receiver2 )
        = receiver1.recv().await.unwrap();

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

      let cont2 = cont(val).await;

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