Simplification afficheur de tactiques non primitive

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

3 files changed, 40 insertions, 50 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 1e839fcc62..d24de56750 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -28,29 +28,16 @@ let pr_name = Ppconstr.pr_name
 let pr_opt = Ppconstr.pr_opt
 let pr_occurrences = Ppconstr.pr_occurrences
 
+type grammar_terminals = string option list
+
   (* Extensions *)
 let prtac_tab_v7 = Hashtbl.create 17
 let prtac_tab = Hashtbl.create 17
 
-(* We need system F typing strength *)
-type ('a,'b) gen_gram_prod_builder =
-  ('a,'b) generic_argument list ->
-    string * Egrammar.grammar_tactic_production list
-let inst1 (f:('a,'b) gen_gram_prod_builder) =
-  (Obj.magic f : (constr_expr,raw_tactic_expr) gen_gram_prod_builder)
-let inst2 (f:('a,'b) gen_gram_prod_builder) =
-  (Obj.magic f : (rawconstr * constr_expr option,glob_tactic_expr) gen_gram_prod_builder)
-let inst3 (f:('a,'b) gen_gram_prod_builder) =
-  (Obj.magic f : (Term.constr,glob_tactic_expr) gen_gram_prod_builder)
-
-let declare_extra_tactic_pprule for_v8 s f =
-  let f = inst1 f in
-  let g = inst2 f in
-  let h = inst3 f in
-  Hashtbl.add prtac_tab_v7 s (f,g,h);
-  if for_v8 then Hashtbl.add prtac_tab s (f,g,h)
-
-let p = prtac_tab
+let declare_extra_tactic_pprule for_v8 s (tags,prods) =
+  Hashtbl.add prtac_tab_v7 (s,tags) prods;
+  if for_v8 then Hashtbl.add prtac_tab (s,tags) prods
+
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
       'a -> std_ppcmds
@@ -357,20 +344,19 @@ let rec pr_generic prc prlc prtac x =
       with Not_found -> str " [no printer for " ++ str s ++ str "]"
 
 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)
+  | Some s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al)
+  | None :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule  pr_gen (l,al)
   | [], [] -> mt ()
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
-let pr_extend_gen proj prgen s l =
+let pr_extend_gen prgen s l =
   let tab = 
     if Options.do_translate() or not !Options.v7 then prtac_tab
     else prtac_tab_v7
   in
   try 
-    let (s,pl) = proj (Hashtbl.find tab s) l in
+    let tags = List.map genarg_tag l in
+    let (s,pl) = Hashtbl.find tab (s,tags) in
     str s ++ pr_tacarg_using_rule prgen (pl,l)
   with Not_found ->
     str s ++ prlist prgen l ++ str " (* Generic printer *)"
@@ -666,11 +652,11 @@ and prtac x = pr6 x
 in (prtac,pr0,pr_match_rule false pr_pat pr_tac)
 
 let pr_raw_extend prc prlc prtac = 
-  pr_extend_gen pi1 (pr_raw_generic prc prlc prtac pr_reference)
+  pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference)
 let pr_glob_extend prc prlc prtac =
-  pr_extend_gen pi2 (pr_glob_generic prc prlc prtac)
+  pr_extend_gen (pr_glob_generic prc prlc prtac)
 let pr_extend prc prlc prtac =
-  pr_extend_gen pi3 (pr_generic prc prlc prtac)
+  pr_extend_gen (pr_generic prc prlc prtac)
 
 let pr_and_constr_expr pr (c,_) = pr c
 
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 5d5f62f389..729947bb8e 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -40,13 +40,11 @@ val declare_extra_genarg_pprule :
   ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) ->
   ('b closed_abstract_argument_type * 'b extra_genarg_printer) -> unit
 
-type ('a,'b) gen_gram_prod_builder =
-  ('a,'b) generic_argument list ->
-    string * Egrammar.grammar_tactic_production list
+type grammar_terminals = string option list
 
   (* if the boolean is false then the extension applies only to old syntax *)
