Nuscrlib.Ltype
Local type management
This module defines local types and basic operations on them.
type t =
| RecvL of Gtype.message * Names.RoleName.t * t | (*
|
| SendL of Gtype.message * Names.RoleName.t * t | (*
|
| ChoiceL of Names.RoleName.t * t Base.list | (*
|
| TVarL of Names.TypeVariableName.t * Expr.t Base.list | (*
|
| MuL of Names.TypeVariableName.t * (Base.bool * Gtype.rec_var) Base.list * t | (*
|
| 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
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