Pour appliquer les noms reserves aussi aux binders

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

3 files changed, 94 insertions, 94 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 087bcc90ac..21486e5110 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -133,24 +133,14 @@ let pr_eqn pr (_,pl,rhs) =
      hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
      spc() ++ pr ltop rhs)
 
-
-(*
-let pr_binder pr (nal,t) =
-  hov 0 (
-    prlist_with_sep sep (pr_located pr_name) nal ++
-    pr_opt_type pr t)
-*)
-
 let surround p = str"(" ++ p ++ str")"
 
 let pr_binder many pr (nal,t) =
   match t with
-      CHole _ -> 
-        prlist_with_sep sep (pr_located pr_name) nal
-    | _ ->
-        let s = 
-          (prlist_with_sep sep (pr_located pr_name) nal ++ str ":" ++ pr t) in
-        hov 1 (if many then surround s else s)
+  | CHole _ -> prlist_with_sep sep (pr_located pr_name) nal
+  | _ ->
+    let s = prlist_with_sep sep (pr_located pr_name) nal ++ str ":" ++ pr t in
+    hov 1 (if many then surround s else s)
 
 let pr_binder_among_many pr_c = function
   | LocalRawAssum (nal,t) ->
@@ -196,11 +186,6 @@ let rec extract_lam_binders = function
       LocalRawAssum (nal,t) :: bl, c
   | c -> [], c
     
-(*
-let pr_arg_binders pr bl =
-  if bl = [] then mt() else (spc() ++ pr_binders pr bl)
-*)
-
 let pr_global vars ref =
   (* pr_global_env vars ref *)
   let s = string_of_qualid (Constrextern.shortest_qualid_of_v7_global vars ref) in
@@ -514,12 +499,33 @@ let rec pr inherited a =
 
 let rec strip_context n iscast t =
   if n = 0 then
-    if iscast then match t with RCast (_,c,_) -> c | _ -> t else t
+    [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
   else match t with
-    | RLambda (_,_,_,c) -> strip_context (n-1) iscast c
-    | RProd (_,_,_,c) -> strip_context (n-1) iscast c
-    | RLetIn (_,_,_,c) -> strip_context (n-1) iscast c
-    | RCast (_,c,_) -> strip_context n false c
+    | CLambdaN (loc,(nal,t)::bll,c) ->
+	let n' = List.length nal in
+	if n' > n then
+	  let nal1,nal2 = list_chop n nal in
+	  [LocalRawAssum (nal1,t)], CLambdaN (loc,(nal2,t)::bll,c)
+	else
+	let bl', c = strip_context (n-n') iscast
+	  (if bll=[] then c else CLambdaN (loc,bll,c)) in
+	LocalRawAssum (nal,t) :: bl', c 
+    | CProdN (loc,(nal,t)::bll,c) ->
+	let n' = List.length nal in
+	if n' > n then
+	  let nal1,nal2 = list_chop n nal in
+	  [LocalRawAssum (nal1,t)], CLambdaN (loc,(nal2,t)::bll,c)
+	else
+	let bl', c = strip_context (n-n') iscast
+	  (if bll=[] then c else CProdN (loc,bll,c)) in
+	LocalRawAssum (nal,t) :: bl', c 
+    | CArrow (loc,t,c) ->
+	let bl', c = strip_context (n-1) iscast c in
+	LocalRawAssum ([loc,Anonymous],t) :: bl', c 
+    | CCast (_,c,_) -> strip_context n false c
+    | CLetIn (_,na,b,c) -> 
+	let bl', c = strip_context (n-1) iscast c in
+	LocalRawDef (na,b) :: bl', c
     | _ -> anomaly "ppconstrnew: strip_context"
 
 let transf istype env n iscast c =
@@ -534,22 +540,24 @@ let transf istype env n iscast c =
       let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in 
       (*msgerrnl (str "Typage OK");*) ()
     with e -> (*msgerrnl (str "Warning: can't type")*) () end;
-    (if istype then Constrextern.extern_rawtype
-    else Constrextern.extern_rawconstr)
-      (Termops.vars_of_env env)
-      (strip_context n iscast r)
-  else c
-
-let pr_constr_env env c = pr lsimple (transf false env 0 false c)
-let pr_lconstr_env env c = pr ltop (transf false env 0 false c)
+    let c =
+      (if istype then Constrextern.extern_rawtype
+      else Constrextern.extern_rawconstr)
+      (Termops.vars_of_env env) r in
+    strip_context n iscast c
+  else [], c
+
+let pr_constr_env env c = pr lsimple (snd (transf false env 0 false c))
+let pr_lconstr_env env c = pr ltop (snd (transf false env 0 false c))
 let pr_constr c = pr_constr_env (Global.env()) c
 let pr_lconstr c = pr_lconstr_env (Global.env()) c
 
