From 79311e8734b5970afa3db069e9452c2521713895 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 16 May 2000 16:49:27 +0000 Subject: Retrait du i pour tclTHEN_i et correction bugs Decompose git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@434 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/refiner.ml | 47 +++++++++++++++++++++-------------------------- proofs/refiner.mli | 25 +++++++++++++++++++++++-- proofs/tacmach.mli | 2 +- 3 files changed, 45 insertions(+), 29 deletions(-) (limited to 'proofs') diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 9e1698c25c..915431d597 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -337,12 +337,11 @@ let thens_tac tac2l taci (sigr,gs,p) = with Failure _ -> errorlabstrm "Refiner.combine_tactics" [<'sTR "Wrong number of tactics.">] in let tac2gl = - List.combine gl tac2l @ list_map_i (fun i g -> (g, taci i)) 0 gi in + List.combine gl tac2l @ list_map_i (fun i g -> (g, taci i)) 1 gi in let gll,pl = List.split(List.map (fun (g,tac2) -> apply_sig_tac sigr tac2 g) tac2gl) in (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl)) -;; let then_tac tac = thens_tac [] (fun _ -> tac);; @@ -350,55 +349,51 @@ let then_tac tac = thens_tac [] (fun _ -> tac);; let non_existent_goal n = errorlabstrm ("No such goal: "^(string_of_int n)) [< 'sTR"Trying to apply a tactic to a non existent goal" >] -;; (* Apply tac on the i-th goal (if i>0). If i<0, then start counting from the last goal (i=-1). *) let theni_tac i tac ((_,gl,_) as subgoals) = let nsg = List.length gl in - let k = if i < 0 then nsg + i else (i-1) in + let k = if i < 0 then nsg + i + 1 else i in if nsg < 1 then errorlabstrm "theni_tac" [< 'sTR"No more subgoals.">] - else if k >= 0 & k < nsg then + else if k >= 1 & k <= nsg then thens_tac [] (fun i -> if i = k then tac else tclIDTAC) subgoals - else non_existent_goal (k+1) -;; + else non_existent_goal k - -(* tclTHENSi tac1 [t1 ; ... ; tn] taci gls applies the tactic tac1 to gls and - applies t1,..., tn to the n first resulting subgoals, and (taci i) to the - (i+n+1)-th goal. Raises an error if the number of resulting subgoals - is less than n *) +(* [tclTHENSi tac1 [t1 ; ... ; tn] taci gls] applies the tactic [tac1] + to [gls] and applies [t1], ..., [tn] to the [n] first resulting + subgoals, and [(taci i)] to the (i+n)-th goal. Raises an error if + the number of resulting subgoals is less than [n] *) let tclTHENSi tac1 tac2l taci gls = finish_tac (thens_tac tac2l taci (then_tac tac1 (start_tac gls))) ;; -(* tclTHEN tac1 tac2 gls applies the tactic tac1 to gls and applies tac2 to - every resulting subgoals *) +(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) let tclTHEN tac1 tac2 = tclTHENSi tac1 [] (fun _ -> tac2);; -(* tclTHEN_i tac1 tac2 n gls applies the tactic tac1 to gls and applies - tac2 (i+n-1) to the i_th resulting subgoal *) -let tclTHEN_i tac1 tac2 n = tclTHENSi tac1 [] (fun i -> tac2 (i+n));; +(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [(tac2 i)] to the i_th resulting subgoal (starting from 1) *) +let tclTHEN_i tac1 tac2 = tclTHENSi tac1 [] tac2;; -(* 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 *) +(* [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] *) let tclTHENS tac1 tac2l = tclTHENSi tac1 tac2l (fun _ -> tclFAIL_s "Wrong number of tactics.");; -(* Same as tclTHENS but completes with Idtac if the number resulting subgoals - is strictly less than n *) +(* Same as [tclTHENS] but completes with [Idtac] if the number resulting + subgoals is strictly less than [n] *) let tclTHENSI tac1 tac2l = tclTHENSi tac1 tac2l (fun _ -> tclIDTAC);; - -(* tclTHENL tac1 tac2 gls applies the tactic tac1 to gls and tac2 +(* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the last resulting subgoal *) let tclTHENL (tac1 : tactic) (tac2 : tactic) (gls : goal sigma) = finish_tac (theni_tac (-1) tac2 (then_tac tac1 (start_tac gls))) ;; -(* tclTHENLIST [t1;..;tn] applies t1;..tn. More convenient than tclTHEN - when n is large. *) +(* [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) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 4b821596e4..98c6ab96fe 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -45,14 +45,35 @@ val extract_open_proof : (*s Tacticals. *) +(* [tclIDTAC] is the identity tactic *) val tclIDTAC : tactic -val tclORELSE : tactic -> tactic -> tactic + +(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) val tclTHEN : tactic -> tactic -> tactic + +(* [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More + convenient than [tclTHEN] when [n] is large *) val tclTHENLIST : tactic list -> tactic -val tclTHEN_i : tactic -> (int -> tactic) -> int -> tactic + +(* [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 + +(* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the last resulting subgoal *) val tclTHENL : tactic -> tactic -> tactic + +(* [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 tclTHENS : tactic -> tactic list -> tactic + +(* Same as [tclTHENS] but completes with [Idtac] if the number resulting + subgoals is strictly less than [n] *) val tclTHENSI : tactic -> tactic list -> tactic + +val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic val tclFIRST : tactic list -> tactic val tclSOLVE : tactic list -> tactic diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index afb9016ea5..b27b0b789e 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -117,7 +117,7 @@ val tclIDTAC : tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic val tclTHENLIST : tactic list -> tactic -val tclTHEN_i : tactic -> (int -> tactic) -> int -> tactic +val tclTHEN_i : tactic -> (int -> tactic) -> tactic val tclTHENL : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic val tclTHENSI : tactic -> tactic list -> tactic -- cgit v1.2.3