Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

12 files changed, 92 insertions, 60 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b67dbc6e2..504f38b82 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -108,9 +108,9 @@ let declare_variable_common id obj =
 
 (* for initial declaration *)
 let declare_variable id obj =
-  let (_,kn as oname) = declare_variable_common id obj in
-  !xml_declare_variable kn;
-  Dischargedhypsmap.set_discharged_hyps (fst oname) [];
+  let (sp,kn as oname) = declare_variable_common id obj in
+  !xml_declare_variable oname;
+  Dischargedhypsmap.set_discharged_hyps sp [];
   oname
 
 (* when coming from discharge: no xml output *)
@@ -185,10 +185,10 @@ let hcons_constant_declaration = function
 
 let declare_constant id (cd,kind) =
   (* let cd = hcons_constant_declaration cd in *)
-  let (_,kn as oname) = add_leaf id (in_constant (ConstantEntry cd,kind)) in
+  let (sp,kn as oname) = add_leaf id (in_constant (ConstantEntry cd,kind)) in
   if is_implicit_args() then declare_constant_implicits kn;
-  Dischargedhypsmap.set_discharged_hyps (fst oname) [] ;
-  !xml_declare_constant kn;
+  Dischargedhypsmap.set_discharged_hyps sp [] ;
+  !xml_declare_constant oname;
   oname
 
 (* when coming from discharge *)
@@ -285,9 +285,9 @@ let declare_inductive_common mie =
 
 (* for initial declaration *)
 let declare_mind mie =
-  let (_,kn as oname) = declare_inductive_common mie in
-  Dischargedhypsmap.set_discharged_hyps (fst oname) [] ;
-  !xml_declare_inductive kn;
+  let (sp,kn as oname) = declare_inductive_common mie in
+  Dischargedhypsmap.set_discharged_hyps sp [] ;
+  !xml_declare_inductive oname;
   oname
 
 (* when coming from discharge: no xml output *)
@@ -361,13 +361,6 @@ let context_of_global_reference = function
   | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
   | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
 
