Renamig support added to "Arguments"

Example:
  Arguments eq_refl {B y}, [B] y.
  Check (eq_refl (B := nat)).

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

4 files changed, 145 insertions, 3 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
new file mode 100644
index 0000000000..5e2284e137
--- /dev/null
+++ b/pretyping/arguments_renaming.ml
@@ -0,0 +1,118 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i*)
+open Names
+open Libnames
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Util
+open Pp
+open Libobject
+open Nameops
+(*i*)
+
+let empty_name_table = (Refmap.empty : name list list Refmap.t)
+let name_table = ref empty_name_table
+
+let _ =
+  Summary.declare_summary "rename-arguments"
+    { Summary.freeze_function = (fun () -> !name_table);
+      Summary.unfreeze_function = (fun r -> name_table := r);
+      Summary.init_function = (fun () -> name_table := empty_name_table) }
+
+type req =
+  | ReqLocal
+  | ReqGlobal of global_reference * name list list
+
+let load_rename_args _ (_, (_, (r, names))) =
+  name_table := Refmap.add r names !name_table
+
+let cache_rename_args o = load_rename_args 1 o
+
+let classify_rename_args = function
+  | ReqLocal, _ -> Dispose
+  | ReqGlobal _, _ as o -> Substitute o
+
+let subst_rename_args (subst, (_, (r, names as orig))) = 
+  ReqLocal,
+  let r' = fst (subst_global subst r) in 
+  if r==r' then orig else (r', names)
+
+let section_segment_of_reference = function
+  | ConstRef con -> Lib.section_segment_of_constant con
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+      Lib.section_segment_of_mutual_inductive kn
+  | _ -> []
+
+let discharge_rename_args = function
+  | _, (ReqGlobal (c, names), _) ->
+     let c' = pop_global_reference c in
+     let vars = section_segment_of_reference c in
+     let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
+     let names' = List.map (fun l -> var_names @ l) names in
+     Some (ReqGlobal (c', names), (c', names'))
+  | _ -> None
+
+let rebuild_rename_args x = x
+
+let inRenameArgs = declare_object { (default_object "RENAME-ARGUMENTS" ) with
+  load_function = load_rename_args;
+  cache_function = cache_rename_args;
+  classify_function = classify_rename_args;
+  subst_function = subst_rename_args;
+  discharge_function = discharge_rename_args;
+  rebuild_function = rebuild_rename_args;
+}
+
+let rename_arguments local r names =
+  let req = if local then ReqLocal else ReqGlobal (r, names) in
+  Lib.add_anonymous_leaf (inRenameArgs (req, (r, names)))       
+
+let arguments_names r = Refmap.find r !name_table
+
+let rec rename_prod c = function 
+  | [] -> c
+  | (Name _ as n) :: tl -> 
+      (match kind_of_type c with
+      | ProdType (_, s, t) -> mkProd (n, s, rename_prod t tl)
+      | _ -> c)
+  | _ :: tl -> 
+      match kind_of_type c with
+      | ProdType (n, s, t) -> mkProd (n, s, rename_prod t tl)
+      | _ -> c
+        
+let rename_type ty ref =
+  try rename_prod ty (List.hd (arguments_names ref))
+  with Not_found -> ty
+
+let rename_type_of_constant env c =
+  let ty = Typeops.type_of_constant env c in
+  rename_type ty (ConstRef c)
+
+let rename_type_of_inductive env ind =
+  let ty = Inductiveops.type_of_inductive env ind in
+  rename_type ty (IndRef ind)
+
+let rename_type_of_constructor env cstruct =
+  let ty = Inductiveops.type_of_constructor env cstruct in
+  rename_type ty (ConstructRef cstruct)
+
+let rename_typing env c =
+  let j = Typeops.typing env c in
+  match kind_of_term c with
+  | Const c -> { j with uj_type = rename_type j.uj_type (ConstRef c) }
+  | Ind i -> { j with uj_type = rename_type j.uj_type (IndRef i) }
+  | Construct k -> { j with uj_type = rename_type j.uj_type (ConstructRef k) }
+  | _ -> j
+
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
new file mode 100644
index 0000000000..a484ecf7f8
--- /dev/null
+++ b/pretyping/arguments_renaming.mli
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Libnames
+open Environ
+open Term
+
+val rename_arguments : bool -> global_reference -> name list list -> unit
+
+(** [Not_found] is raised is no names are defined for [r] *)
+val arguments_names : global_reference -> name list list
+
+val rename_type_of_constant : env -> constant -> types
+val rename_type_of_inductive : env -> inductive -> types
+val rename_type_of_constructor : env -> constructor -> types
+val rename_typing : env -> constr -> unsafe_judgment
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 6e2c0a761d..9eec941463 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -11,6 +11,7 @@ Evarutil
 Term_dnet
 Recordops
 Evarconv
+Arguments_renaming
 Typing
 Glob_term
 Pattern
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 344a2e91f5..efcdff9dc6 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -17,6 +17,7 @@ open Inductive
 open Inductiveops
 open Typeops
 open Evd
+open Arguments_renaming
 
 let meta_type evd mv =
   let ty =
@@ -159,13 +160,13 @@ let rec execute env evdref cstr =
         judge_of_variable env id
 
     | Const c ->
-        make_judge cstr (type_of_constant env c)
+        make_judge cstr (rename_type_of_constant env c)
 
     | Ind ind ->
-	make_judge cstr (type_of_inductive env ind)
+	make_judge cstr (rename_type_of_inductive env ind)
 
     | Construct cstruct ->
-	make_judge cstr (type_of_constructor env cstruct)
+	make_judge cstr (rename_type_of_constructor env cstruct)
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evdref c in