Module `Nuscrlib.Ltype`

Local type management

type t =

| RecvL of Gtype.message * Names.RoleName.t * t
(*
RecvL (msg, name, t) waits for message msg from name and continues as t
*)
| SendL of Gtype.message * Names.RoleName.t * t
(*
SendL (msg, name, t) sends message msg to name and continues as t
*)
| ChoiceL of Names.RoleName.t * t Base.list
(*
ChoiceL (name, ts) is a choice (internal or external) from name between the ts
*)
| TVarL of Names.TypeVariableName.t * Expr.t Base.list
(*
TVarL (type_var, exprs) 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.
*)
| MuL of Names.TypeVariableName.t * (Base.bool * Gtype.rec_var) Base.list * t
(*
MuL (type_var, rec_vars, l) is a recursive type, corresponding to the syntax `\mu t. L`, where t is represented by type_var and L is represented by t. rec_vars are recursion parameters, where the first component represents whether the variable is a silent variable (with multiplicity 0). These parameters are used in RefinementTypes extension for parameterised recursion, an empty list is supplied when that feature is not used.
*)
| EndL
(*
Empty type
*)
| InviteCreateL of Names.RoleName.t Base.list * Names.RoleName.t Base.list * Names.ProtocolName.t * t
(*
Send invitations to existing roles and set up/create dynamic pariticipants, used only in NestedProtocols extension
*)
| AcceptL of Names.RoleName.t * Names.ProtocolName.t * Names.RoleName.t Base.list * Names.RoleName.t Base.list * Names.RoleName.t * t
(*
accept role@Proto(roles...; new roles...) from X; t, used only in Nested Protocols extension
*)
| SilentL of Names.VariableName.t * Expr.payload_type * t
(*
Used with refinement types to indicate knowledge obtained via a global protocol, used only in RefinementTypes extension
*)

Local types. See also LiteratureSyntax.local for a simpler syntax.

module LocalProtocolId : sig ... end

Unique id identifying a local protocol

type nested_t = (Names.RoleName.t Base.list * t) Base.Map.M(LocalProtocolId).t

Mapping of local protocol id to the protocol's roles and local type

val show : t -> Base.string

Converts a local type to a string.

val show_nested_t : nested_t -> Base.string

val project : Names.RoleName.t -> Gtype.t -> t

Project a global type into a particular role.

val project_nested_t : Gtype.nested_t -> nested_t

Generate the local protocols for a given global_t

val ensure_unique_tvars : nested_t -> nested_t

Ensure that all the local variables in each local protocol are globally unique, renaming variables to resolve conflicts

type local_proto_name_lookup =
  Names.LocalProtocolName.t Base.Map.M(LocalProtocolId).t

Mapping from local protocol ids to their unique local protocol names

val build_local_proto_name_lookup : nested_t -> local_proto_name_lookup

Builds a map containing the unique string representations for the unique local protocol ids

val show_lookup_table : local_proto_name_lookup -> Base.string

Converts a local protocol name lookup table to a string

val lookup_local_protocol : 
  local_proto_name_lookup ->
  Names.ProtocolName.t ->
  Names.RoleName.t ->
  Names.LocalProtocolName.t

Return the unique local protocol name for a (role, protocol) pair

val lookup_protocol_id : 
  local_proto_name_lookup ->
  LocalProtocolId.t ->
  Names.LocalProtocolName.t

Look up the unique name for a local protocol id

package nuscr

Module Nuscrlib.Ltype

Module `Nuscrlib.Ltype`