nuscr 2.0.0 · OCaml Package

Parsing

Main entry point of the library

This section deals with parsing protocols.

val parse_string : string -> Syntaxtree.Syntax.scr_module

Parse a string into a Syntax.scr_module.

val parse : string -> Stdio.In_channel.t -> Syntaxtree.Syntax.scr_module

Parse from an input channel. The first parameter is the filename, for use in error messages.

Validation

val validate_exn : Syntaxtree.Syntax.scr_module -> unit

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

val enumerate : 
  Syntaxtree.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 : 
  Syntaxtree.Syntax.scr_module ->
  protocol:Names.ProtocolName.t ->
  role:Names.RoleName.t ->
  Mpst.Ltype.t

project_role module protocol role computes the local type for role role in the protocol protocol.

val get_global_type : 
  Syntaxtree.Syntax.scr_module ->
  protocol:Names.ProtocolName.t ->
  Mpst.Gtype.t

get_global_type module gets the corresponding global type for a module

val generate_fsm : 
  Syntaxtree.Syntax.scr_module ->
  protocol:Names.ProtocolName.t ->
  role:Names.RoleName.t ->
  Mpst.Efsm.state * Mpst.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 : 
  Syntaxtree.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 ->
  Syntaxtree.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 : 
  Syntaxtree.Syntax.scr_module ->
  protocol:Names.ProtocolName.t ->
  string

val generate_ast : 
  monad:bool ->
  Syntaxtree.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 : 
  Syntaxtree.Syntax.scr_module ->
  protocol:Names.ProtocolName.t ->
  role:Names.RoleName.t ->
  string

Generate F* code, with support for refinement types

module Pragma = Pragma

module Gtype = Mpst.Gtype

module Ltype = Mpst.Ltype

module Efsm = Mpst.Efsm

module Err = Err

package nuscr

Parsing

Validation

Other operations