From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- proofs/refiner.ml | 124 ++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 78 insertions(+), 46 deletions(-) (limited to 'proofs/refiner.ml') diff --git a/proofs/refiner.ml b/proofs/refiner.ml index a1d7e011..172a7d70 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml 9573 2007-01-31 20:18:18Z notin $ *) +(* $Id: refiner.ml 11021 2008-05-29 16:48:18Z barras $ *) open Pp open Util @@ -108,13 +108,23 @@ let rec frontier p = open_subgoals = and_status (List.map pf_status pfl'); ref = Some(r,pfl')})) +(* TODO LEM: I might have to make sure that these hooks are called + only when called from solve_nth_pftreestate; I can build the hook + call into the "f", then. + *) +let solve_hook = ref ignore +let set_solve_hook = (:=) solve_hook let rec frontier_map_rec f n p = if n < 1 || n > p.open_subgoals then p else match p.ref with | None -> let p' = f p in - if Evd.eq_evar_info p'.goal p.goal then p' + if Evd.eq_evar_info p'.goal p.goal then + begin + !solve_hook p'; + p' + end else errorlabstrm "Refiner.frontier_map" (str"frontier_map was handed back a ill-formed proof.") @@ -140,7 +150,11 @@ let rec frontier_mapi_rec f i p = match p.ref with | None -> let p' = f i p in - if Evd.eq_evar_info p'.goal p.goal then p' + if Evd.eq_evar_info p'.goal p.goal then + begin + !solve_hook p'; + p' + end else errorlabstrm "Refiner.frontier_mapi" (str"frontier_mapi was handed back a ill-formed proof.") @@ -223,9 +237,7 @@ let refiner = function ref = Some(Daimon,[])}) -let local_Constraints gl = refiner (Prim Change_evars) gl - -let norm_evar_tac = local_Constraints +let norm_evar_tac gl = refiner (Prim Change_evars) gl let norm_evar_proof sigma pf = let nf_subgoal i sgl = @@ -312,6 +324,9 @@ let idtac_valid = function (* [goal_goal_list : goal sigma -> goal list sigma] *) let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} +(* forces propagation of evar constraints *) +let tclNORMEVAR = norm_evar_tac + (* identity tactic without any message *) let tclIDTAC gls = (goal_goal_list gls, idtac_valid) @@ -334,29 +349,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 apply_sig_tac sigr (if i + apply_sig_tac sigr (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 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 +393,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 +424,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 +442,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 @@ -437,18 +453,17 @@ let rec tclTHENLIST = function (* various progress criterions *) let same_goal gl subgoal = - eq_named_context_val (hypotheses subgoal) (hypotheses gl) && - eq_constr (conclusion subgoal) (conclusion gl) + eq_constr (conclusion subgoal) (conclusion gl) && + eq_named_context_val (hypotheses subgoal) (hypotheses gl) let weak_progress gls ptree = - (List.length gls.it <> 1) or + (List.length gls.it <> 1) || (not (same_goal (List.hd gls.it) ptree.it)) -(* Il y avait ici un ts_eq ........ *) let progress gls ptree = - (weak_progress gls ptree) or - (not (ptree.sigma == gls.sigma)) + (not (ptree.sigma == gls.sigma)) || + (weak_progress gls ptree) (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves @@ -476,24 +491,39 @@ let tclNOTSAMEGOAL (tac : tactic) goal = (str"Tactic generated a subgoal identical to the original goal.") else rslt - +let catch_failerror = function + | e when catchable_exception e -> check_for_interrupt () + | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> + check_for_interrupt () + | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) + | Stdpp.Exc_located (s,FailError (lvl,s')) -> + raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) + | e -> raise e (* 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 catchable_exception e -> check_for_interrupt (); t2 g - | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> - check_for_interrupt (); t2 g - | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located (s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) + | e -> 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 -> catch_failerror e; None + with + | None -> t2else gls + | Some (sgl,v) -> + let (sigr,gl) = unpackage sgl in + finish_tac (then_tac t2then (sigr,gl,v)) + (* TRY f tries to apply f, and if it fails, leave the goal unchanged *) let tclTRY f = (tclORELSE0 f tclIDTAC) @@ -558,9 +588,10 @@ let tclDO n t = in dorec n + (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = - (tclORELSE (tclTHEN t (tclREPEAT t)) tclIDTAC) g + tclORELSE_THEN t (tclREPEAT t) tclIDTAC g let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) @@ -847,6 +878,7 @@ let prev_unproven pts = let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) +(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *) let change_rule f pts = let mark_top _ pt = match pt.ref with -- cgit v1.2.3