package nuscr
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=4798916862412a0ac4721f63b77c243d7d7327c8ff2d18d379eb2f4202d43e4d
sha512=8475f03a5e81fbde01fb6ddd90f2c07d8a327d5d71301a8da6e169c5c1c8a8f94f528296b2c2d2be7abfbe10fceee048834926abbf5e739a62274f904a8f0869
doc/nuscr.lib/Nuscrlib/index.html
Module Nuscrlib
Source
Parsing
Main entry point of the library
This section deals with parsing protocols.
Parse a string into a Syntax.scr_module
.
Parse from an input channel. The first parameter is the filename, for use in error messages.
Validation
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
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)
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