-let pr_lconstr_env_n env n b c = pr ltop (transf false env n b c)
-let pr_type_env_n env n c = pr ltop (transf true env n false c)
-let pr_type c = pr ltop (transf true (Global.env()) 0 false c)
+let pr_binders = pr_undelimited_binders (pr ltop)
 
-let pr_binders = pr_undelimited_binders pr_lconstr
+let pr_lconstr_env_n env n b c =
+  let bl, c = transf false env n b c in bl, pr ltop c
+let pr_type_env_n env n c = pr ltop (snd (transf true env n false c))
+let pr_type c = pr ltop (snd (transf true (Global.env()) 0 false c))
 
 let transf_pattern env c =
   if Options.do_translate() then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 9b277cbd3f..6952bed566 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -51,7 +51,8 @@ val pr_constr : constr_expr -> std_ppcmds
 val pr_lconstr : constr_expr -> std_ppcmds
 val pr_constr_env : env -> constr_expr -> std_ppcmds
 val pr_lconstr_env : env -> constr_expr -> std_ppcmds
-val pr_lconstr_env_n : env -> int -> bool -> constr_expr -> std_ppcmds
+val pr_lconstr_env_n : env -> int -> bool -> constr_expr -> 
+  local_binder list * std_ppcmds
 val pr_type_env_n : env -> int -> constr_expr -> std_ppcmds
 val pr_type : constr_expr -> std_ppcmds
 val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index ef06671202..22a068ceea 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -311,30 +311,31 @@ let pr_decl_notation =
     str "as " ++ str (quote ntn) ++ 
     pr_opt (fun sc -> str " :" ++ str sc) scopt)
 
-let anonymize_binder na c =
-  if Options.do_translate() then
-    Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env()))
-      (Reserve.anonymize_if_reserved na
-      (Constrintern.for_grammar
-        (Constrintern.interp_rawconstr Evd.empty (Global.env())) c))
-  else c
-
-let surround p = str"(" ++ p ++ str")"
-
-(*
-let pr_binder pr_c ty na =
-  match anonymize_binder (snd na) ty with
-      CHole _ -> pr_located pr_name na
-    | _ ->
-        hov 1
-        (surround (pr_located pr_name na ++ str":" ++ cut() ++ pr_c ty))
-*)
+let rec abstract_rawconstr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+      (abstract_rawconstr c bl)
+      
+let rec prod_rawconstr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+      (prod_rawconstr c bl)
 
 let pr_vbinders l =
   hv 0 (pr_binders l)
 
-let pr_binders_arg bl =
-  if bl = [] then mt () else spc () ++ pr_binders bl
+let pr_binders_arg =
+  pr_ne_sep spc pr_binders
+
+let pr_and_type_binders_arg bl =
+  let n = local_binders_length bl in
+  let c = abstract_rawconstr (CHole dummy_loc) bl in
+  let bl, _ = pr_lconstr_env_n (Global.env()) n false c in
+  pr_binders_arg bl
 
 let pr_onescheme (id,dep,ind,s) =
   hov 0 (pr_id id ++ str" :=") ++ spc() ++
@@ -599,18 +600,6 @@ let rec pr_vernac = function
             str" in" ++ spc() in
       let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) in
       let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) in
-      let rec abstract_rawconstr c = function
-        | [] -> c
-        | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
-        | LocalRawAssum (idl,t)::bl ->
-            List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
-            (abstract_rawconstr c bl) in
-      let rec prod_rawconstr c = function
-        | [] -> c
-        | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl)
-        | LocalRawAssum (idl,t)::bl ->
-            List.fold_right (fun x b -> mkProdC([x],t,b)) idl
-            (prod_rawconstr c bl) in
       let pr_def_body = function
         | DefineBody (bl,red,c,d) ->
             let (bl2,body,ty) = match d with
@@ -619,23 +608,19 @@ let rec pr_vernac = function
                   (bl2,body,mt())
               | Some ty ->
                   let bl2,body,ty' = extract_def_binders c ty in
