aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-08-27 14:21:29 +0000
committerGravatar regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-08-27 14:21:29 +0000
commit16e0fd71ac54a1953d9bc8b86528b000b6721a18 (patch)
tree8c691314da83e433c8d37db499f4aa8bc6beb43a /checker
parent0b8e0849345efb93a7bd15091223281be081b42e (diff)
* checker/Safe_typing.LightenLibrary:
Remove the function "save" as the checker only needs to read vo files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13387 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker')
-rw-r--r--checker/safe_typing.ml32
-rw-r--r--checker/safe_typing.mli4
2 files changed, 0 insertions, 36 deletions
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 39904df8d..70eccf952 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -79,7 +79,6 @@ type compiled_library =
module LightenLibrary : sig
type table
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
@@ -132,37 +131,6 @@ end = struct
in
fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s)
- (* To disburden a library from opaque definitions, we simply
- traverse it and add an indirection between the module body
- and its reference to a [const_body]. *)
- let save library =
- let ((insert : constr_substituted -> constr_substituted),
- (get_table : unit -> table)) =
- (* We use an integer as a key inside the table. *)
- let counter = ref 0 in
- (* ... but it is wrapped inside a [constr_substituted]. *)
- let key_as_constr key = Declarations.from_val (Term.Rel key) in
-
- (* During the traversal, the table is implemented by a list
- to get constant time insertion. *)
- let opaque_definitions = ref [] in
-
- ((* Insert inside the table. *)
- (fun opaque_definition ->
- incr counter;
- opaque_definitions := opaque_definition :: !opaque_definitions;
- key_as_constr !counter),
-
- (* Get the final table representation. *)
- (fun () -> Array.of_list (List.rev !opaque_definitions)))
- in
- let encode_const_body : constr_substituted option -> constr_substituted option = function
- | None -> None
- | Some ct -> Some (insert ct)
- in
- let lightened_library = traverse_library encode_const_body library in
- (lightened_library, get_table ())
-
(* Loading is also a traversing that decodes the embedded keys that
are inside the [lightened_library]. If the [load_proof] flag is
set, we lookup inside the table to graft the
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 78107455c..73f705182 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -34,10 +34,6 @@ sig
type table
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 ()].