package nuscr

You can search for identifiers within the package.

in-package search v0.2.0

A tool to manipulate and validate Scribble-style multiparty protocols

Install

sha256=4798916862412a0ac4721f63b77c243d7d7327c8ff2d18d379eb2f4202d43e4d

sha512=8475f03a5e81fbde01fb6ddd90f2c07d8a327d5d71301a8da6e169c5c1c8a8f94f528296b2c2d2be7abfbe10fceee048834926abbf5e739a62274f904a8f0869

A Multiparty Session Type representation that is similar to those used in the literature

type 'a cont_list =
  (Names.LabelName.t * Names.PayloadTypeName.t Base.list * 'a) Base.list

type global =

Global Types with basic features, in a form that is similar to those seen in standard literature. (No choice constructor, all choices are directed)

type local =

| SendL of Names.RoleName.t * local cont_list
(*
!p { l_i(S_i) . L_i }_{i \in I}
*)
| RecvL of Names.RoleName.t * local cont_list
(*
?p { l_i(S_i) . L_i }_{i \in I}
*)
| MuL of Names.TypeVariableName.t * local
(*
mu t. L
*)
| TVarL of Names.TypeVariableName.t
(*
t
*)
| EndL
(*
end
*)

val from_gtype : Gtype.t -> global

Convert from a Gtype.t

val from_ltype : Ltype.t -> local

Convert from a Ltype.t

val show_gtype_mpstk : global -> Base.string

Output the global type in a form recognised by MPSTK. https://github.com/alcestes/mpstk

val show_ltype_mpstk : local -> Base.string

Output the local type in a form recognised by MPSTK. https://github.com/alcestes/mpstk