From d3b2c6f8a6864c44236b1f4b2ac89a025f49b7cd Mon Sep 17 00:00:00 2001
From: courtieu
Date: Mon, 1 Oct 2012 16:17:51 +0000
Subject: 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
---
 proofs/refiner.ml  | 38 ++++++++++++++++++++++++++++++++++++++
 proofs/refiner.mli |  1 +
 2 files changed, 39 insertions(+)

(limited to 'proofs')

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,
-- 
cgit v1.2.3