module Logic

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

3 files changed, 51 insertions, 1 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 60a1c5960d..cb5ec1b40d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -3,6 +3,9 @@
 
 open Util
 open Names
+open Generic
+open Term
+open Sign
 open Constant
 open Inductive
 open Libobject
@@ -126,3 +129,42 @@ let declare_mind mie =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
+
+(* Global references. *)
+
+let first f v =
+  let n = Array.length v in
+  let rec look_for i =
+    if i = n then raise Not_found;
+    try f i v.(i) with Not_found -> look_for (succ i)
+  in
+  look_for 0
+
+let mind_oper_of_id sp id mib =
+  first 
+    (fun tyi mip ->
+       if id = mip.mind_typename then 
+	 MutInd (sp,tyi)
+       else
+	 first 
+	   (fun cj cid -> 
+	      if id = cid then 
+		MutConstruct((sp,tyi),succ cj) 
+	      else raise Not_found) 
+	   mip.mind_consnames)
+    mib.mind_packets
+
+let global_operator sp id =
+  try
+    let _ = Global.lookup_constant sp in Const sp
+  with Not_found -> 
+    let mib = Global.lookup_mind sp in
+    mind_oper_of_id sp id mib
+
+let global_reference id =
+  let sp = Nametab.sp_of_id CCI id in
+  let oper = global_operator sp id in
+  let hyps = get_globals (Global.context ()) in
+  let ids =  ids_of_sign hyps in
+  DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+
diff --git a/library/declare.mli b/library/declare.mli
index 21486c250e..f7a0fa0884 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -23,3 +23,11 @@ val declare_constant : identifier -> constant_entry -> unit
 
 val declare_mind : mutual_inductive_entry -> unit
 
+
+(*s It also provides a function [global_reference] to construct a global
+  constr (a constant, an inductive or a constructor) from an identifier.
+  To do so, it first looks for the section path using [Nametab.sp_of_id] and
+  then constructs the corresponding term, associated to the current 
+  environment of variables. *)
+
+val global_reference : identifier -> constr
diff --git a/library/global.mli b/library/global.mli
index 89cc83cbd5..2e0a541df2 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -13,7 +13,7 @@ open Typing
 (*i*)
 
 (* This module defines the global environment of Coq. 
-   The functions below are the exactly the same as the ones in [Typing],
+   The functions below are exactly the same as the ones in [Typing],
    operating on that global environment. *)
 
 val env : unit -> environment