diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 22 | ||||
| -rw-r--r-- | proofs/refiner.mli | 7 |
2 files changed, 29 insertions, 0 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index dad31af9cb..e68b4bf4a5 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -530,6 +530,28 @@ let rec tclFIRST = function | [] -> tclFAIL_s "No applicable tactic." | t::rest -> tclORELSE0 t (tclFIRST rest) +let ite_gen tcal tac_if continue tac_else= + let success=ref false in + let tac_if0 gl= + let result=tac_if gl in + success:=true;result in + let tac_else0 gl= + if !success then + tclFAIL_s "failure in THEN branch" gl + else + tac_else gl in + tclORELSE0 (tcal tac_if0 continue) (tac_else0) + +(* Try the first tactic and, if it succeeds, continue with + the second one, and if it fails, use the third one *) + +let tclIFTHENELSE=ite_gen tclTHEN + +(* Idem with tclTHENS and tclTHENSV *) + +let tclIFTHENSELSE=ite_gen tclTHENS + +let tclIFTHENSVELSE=ite_gen tclTHENSV (* Fails if a tactic did not solve the goal *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 01ffae0d49..2e6f22de19 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -137,6 +137,13 @@ val tclWEAK_PROGRESS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic val tclINFO : tactic -> tactic +(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, + if it succeeds, applies [tac2] to the resulting subgoals, + and if not applies [tac3] to the initial goal [gls] *) +val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic +val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic +val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic + (*s Tactics handling a list of goals. *) type validation_list = proof_tree list -> proof_tree list |