-                  (bl2,body, spc() ++ str":" ++ spc () ++
+                  (bl2,CCast (dummy_loc,body,ty'), spc() ++ str":" ++ spc () ++
                     pr_type_env_n (Global.env())
                     (local_binders_length bl + local_binders_length bl2)
                     (prod_rawconstr ty bl)) in
-            let bindings =
-	      pr_ne_sep spc pr_vbinders bl ++ pr_binders_arg bl2 in
 	    let n = local_binders_length bl + local_binders_length bl2 in
-	    let c',iscast = match d with None -> c, false
-	      | Some d -> CCast (dummy_loc,c,d), true in
-            let ppred =
-              Some (pr_reduce red ++
-              pr_lconstr_env_n (Global.env()) n iscast
-		(abstract_rawconstr c' bl))
-            in
-            (bindings,ty,ppred)
+	    let iscast = d <> None in
+            let bindings,ppred =
+	      pr_lconstr_env_n (Global.env()) n iscast
+		(abstract_rawconstr (abstract_rawconstr body bl2) bl) in
+            (pr_binders_arg bindings,ty,Some (pr_reduce red ++ ppred))
         | ProveBody (bl,t) ->
-            (pr_vbinders bl, str" :" ++ spc () ++ pr_type t, None) in
+            (pr_and_type_binders_arg bl, str" :" ++ spc () ++ pr_type t, None)
+      in
       let (binds,typ,c) = pr_def_body b in
       hov 2 (pr_def_token e ++ spc() ++ pr_id id ++ binds ++ typ ++
       (match c with
@@ -751,8 +736,8 @@ pr_vbinders bl ++ spc())
       let pr_oneind key (id,ntn,indpar,s,lc) =
 	hov 0 (
           str key ++ spc() ++
-          pr_id id ++ pr_binders_arg indpar ++ spc() ++ str":" ++ spc() ++
-          pr_type s ++ 
+          pr_id id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
+	  spc() ++ pr_type s ++ 
 	  pr_decl_notation ntn ++ str" :=") ++ pr_constructor_list lc in
 
       (* Copie simplifiée de command.ml pour déclarer les notations locales *)
@@ -823,11 +808,12 @@ pr_vbinders bl ++ spc())
                 spc() ++ str "{struct " ++
                 pr_name (snd (List.nth ids n)) ++ str"}"
               else mt() in
-            pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc()
+	    let bl, ppc = 
+              pr_lconstr_env_n rec_sign (local_binders_length bl)
+		true (abstract_rawconstr (CCast (dummy_loc,def,type_)) bl) in
+            pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_type c) type_
-            ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++
-            pr_lconstr_env_n rec_sign (local_binders_length bl)
-	      true (CCast (dummy_loc,def0,type_0))
+            ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++ ppc
       in
       hov 1 (str"Fixpoint" ++ spc() ++
         prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
@@ -862,7 +848,8 @@ pr_vbinders bl ++ spc())
       hov 2
         (str (if b then "Record" else "Structure") ++
          (if oc then str" > " else str" ") ++ pr_id name ++ 
-         pr_binders_arg ps ++ str" :" ++ spc() ++ pr_type s ++ str" := " ++
+          pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ pr_type s ++ 
+	  str" := " ++
          (match c with
            | None -> mt()
            | Some sc -> pr_id sc) ++
@@ -989,19 +976,23 @@ pr_vbinders bl ++ spc())
   | VernacSetOpacity (fl,l) ->
       hov 1 ((if fl then str"Opaque" else str"Transparent") ++
              spc() ++ prlist_with_sep sep pr_reference l)
-  | VernacUnsetOption na ->
-      hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
-  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> str"Set Implicit Arguments" 
+
+  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> 
+      str"Set Implicit Arguments" 
       ++
       (if !Options.translate_strict_impargs then
 	sep_end () ++ fnl () ++ str"Unset Strict Implicits"
       else mt ())
+  | VernacUnsetOption (Goptions.SecondaryTable ("Implicit","Arguments"))
   | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> 
-      str"Set Strict Implicits" 
-      ++
       (if !Options.translate_strict_impargs then
-	sep_end () ++ fnl () ++ str"Unset Implicit Arguments"
+	str"Set Strict Implicits" ++ sep_end () ++ fnl ()
       else mt ())
+      ++
+      str"Unset Implicit Arguments" 
+
+  | VernacUnsetOption na ->
+      hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
   | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v)
   | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
   | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))