Revised infrastructure for lazy loading of opaque proofs

 Get rid of the LightenLibrary hack : no more last-minute
 collect of opaque terms and Obj.magic tricks. Instead, we
 make coqc accumulate the opaque terms as soon as constant_bodies
 are created outside sections. In these cases, the opaque
 terms are placed in a special table, and some (DirPath.t * int)
 are used as indexes in constant_body. In an interactive session,
 the local opaque terms stay directly stored in the constant_body.

 The structure of .vo file stays similar : magic number, regular
 library structure, digest of the first part, array of opaque terms.
 In addition, we now have a final checksum for checking the
 integrity of the whole .vo file. The other difference is that
 lazy_constr aren't changed into int indexes in .vo files, but are
 now coded as (substitution list * DirPath.t * int). In particular
 this approach allows to refer to opaque terms from another
 library. This (and accumulating substitutions in lazy_constr)
 seems to greatly help decreasing the size of opaque tables :
 -20% of vo size on the standard library :-). The compilation times
 are slightly better, but that can be statistic noise.

 The -force-load-proofs isn't active anymore : it behaves now
 just like -lazy-load-proofs. The -dont-load-proofs mode has
 slightly changed : opaque terms aren't seen as axioms anymore,
 but accessing their bodies will raise an error.

 Btw, API change : Declareops.body_of_constant now produces directly
 a constr option instead of a constr_substituted option

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 16 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c70a3f2eb8..67d80fa500 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -80,26 +80,31 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
+let check_declared_variables declared inferred =
+  let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
+  let undeclared_set = Id.Set.diff (mk_set inferred) (mk_set declared) in
+  if not (Id.Set.is_empty undeclared_set) then
+    error ("The following section variables are used but not declared:\n"^
+              (String.concat ", "
+                 (List.map Id.to_string (Id.Set.elements undeclared_set))))
+
 let build_constant_declaration env (def,typ,cst,inline_code,ctx) =
-  let hyps = 
+  let hyps =
     let inferred =
       let ids_typ = global_vars_set_constant_type env typ in
       let ids_def = match def with
-      | Undef _ -> Id.Set.empty
-      | Def cs -> global_vars_set env (Lazyconstr.force cs)
-      | OpaqueDef lc -> 
-          global_vars_set env (Lazyconstr.force_opaque lc) in
-      keep_hyps env (Id.Set.union ids_typ ids_def) in
-    let declared = match ctx with
-      | None -> inferred 
-      | Some declared -> declared in
-    let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
-    let inferred_set, declared_set = mk_set inferred, mk_set declared in
-    if not (Id.Set.subset inferred_set declared_set) then
-      error ("The following section variable are used but not declared:\n"^
-        (String.concat ", " (List.map Id.to_string
-          (Id.Set.elements (Id.Set.diff inferred_set declared_set)))));
-    declared in
+        | Undef _ -> Id.Set.empty
+        | Def cs -> global_vars_set env (Lazyconstr.force cs)
+        | OpaqueDef lc -> global_vars_set env (Lazyconstr.force_opaque lc)
+      in
+      keep_hyps env (Id.Set.union ids_typ ids_def)
+    in
+    match ctx with
+      | None -> inferred
+      | Some declared ->
+        check_declared_variables declared inferred;
+        declared
+  in
   let tps = Cemitcodes.from_val (compile_constant_body env def) in
   { const_hyps = hyps;
     const_body = def;