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

11 files changed, 359 insertions, 21 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 4df8b9cc4..6a42678e4 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -80,6 +80,7 @@ Evarutil
 Term_dnet
 Recordops
 Evarconv
+Arguments_renaming
 Typing
 Pattern
 Matching
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 08a935a44..546f277e4 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -16,4 +16,3 @@ Constrextern
 Coqlib
 Discharge
 Declare
-
diff --git a/library/impargs.ml b/library/impargs.ml
index 5d689faa0..4cf8e9822 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -457,7 +457,17 @@ type implicit_discharge_request =
 let implicits_table = ref Refmap.empty
 
 let implicits_of_global ref =
-  try Refmap.find ref !implicits_table with Not_found -> [DefaultImpArgs,[]]
+  try
+    let l = Refmap.find ref !implicits_table in
+    try
+      let rename_l = Arguments_renaming.arguments_names ref in
+      let rename imp name = match imp, name with
+       | Some (_, x,y), Name id -> Some (id, x,y)
+       | _ -> imp in
+      List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
+    with Not_found -> l
+    | Invalid_argument _ -> anomaly "renaming implicits"
+  with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
   implicits_table := Refmap.add ref imps !implicits_table
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 741f9201e..3151fa6d0 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -119,6 +119,11 @@ let print_impargs_list prefix l =
 	    then print_one_impargs_list imps
 	    else [str "No implicit arguments"]))])]) l)
 
