Mise en place systeme de renommage des noms de variables liees dans la bibliotheque standard

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

4 files changed, 118 insertions, 3 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 4397f67695..ccda07549e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -115,7 +115,12 @@ let pr_bindings prc prlc = function
   | NoBindings -> mt ()
 
 let pr_with_bindings prc prlc (c,bl) =
-  prc c ++ hv 0 (pr_bindings prc prlc bl)
+  if Options.do_translate () then
+    (* translator calls pr_with_bindings on rawconstr: we cast it! *)
+    let bl' = Ppconstrnew.translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in
+    prc c ++ hv 0 (pr_bindings prc prlc bl')
+  else
+    prc c ++ hv 0 (pr_bindings prc prlc bl)
 
 let pr_with_constr prc = function
   | None -> mt ()
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 0154110e55..f708f12d1d 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -709,3 +709,103 @@ let pr_constr_pattern_env env c =
 let pr_constr_pattern t =
   pr lsimple
     (Constrextern.extern_pattern (Global.env()) Termops.empty_names_context t)
+
+
+(************************************************************************)
+(* Automatic standardisation of names in Arith and ZArith by translator *)
+(* Very not robust *)
+
+let is_arith_dir dir id =
+  let dirs = List.map string_of_id (repr_dirpath dir) in
+  match List.rev dirs with
+  | "Coq"::"Arith"::"Between"::_ -> false
+  | "Coq"::"ZArith"::("Wf_Z"|"Zpower"|"Zlogarithm"|"Zbinary"|"Zdiv")::_ -> false
+  | "Coq"::("Arith"|"NArith"|"ZArith")::_ -> true
+  | "Coq"::"Init"::"Peano"::_ -> true
+  | "Coq"::"Init"::"Logic"::_ when string_of_id id = "iff_trans" -> true
+  | _ -> false
+
+let is_arith ref =
+  let sp = sp_of_global ref in
+  is_arith_dir (dirpath sp) (basename sp)
+
+let get_name (ln,lp,lz) id n =
+  let id' = string_of_id n in
+  (match id' with
+    | "nat" -> (id_of_string (List.hd ln),(List.tl ln,lp,lz))
+    | "positive" -> (id_of_string (List.hd lp),(ln,List.tl lp,lz))
+    | "Z" -> (id_of_string (List.hd lz),(ln,lp,List.tl lz))
+    | _ -> id,(ln,lp,lz))
+
+let get_name_constr names id t = match kind_of_term t with
+  | Ind ind ->
+      let n = basename (sp_of_global (IndRef ind)) in
+      get_name names id n
+  | _ -> id,names
+
+let names = (["n";"m";"p";"q"],["p";"q";"r";"s"],["n";"m";"p";"q"])
+
+let znames t =
+  let rec aux c names = match kind_of_term c with
+    | Prod (Name id as na,t,c) ->
+	let (id,names) = get_name_constr names id t in
+	(na,id) :: aux c names
+    | Prod (Anonymous,t,c) ->
+	(Anonymous,id_of_string "ZZ") :: aux c names
+    | _ -> []
+  in aux t names
+
+let get_name_raw names id t = match t with
+  | CRef(Ident (_,n)) -> get_name names id n
+  | _ -> id,names
+
+let rename_bound_variables id t =
+  if is_arith_dir (Lib.library_dp()) id then
+  let rec aux c names subst = match c with
+    | CProdN (loc,bl,c) ->
+	let rec aux2 names subst = function
+	  | (nal,t)::bl ->
+	      let rec aux3 names subst = function
+		| (loc,Name id)::nal ->
+		    let (id',names) = get_name_raw names id t in
+		    let (nal,names,subst) = aux3 names ((id,id')::subst) nal in
+		    (loc,Name id')::nal, names, subst
+		| x::nal -> 
+		    let (nal,names,subst) = aux3 names subst nal in
+		    x::nal,names,subst
+		| [] -> [],names,subst in
+	      let t = replace_vars_constr_expr subst t in
+	      let nal,names,subst = aux3 names subst nal in
+	      let bl,names,subst = aux2 names subst bl in
+	      (nal,t)::bl, names, subst
+	  | [] -> [],names,subst in
+	let bl,names,subst = aux2 names subst bl in
+	CProdN (loc,bl,aux c names subst)
+    | CArrow (loc,t,u) ->
+	let u = aux u names subst in
+	CArrow (loc,replace_vars_constr_expr subst t,u)
+    | _ -> replace_vars_constr_expr subst c
+  in aux t names []
+  else t
+
+let translate_binding kn n ebl =
+  let t = Retyping.get_type_of (Global.env()) Evd.empty (mkConst kn) in
+  let subst = znames t in
+  try
+    let _,subst' = list_chop n subst in
+    List.map (function
+      | (x,NamedHyp id,c) -> (x,NamedHyp (List.assoc (Name id) subst'),c)
+      |  x -> x) ebl
+  with _ -> ebl
+
+let translate_with_bindings c bl =
+  match bl with
+    | ExplicitBindings l -> ExplicitBindings
+	(match c with
+	  | RRef (_,(ConstRef kn as ref)) when is_arith ref -> 
+	      translate_binding kn 0 l
+	  | RApp (_,RRef (_,(ConstRef kn as ref)), args) when is_arith ref ->
+	      translate_binding kn (List.length args) l
+	  | _ ->
+	      l)
+    | x -> x
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 44277a5552..968464f651 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -82,3 +82,7 @@ val pr_lterm : constr -> std_ppcmds
 
 val pr_constr_pattern_env : env -> Pattern.constr_pattern -> std_ppcmds
 val pr_constr_pattern : Pattern.constr_pattern -> std_ppcmds
+
+(* To translate names in ZArith *)
+val translate_with_bindings : rawconstr -> 'a bindings -> 'a bindings
+val rename_bound_variables : identifier -> constr_expr -> constr_expr
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index a0ef088f76..97fe4ba2e8 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -185,7 +185,13 @@ let pr_bindings_gen for_ex prlc prc = function
 
 let pr_bindings prlc prc = pr_bindings_gen false prlc prc
 
-let pr_with_bindings prlc prc (c,bl) = prc c ++ pr_bindings prlc prc bl
+let pr_with_bindings prlc prc (c,bl) =
+  if Options.do_translate () then
+    (* translator calls pr_with_bindings on rawconstr: we cast it! *)
+    let bl' = translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in
+    prc c ++ pr_bindings prlc prc bl'
+  else
+    prc c ++ pr_bindings prlc prc bl
 
 let pr_with_constr prc = function
   | None -> mt ()
@@ -214,7 +220,7 @@ let pr_hyp_location pr_id (id,(hl,hl')) =
   if !hl' <> None then pr_hyp_location pr_id (id,out_some !hl')
   else
     (if hl = InHyp && Options.do_translate () then 
-      msgerrnl (str "Warning: Unable to detect if " ++ pr_id id ++ str " denots a local definition; if it is the case, the translation is wrong");
+      msgerrnl (str "Translator warning: Unable to detect if " ++ pr_id id ++ str " denotes a local definition");
     pr_hyp_location pr_id (id,hl))
 
 let pr_clause pr_id = function