Safe_typing code refactoring

 - No more modinfo sub-record in the safe_environment record,
   this was a syntactic pain.
     senv.modinfo.modpath --> senv.modpath
     senv.modinfo.variant --> senv.modvariant
     senv.modinfo.resolver --> senv.modresolver
     senv.modinfo.resolver_of_param --> senv.paramresolver
     senv.modinfo.label : removed (can be inferred from modpath)

 - No more systematic chaining of safe_environment ('old' field).
   Instead, earlier safe_environment is stored in the modvariant field
   when necessary (STRUCT and SIG case).

 - Improved sharing between end_module and end_modtype

 - More qualified names instead of open, better comments, ...

 - Some user errors are now checked earlier elsewhere (see for
   instance vernac_end_segment), so we can turn these errors into
   asserts. The user error about higher-order include is now algebraic.

 - Highlight the idea of a state monad in Safe_typing :
   type 'a safe_transformer = safe_environment -> 'a * safe_environment
   More systematic code in Global, thanks to 'globalize' function.

 - Declaremods : less informations stored in openmod_info

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

1 files changed, 55 insertions, 94 deletions

diff --git a/library/global.ml b/library/global.ml
index 22b69e4f2..fd6cce46f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -9,20 +9,19 @@
 open Names
 open Term
 open Environ
-open Safe_typing
 
-(* We introduce here the global environment of the system, and we declare it
-   as a synchronized table. *)
+(** We introduce here the global environment of the system,
+    and we declare it as a synchronized table. *)
 
 module GlobalSafeEnv : sig
 
-  val safe_env : unit -> safe_environment
-  val set_safe_env : safe_environment -> unit
+  val safe_env : unit -> Safe_typing.safe_environment
+  val set_safe_env : Safe_typing.safe_environment -> unit
   val join_safe_environment : unit -> unit
 
 end = struct
 
-let global_env = ref empty_environment
+let global_env = ref Safe_typing.empty_environment
 
 let join_safe_environment () =
   global_env := Safe_typing.join_safe_environment !global_env
@@ -37,7 +36,7 @@ let () =
         | `No -> !global_env
         | `Shallow -> prune_safe_environment !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
-      init_function = (fun () -> global_env := empty_environment) }
+      init_function = (fun () -> global_env := Safe_typing.empty_environment) }
 
 let assert_not_parsing () =
   if !Flags.we_are_parsing then
@@ -50,89 +49,57 @@ let set_safe_env e = global_env := e
 
 end
 
-open GlobalSafeEnv
-let safe_env = safe_env
-let join_safe_environment = join_safe_environment
+let safe_env = GlobalSafeEnv.safe_env
+let join_safe_environment = GlobalSafeEnv.join_safe_environment
 
-let env () = env_of_safe_env (safe_env ())
+let env () = Safe_typing.env_of_safe_env (safe_env ())
 
-let env_is_empty () = is_empty (safe_env ())
+let env_is_initial () = Safe_typing.is_initial (safe_env ())
 
-(* Then we export the functions of [Typing] on that environment. *)
-
-let universes () = universes (env())
-let named_context () = named_context (env())
-let named_context_val () = named_context_val (env())
-
-let push_named_assum a =
-  let (cst,env) = push_named_assum a (safe_env ()) in
-  set_safe_env env;
-  cst
-let push_named_def d =
-  let (cst,env) = push_named_def d (safe_env ()) in
-  set_safe_env env;
-  cst
+(** Turn ops over the safe_environment state monad to ops on the global env *)
 
+let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ()))
 
-let add_thing add dir id thing =
-  let kn, newenv = add dir (Label.of_id id) thing (safe_env ()) in
-    set_safe_env newenv;
-    kn
+let globalize f =
+  let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res
 
-let add_constant = add_thing add_constant
-let add_mind = add_thing add_mind
-let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y
+let globalize_with_summary fs f =
+  let res,env = f (safe_env ()) in
+  Summary.unfreeze_summaries fs;
+  GlobalSafeEnv.set_safe_env env;
+  res
 
+(** [Safe_typing] operations, now operating on the global environment *)
 
-let add_module id me inl =
-  let l = Label.of_id id in
-  let mp,resolve,new_env = add_module l me inl (safe_env ()) in
-    set_safe_env new_env;
-    mp,resolve
-    
+let i2l = Label.of_id
 