+let print_renames_list prefix l =
+  if l = [] then [prefix] else
+  [add_colon prefix ++ str "Arguments are renamed to " ++
+    hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
+
 let need_expansion impl ref =
   let typ = Global.type_of_global ref in
   let ctx = (prod_assum typ) in
@@ -231,6 +236,8 @@ let print_opacity ref =
 let print_name_infos ref =
   let impls = implicits_of_global ref in
   let scopes = Notation.find_arguments_scope ref in
+  let renames =
+    try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in
   let type_info_for_implicit =
     if need_expansion (select_impargs_size 0 impls) ref then
       (* Need to reduce since implicits are computed with products flattened *)
@@ -239,6 +246,7 @@ let print_name_infos ref =
     else
       [] in
   type_info_for_implicit @
+  print_renames_list (mt()) renames @
   print_impargs_list (mt()) impls @
   print_argument_scopes (mt()) scopes
 
@@ -263,6 +271,12 @@ let print_inductive_implicit_args =
     implicits_of_global (fun l -> positions_of_implicits l <> [])
     print_impargs_list
 
+let print_inductive_renames =
+  print_args_data_of_inductive_ids
+    (fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> [])
+    ((<>) Anonymous)
+    print_renames_list
+
 let print_inductive_argument_scopes =
   print_args_data_of_inductive_ids
     Notation.find_arguments_scope ((<>) None) print_argument_scopes
@@ -380,7 +394,8 @@ let gallina_print_inductive sp =
   let mipv = mib.mind_packets in
   pr_mutual_inductive_body env sp mib ++ fnl () ++
   with_line_skip
-    (print_inductive_implicit_args sp mipv @
+    (print_inductive_renames sp mipv @
+     print_inductive_implicit_args sp mipv @
      print_inductive_argument_scopes sp mipv)
 
 let print_named_decl id =
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
new file mode 100644
index 000000000..5e2284e13
--- /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 000000000..a484ecf7f
--- /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 6e2c0a761..9eec94146 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 344a2e91f..efcdff9dc 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
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
new file mode 100644
index 000000000..ed08334e7
--- /dev/null
+++ b/test-suite/output/Arguments_renaming.out
@@ -0,0 +1,104 @@
+@eq_refl
+     : forall (B : Type) (y : B), y = y
+eq_refl
+     : forall x : nat, x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+
+For eq_refl: Arguments are renamed to B, y
+For eq: Argument A is implicit and maximally inserted
+For eq_refl, when applied to no arguments:
+  Arguments B, y are implicit and maximally inserted
+For eq_refl, when applied to 1 argument:
+  Argument B is implicit
+For eq: Argument scopes are [type_scope _ _]
+For eq_refl: Argument scopes are [type_scope _]
+eq_refl : forall (A : Type) (x : A), x = x
+
+Arguments are renamed to B, y
+When applied to no arguments:
+  Arguments B, y are implicit and maximally inserted
+When applied to 1 argument:
+  Argument B is implicit
+Argument scopes are [type_scope _]
+Expands to: Constructor Coq.Init.Logic.eq_refl
+Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
+
+For myrefl: Arguments are renamed to C, x, _
+For myrefl: Argument C is implicit and maximally inserted
+For myEq: Argument scopes are [type_scope _ _]
+For myrefl: Argument scopes are [type_scope _ _]
+myrefl : forall (B : Type) (x : A), B -> myEq B x x
+
+Arguments are renamed to C, x, _
+Argument C is implicit and maximally inserted
+Argument scopes are [type_scope _ _]
+Expands to: Constructor Top.Test1.myrefl
+myplus = 
+fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S n' => S (myplus T t n' m)
+  end
+     : forall T : Type, T -> nat -> nat -> nat
+
+Arguments are renamed to Z, t, n, m
+Argument Z is implicit and maximally inserted
+Argument scopes are [type_scope _ nat_scope nat_scope]
+myplus : forall T : Type, T -> nat -> nat -> nat
+
+Arguments are renamed to Z, t, n, m
+Argument Z is implicit and maximally inserted
+Argument scopes are [type_scope _ nat_scope nat_scope]
+The simpl tactic unfolds myplus
+  when the 2nd and 3rd arguments evaluate to a constructor 
+myplus is transparent
+Expands to: Constant Top.Test1.myplus
+myplus
+     : forall Z : Type, Z -> nat -> nat -> nat
+Inductive myEq (A B : Type) (x : A) : A -> Prop :=
+    myrefl : B -> myEq A B x x
+
+For myrefl: Arguments are renamed to A, C, x, _
+For myrefl: Argument C is implicit and maximally inserted
+For myEq: Argument scopes are [type_scope type_scope _ _]
+For myrefl: Argument scopes are [type_scope type_scope _ _]
+myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
+
+Arguments are renamed to A, C, x, _
+Argument C is implicit and maximally inserted
+Argument scopes are [type_scope type_scope _ _]
+Expands to: Constructor Top.myrefl
+myrefl
+     : forall (A C : Type) (x : A), C -> myEq A C x x
+myplus = 
+fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S n' => S (myplus T t n' m)
+  end
+     : forall T : Type, T -> nat -> nat -> nat
+
+Arguments are renamed to Z, t, n, m
+Argument Z is implicit and maximally inserted
+Argument scopes are [type_scope _ nat_scope nat_scope]
+myplus : forall T : Type, T -> nat -> nat -> nat
+
+Arguments are renamed to Z, t, n, m
+Argument Z is implicit and maximally inserted
+Argument scopes are [type_scope _ nat_scope nat_scope]
+The simpl tactic unfolds myplus
+  when the 2nd and 3rd arguments evaluate to a constructor 
+myplus is transparent
+Expands to: Constant Top.myplus
+myplus
+     : forall Z : Type, Z -> nat -> nat -> nat
+The command has indeed failed with message:
+=> Error: All arguments lists must declare the same names
+The command has indeed failed with message:
+=> Error: The following arguments are not declared: x
+The command has indeed failed with message:
+=> Error: Arguments names must be distinct
+The command has indeed failed with message:
+=> Error: Argument z is anonymous and cannot be declared implicit
+The command has indeed failed with message:
+=> Error: Extra argument y
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
new file mode 100644
index 000000000..7cbb6801e
--- /dev/null
+++ b/test-suite/output/Arguments_renaming.v
@@ -0,0 +1,48 @@
+Arguments eq_refl {B y}, [B] y.
+Check @eq_refl.
+Check (eq_refl (B := nat)).
+Print eq_refl.
+About eq_refl.
+
+Goal 3 = 3.
+apply @eq_refl with (B := nat).
+Undo.
+apply @eq_refl with (y := 3).
+Undo.
+pose (y := nat).
+apply (@eq_refl y) with (y0 := 3).
+Qed.
+
+Section Test1.
+
+Variable A : Type.
+
+Inductive myEq B (x : A) : A -> Prop := myrefl : B -> myEq B x x.
+
+Global Arguments myrefl {C} x _.
+Print myrefl.
+About myrefl.
+
+Fixpoint myplus T (t : T) (n m : nat) {struct n} :=
+  match n with O => m | S n' => S (myplus T t n' m) end.
+
+Global Arguments myplus {Z} !t !n m.
+
+Print myplus.
+About myplus.
+Check @myplus.
+
+End Test1.
+Print myrefl.
+About myrefl.
+Check myrefl.
+
+Print myplus.
+About myplus.
+Check @myplus.
+
+Fail Arguments eq_refl {F g}, [H] k.
+Fail Arguments eq_refl {F}, [F].
+Fail Arguments eq_refl {F F}, [F] F.
+Fail Arguments eq {F} x [z].
+Fail Arguments eq {F} x z y.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 71bd31189..916a305c2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -768,23 +768,42 @@ let vernac_declare_arguments local r l nargs flags =
   let names, rest = List.hd names, List.tl names in
   if List.exists ((<>) names) rest then
     error "All arguments lists must declare the same names";
