environement global

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

2 files changed, 72 insertions, 0 deletions

diff --git a/library/global.ml b/library/global.ml
new file mode 100644
index 0000000000..d669410b89
--- /dev/null
+++ b/library/global.ml
@@ -0,0 +1,37 @@
+
+(* $Id$ *)
+
+open Typing
+open Summary
+
+(* We introduce here the global environment of the system, and we declare it
+   as a synchronized table. *)
+
+let global_env = ref empty_environment
+
+let _ = 
+  declare_summary "Global environment"
+    { freeze_function = (fun () -> !global_env);
+      unfreeze_function = (fun fr -> global_env := fr);
+      init_function = (fun () -> global_env := empty_environment) }
+
+(* Then we export the functions of [Typing] on that environment. *)
+
+let evar_map () = evar_map !global_env
+let universes () = universes !global_env
+let metamap () = metamap !global_env
+let context () = context !global_env
+
+let push_var idc = global_env := push_var idc !global_env
+let push_rel nac = global_env := push_rel nac !global_env
+let add_constant sp ce = global_env := add_constant sp ce !global_env
+let add_parameter sp c = global_env := add_parameter sp c !global_env
+let add_mind sp mie = global_env := add_mind sp mie !global_env
+
+let lookup_var id = lookup_var id !global_env
+let lookup_rel n = lookup_rel n !global_env
+let lookup_constant sp = lookup_constant sp !global_env
+let lookup_mind sp = lookup_mind sp !global_env
+let lookup_mind_specif c = lookup_mind_specif c !global_env
+let lookup_meta n = lookup_meta n !global_env
+
diff --git a/library/global.mli b/library/global.mli
new file mode 100644
index 0000000000..4f04d2e51f
--- /dev/null
+++ b/library/global.mli
@@ -0,0 +1,35 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Univ
+open Term
+open Sign
+open Evd
+open Constant
+open Inductive
+(*i*)
+
+(* This module defines the global environment of Coq. 
+   The functions below are the exactly the same as the ones in [Typing],
+   operating on that global environment. *)
+
+val evar_map : unit -> unit evar_map
+val universes : unit -> universes
+val metamap : unit -> (int * constr) list
+val context : unit -> context
+
+val push_var : identifier * constr -> unit
+val push_rel : name * constr -> unit
+val add_constant : section_path -> constant_entry -> unit
+val add_parameter : section_path -> constr -> unit
+val add_mind : section_path -> mutual_inductive_entry -> unit
+
+val lookup_var : identifier -> name * typed_type
+val lookup_rel : int -> name * typed_type
+val lookup_constant : section_path -> constant_body
+val lookup_mind : section_path -> mutual_inductive_body
+val lookup_mind_specif : constr -> mind_specif
+val lookup_meta : int -> constr
+