Library
Module
Module type
Parameter
Class
Class type
Main entry point of the library
This section deals with parsing protocols.
Parse from an input channel. The first parameter is the filename, for use in error messages.
validate_exn module
validates the module module
by performing standard checks. If verbose is set to true in the config, debugging messages will be printed
val protocols_names_of :
Nuscrlib__.Syntax.scr_module ->
Names.ProtocolName.t list
Other operations
protocols_names_of module
returns the list of the names of protocols * occuring in module
val enumerate :
Nuscrlib__.Syntax.scr_module ->
(Names.ProtocolName.t * Names.RoleName.t) list
enumerate module
enumerates the roles occurring in module
. The output is a list of pair (protocol, role-name)
.
val project_role :
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
role:Names.RoleName.t ->
Ltype.t
project_role module protocol role
computes the local type for role role
in the protocol protocol
.
val get_global_type :
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
Gtype.t
get_global_type module ~protocol
gets the corresponding global type for a protocol in a module
val get_global_type_literature_syntax :
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
LiteratureSyntax.global
get_global_type module_literature_syntax ~protocol
gets the corresponding global type for a protocol in a module in literature syntax
val generate_fsm :
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
role:Names.RoleName.t ->
Efsm.state * Efsm.t
generate_fsm module protocol role
computes the finite state machine of role role
in protocol protocol
, in module module
. It returns a pair (v, g)
where g
is the graph describing the fsm, and v
is the root index.
val generate_go_code :
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
out_dir:string ->
go_path:string option ->
string
generate_code module protocol out_dir go_path
generates Golang implementation for protocol
. The protocol implementation designed to be a subpackage within a project. out_dir
is the path from the root of the project until the package inside which the protocol implementation (subpackage) should be generated - it is needed to generate imports. go_path
is the path to the project root, which can optionally be provided in order to write the implementation to the file system.
val generate_ocaml_code :
monad:bool ->
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
role:Names.RoleName.t ->
string
generate_code ~monad module protocol role
generates event-style OCaml code for the role
in protocol
, inside a module
monad
indicates whether the generated code uses a monad for transport (e.g. Lwt, Async)
val generate_sexp :
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
string
generate_code ~monad module protocol role
generates event-style OCaml code for the role
in protocol
, inside a module
monad
indicates whether the generated code uses a monad for transport (e.g. Lwt, Async)
val generate_ast :
monad:bool ->
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
role:Names.RoleName.t ->
Ppxlib_ast.Parsetree.structure
generate_ast ~monad module protocol role
is similar to generate_code
, except it returns an AST instead of a string
val generate_fstar_code :
Nuscrlib__.Syntax.scr_module ->
protocol:Names.ProtocolName.t ->
role:Names.RoleName.t ->
string
Generate F* code, with support for refinement types
module Pragma : sig ... end
This module contains variables configuarations, to be set by pragmas or command line arguments, not to be changed for the duration of the program
module Expr : sig ... end
Expressions, used in RefinementTypes
pragma
module Gtype : sig ... end
Global types
module Ltype : sig ... end
Local type management
module Efsm : sig ... end
module Err : sig ... end
module Names : sig ... end
module Loc : sig ... end
module LiteratureSyntax : sig ... end
A Multiparty Session Type representation that is similar to those used in the literature