package nuscr

  1. Overview
  2. Docs

Module Nuscrlib.Gtype

Global types

val equal_payload : payload -> payload -> Ppx_deriving_runtime.bool
val sexp_of_payload : payload -> Sexplib0.Sexp.t
val show_payload : payload -> Ppx_deriving_runtime.string
val compare_payload : payload -> payload -> Ppx_deriving_runtime.int
type message = {
  1. label : Names.LabelName.t;
  2. 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 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 = {
  1. rv_name : Names.VariableName.t;
    (*

    Variable Name

    *)
  2. rv_roles : Names.RoleName.t Base.list;
    (*

    Which roles know this variable

    *)
  3. rv_ty : Expr.payload_type;
    (*

    What type does the variable carry

    *)
  4. 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 =
  1. | 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

    *)
  2. | 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.

    *)
  3. | 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.

    *)
  4. | ChoiceG of Names.RoleName.t * t Base.list
    (*

    ChoiceG (name, ts) expresses a choice located at participant name between the ts

    *)
  5. | EndG
    (*

    Empty global type

    *)
  6. | 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 = {
  1. static_roles : Names.RoleName.t Base.list;
  2. dynamic_roles : Names.RoleName.t Base.list;
  3. nested_protocol_names : Names.ProtocolName.t Base.list;
  4. gtype : 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

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