package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.library/Goptions/index.html

Module GoptionsSource

This module manages customization parameters at the vernacular level

Two kinds of things are managed : tables and options value

  • Tables are created by applying the MakeTable functor.
  • Variables storing options value are created by applying one of the declare_int_option, declare_bool_option, ... functions.

Each table/option is uniquely identified by a key of type option_name which consists in a list of strings. Note that for parsing constraints, table names must not be made of more than 2 strings while option names can be of arbitrary length.

The declaration of a table, say of name ["Toto";"Titi"] automatically makes available the following vernacular commands:

Add Toto Titi foo. Remove Toto Titi foo. Print Toto Titi. Test Toto Titi.

The declaration of a non boolean option value, say of name ["Tata";"Tutu";"Titi"], automatically makes available the following vernacular commands:

Set Tata Tutu Titi val. Print Table Tata Tutu Titi.

If it is the declaration of a boolean value, the following vernacular commands are made available:

Set Tata Tutu Titi. Unset Tata Tutu Titi. Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *)

All options are synchronized with the document.

Sourcetype option_name = string list
Sourcetype _ option_kind =
  1. | BoolKind : bool option_kind
  2. | IntKind : int option option_kind
  3. | StringKind : string option_kind
  4. | StringOptKind : string option option_kind
Sourcetype option_locality =
  1. | OptDefault
  2. | OptLocal
  3. | OptExport
  4. | OptGlobal
Tables.

The functor MakeStringTable declares a table containing objects of type string; the function member_message say what to print when invoking the "Test Toto Titi foo." command; at the end title is the table name printed when invoking the "Print Toto Titi." command; active is roughly the internal version of the vernacular "Test ...": it tells if a given object is in the table; elements returns the list of elements of the table

Sourcemodule MakeStringTable (_ : sig ... end) : sig ... end

The functor MakeRefTable declares a new table of objects of type A.t practically denoted by reference; the encoding function encode : env -> reference -> A.t is typically a globalization function, possibly with some restriction checks; the function member_message say what to print when invoking the "Test Toto Titi foo." command; at the end title is the table name printed when invoking the "Print Toto Titi." command; active is roughly the internal version of the vernacular "Test ...": it tells if a given object is in the table.

Sourcemodule type RefConvertArg = sig ... end
Sourcemodule MakeRefTable (A : RefConvertArg) : sig ... end
Options.

These types and function are for declaring a new option of name key and access functions read and write; the parameter name is the option name used when printing the option value (command "Print Toto Titi."

The declare_*_option functions are low-level, to be used when implementing complex option workflows, e.g. when the option data is in the global env. For most use cases, you should use the helper functions declare_*_option_and_ref.

Sourcetype 'a option_sig = {
  1. optstage : Summary.Stage.t;
  2. optdepr : Deprecation.t option;
    (*

    whether the option is DEPRECATED

    *)
  3. optkey : option_name;
    (*

    the low-level name of this option

    *)
  4. optread : unit -> 'a;
  5. optwrite : 'a -> unit;
}
Sourceval declare_option : ?preprocess:('a -> 'a) -> ?no_summary:bool -> kind:'a option_kind -> 'a option_sig -> unit

The preprocess function is triggered before setting the option. It can be used to emit a warning on certain values, and clean-up the final value.

By default no_summary:false, and declare_option declares a summary entry to synchronize the backing state by calling read and write. If you pass no_summary:true you must handle synchronization separately.

StringOptKind should be preferred to StringKind because it supports "Unset".

Sourceval declare_append_only_option : ?preprocess:(string -> string) -> sep:string -> string option_sig -> unit

Helpers to declare a reference controlled by an option.

Sourcetype 'a getter = {
  1. get : unit -> 'a;
}

Wrapper type to separate the function calls to register the option at toplevel from the calls to read the option value.

Sourcetype 'a opt_decl = ?stage:Summary.Stage.t -> ?depr:Deprecation.t -> key:option_name -> value:'a -> unit -> 'a getter
Sourceval declare_int_option_and_ref : int opt_decl
Sourceval declare_intopt_option_and_ref : int option opt_decl
Sourceval declare_nat_option_and_ref : int opt_decl
Sourceval declare_bool_option_and_ref : bool opt_decl
Sourceval declare_string_option_and_ref : string opt_decl
Sourceval declare_stringopt_option_and_ref : string option opt_decl
Sourceval declare_interpreted_string_option_and_ref : (string -> 'a) -> ('a -> string) -> 'a opt_decl
Special functions supposed to be used only in vernacentries.ml
Sourcetype 'a table_of_A = {
  1. add : Environ.env -> Libobject.locality -> 'a -> unit;
  2. remove : Environ.env -> Libobject.locality -> 'a -> unit;
  3. mem : Environ.env -> 'a -> unit;
  4. print : unit -> unit;
}
Sourceval get_string_table : option_name -> string table_of_A
Sourceval set_int_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> int option -> unit

The first argument is a locality flag. If stage is provided, the option is set/unset only if it is declared in the corresponding stage. If omitted, the option is always set/unset.

Sourceval set_bool_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> bool -> unit
Sourceval set_string_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> string -> unit
Sourceval unset_option_value_gen : ?locality:option_locality -> ?stage:Summary.Stage.t -> option_name -> unit
Sourceval set_int_option_value : ?stage:Summary.Stage.t -> option_name -> int option -> unit
Sourceval set_bool_option_value : ?stage:Summary.Stage.t -> option_name -> bool -> unit
Sourceval set_string_option_value : ?stage:Summary.Stage.t -> option_name -> string -> unit
Sourceval print_option_value : option_name -> unit
Sourcetype option_value =
  1. | BoolValue of bool
  2. | IntValue of int option
  3. | StringValue of string
  4. | StringOptValue of string option
Sourcetype table_value =
  1. | StringRefValue of string
  2. | QualidRefValue of Libnames.qualid
Sourceval get_option_value : option_name -> (unit -> option_value) option

get_option_value key returns None if option with name key was not found.

Sourcetype 'a check_and_cast = {
  1. check_and_cast : 'b. 'a -> 'b option_kind -> 'b;
}
Sourceval set_option_value : ?locality:option_locality -> ?stage:Summary.Stage.t -> 'a check_and_cast -> option_name -> 'a -> unit

set_option_value ?locality f name v sets name to the result of applying f to v and name's option kind. Use for behaviour depending on the type of the option, eg erroring when 'a doesn't match it.

Sourcetype option_state = {
  1. opt_depr : Deprecation.t option;
  2. opt_value : option_value;
}

Summary of an option status

Sourceval get_tables : unit -> option_state OptionMap.t
Sourceval print_tables : unit -> Pp.t
Sourcetype iter_table_aux = {
  1. aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit;
}
Sourceval iter_table : Environ.env -> iter_table_aux -> option_name -> table_value list -> unit
Sourceval error_undeclared_key : option_name -> 'a

Compat

Sourceval declare_int_option : ?preprocess:(int option -> int option) -> int option option_sig -> unit
Sourceval declare_bool_option : ?preprocess:(bool -> bool) -> bool option_sig -> unit
Sourceval declare_string_option : ?preprocess:(string -> string) -> string option_sig -> unit
Sourceval declare_stringopt_option : ?preprocess:(string option -> string option) -> string option option_sig -> unit