Ajout nat_path et find_reference

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

2 files changed, 45 insertions, 21 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index b8a93cf3a5..8a55bfc2c8 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -19,18 +19,22 @@ open Nametab
 (************************************************************************)
 (* Generic functions to find Coq objects *)
 
+type message = string
+
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
-let gen_reference locstr dir s =
-  let dir = make_dir ("Coq"::dir) in
-  let sp = Libnames.make_path dir (id_of_string s) in
+let find_reference locstr dir s =
+  let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
   try
     Nametab.absolute_reference sp
   with Not_found ->
     anomaly (locstr^": cannot find "^(string_of_path sp))
-    
-let gen_constant locstr dir s = 
-  constr_of_global (gen_reference locstr dir s)
+
+let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
+let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
+
+let gen_reference = coq_reference
+let gen_constant = coq_constant
 
 let list_try_find f = 
   let rec try_find_f = function
@@ -111,32 +115,33 @@ let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
 let arith_module = make_dir ["Coq";"Arith";"Arith"]
 
 (* TODO: temporary hack *)
-let make_path dir id = Libnames.encode_kn dir id
+let make_kn dir id = Libnames.encode_kn dir id
 
 (** Natural numbers *)
-let nat_path = make_path datatypes_module (id_of_string "nat")
+let nat_kn = make_kn datatypes_module (id_of_string "nat")
+let nat_path = Libnames.make_path datatypes_module (id_of_string "nat")
 
-let glob_nat = IndRef (nat_path,0)
+let glob_nat = IndRef (nat_kn,0)
 
-let path_of_O = ((nat_path,0),1)
-let path_of_S = ((nat_path,0),2)
+let path_of_O = ((nat_kn,0),1)
+let path_of_S = ((nat_kn,0),2)
 let glob_O = ConstructRef path_of_O
 let glob_S = ConstructRef path_of_S
 
 (** Booleans *)
-let bool_path = make_path datatypes_module (id_of_string "bool")
+let bool_kn = make_kn datatypes_module (id_of_string "bool")
 
-let glob_bool = IndRef (bool_path,0)
+let glob_bool = IndRef (bool_kn,0)
 
-let path_of_true = ((bool_path,0),1)
-let path_of_false = ((bool_path,0),2)
+let path_of_true = ((bool_kn,0),1)
+let path_of_false = ((bool_kn,0),2)
 let glob_true  = ConstructRef path_of_true
 let glob_false  = ConstructRef path_of_false
 
 (** Equality *)
-let eq_path = make_path logic_module (id_of_string "eq")
+let eq_kn = make_kn logic_module (id_of_string "eq")
 
-let glob_eq = IndRef (eq_path,0)
+let glob_eq = IndRef (eq_kn,0)
 
 type coq_sigma_data = {
   proj1 : constr;
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 0848c30846..ed5e46c1a0 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -19,11 +19,29 @@ open Pattern
 (*s This module collects the global references, constructions and
     patterns of the standard library used in ocaml files *)
 
-(*s Some utilities, the first argument is used for error messages.
-    Must be used lazyly. s*)
+(*s [find_reference caller_message [dir;subdir;...] s] returns a global
+   reference to the name dir.subdir.(...).s; the corresponding module
+   must have been required or in the process of being compiled so that
+   it must be used lazyly; it raises an anomaly with the given message
+   if not found *)
 
-val gen_reference : string->string list -> string -> global_reference
-val gen_constant : string->string list -> string -> constr
+type message = string
+
+val find_reference : message -> string list -> string -> global_reference
+
+(* [coq_reference caller_message [dir;subdir;...] s] returns a
+   global reference to the name Coq.dir.subdir.(...).s *)
+
+val coq_reference : message -> string list -> string -> global_reference
+
+(* idem but return a term *)
+
+val coq_constant : message -> string list -> string -> constr
+
+(* Synonyms of [coq_constant] and [coq_reference] *)
+
+val gen_constant : message -> string list -> string -> constr
+val gen_reference :  message -> string list -> string -> global_reference
 
 (* Search in several modules (not prefixed by "Coq") *)
 val gen_constant_in_modules : string->string list list-> string -> constr
@@ -41,6 +59,7 @@ val logic_module : dir_path
 val logic_type_module : dir_path
 
 (* Natural numbers *)
+val nat_path : section_path
 val glob_nat : global_reference
 val path_of_O : constructor
 val path_of_S : constructor