package nuscr

  1. Overview
  2. Docs
package nuscr
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

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

enumerate module enumerates the roles occurring in module. The output is a list of pair (protocol, role-name).

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

get_global_type module gets the corresponding global type for a module

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

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_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