-let reference_of_constr c = match kind_of_term c with
-  | Const sp -> ConstRef sp
-  | Ind ind_sp -> IndRef ind_sp
-  | Construct cstr_cp -> ConstructRef cstr_cp
-  | Var id -> VarRef id
-  |  _ -> raise Not_found
-
 let last_section_hyps dir =
   fold_named_context
     (fun (id,_,_) sec_ids ->
@@ -378,12 +371,6 @@ let last_section_hyps dir =
     (Environ.named_context (Global.env()))
     ~init:[]
 
-let constr_of_reference = function
-  | VarRef id -> mkVar id
-  | ConstRef sp -> mkConst sp
-  | ConstructRef sp -> mkConstruct sp
-  | IndRef sp -> mkInd sp
-
 let construct_absolute_reference sp =
   constr_of_reference (Nametab.absolute_reference sp)
 
diff --git a/library/declare.mli b/library/declare.mli
index 3c04ddf57..3a7849232 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -92,13 +92,6 @@ val clear_proofs : named_context -> named_context
 
 val context_of_global_reference : global_reference -> section_context
 
-(* Turn a global reference into a construction *)
-val constr_of_reference : global_reference -> constr
-
-(* Turn a construction denoting a global into a reference;
-   raise [Not_found] if not a global *)
-val reference_of_constr : constr -> global_reference
-
 val global_qualified_reference : qualid -> constr
 val global_absolute_reference : section_path -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
@@ -120,6 +113,6 @@ val strength_of_global : global_reference -> strength
 val library_part : global_reference -> dir_path
 
 (* hooks for XML output *)
-val set_xml_declare_variable : (kernel_name -> unit) -> unit
-val set_xml_declare_constant : (kernel_name -> unit) -> unit
-val set_xml_declare_inductive : (kernel_name -> unit) -> unit
+val set_xml_declare_variable : (object_name -> unit) -> unit
+val set_xml_declare_constant : (object_name -> unit) -> unit
+val set_xml_declare_inductive : (object_name -> unit) -> unit
diff --git a/library/goptions.ml b/library/goptions.ml
index 4d505b5aa..4c2d15206 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -177,7 +177,7 @@ let get_ref_table k = List.assoc (nickname k) !ref_table
 module type RefConvertArg =
 sig
   type t
-  val encode : qualid located -> t
+  val encode : reference -> t
   val subst : substitution -> t -> t
   val printer : t -> std_ppcmds
   val key : option_name
@@ -189,7 +189,7 @@ end
 module RefConvert = functor (A : RefConvertArg) -> 
 struct
   type t = A.t
-  type key = qualid located
+  type key = reference
   let table = ref_table
   let encode = A.encode
   let subst = A.subst
diff --git a/library/goptions.mli b/library/goptions.mli
index 28da69ea6..f19d99aaa 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -94,8 +94,8 @@ sig
 end
 
 (* The functor [MakeRefTable] declares a new table of objects of type
-   [A.t] practically denoted by [qualid]; the encoding function
-   [encode : qualid -> A.t] is typically a globalization function,
+   [A.t] practically denoted by [reference]; the encoding function
+   [encode : reference -> A.t] is typically a globalization function,
    possibly with some restriction checks; the function
    [member_message] say what to print when invoking the "Test Toto
    Titi foo." command; at the end [title] is the table name printed
@@ -107,7 +107,7 @@ module MakeRefTable :
   functor
     (A : sig
            type t
-           val encode : qualid located -> t
+           val encode : reference -> t
 	   val subst : substitution -> t -> t
            val printer : t -> std_ppcmds
            val key : option_name
@@ -156,9 +156,9 @@ val get_string_table :
 
 val get_ref_table :
   option_name ->
-    < add : qualid located -> unit;
-      remove : qualid located -> unit;
-      mem : qualid located -> unit;
+    < add : reference -> unit;
+      remove : reference -> unit;
+      mem : reference -> unit;
       print : unit >
 
 val set_int_option_value    : option_name -> int option -> unit
diff --git a/library/lib.ml b/library/lib.ml
index 323ca60de..243fc1aca 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -471,12 +471,12 @@ let reset_to sp =
   let (after,_,_) = split_lib spf in
   recache_context after
 
-let reset_name id =
+let reset_name (loc,id) =
   let (sp,_) = 
     try
       find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
     with Not_found ->
-      error (string_of_id id ^ ": no such entry")
+      user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
   in
   reset_to sp
 
diff --git a/library/lib.mli b/library/lib.mli
index 56e79b661..022ddb5cd 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (*i*)
+open Util
 open Names
 open Libnames
 open Libobject
@@ -141,7 +142,7 @@ val current_prefix : unit -> module_path * dir_path
 (*s Backtracking (undo). *)
 
 val reset_to : object_name -> unit
-val reset_name : identifier -> unit
+val reset_name : identifier located -> unit
 
 (* [back n] resets to the place corresponding to the $n$-th call of 
    [mark_end_of_command] (counting backwards) *)
diff --git a/library/libnames.ml b/library/libnames.ml
index 19e7d2833..79acb7231 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -11,6 +11,8 @@
 open Pp
 open Util
 open Names
+open Nameops
+open Term
 
 type global_reference =
   | VarRef of variable
@@ -30,6 +32,18 @@ let subst_global subst ref = match ref with
       let kn' = subst_kn subst kn in if kn==kn' then ref else
           ConstructRef ((kn',i),j)
 
+let reference_of_constr c = match kind_of_term c with
+  | Const sp -> ConstRef sp
+  | Ind ind_sp -> IndRef ind_sp
+  | Construct cstr_cp -> ConstructRef cstr_cp
+  | Var id -> VarRef id
+  |  _ -> raise Not_found
+
+let constr_of_reference = function
+  | VarRef id -> mkVar id
+  | ConstRef sp -> mkConst sp
+  | ConstructRef sp -> mkConstruct sp
+  | IndRef sp -> mkInd sp
 
 (**********************************************)
 
@@ -205,3 +219,23 @@ type global_dir_reference =
       let kn' = subst_kernel_name subst kn in if kn==kn' then ref else
           ModTypeRef kn'
 *)
+
+type reference = 
+  | Qualid of qualid located
+  | Ident of identifier located
+
+let qualid_of_reference = function
+  | Qualid (loc,qid) -> loc, qid
+  | Ident (loc,id) -> loc, make_short_qualid id
+
+let string_of_reference = function
+  | Qualid (loc,qid) -> string_of_qualid qid
+  | Ident (loc,id) -> string_of_id id
+
+let pr_reference = function 
+  | Qualid (_,qid) -> pr_qualid qid
+  | Ident (_,id) -> pr_id id
+
+let loc_of_reference = function
+  | Qualid (loc,qid) -> loc
+  | Ident (loc,id) -> loc
diff --git a/library/libnames.mli b/library/libnames.mli
index 04e552f4d..e8dd2a5ff 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -10,7 +10,9 @@
 
 (*i*)
 open Pp
+open Util
 open Names
+open Term
 (*i*)
 
 (*s Global reference is a kernel side type for all references together *)
@@ -22,7 +24,14 @@ type global_reference =
 
 val subst_global : substitution -> global_reference -> global_reference
 
-(* dirpaths *)
+(* Turn a global reference into a construction *)
+val constr_of_reference : global_reference -> constr
+
+(* Turn a construction denoting a global into a reference;
+   raise [Not_found] if not a global *)
+val reference_of_constr : constr -> global_reference
+
+(*s Dirpaths *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
 val dirpath_of_string : string -> dir_path
@@ -111,3 +120,13 @@ type global_dir_reference =
   | DirModule of object_prefix
   | DirClosedSection of dir_path
       (* this won't last long I hope! *)
+
+type reference = 
+  | Qualid of qualid located
+  | Ident of identifier located
+
+val qualid_of_reference : reference -> qualid located
+val string_of_reference : reference -> string
+val pr_reference : reference -> std_ppcmds
+val loc_of_reference : reference -> loc
+
diff --git a/library/nameops.ml b/library/nameops.ml
index 0fd9ec0d1..a61ba754b 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -11,9 +11,6 @@
 open Pp
 open Util
 open Names
-open Declarations
-open Environ
-open Term
 
 (* Identifiers *)
 
@@ -133,6 +130,11 @@ let out_name = function
   | Name id -> id
   | Anonymous -> anomaly "out_name: expects a defined name"
 
+let name_fold f na a =
+  match na with
+  | Name id -> f id a
+  | Anonymous -> a
+
 let next_name_away_with_default default name l = 
   match name with
     | Name str  -> next_ident_away str l
diff --git a/library/nameops.mli b/library/nameops.mli
index 591e9030d..50260d731 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -9,8 +9,6 @@
 (* $Id$ *)
 
 open Names
-open Term
-open Environ
 
 (* Identifiers and names *)
 val pr_id : identifier -> Pp.std_ppcmds
@@ -34,6 +32,7 @@ val next_name_away_with_default :
 
 val out_name : name -> identifier
 
+val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
 
 val pr_lab : label -> Pp.std_ppcmds
 
diff --git a/library/nametab.ml b/library/nametab.ml
index e50a0e6b9..d4707ecbc 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -387,7 +387,8 @@ let absolute_reference sp =
 let locate_in_absolute_module dir id =
   absolute_reference (make_path dir id)
 
-let global (loc,qid) =
+let global r =
+  let (loc,qid) = qualid_of_reference r in
   try match extended_locate qid with
     | TrueGlobal ref -> ref
     | SyntacticDef _ -> 
@@ -397,9 +398,6 @@ let global (loc,qid) =
   with Not_found ->
     error_global_not_found_loc loc qid
 
-
-
-
 (* Exists functions ********************************************************)
 
 let exists_cci sp = SpTab.exists sp !the_ccitab
@@ -452,12 +450,12 @@ let pr_global_env env ref =
   let s = string_of_qualid (shortest_qualid_of_global env ref) in
   (str s)
 
-let global_inductive (loc,qid as locqid) =
-  match global locqid with
+let global_inductive r =
+  match global r with
   | IndRef ind -> ind
   | ref ->
-      user_err_loc (loc,"global_inductive",
-        pr_qualid qid ++ spc () ++ str "is not an inductive type")
+      user_err_loc (loc_of_reference r,"global_inductive",
+        pr_reference r ++ spc () ++ str "is not an inductive type")
 
 (********************************************************************)
 
@@ -500,4 +498,3 @@ let _ =
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
       Summary.survive_section = false }
-
diff --git a/library/nametab.mli b/library/nametab.mli
index 2790e1536..d18a6c69d 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -85,10 +85,10 @@ val locate : qualid -> global_reference
 
 (* This function is used to transform a qualified identifier into a
    global reference, with a nice error message in case of failure *)
-val global : qualid located -> global_reference
+val global : reference -> global_reference
 
 (* The same for inductive types *)
-val global_inductive : qualid located -> inductive
+val global_inductive : reference -> inductive
 
 (* This locates also syntactic definitions *)
 val extended_locate : qualid -> extended_global_reference