sesstype 0.2.4

An implementation of Multiparty Session Types
Documentation 
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

# sesstype

[![Build Status](https://travis-ci.org/nickng/sesstype.rs.svg?branch=master)](https://travis-ci.org/nickng/sesstype.rs)
[![Crates.io Version](https://img.shields.io/crates/v/sesstype.svg)](https://crates.io/crates/sesstype)


This is an implementation of Multiparty Session Types in Rust.
The `sesstype` crate contains core data structures and utility functions
to model and manipulate a multiparty session type language.

## Build

The best way to build this library is by Rust's `cargo` package manager.

```
$ cargo build
```

## Usage

See the documentation for details usage.

```
$ cargo doc --open
```

### Quickstart

Given the following source code (with the correct dependencies):

```rust
extern crate sesstype;

fn main() {
    let alice = sesstype::Role::new("Alice"); // Alice role
    let bob = sesstype::Role::new("Bob"); // Bob role

    // Creates an interaction between alice and bob (without message/continuation)
    let g0 = sesstype::global::Type::interaction(&alice, &bob);
    let global_type = sesstype::global::Type::add_message(
        g0,
        sesstype::Message::new("lab"), // Message (with "lab" as label)
        sesstype::global::Type::end(), // Continuation
    );

    let local_type = sesstype::project(&global_type, &bob);
    match local_type {
        Some(l) => {
            println!("Global type G: {}", global_type.to_string());
            println!("Local Type G@Bob: {}", l.to_string());
        }
        None => println!("Cannot project: {}", global_type.to_string()),
    }
}
```

Should give the following output:
```
$ cargo run
Global type G: Alice → Bob:lab().end
Local Type G@Bob: Bob?lab().end
```

### Parsing

Alternative way of using the library is through a simple type language with the
grammar:

#### Common

```
ident   = [A-Za-z][A-Za-z0-9]*
role    = ident
message = ident payload
payload = "()"
        | "(" ident ")"
```

#### Global Types

```
global   = role "->" role ":" interact
         | recur
         | typevar
         | end
interact = sendrecv | "{" sendrecv ("," sendrecv)+ "}"
sendrecv = message "." global
recur    = "*" ident "." global
typevar  = ident
end      = "end"
```

#### Local Types

```
local    = role "&" branch
         | role "+" select
         | lrecur
         | ltypevar
         | end
branch   = recv | "{" recv ("," recv)+ "}"
recv     = "?" message "." local
select   = send | "{" send ("," send)+ "}"
send     = "!" message "." local
lrecur   = "*" ident "." local
ltypevar = ident
lend     = "end"
```

### Parsing example:

This program parses an input string, then re-parses the output global type:
```
extern crate sesstype;

let input = String::from("*T . A -> B: { l().T, l2(int).end }");
let (global, _registry) = sesstype::parser::parse_global_type(input.clone()).unwrap();
let parsed = global.to_string();
let (reparsed, registry) = sesstype::parser::parse_global_type(parsed.clone()).unwrap();
print!(
    "Input:\n\t{}\nParsed:\n\t{}\nRe-parsed:\n\t{}\n",
    input,
    parsed,
    reparsed.to_string()
);

// Project for A
let role_a = registry.find_role_str("A").unwrap();
let local = sesstype::project(&reparsed, &role_a).unwrap();
print!(
    "Projected (for A):\n\t{}\n",
    local.to_string()
);
```

This is one of the expected output (because branches order in interactions are non-deterministic):

```
Input:
	*T . A -> B: { l().T, l2(int).end }
Parsed:
	μT.A → B:{ l().T, l2(int).end }
Re-parsed:
	μT.A → B:{ l().T, l2(int).end }
Projected (for A):
	μT.A⊕{ !l().T, !l2(int).end }
```

## License

sesstype is licensed under the [Apache License](http://www.apache.org/licenses/LICENSE-2.0).