package nuscr

  1. Overview
  2. Docs

This module contains variables configuarations, to be set by pragmas or command line arguments, not to be changed for the duration of the program

type t =
  1. | NestedProtocols
  2. | ShowPragmas
  3. | PrintUsage
  4. | RefinementTypes
  5. | SenderValidateRefinements
  6. | ReceiverValidateRefinements
  7. | ValidateRefinementSatisfiability
  8. | ValidateRefinementProgress
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val pragma_of_string : string -> t
type pragmas = (t * string option) list
val pp_pragmas : Ppx_deriving_runtime.Format.formatter -> pragmas -> Ppx_deriving_runtime.unit
val show_pragmas : pragmas -> Ppx_deriving_runtime.string
val solver_show_queries : unit -> bool

Whether to display queries to SMT solvers (with RefinementTypes pragma)

val set_solver_show_queries : bool -> unit

Set solver_show_queries

val nested_protocol_enabled : unit -> bool

Whether NestedProtocol pragma is enabled

val set_nested_protocol : bool -> unit

Set nested_protocol_enabled

val refinement_type_enabled : unit -> bool

Whether RefinementTypes pragma is enabled

val set_refinement_type : bool -> unit

Set refinement_type

val sender_validate_refinements : unit -> bool

When refinement types are enabled, senders should validate refinements

val set_sender_validate_refinements : bool -> unit

Set sender_validate_refinements

val receiver_validate_refinements : unit -> bool

When refinement types are enabled, receivers should validate refinements

val set_receiver_validate_refinements : bool -> unit

Set receiver_validate_refinements

val validate_refinement_satisfiability : unit -> bool

Validate whether a refined global type is semantically satisfiable

val set_validate_refinement_satisfiability : bool -> unit

Set validate_refinement_satisfiability

val validate_refinement_progress : unit -> bool

Validate whether a refined global type satisfies progress semantically

val set_validate_refinement_progress : bool -> unit

Set validate_refinement_progress

val verbose : unit -> bool

Whether to produce verbose outputs

val set_verbose : bool -> unit

Set verbose

val reset : unit -> unit

Reset all configuration to default

val load_from_pragmas : pragmas -> unit

Load config from pragmas

OCaml

Innovation. Community. Security.