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=c5a419fd1fdea78fb63b3a3c335b0e6b0f2b08d65b79870565bdcc0f997bc728

sha512=83ef593ed514eeef1b10069af54562833d617d1c338c5adaf82ee5c3ea7ec4569b3643fcbb237b3cb79ce2f579094cbd17217efa5f4e522bd20f67e1df3a7dbd

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 a global type in a form recognised by MPSTK. https://github.com/alcestes/mpstk

val show_ltype_mpstk : local -> Base.string

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

val show_gtype_tex : global -> Base.string

Output a global type in a tex format using the package mpstmacros. https://github.com/fangyi-zhou/mpstmacros

WARNING: identifiers are provided "as is", manual escaping may be required

val show_ltype_tex : local -> Base.string

Output a local type in a tex format using the package mpstmacros. https://github.com/fangyi-zhou/mpstmacros

WARNING: identifiers are provided "as is", manual escaping may be required