Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux niveaux syntaxiques des tacticielles

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

3 files changed, 60 insertions, 68 deletions

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 141ae1cbe6..c7b01607fc 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -386,10 +386,24 @@ let rec pr_tacarg_using_rule pr_gen = function
 
 let pr_then () = str ";"
 
+let ltop = (5,E)
+let lseq = 5
+let ltactical = 3
+let lorelse = 2
+let llet = 1
+let lfun = 1
+let labstract = 3
+let lmatch = 1
+let latom = 0
+let lcall = 1
+let leval = 1
+let ltatom = 1
+
+let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
 
 open Closure
 
-let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) =
+let make_pr_tac (pr_tac_level,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) =
 
 let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in
 let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
@@ -467,10 +481,10 @@ and pr_atom1 env = function
       errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0")
   | TacExtend (loc,s,l) ->
       pr_with_comments loc
-        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l)
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) 1 s l)
   | TacAlias (loc,s,l,_) ->
       pr_with_comments loc
-        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) 1 s
           (List.map snd l))
 
   (* Basic tactics *)
@@ -633,7 +647,7 @@ 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_tac0 env) t)
+      hov 1 (str "constructor" ++ pr_arg (pr_tac_level env (latom,E)) t)
   | TacAnyConstructor None as t -> pr_atom0 env t
   | TacConstructor (n,l) ->
       hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++
@@ -676,19 +690,6 @@ and pr_atom1 env = function
 
 in
 
-let ltop = (5,E) in
-let lseq = 5 in
-let ltactical = 3 in
-let lorelse = 2 in
-let llet = 1 in
-let lfun = 1 in
-let labstract = 3 in
-let lmatch = 1 in
-let latom = 0 in
-let lcall = 1 in
-let leval = 1 in
-let ltatom = 1 in
-
 let rec pr_tac env inherited tac =
   let (strm,prec) = match tac with
   | TacAbstract (t,None) ->
@@ -791,9 +792,14 @@ let rec pr_tac env inherited tac =
       str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
   | TacId "" -> str "idtac", latom
   | TacId s -> str "idtac" ++ (qsnew s), latom
+  | TacAtom (loc,TacAlias (_,s,l,_)) ->
+      pr_with_comments loc
+        (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env)
+	  (level_of inherited) s
+          (List.map snd l)), latom
   | TacAtom (loc,t) ->
       pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
-  | TacArg(Tacexp e) -> pr_tac0 env e, latom
+  | TacArg(Tacexp e) -> pr_tac_level env (latom,E) e, latom
   | TacArg(ConstrMayEval (ConstrTerm c)) ->
       str "constr:" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
@@ -826,13 +832,7 @@ and pr_tacarg env = function
   | (TacCall _|Tacexp _|Integer _) as a ->
       str "ltac:" ++ pr_tac env (latom,E) (TacArg a)
 
-in ((fun env -> pr_tac env ltop),
-    (fun env -> pr_tac env (latom,E)),
-    pr_match_rule)
-
-let pi1 (a,_,_) = a
-let pi2 (_,a,_) = a
-let pi3 (_,_,a) = a
+in (pr_tac, pr_match_rule)
 
 let strip_prod_binders_rawterm n (ty,_) =
   let rec strip_ty acc n ty =
@@ -852,10 +852,8 @@ let strip_prod_binders_constr n ty =
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
-
 let rec raw_printers =
