Globalisation des noms de tactiques dans les définitions de tactiques

pour compatibilité avec les modules.
Globalisation partielle des invocations de tactiques hors définitions
(partielle car noms des Intros/Assert/Inversion/... non connus).


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

5 files changed, 139 insertions, 90 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index eee2042a0..96c65b54c 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -456,6 +456,11 @@ let pr_lconstr_env env c = pr ltop (transf env c)
 let pr_constr c = pr_constr_env (Global.env()) c
 let pr_lconstr c = pr_lconstr_env (Global.env()) c
 
+let pr_rawconstr_env env c =
+  pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
+let pr_lrawconstr_env env c =
+  pr_lconstr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
+
 let anonymize_binder na c =
   if Options.do_translate() then
     Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env()))
@@ -495,10 +500,6 @@ let pr_red_flag pr r =
 
 open Genarg
 
-let pr_metanum pr = function
-  | AN x -> pr x
-  | MetaNum (_,n) -> str "?" ++ int n
-
 let pr_metaid id = str"?" ++ pr_id id
 
 let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
@@ -524,11 +525,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | ExtraRedExpr (s,c) ->
       hov 1 (str s ++ pr_arg pr_constr c)
 
-let rec pr_may_eval prc prlc  = function
+let rec pr_may_eval prc prlc pr2 = function
   | ConstrEval (r,c) ->
       hov 0
         (str "eval" ++ brk (1,1) ++
-         pr_red_expr (prc,prlc,pr_metanum pr_reference) r ++
+         pr_red_expr (prc,prlc,pr2) r ++
 	 str " in" ++ spc() ++ prlc c)
   | ConstrContext ((_,id),c) ->
       hov 0
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index fe1c560ca..9cd75607b 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -19,6 +19,7 @@ open Coqast
 open Topconstr
 open Names
 open Util
+open Genarg
 
 val extract_lam_binders :
   constr_expr -> (name located list * constr_expr) list * constr_expr
@@ -51,6 +52,9 @@ val pr_lconstr_env : env -> constr_expr -> std_ppcmds
 val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
 val pr_binders : (name located  list * constr_expr) list -> std_ppcmds
 val pr_may_eval :
-  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds
-val pr_metanum : ('a -> std_ppcmds) -> 'a or_metanum -> std_ppcmds
+  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
+    -> std_ppcmds
 val pr_metaid : identifier -> std_ppcmds
+
+val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
+val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 38cbc3109..157999b10 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -21,34 +21,17 @@ open Rawterm
 open Topconstr
 open Genarg
 open Libnames
-
-(* [pr_rawtac] is here to cheat with ML typing system,
-   gen_tactic_expr is polymorphic but with some occurrences of its
-   instance raw_tactic_expr in it; then pr_tactic should be
-   polymorphic but with some calls to instance of itself, what ML does
-   not accept; pr_rawtac0 denotes this instance of pr_tactic on
-   raw_tactic_expr *)
-
-let pr_rawtac =
-  ref (fun _ -> failwith "Printer for raw tactic expr is not defined"
-       : env -> raw_tactic_expr -> std_ppcmds)
-let pr_rawtac0 =
-  ref (fun _ -> failwith "Printer for raw tactic expr is not defined"
-       : env -> raw_tactic_expr -> std_ppcmds)
+open Pptactic
 
 let pr_arg pr x = spc () ++ pr x
 
-let pr_metanum pr = function
-  | AN x -> pr x
-  | MetaNum (_,n) -> str "?" ++ int n
+let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp)
 
-let pr_or_var pr = function
-  | ArgArg x -> pr x
-  | ArgVar (_,s) -> pr_id s
+let pr_evaluable_reference = function 
+  | EvalVarRef id -> pr_id id
+  | EvalConstRef sp -> pr_global Idset.empty (Libnames.ConstRef sp)
 
-let pr_or_meta pr = function
-  | AI x -> pr x
-  | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable"
+let pr_inductive vars ind = pr_global vars (Libnames.IndRef ind)
 
 let pr_quantified_hypothesis = function
   | AnonHyp n -> int n
