Added a new tactical infoH tac, that displays the names of hypothesis created by tac, in the 'as' format. Interfaces can use this to insert automatically an 'as' close at the end of the tactic (afterward).

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

9 files changed, 51 insertions, 1 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3fd4600587..aae1d9de2a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -449,6 +449,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >>
   | Tacexpr.TacProgress t ->
       <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >>
+  | Tacexpr.TacShowHyps t ->
+      <:expr< Tacexpr.TacShowHyps $mlexpr_of_tactic t$ >>
   | Tacexpr.TacId l ->
       <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >>
   | Tacexpr.TacFail (n,l) ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index b07b86fbf9..3612635d6e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -183,6 +183,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr =
   | TacTimeout of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
   | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
   | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+  | TacShowHyps of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
   | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option
   | TacId of 'id message_token list
   | TacFail of int or_var * 'id message_token list
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 51839ee880..bc2803ae5e 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -61,6 +61,7 @@ GEXTEND Gram
       | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
+      | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c317d4f3f9..8bdea1356b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -906,6 +906,9 @@ let rec pr_tac inherited tac =
   | TacProgress t ->
       hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t),
       ltactical
+  | TacShowHyps t ->
+      hov 1 (str "infoH" ++ spc () ++ spc () ++ pr_tac (ltactical,E) t),
+      ltactical
   | TacInfo t ->
       hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
       linfo
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 0652f19864..a41bfdd49f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -230,6 +230,44 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
+let rec subtrac l1 l2 =
+  match l1,l2 with
+    | [],l -> l
+    | _,[] -> []
+    | _,(e2::l2') -> 
+      if List.mem e2 l1 then subtrac l1 l2'
+      else e2:: subtrac l1 l2'
+      
+
+(* Execute tac and show the names of hypothesis create by tac in
+   the "as" format. The resulting goals are printed *after* the
+   as-expression, which forces pg to some gymnastic. TODO: Have
+   something similar (better?) in the xml protocol. *)
+let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
+    :Proof_type.goal list Evd.sigma =
+  let oldhyps:Sign.named_context = pf_hyps goal in
+  let rslt:Proof_type.goal list Evd.sigma = tac goal in
+  let {it=gls;sigma=sigma} = rslt in
+  let hyps:Sign.named_context list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma}) gls in
+  let newhyps =
+    List.map (fun hypl -> subtrac oldhyps hypl)
+      hyps in
+  let emacs_str s =
+    if !Flags.print_emacs then s else "" in
+  let s = 
+    let frst = ref true in
+    List.fold_left
+    (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
+      ^ (List.fold_left
+	   (fun acc (nm,_,_) -> (Names.string_of_id nm) ^ " " ^ acc)
+	   "" lh))
+    "" newhyps in
+  pp (str (emacs_str "<infoH>")
+      ++  (hov 0 (str s))
+      ++  (str (emacs_str "</infoH>")) ++ fnl());
+  rslt;;
+
+
 let catch_failerror e =
   if catchable_exception e then check_for_interrupt ()
   else match e with
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 4e30c9c0b2..b5fc9ee66f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -136,6 +136,7 @@ val tclDO            : int -> tactic -> tactic
 val tclTIMEOUT       : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
+val tclSHOWHYPS      : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 057a268f56..9bbb095893 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -839,7 +839,7 @@ and intern_tactic_seq onlytac ist = function
   | TacId l -> ist.ltacvars, TacId (intern_message ist l)
   | TacFail (n,l) ->
       ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
-  | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)
+  | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)  | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac)
   | TacAbstract (tac,s) ->
       ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s)
   | TacThen (t1,[||],t2,[||]) ->
@@ -1809,6 +1809,7 @@ and eval_tactic ist = function
       db_breakpoint ist.debug s; res
   | TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
+  | TacShowHyps tac -> tclSHOWHYPS (interp_tactic ist tac)
   | TacAbstract (tac,ido) ->
       fun gl -> Tactics.tclABSTRACT
         (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl
@@ -2940,6 +2941,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr)
   | TacId _ | TacFail _ as x -> x
   | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
+  | TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr)
   | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
   | TacThen (t1,tf,t2,tl) ->
       TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 637269a663..69cee21487 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -53,6 +53,7 @@ let tclDO            = Refiner.tclDO
 let tclTIMEOUT       = Refiner.tclTIMEOUT
 let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclPROGRESS      = Refiner.tclPROGRESS
+let tclSHOWHYPS      = Refiner.tclSHOWHYPS
 let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
 let tclTHENTRY       = Refiner.tclTHENTRY
 let tclIFTHENELSE    = Refiner.tclIFTHENELSE
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4e9198d37d..39f60e1968 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -54,6 +54,7 @@ val tclFAIL_lazy     : int -> std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
+val tclSHOWHYPS      : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic