aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/debug_tac.ml410
-rw-r--r--contrib/interface/pbp.ml2
-rw-r--r--contrib/interface/xlate.ml3
-rw-r--r--parsing/g_constr.ml44
-rw-r--r--parsing/g_ltac.ml428
-rw-r--r--parsing/pptactic.ml17
-rw-r--r--parsing/q_coqast.ml44
-rw-r--r--proofs/refiner.ml53
-rw-r--r--proofs/refiner.mli7
-rw-r--r--proofs/tacexpr.ml8
-rw-r--r--tactics/tacinterp.ml26
11 files changed, 107 insertions, 55 deletions
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index 890bb3ce55..aad3a765de 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -113,7 +113,7 @@ let count_subgoals2
let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
TacThens (a,l) ->
(fun report_holder -> checked_thens report_holder a l)
- | TacThen (a,b) ->
+ | TacThen (a,[||],b,[||]) ->
(fun report_holder -> checked_then report_holder a b)
| t ->
(fun report_holder g ->
@@ -279,7 +279,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
| Failed n -> TacId []
| Tree_fail r -> reconstruct_success_tac a r
| Mismatch (n,p) -> a)
- | TacThen (a,b) ->
+ | TacThen (a,[||],b,[||]) ->
(function
Report_node(true, n, l) -> tac
| Report_node(false, n, rl) ->
@@ -340,7 +340,7 @@ Tacinterp.add_tactic "OnThen" on_then;;
let rec clean_path tac l =
match tac, l with
- | TacThen (a,b), fst::tl ->
+ | TacThen (a,[||],b,[||]), fst::tl ->
fst::(clean_path (if fst = 1 then a else b) tl)
| TacThens (a,l), 1::tl ->
1::(clean_path a tl)
@@ -390,7 +390,7 @@ let rec report_error
| t::tl -> (report_error t the_goal the_ast returned_path (n::2::path))::
(fold_num (n + 1) tl) in
fold_num 1 l)
- | TacThen (a,b) ->
+ | TacThen (a,[||],b,[||]) ->
let the_count = ref 1 in
tclTHEN
(fun g ->
@@ -398,7 +398,7 @@ let rec report_error
report_error a the_goal the_ast returned_path (1::path) g
with
e ->
- (the_ast := TacThen (!the_ast, b);
+ (the_ast := TacThen (!the_ast,[||], b,[||]);
raise e))
(fun g ->
try
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index d2f71bfc2f..b1809523c4 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -156,7 +156,7 @@ let make_pbp_pattern x =
let rec make_then = function
| [] -> TacId []
| [t] -> t
- | t1::t2::l -> make_then (TacThen (t1,t2)::l)
+ | t1::t2::l -> make_then (TacThen (t1,[||],t2,[||])::l)
let make_pbp_atomic_tactic = function
| PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption))
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 57116c0709..6d52be45d9 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -775,10 +775,11 @@ and xlate_tactic =
| TacFun (largs, t) ->
let fst, rest = xlate_largs_to_id_opt largs in
CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t)
- | TacThen (t1,t2) ->
+ | TacThen (t1,[||],t2,[||]) ->
(match xlate_tactic t1 with
CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
| t -> CT_then (t,[xlate_tactic t2]))
+ | TacThen _ -> xlate_error "TacThen generalization TODO"
| TacThens(t1,[]) -> assert false
| TacThens(t1,t::l) ->
let ct = xlate_tactic t in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index fb3c7940ba..bdea94a048 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -131,7 +131,7 @@ GEXTEND Gram
[ [ c = operconstr LEVEL "200" -> c ] ]
;
constr:
- [ [ c = operconstr LEVEL "9" -> c ] ]
+ [ [ c = operconstr LEVEL "1" -> c ] ]
;
operconstr:
[ "200" RIGHTA
@@ -210,7 +210,7 @@ GEXTEND Gram
appl_arg:
[ [ id = lpar_id_coloneq; c=lconstr; ")" ->
(c,Some (loc,ExplByName id))
- | c=constr -> (c,None) ] ]
+ | c=operconstr LEVEL "9" -> (c,None) ] ]
;
atomic_constr:
[ [ g=global -> CRef g
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 4b954b174c..5755aee645 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -46,16 +46,31 @@ GEXTEND Gram
GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg
constr_may_eval;
+ tactic_then_last:
+ [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
+ Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta)
+ | -> [||]
+ ] ]
+ ;
+ tactic_then_gen:
+ [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last)
+ | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l))
+ | ".."; l = tactic_then_last -> ([], Some (TacId [], l))
+ | ta = tactic_expr -> ([ta], None)
+ | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last)
+ | -> ([TacId []], None)
+ ] ]
+ ;
tactic_expr:
[ "5" RIGHTA
[ te = binder_tactic -> te ]
| "4" LEFTA
- [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
- | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
- | ta = tactic_expr; ";";
- "["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
- let lta = List.map (function None -> TacId [] | Some t -> t) lta in
- TacThens (ta, lta) ]
+ [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, [||], ta1, [||])
+ | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, [||], ta1, [||])
+ | ta0 = tactic_expr; ";"; "["; (first,tail) = tactic_then_gen; "]" ->
+ match tail with
+ | Some (t,last) -> TacThen (ta0, Array.of_list first, t, last)
+ | None -> TacThens (ta0,first) ]
| "3" RIGHTA
[ IDENT "try"; ta = tactic_expr -> TacTry ta
| IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
@@ -114,6 +129,7 @@ GEXTEND Gram
(* Tactic arguments *)
tactic_arg:
[ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a
+ | IDENT "ltac"; ":"; n = natural -> Integer n
| IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat
| a = may_eval_arg -> a
| r = reference -> Reference r
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 4956345120..a70c9acdbb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -487,6 +487,17 @@ let pr_seq_body pr tl =
prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
str " ]")
+let pr_opt_tactic pr = function
+ | TacId [] -> mt ()
+ | t -> pr t
+
+let pr_then_gen pr tf tm tl =
+ hv 0 (str "[ " ++
+ prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
+ pr_opt_tactic pr tm ++ str ".." ++
+ prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl ++
+ str " ]")
+
let pr_hintbases = function
| None -> spc () ++ str "with *"
| Some [] -> mt ()
@@ -858,10 +869,14 @@ let rec pr_tac inherited tac =
hov 1 (pr_tac (lseq,E) t ++ pr_then () ++ spc () ++
pr_seq_body (pr_tac ltop) tl),
lseq
- | TacThen (t1,t2) ->
+ | TacThen (t1,[||],t2,[||]) ->
hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
pr_tac (lseq,L) t2),
lseq
+ | TacThen (t1,tf,t2,tl) ->
+ hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
+ pr_then_gen (pr_tac ltop) tf t2 tl),
+ lseq
| TacTry t ->
hov 1 (str "try" ++ spc () ++ pr_tac (ltactical,E) t),
ltactical
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 56dd32c555..bea93a39c3 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -398,8 +398,8 @@ let rec mlexpr_of_atomic_tactic = function
and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
| Tacexpr.TacAtom (loc,t) ->
<:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >>
- | Tacexpr.TacThen (t1,t2) ->
- <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >>
+ | Tacexpr.TacThen (t1,[||],t2,[||]) ->
+ <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ [||] $mlexpr_of_tactic t2$ [||]>>
| Tacexpr.TacThens (t,tl) ->
<:expr< Tacexpr.TacThens $mlexpr_of_tactic t$ $mlexpr_of_list mlexpr_of_tactic tl$>>
| Tacexpr.TacFirst tl ->
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a03e0b9e69..76fe0129f0 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -334,29 +334,25 @@ let start_tac gls =
let finish_tac (sigr,gl,p) = (repackage sigr gl, p)
-(* Apply [taci.(i)] on the first n-th subgoals and [tac] on the others *)
-let thensf_tac taci tac (sigr,gs,p) =
- let n = Array.length taci in
- let nsg = List.length gs in
- if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
+let thens3parts_tac tacfi tac tacli (sigr,gs,p) =
+ let nf = Array.length tacfi in
+ let nl = Array.length tacli in
+ let ng = List.length gs in
+ if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
let gll,pl =
List.split
- (list_map_i (fun i -> apply_sig_tac sigr (if i<n then taci.(i) else tac))
+ (list_map_i (fun i ->
+ apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
0 gs) in
(sigr, List.flatten gll,
compose p (mapshape (List.map List.length gll) pl))
-(* Apply [taci.(i)] on the last n-th subgoals and [tac] on the others *)
-let thensl_tac tac taci (sigr,gs,p) =
- let n = Array.length taci in
- let nsg = List.length gs in
- if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
- let gll,pl =
- List.split
- (list_map_i (fun i -> apply_sig_tac sigr (if i<0 then tac else taci.(i)))
- (n-nsg) gs) in
- (sigr, List.flatten gll,
- compose p (mapshape (List.map List.length gll) pl))
+(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
+let thensf_tac taci tac = thens3parts_tac taci tac [||]
+
+(* Apply [taci.(i)] on the last n subgoals and [tac] on the others *)
+let thensl_tac tac taci = thens3parts_tac [||] tac taci
(* Apply [tac i] on the ith subgoal (no subgoals number check) *)
let thensi_tac tac (sigr,gs,p) =
@@ -382,19 +378,25 @@ let theni_tac i tac ((_,gl,_) as subgoals) =
subgoals
else non_existent_goal k
+(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
+ applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
+ the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
+ subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
+ error if the number of resulting subgoals is strictly less than [n+m] *)
+let tclTHENS3PARTS tac1 tacfi tac tacli gls =
+ finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls)))
+
(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1]
- to [gls] and applies [t1], ..., [tn] to the [n] first resulting
+ to [gls] and applies [t1], ..., [tn] to the first [n] resulting
subgoals, and [tac2] to the others subgoals. Raises an error if
the number of resulting subgoals is strictly less than [n] *)
-let tclTHENSFIRSTn tac1 taci tac gls =
- finish_tac (thensf_tac taci tac (then_tac tac1 (start_tac gls)))
+let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||]
(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1]
- to [gls] and applies [t1], ..., [tn] to the [n] last resulting
+ to [gls] and applies [t1], ..., [tn] to the last [n] resulting
subgoals, and [tac2] to the other subgoals. Raises an error if the
number of resulting subgoals is strictly less than [n] *)
-let tclTHENSLASTn tac1 tac taci gls =
- finish_tac (thensl_tac tac taci (then_tac tac1 (start_tac gls)))
+let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci
(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies
[(taci i)] to the i_th resulting subgoal (starting from 1), whatever the
@@ -407,13 +409,13 @@ let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC
(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[tac2] to every resulting subgoals *)
-let tclTHEN tac1 tac2 = tclTHENSFIRSTn tac1 [||] tac2
+let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||]
(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
[gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
an error if the number of resulting subgoals is not [n] *)
let tclTHENSV tac1 tac2v =
- tclTHENSFIRSTn tac1 tac2v (tclFAIL_s "Wrong number of tactics.")
+ tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||]
let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l)
@@ -425,7 +427,6 @@ let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|]
to the first resulting subgoal *)
let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC
-
(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
convenient than [tclTHEN] when [n] is large. *)
let rec tclTHENLIST = function
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index b4b37fdf39..43d5af159d 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -100,6 +100,13 @@ val tclTHENS : tactic -> tactic list -> tactic
val tclTHENST : tactic -> tactic array -> tactic -> tactic
*)
+(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
+ applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
+ the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
+ subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
+ error if the number of resulting subgoals is strictly less than [n+m] *)
+val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic
+
(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index caa7523a6d..633a9a42d3 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -197,8 +197,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
| TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
- | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
- | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+ | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array
+ | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
+ ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
| TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
| TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
| TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 75f517023f..e0c279a071 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -764,15 +764,21 @@ and intern_tactic_seq ist = function
ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
| TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
| TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
- | TacThen (t1,t2) ->
+ | TacThen (t1,[||],t2,[||]) ->
let lfun', t1 = intern_tactic_seq ist t1 in
let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in
- lfun'', TacThen (t1,t2)
+ lfun'', TacThen (t1,[||],t2,[||])
+ | TacThen (t1,tf,t2,tl) ->
+ let lfun', t1 = intern_tactic_seq ist t1 in
+ let ist' = { ist with ltacvars = lfun' } in
+ (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
+ lfun', TacThen (t1,Array.map (intern_tactic ist') tf,intern_tactic ist' t2,
+ Array.map (intern_tactic ist') tl)
| TacThens (t,tl) ->
let lfun', t = intern_tactic_seq ist t in
+ let ist' = { ist with ltacvars = lfun' } in
(* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
- lfun',
- TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl)
+ lfun', TacThens (t, List.map (intern_tactic ist') tl)
| TacDo (n,tac) ->
ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac)
| TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
@@ -1532,9 +1538,10 @@ and eval_tactic ist = function
| TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
| TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
| TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
- | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2)
- | TacThens (t,tl) ->
- tclTHENS (interp_tactic ist t) (List.map (interp_tactic ist) tl)
+ | TacThen (t1,tf,t,tl) ->
+ tclTHENS3PARTS (interp_tactic ist t1)
+ (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
+ | TacThens (t1,tl) -> tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
| TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
| TacTry tac -> tclTRY (interp_tactic ist tac)
| TacInfo tac -> tclINFO (interp_tactic ist tac)
@@ -2410,8 +2417,9 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacId _ | TacFail _ as x -> x
| TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
| TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
- | TacThen (t1,t2) ->
- TacThen (subst_tactic subst t1,subst_tactic subst t2)
+ | TacThen (t1,tf,t2,tl) ->
+ TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
+ subst_tactic subst t2,Array.map (subst_tactic subst) tl)
| TacThens (t,tl) ->
TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
| TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 16:52:11 +0000