Module `Nuscrlib.Pragma`

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 =

| NestedProtocols
| ShowPragmas
| PrintUsage
| RefinementTypes
| SenderValidateRefinements
| ReceiverValidateRefinements
| ValidateRefinementSatisfiability
| ValidateRefinementProgress

val pp : 
  Ppx_deriving_runtime.Format.formatter ->
  t ->
  Ppx_deriving_runtime.unit

val show : t -> Ppx_deriving_runtime.string

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/nuscr.lib/Nuscrlib/Pragma/index.html

Module `Nuscrlib.Pragma`

package nuscr

Install

Dune Dependency

Authors

Maintainers

Sources

doc/nuscr.lib/Nuscrlib/Pragma/index.html

Module Nuscrlib.Pragma

Module `Nuscrlib.Pragma`