diff options
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.ml | 228 | ||||
| -rw-r--r-- | proofs/refiner.mli | 98 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 255 |
4 files changed, 226 insertions, 359 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 705a1a62ce..d65c2f0de9 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1103,8 +1103,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> Proofview.V82.tactic begin - tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) - end [@ocaml.warning "-3"] + Tacticals.tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) + end | TacAbstract (t,ido) -> let call = LtacMLCall tac in let trace = push_trace(None,call) ist in diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 874bab277d..3c6a5d1694 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -8,15 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp -open CErrors open Util open Evd type tactic = Proofview.V82.tac -module NamedDecl = Context.Named.Declaration - let sig_it x = x.it let project x = x.sigma @@ -27,235 +23,11 @@ let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig let refiner = Logic.refiner -(*********************) -(* Tacticals *) -(*********************) - - -let unpackage glsig = (ref (glsig.sigma)), glsig.it - -let repackage r v = {it = v; sigma = !r; } - -let apply_sig_tac r tac g = - Control.check_for_interrupt (); (* Breakpoint *) - let glsigma = tac (repackage r g) in - r := glsigma.sigma; - glsigma.it - -(* [goal_goal_list : goal sigma -> goal list sigma] *) -let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; } - -(* identity tactic without any message *) -let tclIDTAC gls = goal_goal_list gls - -(* the message printing identity tactic *) -let tclIDTAC_MESSAGE s gls = - Feedback.msg_info (hov 0 s); tclIDTAC gls - -(* General failure tactic *) -let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) - (* A special exception for levels for the Fail tactic *) exception FailError of int * Pp.t Lazy.t -(* The Fail tactic *) -let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) - -let tclFAIL_lazy lvl s g = raise (FailError (lvl,s)) - -let start_tac gls = - let sigr, g = unpackage gls in - (sigr, [g]) - -let finish_tac (sigr,gl) = repackage sigr gl - -(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last - m subgoals, and [tac] on the others *) -let thens3parts_tac tacfi tac tacli (sigr,gs) = - let nf = Array.length tacfi in - let nl = Array.length tacli in - let ng = List.length gs in - if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals."); - let gll = - (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) - -(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) -let thensf_tac taci tac = thens3parts_tac taci tac [||] - -(* Apply [tac i] on the ith subgoal (no subgoals number check) *) -let thensi_tac tac (sigr,gs) = - let gll = - List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in - (sigr, List.flatten gll) - -let then_tac tac = thensf_tac [||] tac - -(* [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 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 = tclTHENS3PARTS tac1 taci tac [||] - -(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1] - 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 = 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 - number of subgoals is *) -let tclTHEN_i tac taci gls = - finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) - -(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies - [tac2] to every resulting subgoals *) -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 = - tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||] - -let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l) - -(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] - to the last resulting subgoal *) -let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|] - -(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [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 - [] -> tclIDTAC - | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) - -(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) -let tclMAP tacfun l = - List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC - -(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves -the goal unchanged *) -let tclPROGRESS tac ptree = - let rslt = tac ptree in - if Goal.V82.progress rslt ptree then rslt - else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.") - -(* Execute tac, show the names of new hypothesis names created by tac - in the "as" format and then forget everything. From the logical - point of view [tclSHOWHYPS tac] is therefore equivalent to idtac, - except that it takes the time and memory of tac and prints "as" - information). The resulting (unchanged) goals are printed *after* - the as-expression, which forces pg to some gymnastic. - TODO: Have something similar (better?) in the xml protocol. - NOTE: some tactics delete hypothesis and reuse names (induction, - destruct), this is not detected by this tactical. *) -let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) - : Goal.goal list Evd.sigma = - let oldhyps = pf_hyps goal in - let rslt:Goal.goal list Evd.sigma = tac goal in - let { it = gls; sigma = sigma; } = rslt in - let hyps = - List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in - let newhyps = - List.map - (fun hypl -> List.subtract cmp hypl oldhyps) - hyps - 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 d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) - "" lh)) - "" newhyps in - Feedback.msg_notice - (str "<infoH>" - ++ (hov 0 (str s)) - ++ (str "</infoH>")); - tclIDTAC goal;; - - let catch_failerror (e, info) = match e with | FailError (lvl,s) when lvl > 0 -> Exninfo.iraise (FailError (lvl - 1, s), info) | e -> Control.check_for_interrupt () - -(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) -let tclORELSE0 t1 t2 g = - try - t1 g - with (* Breakpoint *) - | e when CErrors.noncritical e -> - let e = Exninfo.capture e in catch_failerror e; t2 g - -(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, - then applies t2 *) -let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 - -(* applies t1;t2then if t1 succeeds or t2else if t1 fails - t2* are called in terminal position (unless t1 produces more than - 1 subgoal!) *) -let tclORELSE_THEN t1 t2then t2else gls = - match - try Some(tclPROGRESS t1 gls) - with e when CErrors.noncritical e -> - let e = Exninfo.capture e in catch_failerror e; None - with - | None -> t2else gls - | Some sgl -> - let sigr, gl = unpackage sgl in - finish_tac (then_tac t2then (sigr,gl)) - -(* TRY f tries to apply f, and if it fails, leave the goal unchanged *) -let tclTRY f = (tclORELSE0 f tclIDTAC) - -let tclTHENTRY f g = (tclTHEN f (tclTRY g)) - -(* Try the first tactic that does not fail in a list of tactics *) - -let rec tclFIRST = function - | [] -> tclFAIL_s "No applicable tactic." - | t::rest -> tclORELSE0 t (tclFIRST rest) - -(* Fails if a tactic did not solve the goal *) -let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") - -(* Iteration tacticals *) - -let tclDO n t = - let rec dorec k = - if k < 0 then user_err ~hdr:"Refiner.tclDO" - (str"Wrong argument : Do needs a positive integer."); - if Int.equal k 0 then tclIDTAC - else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) - in - dorec n - - -(* Beware: call by need of CAML, g is needed *) -let rec tclREPEAT t g = - tclORELSE_THEN t (tclREPEAT t) tclIDTAC g - -let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) - -(* Change evars *) -let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} diff --git a/proofs/refiner.mli b/proofs/refiner.mli index a3cbfb5d5d..0ea630fdbc 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -24,107 +24,9 @@ val pf_hyps : Goal.goal sigma -> named_context val refiner : check:bool -> Constr.t -> unit Proofview.tactic -(** {6 Tacticals. } *) - -(** [tclIDTAC] is the identity tactic without message printing*) -val tclIDTAC : tactic -[@@ocaml.deprecated "Use Tactical.New.tclIDTAC"] -val tclIDTAC_MESSAGE : Pp.t -> tactic -[@@ocaml.deprecated] - -(** [tclEVARS sigma] changes the current evar map *) -val tclEVARS : evar_map -> tactic -[@@ocaml.deprecated "Use Proofview.Unsafe.tclEVARS"] - - -(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies - [tac2] to every resulting subgoals *) -val tclTHEN : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHEN"] - -(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More - convenient than [tclTHEN] when [n] is large *) -val tclTHENLIST : tactic list -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENLIST"] - -(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) -val tclMAP : ('a -> tactic) -> 'a list -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclMAP"] - -(** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies - [(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *) -val tclTHEN_i : tactic -> (int -> tactic) -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHEN_i"] - -(** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] - to the last resulting subgoal (previously called [tclTHENL]) *) -val tclTHENLAST : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENLAST"] - -(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] - to the first resulting subgoal *) -val tclTHENFIRST : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENFIRST"] - -(** [tclTHENS 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] *) -val tclTHENSV : tactic -> tactic array -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENSV"] - -(** Same with a list of tactics *) -val tclTHENS : tactic -> tactic list -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENS"] - -(** [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 -[@@ocaml.deprecated "Use Tactical.New.tclTHENS3PARTS"] - -(** [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 -[@@ocaml.deprecated "Use Tactical.New.tclTHENSLASTn"] - -(** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then - applies [t1],...,[tn] on the first [n] resulting subgoals and - [tac2] for the remaining last subgoals (previously called tclTHENST) *) -val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENSFIRSTn"] - (** A special exception for levels for the Fail tactic *) exception FailError of int * Pp.t Lazy.t (** Takes an exception and either raise it at the next level or do nothing. *) val catch_failerror : Exninfo.iexn -> unit - -val tclORELSE0 : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclORELSE0"] -val tclORELSE : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclORELSE"] -val tclREPEAT : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclREPEAT"] -val tclFIRST : tactic list -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclFIRST"] -val tclTRY : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTRY"] -val tclTHENTRY : tactic -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclTHENTRY"] -val tclCOMPLETE : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclCOMPLETE"] -val tclAT_LEAST_ONCE : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclAT_LEAST_ONCE"] -val tclFAIL : int -> Pp.t -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclFAIL"] -val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclFAIL_lazy"] -val tclDO : int -> tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclDO"] -val tclPROGRESS : tactic -> tactic -[@@ocaml.deprecated "Use Tactical.New.tclPROGRESS"] -val tclSHOWHYPS : tactic -> tactic -[@@ocaml.deprecated "Internal tactic. Do not use."] diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 22c5bbe73f..d1ee55a677 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -23,39 +23,230 @@ open Tactypes module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -(************************************************************************) -(* Tacticals re-exported from the Refiner module *) -(************************************************************************) +(*********************) +(* Tacticals *) +(*********************) type tactic = Proofview.V82.tac -[@@@ocaml.warning "-3"] - -let tclIDTAC = Refiner.tclIDTAC -let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE -let tclORELSE0 = Refiner.tclORELSE0 -let tclORELSE = Refiner.tclORELSE -let tclTHEN = Refiner.tclTHEN -let tclTHENLIST = Refiner.tclTHENLIST -let tclMAP = Refiner.tclMAP -let tclTHEN_i = Refiner.tclTHEN_i -let tclTHENFIRST = Refiner.tclTHENFIRST -let tclTHENLAST = Refiner.tclTHENLAST -let tclTHENS = Refiner.tclTHENS -let tclTHENSV = Refiner.tclTHENSV -let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn -let tclTHENSLASTn = Refiner.tclTHENSLASTn -let tclREPEAT = Refiner.tclREPEAT -let tclFIRST = Refiner.tclFIRST -let tclTRY = Refiner.tclTRY -let tclCOMPLETE = Refiner.tclCOMPLETE -let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE -let tclFAIL = Refiner.tclFAIL -let tclFAIL_lazy = Refiner.tclFAIL_lazy -let tclDO = Refiner.tclDO -let tclPROGRESS = Refiner.tclPROGRESS -let tclSHOWHYPS = Refiner.tclSHOWHYPS -let tclTHENTRY = Refiner.tclTHENTRY +open Evd + +exception FailError = Refiner.FailError + +let unpackage glsig = (ref (glsig.sigma)), glsig.it + +let repackage r v = {it = v; sigma = !r; } + +let apply_sig_tac r tac g = + Control.check_for_interrupt (); (* Breakpoint *) + let glsigma = tac (repackage r g) in + r := glsigma.sigma; + glsigma.it + +(* [goal_goal_list : goal sigma -> goal list sigma] *) +let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; } + +(* identity tactic without any message *) +let tclIDTAC gls = goal_goal_list gls + +(* the message printing identity tactic *) +let tclIDTAC_MESSAGE s gls = + Feedback.msg_info (hov 0 s); tclIDTAC gls + +(* General failure tactic *) +let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) + +(* The Fail tactic *) +let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) + +let tclFAIL_lazy lvl s g = raise (FailError (lvl,s)) + +let start_tac gls = + let sigr, g = unpackage gls in + (sigr, [g]) + +let finish_tac (sigr,gl) = repackage sigr gl + +(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last + m subgoals, and [tac] on the others *) +let thens3parts_tac tacfi tac tacli (sigr,gs) = + let nf = Array.length tacfi in + let nl = Array.length tacli in + let ng = List.length gs in + if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals."); + let gll = + (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) + +(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) +let thensf_tac taci tac = thens3parts_tac taci tac [||] + +(* Apply [tac i] on the ith subgoal (no subgoals number check) *) +let thensi_tac tac (sigr,gs) = + let gll = + List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in + (sigr, List.flatten gll) + +let then_tac tac = thensf_tac [||] tac + +(* [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 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 = tclTHENS3PARTS tac1 taci tac [||] + +(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1] + 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 = 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 + number of subgoals is *) +let tclTHEN_i tac taci gls = + finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) + +(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) +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 = + tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||] + +let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l) + +(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the last resulting subgoal *) +let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|] + +(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [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 + [] -> tclIDTAC + | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) + +(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) +let tclMAP tacfun l = + List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC + +(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves +the goal unchanged *) +let tclPROGRESS tac ptree = + let rslt = tac ptree in + if Goal.V82.progress rslt ptree then rslt + else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.") + +(* Execute tac, show the names of new hypothesis names created by tac + in the "as" format and then forget everything. From the logical + point of view [tclSHOWHYPS tac] is therefore equivalent to idtac, + except that it takes the time and memory of tac and prints "as" + information). The resulting (unchanged) goals are printed *after* + the as-expression, which forces pg to some gymnastic. + TODO: Have something similar (better?) in the xml protocol. + NOTE: some tactics delete hypothesis and reuse names (induction, + destruct), this is not detected by this tactical. *) +let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) + : Goal.goal list Evd.sigma = + let oldhyps = pf_hyps goal in + let rslt:Goal.goal list Evd.sigma = tac goal in + let { it = gls; sigma = sigma; } = rslt in + let hyps = + List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in + let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in + let newhyps = + List.map + (fun hypl -> List.subtract cmp hypl oldhyps) + hyps + 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 d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) + "" lh)) + "" newhyps in + Feedback.msg_notice + (str "<infoH>" + ++ (hov 0 (str s)) + ++ (str "</infoH>")); + tclIDTAC goal;; + +(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) +let tclORELSE0 t1 t2 g = + try + t1 g + with (* Breakpoint *) + | e when CErrors.noncritical e -> + let e = Exninfo.capture e in Refiner.catch_failerror e; t2 g + +(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, + then applies t2 *) +let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 + +(* applies t1;t2then if t1 succeeds or t2else if t1 fails + t2* are called in terminal position (unless t1 produces more than + 1 subgoal!) *) +let tclORELSE_THEN t1 t2then t2else gls = + match + try Some(tclPROGRESS t1 gls) + with e when CErrors.noncritical e -> + let e = Exninfo.capture e in Refiner.catch_failerror e; None + with + | None -> t2else gls + | Some sgl -> + let sigr, gl = unpackage sgl in + finish_tac (then_tac t2then (sigr,gl)) + +(* TRY f tries to apply f, and if it fails, leave the goal unchanged *) +let tclTRY f = (tclORELSE0 f tclIDTAC) + +let tclTHENTRY f g = (tclTHEN f (tclTRY g)) + +(* Try the first tactic that does not fail in a list of tactics *) + +let rec tclFIRST = function + | [] -> tclFAIL_s "No applicable tactic." + | t::rest -> tclORELSE0 t (tclFIRST rest) + +(* Fails if a tactic did not solve the goal *) +let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") + +(* Iteration tacticals *) + +let tclDO n t = + let rec dorec k = + if k < 0 then user_err ~hdr:"Refiner.tclDO" + (str"Wrong argument : Do needs a positive integer."); + if Int.equal k 0 then tclIDTAC + else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) + in + dorec n + + +(* Beware: call by need of CAML, g is needed *) +let rec tclREPEAT t g = + tclORELSE_THEN t (tclREPEAT t) tclIDTAC g + +let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (************************************************************************) (* Tacticals applying on hypotheses *) @@ -245,10 +436,12 @@ let elimination_sort_of_clause = function | None -> elimination_sort_of_goal | Some id -> elimination_sort_of_hyp id +(* Change evars *) +let tclEVARS sigma gls = tclIDTAC {gls with Evd.sigma=sigma} let pf_with_evars glsev k gls = let evd, a = glsev gls in - tclTHEN (Refiner.tclEVARS evd) (k a) gls + tclTHEN (tclEVARS evd) (k a) gls let pf_constr_of_global gr k = pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k |