type 'a summary_declaration = {freeze_function : marshallable:bool -> 'a ;freeze_function true is for marshalling to disk. * e.g. lazy must be forced
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 -> 'a summary_declaration -> unitmodule Dyn : Dyn.S We provide safe projection from the summary to the types stored in it.
val declare_summary_tag : string -> '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 freeze_function can be overridden
val ref : ?freeze:(marshallable:bool -> 'a -> 'a ) -> name:string -> 'a -> 'a Stdlib.refval ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a ) -> name:string -> 'a -> 'a Stdlib.ref'a Dyn.tag module Local : sig ... end val declare_ml_modules_summary : (string option * string) listsummary_declaration -> unitSpecial 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.
val nop : unit -> unittype frozenval empty_frozen : frozen val freeze_summaries : marshallable:bool -> frozen val unfreeze_summaries : ?partial:bool -> frozen -> unitval init_summaries : unit -> unitTyped projection of the summary. Experimental API, use with CARE
val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen val project_from_summary : frozen -> 'a Dyn.tag -> 'a val remove_from_summary : frozen -> 'a Dyn.tag -> frozen val dump : unit -> (int * string) list