Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 78 insertions, 46 deletions

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<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 +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