-let add_constraints c = set_safe_env (add_constraints c (safe_env ()))
+let push_named_assum a = globalize (Safe_typing.push_named_assum a)
+let push_named_def d = globalize (Safe_typing.push_named_def d)
+let add_constraints c = globalize0 (Safe_typing.add_constraints c)
+let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
+let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
+let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
+let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
+let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
 
-let set_engagement c = set_safe_env (set_engagement c (safe_env ()))
-
-let add_include me is_module inl =
-  let resolve,newenv = add_include me is_module inl (safe_env ()) in
-    set_safe_env newenv;
-    resolve
-
-let start_module id =
-  let l = Label.of_id id in
-  let mp,newenv = start_module l (safe_env ()) in
-    set_safe_env newenv;
-    mp
+let start_module id = globalize (Safe_typing.start_module (i2l id))
+let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
 
 let end_module fs id mtyo =
-  let l = Label.of_id id in
-  let mp,resolve,newenv = end_module l mtyo (safe_env ()) in
-    Summary.unfreeze_summaries fs;
-    set_safe_env newenv;
-    mp,resolve
+  globalize_with_summary fs (Safe_typing.end_module (i2l id) mtyo)
 
+let end_modtype fs id =
+  globalize_with_summary fs (Safe_typing.end_modtype (i2l id))
 
 let add_module_parameter mbid mte inl =
-  let resolve,newenv = add_module_parameter mbid mte inl (safe_env ()) in
-    set_safe_env newenv;
-    resolve
+  globalize (Safe_typing.add_module_parameter mbid mte inl)
 
+(** Queries on the global environment *)
 
-let start_modtype id =
-  let l = Label.of_id id in
-  let mp,newenv = start_modtype l (safe_env ()) in
-    set_safe_env newenv;
-    mp
-
-let end_modtype fs id =
-  let l = Label.of_id id in
-  let kn,newenv = end_modtype l (safe_env ()) in
-    Summary.unfreeze_summaries fs;
-    set_safe_env newenv;
-    kn
-
+let universes () = universes (env())
+let named_context () = named_context (env())
+let named_context_val () = named_context_val (env())
 
 let lookup_named id = lookup_named id (env())
 let lookup_constant kn = lookup_constant kn (env())
@@ -142,35 +109,32 @@ let lookup_mind kn = lookup_mind kn (env())
 let lookup_module mp = lookup_module mp (env())
 let lookup_modtype kn = lookup_modtype kn (env())
 
+let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
+
+(** Operations on kernel names *)
+
 let constant_of_delta_kn kn =
-  let resolver,resolver_param = (delta_of_senv (safe_env ())) in
+  let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ())
+  in
   (* TODO : are resolver and resolver_param orthogonal ?
      the effect of resolver is lost if resolver_param isn't
      trivial at that spot. *)
   Mod_subst.constant_of_deltas_kn resolver_param resolver kn
 
 let mind_of_delta_kn kn =
-  let resolver,resolver_param = (delta_of_senv (safe_env ())) in
+  let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ())
+  in
   (* TODO idem *)
   Mod_subst.mind_of_deltas_kn resolver_param resolver kn
 
-let exists_objlabel id = exists_objlabel id (safe_env ())
-
-let start_library dir =
-  let mp,newenv = start_library dir (safe_env ()) in
-    set_safe_env newenv;
-    mp
-
-let export s = export (safe_env ()) s
-
-let import cenv digest =
-  let mp,newenv,values = import cenv digest (safe_env ()) in
-    set_safe_env newenv;
-    mp, values
+(** Operations on libraries *)
 
+let start_library dir = globalize (Safe_typing.start_library dir)
+let export s = Safe_typing.export (safe_env ()) s
+let import cenv digest = globalize (Safe_typing.import cenv digest)
 
 
-(*s Function to get an environment from the constants part of the global
+(** Function to get an environment from the constants part of the global
     environment and a given context. *)
 
 let env_of_context hyps =
@@ -194,9 +158,6 @@ let type_of_global t = type_of_reference (env ()) t
 
 (* spiwack: register/unregister functions for retroknowledge *)
 let register field value by_clause =
-  let entry = kind_of_term value in
-  let senv = Safe_typing.register (safe_env ()) field entry by_clause in
-  set_safe_env senv
+  globalize0 (Safe_typing.register field (kind_of_term value) by_clause)
 
-let register_inline c =
-  set_safe_env (Safe_typing.register_inline c (safe_env ()))
+let register_inline c = globalize0 (Safe_typing.register_inline c)