Goptions (rocq-runtime.Goptions)

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.

type option_name = string list

type _ option_kind =

| BoolKind : bool option_kind
| IntKind : int option option_kind
| StringKind : string option_kind
| StringOptKind : string option option_kind

type option_locality =

| OptDefault
| OptLocal
| OptExport
| OptGlobal

Tables.

type table_value =

| StringRefValue of string
| QualidRefValue of Libnames.qualid

module type ArgSet = sig ... end

module type TableArg = sig ... end

The functor MakeTable declares a table. Vernacular Add, Remove, and Test commands pass each argument as a table_value; encode maps such values to stored elements, possibly globalizing qualified identifiers with the supplied environment. Tables that do not support one of the constructors should raise a user error from encode.

module MakeTable (A : TableArg) : sig ... end

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

MakeStringTable is a specialization of MakeTable for tables whose vernacular arguments are strings.

module type RefConvertArg = sig ... end

MakeRefTable is a specialization of MakeTable for tables whose vernacular arguments are qualified identifiers. The encoding function is typically a globalization function, possibly with extra checks.

module 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.

type 'a option_sig = {

optstage : Summary.Stage.t;
optdepr : Deprecation.t option;
(*
whether the option is DEPRECATED
*)
optkey : option_name;
(*
the low-level name of this option
*)
optread : unit -> 'a;
optwrite : 'a -> unit;

}

val 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".

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

Helpers to declare a reference controlled by an option.

type 'a getter = {

get : unit -> 'a;

}

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

type 'a opt_decl =
  ?stage:Summary.Stage.t ->
  ?depr:Deprecation.t ->
  key:option_name ->
  value:'a ->
  unit ->
  'a getter

val declare_interpreted_option_and_ref : 
  ('a -> 'b) ->
  ('b -> 'a) ->
  stage:Summary.Stage.t ->
  ?depr:Deprecation.t ->
  key:option_name ->
  'a option_kind ->
  value:'b ->
  unit ->
  'b getter

val declare_int_option_and_ref : int opt_decl

val declare_intopt_option_and_ref : int option opt_decl

val declare_nat_option_and_ref : int opt_decl

val declare_bool_option_and_ref : bool opt_decl

val declare_string_option_and_ref : string opt_decl

val declare_stringopt_option_and_ref : string option opt_decl

val declare_interpreted_string_option_and_ref : 
  (string -> 'a) ->
  ('a -> string) ->
  'a opt_decl

Special functions supposed to be used only in vernacentries.ml

module OptionMap : CSig.MapS with type key = option_name

type 'a table_of_A = {

add : Environ.env -> Libobject.locality -> 'a -> unit;
remove : Environ.env -> Libobject.locality -> 'a -> unit;
mem : Environ.env -> 'a -> unit;
print : unit -> unit;

}

val get_table : option_name -> table_value table_of_A

val get_string_table : option_name -> string table_of_A

Compatibility views of get_table.

val get_ref_table : option_name -> Libnames.qualid table_of_A

val 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.

val set_bool_option_value_gen : 
  ?locality:option_locality ->
  ?stage:Summary.Stage.t ->
  option_name ->
  bool ->
  unit

val set_string_option_value_gen : 
  ?locality:option_locality ->
  ?stage:Summary.Stage.t ->
  option_name ->
  string ->
  unit

val unset_option_value_gen : 
  ?locality:option_locality ->
  ?stage:Summary.Stage.t ->
  option_name ->
  unit

val set_int_option_value : 
  ?stage:Summary.Stage.t ->
  option_name ->
  int option ->
  unit

val set_bool_option_value : 
  ?stage:Summary.Stage.t ->
  option_name ->
  bool ->
  unit

val set_string_option_value : 
  ?stage:Summary.Stage.t ->
  option_name ->
  string ->
  unit

val print_option_value : option_name -> unit

type option_value =

| BoolValue of bool
| IntValue of int option
| StringValue of string
| StringOptValue of string option

val get_option_value : option_name -> (unit -> option_value) option

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

type 'a check_and_cast = {

check_and_cast : 'b. 'a -> 'b option_kind -> 'b;

}

val 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.

type option_state = {

opt_depr : Deprecation.t option;
opt_value : option_value;

}

Summary of an option status

val get_tables : unit -> option_state OptionMap.t

val print_tables : unit -> Pp.t

type iter_table_aux = {

aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit;

}

val iter_table : 
  Environ.env ->
  iter_table_aux ->
  option_name ->
  table_value list ->
  unit

val error_undeclared_key : option_name -> 'a

Compat

val declare_int_option : 
  ?preprocess:(int option -> int option) ->
  int option option_sig ->
  unit

val declare_bool_option : ?preprocess:(bool -> bool) -> bool option_sig -> unit

val declare_string_option : 
  ?preprocess:(string -> string) ->
  string option_sig ->
  unit

val declare_stringopt_option : 
  ?preprocess:(string option -> string option) ->
  string option option_sig ->
  unit