Summary
module Stage : sig ... end
This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system.
type 'a summary_declaration = {
stage : Stage.t; |
freeze_function : unit -> 'a; |
unfreeze_function : 'a -> unit; |
init_function : unit -> unit; |
}
Types of global Coq states. The 'a
type should be pure and marshallable by the standard OCaml marshalling function.
For tables registered during the launch of coqtop, the init_function
will be run only once, during an init_summaries
done at the end of coqtop initialization. For tables registered later (for instance during a plugin dynlink), init_function
is used when unfreezing an earlier frozen state that doesn't contain any value for this table.
Beware: for tables registered dynamically after the initialization of Coq, their init functions may not be run immediately. It is hence the responsibility of plugins to initialize themselves properly.
val declare_summary : string -> ?make_marshallable:('a -> 'a) -> 'a summary_declaration -> unit
val declare_summary_tag : string -> ?make_marshallable:('a -> 'a) -> 'a summary_declaration -> 'a Dyn.tag
All-in-one reference declaration + summary registration. It behaves just as OCaml's standard ref
function, except that a declare_summary
is done, with name
as string. The init_function
restores the reference to its initial value. The stage
argument defaults to Interp
and should be changed to Synterp
for references which are read from and written to during the syntactic interpretation.
When local:true
the value is local to the process, i.e. not sent to proof workers. Consequently it doesn't need to be of a marshallable type. It is useful to implement a local cache for example.
ref_tag
is never local.
val ref : ?stage:Stage.t -> ?local:bool -> name:string -> 'a -> 'a Stdlib.ref
val declare_ml_modules_summary : (string option * string) list summary_declaration -> unit
Special summary for ML modules. This summary entry is special because its unfreeze may load ML code and hence add summary entries. Thus is has to be recognizable, and handled properly.
The args correspond to Mltop.PluginSpec.t , that is to say, the optional legacy plugin name, and the findlib name for the plugin.
For global tables registered statically before the end of coqtop launch, the following empty init_function
could be used.
module type FrozenStage = sig ... end
The type frozen
is a snapshot of the states of all the registered tables of the system.
module Synterp : FrozenStage
The type frozen
is a snapshot of the states of all the registered tables of the system.
module Interp : sig ... end