@@ -116,22 +99,22 @@ let pr_induction_arg prc = function
   | ElimOnIdent (_,id) -> pr_id id
   | ElimOnAnonHyp n -> int n
 
-let pr_match_pattern = function
-  | Term a -> pr_pattern a
-  | Subterm (None,a) -> str "[" ++ pr_pattern a ++ str "]"
-  | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pattern a ++ str "]"
+let pr_match_pattern pr_pat = function
+  | Term a -> pr_pat a
+  | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]"
+  | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
-let pr_match_hyps = function
-  | NoHypId mp -> str "_:" ++ pr_match_pattern mp
-  | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern mp
+let pr_match_hyps pr_pat = function
+  | NoHypId mp -> str "_:" ++ pr_match_pattern pr_pat mp
+  | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern pr_pat mp
 
-let pr_match_rule m pr = function
+let pr_match_rule m pr pr_pat = function
   | Pat ([],mp,t) when m ->
-      str "[" ++ pr_match_pattern mp ++ str "]"
+      str "[" ++ pr_match_pattern pr_pat mp ++ str "]"
       ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
   | Pat (rl,mp,t) ->
-      str "[" ++ prlist_with_sep (fun () -> str",") pr_match_hyps rl ++
-      spc () ++ str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++
+      str "[" ++ prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++
+      spc () ++ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
       str "] =>" ++ brk (1,4) ++ pr t
   | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
 
@@ -139,20 +122,20 @@ let pr_funvar = function
   | None -> spc () ++ str "()"
   | Some id -> spc () ++ pr_id id
 
-let pr_let_clause k pr = function
+let pr_let_clause k pr prc pr_cst = function
   | ((_,id),None,t) ->
       hov 0 (str k ++ pr_id id ++ str " :=" ++ brk (1,1) ++
              pr (TacArg t))
   | ((_,id),Some c,t) ->
       hv 0 (str k ++ pr_id id ++ str" :" ++ brk(1,2) ++
-      pr_may_eval pr_constr pr_constr c ++
+      pr_may_eval prc prc pr_cst c ++
       str " :=" ++ brk (1,1) ++ pr (TacArg t))
 
-let pr_let_clauses pr = function
+let pr_let_clauses pr prc pr_cst = function
   | hd::tl ->
       hv 0
-        (pr_let_clause "let " pr hd ++ spc () ++
-         prlist_with_sep spc (pr_let_clause "with " pr) tl)
+        (pr_let_clause "let " pr prc pr_cst hd ++ spc () ++
+         prlist_with_sep spc (pr_let_clause "with " pr prc pr_cst) tl)
   | [] -> anomaly "LetIn must declare at least one binding"
 
 let pr_rec_clause pr ((_,id),(l,t)) =
@@ -181,15 +164,16 @@ let pr_autoarg_usingTDB = function
   | true -> spc () ++ str "Using TDB"
   | false -> mt ()
 
-open Closure
+let rec pr_tacarg_using_rule pr_gen = function
+  | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al)
+  | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al)
+  | [], [] -> mt ()
+  | _ -> failwith "Inconsistent arguments of extended tactic"
 
-let pr_evaluable_reference vars = function 
-  | EvalVarRef id -> pr_id id
-  | EvalConstRef sp -> pr_global vars (Libnames.ConstRef sp)
 
-let pr_inductive vars ind = pr_global vars (Libnames.IndRef ind)
+open Closure
 
-let make_pr_tac (pr_constr,pr_lconstr,pr_cst,pr_ind,pr_ident,pr_extend) =
+let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
 
 let pr_bindings env = pr_bindings (pr_constr env) in
 let pr_ex_bindings env = pr_bindings_gen true (pr_constr env) in
@@ -197,6 +181,7 @@ let pr_with_bindings env = pr_with_bindings (pr_constr env) in
 let pr_eliminator env cb = str "using" ++ pr_arg (pr_with_bindings env) cb in
 let pr_constrarg env c = spc () ++ pr_constr env c in
 let pr_lconstrarg env c = spc () ++ pr_lconstr env c in
+
 let pr_intarg n = spc () ++ int n in
 
   (* Printing tactics as arguments *)
@@ -216,10 +201,9 @@ let rec pr_atom0 env = function
   (* Main tactic printer *)
 and pr_atom1 env = function
   | TacExtend (_,s,l) ->
-      pr_extend (Ppconstrnew.pr_constr_env env) (!pr_rawtac env) s l
+      pr_extend (pr_constr env) (pr_tac env) s l
   | TacAlias (s,l,_) ->
-      pr_extend (Ppconstrnew.pr_constr_env env) (!pr_rawtac env) s
-        (List.map snd l)
+      pr_extend (pr_constr env) (pr_tac env) s (List.map snd l)
 
   (* Basic tactics *)
   | TacIntroPattern [] as t -> pr_atom0 env t
@@ -304,7 +288,7 @@ and pr_atom1 env = function
   | TacDecompose (l,c) ->
       let vars = Termops.vars_of_env env in
       hov 1 (str "decompose" ++ spc () ++
-        hov 0 (str "[" ++ prlist_with_sep spc (pr_metanum (pr_ind vars)) l
+        hov 0 (str "[" ++ prlist_with_sep spc (pr_or_metanum (pr_ind vars)) l
 	  ++ str "]" ++ pr_lconstrarg env c))
   | TacSpecialize (n,c) ->
       hov 1 (str "specialize " ++ pr_opt int n ++ pr_with_bindings env c)
@@ -329,9 +313,9 @@ and pr_atom1 env = function
 
   (* Context management *)
   | TacClear l ->
-      hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l)
+      hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l)
   | TacClearBody l ->
-      hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l)
+      hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l)
   | TacMove (b,(_,id1),(_,id2)) ->
       (* Rem: only b = true is available for users *)
       assert b;
@@ -349,10 +333,10 @@ and pr_atom1 env = function
   | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l)
   | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l)
   | TacAnyConstructor (Some t) ->
-      hov 1 (str "constructor" ++ pr_arg (!pr_rawtac0 env) t)
+      hov 1 (str "constructor" ++ pr_arg (pr_tac0 env) t)
   | TacAnyConstructor None as t -> pr_atom0 env t
   | TacConstructor (n,l) ->
-      hov 1 (str "constructor" ++ pr_or_meta pr_intarg n ++
+      hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++
              pr_bindings env l)
 
   (* Conversion *)  
@@ -406,18 +390,18 @@ let rec pr_tac env inherited tac =
       llet
   | TacLetIn (llc,u) ->
       v 0
-       (hv 0 (pr_let_clauses (pr_tac env ltop) llc ++ str " in") ++
+       (hv 0 (pr_let_clauses (pr_tac env ltop) (pr_constr env) pr_cst llc ++ 
+       str " in") ++
        fnl () ++ pr_tac env (llet,E) u),
       llet
   | TacLetCut llc -> assert false
   | TacMatch (t,lrul) ->
       hov 0 (str "match " ++
-             pr_may_eval (Ppconstrnew.pr_constr_env env)
-               (Ppconstrnew.pr_lconstr_env env) t
+             pr_may_eval (pr_constr env) (pr_lconstr env) pr_cst t
         ++ str " with"
         ++ prlist
 	  (fun r -> fnl () ++ str "| " ++
-            pr_match_rule true (pr_tac env ltop) r)
+            pr_match_rule true (pr_tac env ltop) pr_pat r)
 	lrul
         ++ fnl() ++ str "end"),
       lmatch
@@ -426,7 +410,7 @@ let rec pr_tac env inherited tac =
 	str (if lr then "match reverse context with" else "match context with")
 	++ prlist
 	  (fun r -> fnl () ++ str "| " ++
-            pr_match_rule false (pr_tac env ltop) r)
+            pr_match_rule false (pr_tac env ltop) pr_pat r)
 	lrul
         ++ fnl() ++ str "end"),
       lmatch
@@ -472,13 +456,13 @@ let rec pr_tac env inherited tac =
       str "solve" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet
   | TacId -> str "idtac", latom
   | TacAtom (_,t) -> hov 1 (pr_atom1 env t), ltatom
