aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-08-27 09:17:16 +0000
committerGravatar regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-08-27 09:17:16 +0000
commitd4b6a353ed60816a45bb27e406fb9ea06832ce24 (patch)
tree5dae53f1388c5339257a6aab1767fc7cd2526fff /checker
parent4f7c18174a59027cb3dd8493740b32aad2d99fcd (diff)
* Improve documentation of LightenLibrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13378 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml6
-rw-r--r--checker/safe_typing.ml9
-rw-r--r--checker/safe_typing.mli22
3 files changed, 28 insertions, 9 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 4c05d0d68..917accce9 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -40,7 +40,7 @@ type compilation_unit_name = dir_path
type library_disk = {
md_name : compilation_unit_name;
- md_compiled : Safe_typing.LightenLibrary.lighten_compiled_library;
+ md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
md_objects : library_objects;
md_deps : (compilation_unit_name * Digest.t) list;
md_imports : compilation_unit_name list }
@@ -303,7 +303,9 @@ let intern_from_file (dir, f) =
let ch = with_magic_number_check raw_intern_library f in
let (md:library_disk) = System.marshal_in ch in
let digest = System.marshal_in ch in
- let get_table () = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
+ let get_table () =
+ (System.marshal_in ch : Safe_typing.LightenLibrary.table)
+ in
if dir <> md.md_name then
errorlabstrm "load_physical_library"
(name_clash_message dir md.md_name f);
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 38f5aacf3..a5575892f 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -78,9 +78,10 @@ type compiled_library =
some memory space. *)
module LightenLibrary : sig
type table
- type lighten_compiled_library
- val save : compiled_library -> lighten_compiled_library * table
- val load : load_proof:bool -> (unit -> table) -> lighten_compiled_library -> compiled_library
+ type lightened_compiled_library
+ val save : compiled_library -> lightened_compiled_library * table
+ val load : load_proof:bool -> (unit -> table)
+ -> lightened_compiled_library -> compiled_library
end = struct
(* The table is implemented as an array of [constr_substituted].
@@ -92,7 +93,7 @@ end = struct
(* To avoid any future misuse of the lightened library that could
interpret encoded keys as real [constr_substituted], we hide
these kind of values behind an abstract datatype. *)
- type lighten_compiled_library = compiled_library
+ type lightened_compiled_library = compiled_library
(* Map a [compiled_library] to another one by just updating
the opaque term [t] to [on_opaque_const_body t]. *)
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index f8c5a48f3..78107455c 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -24,10 +24,26 @@ val import :
val unsafe_import :
System.physical_path -> compiled_library -> Digest.t -> unit
+(** Store the body of modules' opaque constants inside a table.
+
+ This module is used during the serialization and deserialization
+ of vo files.
+*)
module LightenLibrary :
sig
type table
- type lighten_compiled_library
- val save : compiled_library -> lighten_compiled_library * table
- val load : load_proof:bool -> (unit -> table) -> lighten_compiled_library -> compiled_library
+ type lightened_compiled_library
+
+ (** [save] splits a library into a lightened library with indexes
+ and a table that maps these indexes to opaque terms. *)
+ val save : compiled_library -> lightened_compiled_library * table
+
+ (** [load lpf get_table lcl] builds a compiled library from a
+ lightened library [lcl] by remplacing every index by its related
+ opaque terms inside the table obtained by [get_table ()].
+ If [lpf] is unset then the table is considered empty, which
+ implies that [get_table] is not evaluated and every index
+ is replaced by [None] inside the compiled library. *)
+ val load : load_proof:bool -> (unit -> table)
+ -> lightened_compiled_library -> compiled_library
end