diff options
Diffstat (limited to 'kernel/lazyconstr.mli')
| -rw-r--r-- | kernel/lazyconstr.mli | 35 |
1 files changed, 27 insertions, 8 deletions
diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli index 17c9bcc76..f6188f536 100644 --- a/kernel/lazyconstr.mli +++ b/kernel/lazyconstr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names open Term open Mod_subst @@ -19,16 +20,34 @@ val force : constr_substituted -> constr val subst_constr_subst : substitution -> constr_substituted -> constr_substituted -(** Opaque proof terms are not loaded immediately, but are there - in a lazy form. Forcing this lazy may trigger some unmarshal of - the necessary structure. *) +(** Opaque proof terms might be in some external tables. The + [force_opaque] function below allows to access these tables, + this might trigger the read of some extra parts of .vo files *) type lazy_constr -val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr -val force_lazy_constr : lazy_constr -> constr_substituted -val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr -val lazy_constr_is_val : lazy_constr -> bool +(** From a [constr] to some (immediate) [lazy_constr]. *) +val opaque_from_val : constr -> lazy_constr + +(** Turn an immediate [lazy_constr] into an indirect one, thanks + to the indirect opaque creator configured below. *) +val turn_indirect : lazy_constr -> lazy_constr +(** From a [lazy_constr] back to a [constr]. This might use the + indirect opaque accessor configured below. *) val force_opaque : lazy_constr -> constr -val opaque_from_val : constr -> lazy_constr + +val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr + +val hcons_lazy_constr : lazy_constr -> lazy_constr + +(** When stored indirectly, opaque terms are indexed by their library + dirpath and an integer index. The following two functions activate + this indirect storage, by telling how to store and retrieve terms. + Default creator always returns [None], preventing the creation of + any indirect link, and default accessor always raises an error. +*) + +val set_indirect_opaque_creator : (constr -> (DirPath.t * int) option) -> unit +val set_indirect_opaque_accessor : (DirPath.t -> int -> constr) -> unit +val reset_indirect_opaque_creator : unit -> unit |