Modules dans COQ\!\!\!\!

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

1 files changed, 77 insertions, 8 deletions

diff --git a/library/global.ml b/library/global.ml
index db0e5f470..cdebc52f5 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -26,7 +26,7 @@ let safe_env () = !global_env
 let env () = env_of_safe_env !global_env
 
 let _ = 
-  declare_summary "Global environment"
+  declare_global_environment
     { freeze_function = (fun () -> !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
       init_function = (fun () -> global_env := empty_environment);
@@ -46,17 +46,81 @@ let push_named_def d =
   global_env := env;
   cst
 
-let add_constant sp ce = global_env := add_constant sp ce !global_env
-let add_mind sp mie = global_env := add_mind sp mie !global_env
+(*let add_thing add kn thing =
+  let _,dir,l = repr_kn kn in
+  let kn',newenv = add dir l thing !global_env in
+    if kn = kn' then
+      global_env := newenv
+    else
+      anomaly "Kernel names do not match."
+*)
+
+let add_thing add dir id thing = 
+  let kn, newenv = add dir (label_of_id id) thing !global_env in
+    global_env := newenv;
+    kn
+
+let add_constant = add_thing add_constant 
+let add_mind = add_thing add_mind
+let add_modtype = add_thing (fun _ -> add_modtype) ()
+let add_module = add_thing (fun _ -> add_module) ()
+
 let add_constraints c = global_env := add_constraints c !global_env
 
+
+
+let start_module dir id params mtyo =
+  let l = label_of_id id in
+  let mp,newenv = start_module dir l params mtyo !global_env in
+    global_env := newenv;
+    mp
+  
+let end_module id =
+  let l = label_of_id id in
+  let mp,newenv = end_module l !global_env in
+    global_env := newenv;
+    mp
+
+
+let start_modtype dir id params = 
+  let l = label_of_id id in
+  let mp,newenv = start_modtype dir l params !global_env in
+    global_env := newenv;
+    mp
+
+let end_modtype id =
+  let l = label_of_id id in
+  let kn,newenv = end_modtype l !global_env in
+    global_env := newenv;
+    kn
+
+
+
+
 let lookup_named id = lookup_named id (env())
-let lookup_constant sp = lookup_constant sp (env())
+let lookup_constant kn = lookup_constant kn (env())
 let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
-let lookup_mind sp = lookup_mind sp (env())
+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 start_library dir = 
+  let mp,newenv = start_library dir !global_env in
+    global_env := newenv; 
+    mp
+
+let export s = snd (export !global_env s)
+
+let import cenv digest = 
+  let mp,newenv = import cenv digest !global_env in 
+    global_env := newenv; 
+    mp
+
 
-let export s = export !global_env s
-let import cenv = global_env := import cenv !global_env
 
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
@@ -64,7 +128,7 @@ let import cenv = global_env := import cenv !global_env
 let env_of_context hyps = 
   reset_with_named_context hyps (env())
 
-open Nametab
+open Libnames
 
 let type_of_reference env = function
   | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t
@@ -73,3 +137,8 @@ let type_of_reference env = function
   | ConstructRef cstr -> Inductive.type_of_constructor env cstr
 
 let type_of_global t = type_of_reference (env ()) t
+
+
+(*let get_kn dp l = 
+  make_kn (current_modpath !global_env) dp l
+*)