nuscr 2.1.0 · OCaml Package

Global types

type payload =

| PValue of Names.VariableName.t Base.option * Expr.payload_type
| PDelegate of Names.ProtocolName.t * Names.RoleName.t

val equal_payload : payload -> payload -> Ppx_deriving_runtime.bool

val sexp_of_payload : payload -> Sexplib0.Sexp.t

val pp_payload : 
  Ppx_deriving_runtime.Format.formatter ->
  payload ->
  Ppx_deriving_runtime.unit

val show_payload : payload -> Ppx_deriving_runtime.string

val compare_payload : payload -> payload -> Ppx_deriving_runtime.int

type message = {

label : Names.LabelName.t;
payload : payload Base.list;

}

A message in a global type carries a label, and a list of payloads.

val equal_message : message -> message -> Ppx_deriving_runtime.bool

val sexp_of_message : message -> Sexplib0.Sexp.t

val pp_message : 
  Ppx_deriving_runtime.Format.formatter ->
  message ->
  Ppx_deriving_runtime.unit

val show_message : message -> Ppx_deriving_runtime.string

val compare_message : message -> message -> Ppx_deriving_runtime.int

val equal_pvalue_payload : payload -> payload -> Base.bool

val typename_of_payload : payload -> Names.PayloadTypeName.t

type rec_var = {

rv_name : Names.VariableName.t;
(*
Variable Name
*)
rv_roles : Names.RoleName.t Base.list;
(*
Which roles know this variable
*)
rv_ty : Expr.payload_type;
(*
What type does the variable carry
*)
rv_init_expr : Expr.t;
(*
What is the initial expression assigned at the beginning of recursion
*)

}

Recursion variable

val sexp_of_rec_var : rec_var -> Sexplib0.Sexp.t

val equal_rec_var : rec_var -> rec_var -> Ppx_deriving_runtime.bool

type t =

| MessageG of message * Names.RoleName.t * Names.RoleName.t * t
(*
MessageG (msg, sender, receiver, t) starts by sending message msg from sender to receiver and continues as t
*)
| MuG of Names.TypeVariableName.t * rec_var Base.list * t
(*
MuG (type_var, rec_vars, g) is a recursive type, corresponding to the syntax `\mu t. G`, where t is represented by type_var and G is represented by t. rec_vars are recursion parameters, used in RefinementTypes extension for parameterised recursion, an empty list is supplied when that feature is not used.
*)
| TVarG of Names.TypeVariableName.t * Expr.t Base.list * t Base.Lazy.t
(*
TVarG (type_var, exprs, g_lazy) is a type variable, scoped inside a recursion. type_var is the name of the type variable, exprs are expressions supplied into paramterised recursion, used in RefinementTypes extension. Otherwise an empty list is supplied when that feature is not used. g_lazy provides a convenient way to access the type that the type variable recurses into.
*)
| ChoiceG of Names.RoleName.t * t Base.list
(*
ChoiceG (name, ts) expresses a choice located at participant name between the ts
*)
| EndG
(*
Empty global type
*)
| CallG of Names.RoleName.t * Names.ProtocolName.t * Names.RoleName.t Base.list * t
(*
CallG (caller, protocol, participants, t) - caller calls protocol, inviting participants to carry out the roles in protocol (dynamic roles in nested protocols are not included)
*)

The type of global types. See also LiteratureSyntax.global for a simpler syntax.

val sexp_of_t : t -> Sexplib0.Sexp.t

Mapping of protocol name to the roles ('static' participants, dynamic participants) participating in the protocol, the names of the nested protocols defined inside it and its global type

type nested_global_info = {

static_roles : Names.RoleName.t Base.list;
dynamic_roles : Names.RoleName.t Base.list;
nested_protocol_names : Names.ProtocolName.t Base.list;
gtype : t;

}

type nested_t = nested_global_info Base.Map.M(Names.ProtocolName).t

val show : t -> Base.string

Provides a textual representation of a global type

val show_nested_t : nested_t -> Base.string

Provides a textual representation of a global type with nested protocols

val call_label : 
  Names.RoleName.t ->
  Names.ProtocolName.t ->
  Names.RoleName.t Base.list ->
  Names.LabelName.t

Generates a unique label for a protocol call based on the caller, the protocol called and the participants involved

val of_protocol : Nuscrlib__.Syntax.raw_global_protocol Loc.located -> t

Turn a raw protocol (from the parser) into a global type, optional argument refined determines whether refinement types are enabled.

val nested_t_of_module : Nuscrlib__.Syntax.scr_module -> nested_t

Turn scribble module (from the parser) into a nested global type

val normalise : t -> t

Normalise a global type. This mainly collapses nested choice on the same participant and unfolds fixpoints

val normalise_nested_t : nested_t -> nested_t

Apply normalisation to all protocols in nested_t

val validate_refinements_exn : t -> Base.unit

Validate refinements in the given global type, requires RefinementTypes pragma

val show_rec_var : rec_var -> Base.string

Convert rec_var to string

package nuscr