-  | TacArg(Tacexp e) -> !pr_rawtac0 env e, latom
+  | TacArg(Tacexp e) -> pr_tac0 env e, latom
   | TacArg(ConstrMayEval (ConstrTerm c)) -> str "'" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
-      pr_may_eval (pr_constr env) (pr_lconstr env) c, leval
+      pr_may_eval (pr_constr env) (pr_lconstr env) pr_cst c, leval
   | TacArg(Integer n) -> int n, latom
   | TacArg(TacCall(_,f,l)) ->
-      hov 1 (pr_reference f ++ spc () ++
+      hov 1 (pr_ref f ++ spc () ++
              prlist_with_sep spc (pr_tacarg env) l),
       lcall
   | TacArg a -> pr_tacarg env a, latom
@@ -488,10 +472,10 @@ let rec pr_tac env inherited tac =
 
 and pr_tacarg env = function
   | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
-  | MetaNumArg (_,n) -> str ("?" ^ string_of_int n )
   | MetaIdArg (_,s) -> str ("$" ^ s)
+  | Identifier id -> pr_id id
   | TacVoid -> str "()"
-  | Reference r -> pr_reference r
+  | Reference r -> pr_ref r
   | ConstrMayEval (ConstrTerm c) -> pr_constr env c
   | (ConstrMayEval _|TacCall _|Tacexp _|Integer _) as a ->
       str "'" ++ pr_tac env (latom,E) (TacArg a)
@@ -500,18 +484,63 @@ in ((fun env -> pr_tac env ltop),
     (fun env -> pr_tac env (latom,E)),
     pr_match_rule)
 
-let (pr_raw_tactic,pr_raw_tactic0,pr_match_rule) =
-  make_pr_tac
-    (Ppconstrnew.pr_constr_env,
+let pi1 (a,_,_) = a
+let pi2 (_,a,_) = a
+let pi3 (_,_,a) = a
+
+let rec raw_printers =
+    (pr_raw_tactic, 
+     pr_raw_tactic0,
+     Ppconstrnew.pr_constr_env,
      Ppconstrnew.pr_lconstr_env,
-     pr_metanum pr_reference,
+     Ppconstrnew.pr_pattern,
+     pr_or_metanum pr_reference,
      (fun _ -> pr_reference),
-     pr_or_meta (fun (loc,id) -> pr_id id),
+     pr_reference,
+     pr_or_metaid (pr_located pr_id),
      Pptactic.pr_raw_extend)
 
-let _ = pr_rawtac := pr_raw_tactic
-let _ = pr_rawtac0 := pr_raw_tactic0
+and pr_raw_tactic env (t:raw_tactic_expr) =
+  pi1 (make_pr_tac raw_printers) env t
+
+and pr_raw_tactic0 env t =
+  pi2 (make_pr_tac raw_printers) env t
+
+and pr_raw_match_rule env t =
+  pi3 (make_pr_tac raw_printers) env t
+
+let pr_and_constr_expr pr (c,_) = pr c
+
+let rec glob_printers =
+    (pr_glob_tactic, 
+     pr_glob_tactic0,
+     (fun env -> pr_and_constr_expr (Ppconstrnew.pr_rawconstr_env env)),
+     (fun env -> pr_and_constr_expr (Ppconstrnew.pr_lrawconstr_env env)),
+     Printer.pr_pattern,
+     pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)),
+     (fun vars -> pr_or_var (pr_inductive vars)),
+     pr_or_var pr_ltac_constant,
+     pr_located pr_id,
+     Pptactic.pr_glob_extend)
 
