sesstype

这是 Rust 中多方会话类型的实现。sesstype 包含核心数据结构和实用函数，用于建模和操作多方会话类型语言。

构建

构建此库的最佳方式是通过 Rust 的 cargo 软件包管理器。

$ cargo build

使用方法

有关详细信息，请参阅文档。

$ cargo doc --open

快速入门

给定以下源代码（具有正确的依赖项）

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()),
    }
}

应生成以下输出

$ cargo run
Global type G: Alice → Bob:lab().end
Local Type G@Bob: Bob?lab().end

解析

通过简单类型语言和语法使用库的另一种方法是

常用

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

全局类型

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

本地类型

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"

解析示例

此程序解析输入字符串，然后重新解析输出全局类型

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()
);

这是预期的输出之一（因为交互分支的顺序是非确定的）

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 }

许可证

sesstype 根据 Apache 许可证 许可。