-    (pr_raw_tactic, 
-     pr_raw_tactic0,
+    (pr_raw_tactic_level, 
      Ppconstrnew.pr_constr_env,
      Ppconstrnew.pr_lconstr_env,
      Ppconstrnew.pr_pattern,
@@ -866,21 +864,17 @@ let rec raw_printers =
      Pptactic.pr_raw_extend,
      strip_prod_binders_expr)
 
-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_tactic_level env n (t:raw_tactic_expr) =
+  fst (make_pr_tac raw_printers) env n t
 
 and pr_raw_match_rule env t =
-  pi3 (make_pr_tac raw_printers) env t
+  snd (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,
+    (pr_glob_tactic_level, 
      (fun env -> pr_and_constr_expr (Ppconstrnew.pr_rawconstr_env_no_translate env)),
      (fun env -> pr_and_constr_expr (Ppconstrnew.pr_lrawconstr_env_no_translate env)),
      (fun c -> Ppconstrnew.pr_constr_pattern_env (Global.env()) c),
@@ -891,19 +885,15 @@ let rec glob_printers =
      Pptactic.pr_glob_extend,
      strip_prod_binders_rawterm)
 
-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_tactic_level env n (t:glob_tactic_expr) =
+  fst (make_pr_tac glob_printers) env n t
 
 and pr_glob_match_rule env t =
-  pi3 (make_pr_tac glob_printers) env t
+  snd (make_pr_tac glob_printers) env t
 
-let (pr_tactic,_,_) =
+let ((pr_tactic_level:env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) =
   make_pr_tac
-    (pr_glob_tactic,
-     pr_glob_tactic0,
+    (pr_glob_tactic_level,
      pr_term_env,
      pr_lterm_env,
      Ppconstrnew.pr_constr_pattern,
@@ -914,6 +904,10 @@ let (pr_tactic,_,_) =
      Pptactic.pr_extend,
      strip_prod_binders_constr)
 
+let pr_raw_tactic env = pr_raw_tactic_level env ltop
+let pr_glob_tactic env = pr_glob_tactic_level env ltop
+let pr_tactic env = pr_tactic_level env ltop
+
 let _ = Tactic_debug.set_tactic_printer
   (fun x -> 
     if !Options.v7 then Pptactic.pr_glob_tactic x
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
index b2e8942ad2..3dafb36151 100644
--- a/translate/pptacticnew.mli
+++ b/translate/pptacticnew.mli
@@ -14,15 +14,19 @@ open Tacexpr
 open Proof_type
 open Topconstr
 open Names
+open Environ
+open Ppextend
 
 val qsnew : string -> std_ppcmds
 
 val pr_intro_pattern : intro_pattern_expr -> std_ppcmds
 
-val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds
+val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds
+
+val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds
  
-val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds
+val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
 
-val pr_tactic : Environ.env -> Proof_type.tactic_expr -> std_ppcmds
+val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds
 
 val id_of_ltac_v7_id : identifier -> identifier
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 985280cfdc..86f20bb6f6 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -91,7 +91,7 @@ let pr_raw_tactic_env l env t =
 let pr_gen env t =
   Pptactic.pr_raw_generic (Ppconstrnew.pr_constr_env env)
     (Ppconstrnew.pr_lconstr_env env)
-    (Pptacticnew.pr_raw_tactic env) pr_reference t
+    (Pptacticnew.pr_raw_tactic_level env) pr_reference t
 
 let pr_raw_tactic tac =
   Pptacticnew.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic tac)
@@ -103,8 +103,8 @@ let rec extract_signature = function
 
 let rec match_vernac_rule tys = function
     [] -> raise Not_found
-  | (s,pargs)::rls ->
-      if extract_signature pargs = tys then (s,pargs)
+  | pargs::rls ->
+      if extract_signature pargs = tys then pargs
       else match_vernac_rule tys rls
 
 let sep = fun _ -> spc()
@@ -400,16 +400,12 @@ let pr_syntax_modifiers = function
   | l -> spc() ++ 
       hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
-let pr_grammar_tactic_rule (name,(s,pil),t) =
-(*
-  hov 0 (
-  (* str name ++ spc() ++ *)
-  hov 0 (str"[" ++ qsnew s ++ spc() ++
-  prlist_with_sep sep pr_production_item pil ++ str"]") ++
-  spc() ++ hov 0 (str"->" ++ spc() ++ str"[" ++ pr_raw_tactic t ++ str"]"))
-*)
-  hov 2 (str "Tactic Notation" ++ spc() ++ 
-    hov 0 (qsnew s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++
+let print_level n =
+  if n <> 0 then str " (at level " ++ int n ++ str ")" else mt ()
+
+let pr_grammar_tactic_rule n (name,pil,t) =
+  hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++ 
+    hov 0 (prlist_with_sep sep pr_production_item pil ++
     spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
 
 let pr_box b = let pr_boxkind = function
@@ -526,11 +522,9 @@ let rec pr_vernac = function
   | VernacGrammar _ -> 
       msgerrnl (str"Warning : constr Grammar is discontinued; use Notation");
       str"(* <Warning> : Grammar is replaced by Notation *)"
-  | VernacTacticGrammar l ->
-      prlist_with_sep (fun () -> sep_end() ++ fnl()) pr_grammar_tactic_rule l
-(*
-      hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***)
-*)      
+  | VernacTacticGrammar (n,l) ->
+      prlist_with_sep (fun () -> sep_end() ++ fnl())
+        (pr_grammar_tactic_rule n) l
   | VernacSyntax (u,el) ->
       msgerrnl (str"Warning : Syntax is discontinued; use Notation");
       str"(* <Warning> : Syntax is discontinued" ++ 
@@ -1095,7 +1089,7 @@ and pr_extend s cl =
       | "HintRewriteV8", [a;b;c;d] -> [a;b;d;c]
       | _ -> cl in
     let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in
-    let (hd,rl) = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
+    let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
     let (pp,_) =
       List.fold_left
         (fun (strm,args) pi ->
@@ -1104,7 +1098,7 @@ and pr_extend s cl =
                 (strm ++ pr_gen (Global.env()) (List.hd args),
                 List.tl args)
             | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
-        (str hd,cl) rl in
+        (mt(),cl) rl in
     hov 1 pp
     ++ (if s = "Correctness" then sep_end () ++ fnl() ++ str "Proof" else mt())
   with Not_found ->