-let pr_gen env =
-  Pptactic.pr_rawgen (Ppconstrnew.pr_constr_env env)
-    (pr_raw_tactic env)
+and pr_glob_tactic env (t:glob_tactic_expr) =
+  pi1 (make_pr_tac glob_printers) env t
+
+and pr_glob_tactic0 env t =
+  pi2 (make_pr_tac glob_printers) env t
+
+and pr_glob_match_rule env t =
+  pi3 (make_pr_tac glob_printers) env t
+
+let (pr_tactic,_,_) =
+  make_pr_tac
+    (pr_glob_tactic,
+     pr_glob_tactic0,
+     Printer.prterm_env,
+     Printer.prterm_env,
+     Printer.pr_pattern,
+     pr_evaluable_reference,
+     pr_inductive,
+     pr_ltac_constant,
+     pr_id,
+     Pptactic.pr_extend)
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
index 41fc97da9..e6772405f 100644
--- a/translate/pptacticnew.mli
+++ b/translate/pptacticnew.mli
@@ -15,5 +15,7 @@ open Proof_type
 open Topconstr
 
 val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds
-val pr_gen : Environ.env ->
-  (constr_expr, raw_tactic_expr) generic_argument -> std_ppcmds
+ 
+val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds
+
+val pr_tactic : Environ.env -> Proof_type.tactic_expr -> std_ppcmds
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index de0abed00..8e7aa2fc1 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -26,11 +26,22 @@ open Libnames
 open Ppextend
 open Topconstr
 
+open Tacinterp
+
+(* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *)
+let pr_raw_tactic_env l env t = 
+  Pptacticnew.pr_raw_tactic env t
+
+let pr_gen env t =
+  Pptactic.pr_raw_generic (Ppconstrnew.pr_constr_env env)
+    (Pptacticnew.pr_raw_tactic env) t
+
 let pr_raw_tactic tac =
-  Pptacticnew.pr_raw_tactic (Global.env()) tac
+  pr_raw_tactic_env [] (Global.env()) tac
+
 let pr_raw_tactic_goal n tac =
   let (_,env) = Pfedit.get_goal_context n in
-  Pptacticnew.pr_raw_tactic env tac
+  pr_raw_tactic_env [] env tac
 let pr_lconstr_goal n c =
   let (_,env) = Pfedit.get_goal_context n in
   Ppconstrnew.pr_lconstr_env env c
@@ -451,7 +462,7 @@ let rec pr_vernac = function
         | None -> mt()
         | Some r ->
             str"Eval" ++ spc() ++
-            pr_red_expr (pr_constr, pr_lconstr, pr_metanum pr_reference) r ++
+            pr_red_expr (pr_constr, pr_lconstr, Pptactic.pr_or_metanum pr_reference) r ++
             str" in" ++ spc() in
       let pr_def_body = function
         | DefineBody (bl,red,c,d) ->
@@ -635,7 +646,9 @@ let rec pr_vernac = function
                  b
             | _ -> mt(), body in
         pr_located pr_id id ++ ppb ++ str" :=" ++ brk(1,1) ++
-        pr_raw_tactic body in
+        pr_raw_tactic_env
+          (List.map (fun ((_,id),_) -> (id,Lib.make_path id)) l) 
+          (Global.env()) body in
       hov 1
         ((if rc then str "Recursive " else mt()) ++
          str "Tactic Definition " ++
@@ -676,7 +689,7 @@ let rec pr_vernac = function
       let pr_mayeval r c = match r with 
       | Some r0 ->
           hov 2 (str"Eval" ++ spc() ++
-          pr_red_expr (pr_constr,pr_lconstr,pr_metanum pr_reference) r0 ++
+          pr_red_expr (pr_constr,pr_lconstr,Pptactic.pr_or_metanum pr_reference) r0 ++
           spc() ++ str"in" ++ spc () ++ pr_lconstr c)
       | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c) 
       in pr_mayeval r c
@@ -734,7 +747,7 @@ let rec pr_vernac = function
 
 and pr_extend s cl =
   let pr_arg a =
-    try Pptacticnew.pr_gen (Global.env()) a
+    try pr_gen (Global.env()) a
     with Failure _ -> str ("<error in "^s^">") in
   try
     let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in
@@ -744,7 +757,7 @@ and pr_extend s cl =
         (fun (strm,args) pi ->
           match pi with
               Egrammar.TacNonTerm _ -> 
-                (strm ++ Pptacticnew.pr_gen (Global.env()) (List.hd args),
+                (strm ++ pr_gen (Global.env()) (List.hd args),
                 List.tl args)
             | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
         (str hd,cl) rl in