-val declare_extra_tactic_pprule : 
-  bool -> string -> ('a,'b) gen_gram_prod_builder -> unit
+val declare_extra_tactic_pprule : bool -> string -> 
+  argument_type list * (string * grammar_terminals) -> unit
 
 val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
 
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 218a9e0db3..7c6194871b 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -102,22 +102,31 @@ let mlexpr_of_grammar_production = function
   | TacNonTerm (loc,nt,g,sopt) ->
       <:expr< Egrammar.TacNonTerm $default_loc$ ($g$,$mlexpr_of_argtype loc nt$) $mlexpr_of_option mlexpr_of_string sopt$ >>
 
+let mlexpr_terminals_of_grammar_production = function
+  | TacTerm s -> <:expr< Some $mlexpr_of_string s$ >>
+  | TacNonTerm (loc,nt,g,sopt) -> <:expr< None >>
+
 let mlexpr_of_semi_clause =
   mlexpr_of_pair mlexpr_of_string (mlexpr_of_list mlexpr_of_grammar_production)
 
 let mlexpr_of_clause =
   mlexpr_of_list (fun (a,b,c) -> mlexpr_of_semi_clause (a,b))
 
+let rec make_tags loc = function
+  | [] -> <:expr< [] >>
+  | TacNonTerm(loc',t,_,Some p)::l ->
+      let l = make_tags loc l in
+      let loc = join_loc loc' loc in
+      let t = mlexpr_of_argtype loc' t in
+      <:expr< [ $t$ :: $l$ ] >>
+  | _::l -> make_tags loc l
 
-let add_printing_clause (s,pt,e) l =
-  let p = make_patt pt in
-  let w = Some (make_when (MLast.loc_of_expr e) pt) in
-  (p, w, mlexpr_of_semi_clause (s,pt))::l
+let make_one_printing_rule (s,pt,e) =
+  let loc = MLast.loc_of_expr e in
+  let prods = mlexpr_of_list mlexpr_terminals_of_grammar_production pt in
+  <:expr< ($make_tags loc pt$, ($str:s$, $prods$)) >>
 
-let make_printing_rule l =
-  let default =
-    (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in
-  List.fold_right add_printing_clause l [default]
+let make_printing_rule = mlexpr_of_list make_one_printing_rule
 
 let new_tac_ext (s,cl) =
   (String.lowercase s, List.map 
@@ -129,7 +138,7 @@ let new_tac_ext (s,cl) =
     cl)
 
 let declare_tactic_v7 loc s cl =
-  let pl = make_printing_rule cl in
+  let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
   let hide_tac (_,p,e) =
     (* reste a definir les fonctions cachees avec des noms frais *)
@@ -147,17 +156,16 @@ let declare_tactic_v7 loc s cl =
     declare
       open Pcoq;
       Egrammar.extend_tactic_grammar $se$ $gl$;
-      let pp = fun [ $list:pl$ ] in
-      Pptactic.declare_extra_tactic_pprule False $se$ pp;
+      List.iter (Pptactic.declare_extra_tactic_pprule False $se$) $pp$;
     end
   >>
 
 let declare_tactic loc s cl =
   let (s',cl') = new_tac_ext (s,cl) in
-  let pl' = make_printing_rule cl' in
+  let pp' = make_printing_rule cl' in
   let gl' = mlexpr_of_clause cl' in
   let se' = mlexpr_of_string s' in
-  let pl = make_printing_rule cl in
+  let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
   let hide_tac (_,p,e) =
     (* reste a definir les fonctions cachees avec des noms frais *)
@@ -181,10 +189,8 @@ let declare_tactic loc s cl =
       with e -> Pp.pp (Cerrors.explain_exn e);
       if Options.v7.val then Egrammar.extend_tactic_grammar $se'$ $gl$
       else Egrammar.extend_tactic_grammar $se'$ $gl'$;
-      let pp' = fun [ $list:pl'$ ] in
-      Pptactic.declare_extra_tactic_pprule True $se'$ pp';
-      let pp = fun [ $list:pl$ ] in
-      Pptactic.declare_extra_tactic_pprule False $se'$ pp;
+      List.iter (Pptactic.declare_extra_tactic_pprule True $se'$) $pp'$;
+      List.iter (Pptactic.declare_extra_tactic_pprule False $se'$) $pp$;
     end
   >>