Browse files

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
  • Loading branch information...
1 parent 4a10b5e commit d3b2c6f8a6864c44236b1f4b2ac89a025f49b7cd courtieu committed Oct 1, 2012
Showing with 51 additions and 1 deletion.
  1. +2 −0 grammar/q_coqast.ml4
  2. +1 −0 intf/tacexpr.mli
  3. +1 −0 parsing/g_ltac.ml4
  4. +3 −0 printing/pptactic.ml
  5. +38 −0 proofs/refiner.ml
  6. +1 −0 proofs/refiner.mli
  7. +3 −1 tactics/tacinterp.ml
  8. +1 −0 tactics/tacticals.ml
  9. +1 −0 tactics/tacticals.mli
View
2 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) ->
View
1 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
View
1 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 ->
View
3 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
View
38 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
View
1 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,
View
4 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,
View
1 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
View
1 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

0 comments on commit d3b2c6f

Please sign in to comment.