+  if not (Util.list_distinct (List.filter ((<>) Anonymous) names)) then
+    error "Arguments names must be distinct";
+  let sr = smart_global r in
   let inf_names =
-    Impargs.compute_implicits_names (Global.env())
-      (Global.type_of_global (smart_global r)) in
+    Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in
   let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in
-  let rec check ld li = match ld, li with
+  let rec check li ld = match li, ld with
     | [], [] -> ()
-    | [], l -> error ("The following arguments are not declared: " ^
+    | [], x::_ -> error ("Extra argument " ^ string_of_name x)
+    | l, [] -> error ("The following arguments are not declared: " ^
        (String.concat ", " (List.map string_of_name l)))
-    | x::_, [] -> error ("Extra argument " ^ string_of_name x)
-    | Name x::_, Name y::_ when x <> y -> error ("The declared name " ^
-        string_of_id x ^ " and the inferred one " ^ string_of_id y ^
-        " are different")
-    | _::ld, _::li -> check ld li in
-  if names <> [] then check names inf_names;
-  let implicits = List.map (Util.list_map_filter (function
-    | (Anonymous, _,_,_,_) | (_,_,_, false, _) -> None
-    | (Name id, _,_, true, max) -> Some (ExplByName id,max,false))) l in
+    | _::li, _::ld -> check li ld in
+  if names <> [] then
+    List.iter (fun l -> check inf_names l) (names :: rest);
+  let some_renaming_specified, implicits =
+    if names = [] then false, [[]] else
+    let never_implicit x =
+      not (List.exists (List.exists (fun (y, _,_, b, _) -> b && y = x)) l) in
+    Util.list_fold_map (fun sr il ->
+      let sr', impl = Util.list_fold_map (fun b -> function
+        | (Anonymous, _,_, true, _), _ ->
+            error "Implicit arguments must have a name"
+        | (Name x,_,_,false,_),Name y when x <> y && never_implicit (Name x)->
+            error ("Reanaming a non implicit argument " ^ string_of_id y ^
+              " to " ^ string_of_id x)
+        | (Name x, _,_, true, _), Anonymous ->
+            error ("Argument "^string_of_id x^" is anonymous and cannot be"^
+              " declared implicit")
+        | (Name iid, _,_, true, max), Name id ->
+           b || iid <> id, Some (ExplByName id, max, false)
+        | _ -> b, None)
+        false (List.combine il inf_names) in
+      sr || sr', Util.list_map_filter (fun x -> x) impl)
+      false l in
+  if some_renaming_specified then
+    Arguments_renaming.rename_arguments local sr (names :: rest);
   (* All other infos are in the first item of l *)
   let l = List.hd l in
   let some_implicits_specified = implicits <> [[]] in
@@ -810,7 +829,7 @@ let vernac_declare_arguments local r l nargs flags =
     | [] -> [] | _ :: tl -> narrow tl in
   let flags = narrow flags in
   if rargs <> [] || nargs >= 0 || flags <> [] then
-    match smart_global r with
+    match sr with
     | ConstRef _ as c ->
        Tacred.set_simpl_behaviour local c (rargs, nargs, flags)
     | _ -> error "Simpl behaviour can be declared for constants only"
@@ -1096,7 +1115,7 @@ let vernac_check_may_eval redexp glopt rc =
   let j =
     try
       Evarutil.check_evars env sigma sigma' c;
-      Typeops.typing env c
+      Arguments_renaming.rename_typing env c
     with P.PretypeError (_,_,P.UnsolvableImplicit _)
       | Compat.Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) ->
       Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in