Nuscrlib.Gtype
Global types
type global_protocol = Nuscrlib__Syntax.raw_global_protocol Loc.located
type payload =
| PValue of Names.VariableName.t Base.option * Expr.payload_type |
| PDelegate of Names.ProtocolName.t * Names.RoleName.t |
val pp_payload :
Ppx_deriving_runtime.Format.formatter ->
payload ->
Ppx_deriving_runtime.unit
val show_payload : payload -> Ppx_deriving_runtime.string
val sexp_of_payload : payload -> Sexplib0.Sexp.t
A message in a global type carries a label, and a list of payloads.
val pp_message :
Ppx_deriving_runtime.Format.formatter ->
message ->
Ppx_deriving_runtime.unit
val show_message : message -> Ppx_deriving_runtime.string
val sexp_of_message : message -> Sexplib0.Sexp.t
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
type t =
| MessageG of message * Names.RoleName.t * Names.RoleName.t * t | (*
|
| MuG of Names.TypeVariableName.t * rec_var Base.list * t | (*
|
| TVarG of Names.TypeVariableName.t * Expr.t Base.list * t Base.Lazy.t | (*
|
| ChoiceG of Names.RoleName.t * t Base.list | (*
|
| EndG | (* Empty global type *) |
| CallG of Names.RoleName.t
* Names.ProtocolName.t
* Names.RoleName.t Base.list
* t | (*
|
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(Nuscrlib__.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 : global_protocol -> t
Turn a raw protocol (from the parser) into a global type.
val nested_t_of_module : scr_module -> nested_t
Turn scribble module (from the parser) into a nested global type
Normalise a global type. This mainly collapses nested choice on the same participant and unfolds fixpoints
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