simplification de solve_subgoal: n'utilise plus frontier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3458 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 92 insertions, 61 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 153d3f637..ce43da5de 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -565,7 +565,7 @@ let vire_extvar s =
 
 let blast gls =
    let leaf g = {
-      status = Incomplete_proof;
+      open_subgoals = 1;
       goal = g;
       ref = None } in
      try (let (sgl,v) as res = !blast_tactic gls in
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 80b45cc6d..03d45828d 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -48,7 +48,7 @@ let nf_evar sigma ~preserve =
 (* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *)
 let rec unshare_proof_tree =
  let module PT = Proof_type in
-  function {PT.status = status ; PT.goal = goal ; PT.ref = ref} ->
+  function {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = ref} ->
    let unshared_ref =
     match ref with
        None -> None
@@ -62,7 +62,7 @@ let rec unshare_proof_tree =
         in
          Some (unshared_rule, List.map unshare_proof_tree pfs)
    in
-    {PT.status = status ; PT.goal = goal ; PT.ref = unshared_ref}
+    {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = unshared_ref}
 ;;
 
 module ProofTreeHash =
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 34e9a06e7..830a4f9ec 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -55,9 +55,9 @@ let subproof_of_proof pf = match pf.ref with
   | Some (Tactic (_,pf), _) -> pf
   | _ -> failwith "subproof_of_proof"
 
-let status_of_proof pf = pf.status
+let status_of_proof pf = pf.open_subgoals
 
-let is_complete_proof pf = pf.status = Complete_proof
+let is_complete_proof pf = pf.open_subgoals = 0
 
 let is_leaf_proof pf = (pf.ref = None)
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 889c16aba..3181adb9b 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -28,7 +28,7 @@ val ref_of_proof      : proof_tree -> (rule * proof_tree list)
 val children_of_proof : proof_tree -> proof_tree list
 val goal_of_proof     : proof_tree -> goal
 val subproof_of_proof : proof_tree -> proof_tree
-val status_of_proof   : proof_tree -> pf_status
+val status_of_proof   : proof_tree -> int
 val is_complete_proof : proof_tree -> bool
 val is_leaf_proof     : proof_tree -> bool
 val is_tactic_proof   : proof_tree -> bool
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 405d5e5da..6f4cf4640 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -23,10 +23,6 @@ open Genarg
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by Proof_tree and Refiner *)
 
-type pf_status =
-  | Complete_proof
-  | Incomplete_proof
-
 type prim_rule =
   | Intro of identifier
   | Intro_replacing of identifier
@@ -54,7 +50,7 @@ type 'a sigma = {
   if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
   that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
-  status : pf_status;
+  open_subgoals : int;
   goal : goal;
   ref : (rule * proof_tree list) option }
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 69aa0aff0..bf5d4f316 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -23,10 +23,6 @@ open Genarg
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
 
-type pf_status =
-  | Complete_proof
-  | Incomplete_proof
-
 type prim_rule =
   | Intro of identifier
   | Intro_replacing of identifier
@@ -82,7 +78,7 @@ type 'a sigma = {
   if [ref = (Some(Tactic (t,p),l))] then [p] is the proof 
   that the goal can be proven if the goals in [l] are solved. *)
 type proof_tree = {
-  status : pf_status;
+  open_subgoals : int;
   goal : goal;
   ref : (rule * proof_tree list) option }
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 41043eac0..293a2434a 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -35,16 +35,13 @@ let sig_sig x = x.sigma
 
 let project_with_focus gls = rc_of_gc (gls.sigma) (gls.it)
 
-let pf_status pf = pf.status
+let pf_status pf = pf.open_subgoals
 
-let is_complete pf = (Complete_proof = (pf_status pf))
+let is_complete pf = (0 = (pf_status pf))
 
 let on_open_proofs f pf = if is_complete pf then pf else f pf
 
-let rec and_status = function
-  | [] -> Complete_proof
-  | Complete_proof :: l -> and_status l
-  | _ -> Incomplete_proof
+let and_status = List.fold_left (+) 0
 
 (* Normalizing evars in a goal. Called by tactic Local_constraints
    (i.e. when the sigma of the proof tree changes). Detect if the
@@ -98,28 +95,69 @@ let rec frontier p =
     	(List.flatten gll,
          (fun retpfl ->
             let pfl' = mapshape (List.map List.length gll) vl retpfl in
-            { status = and_status (List.map pf_status pfl');
+            { open_subgoals = and_status (List.map pf_status pfl');
               goal = p.goal;
               ref = Some(r,pfl')}))
 
+
+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 p'.goal == p.goal || p'.goal = p.goal then p'
+        else 
+	  errorlabstrm "Refiner.frontier_map"
+            (str"frontier_map was handed back a ill-formed proof.")
+    | Some(r,pfl) ->
+        let (_,rpfl') =
+          List.fold_left
+            (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
+            (n,[]) pfl in
+        let pfl' = List.rev rpfl' in
+        { open_subgoals = and_status (List.map pf_status pfl');
+          goal = p.goal;
+          ref = Some(r,pfl')}
+
+let frontier_map f n p =
+  let nmax = p.open_subgoals in
+  let n = if n < 0 then nmax + n + 1 else n in
+  if n < 1 || n > nmax then
+    errorlabstrm "Refiner.frontier_map" (str "No such subgoal"); 
+  frontier_map_rec f n p
+
+let rec frontier_mapi_rec f i p =
+  if p.open_subgoals = 0 then p else
+  match p.ref with
+    | None -> 
+        let p' = f i p in
+        if p'.goal == p.goal || p'.goal = p.goal then p'
+        else 
+	  errorlabstrm "Refiner.frontier_mapi"
+            (str"frontier_mapi was handed back a ill-formed proof.")
+    | Some(r,pfl) ->
+        let (_,rpfl') =
+          List.fold_left
+            (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
+            (i,[]) pfl in
+        let pfl' = List.rev rpfl' in
+        { open_subgoals = and_status (List.map pf_status pfl');
+          goal = p.goal;
+          ref = Some(r,pfl')}
+
+let frontier_mapi f p = frontier_mapi_rec f 1 p
+
 (* [list_pf p] is the lists of goals to be solved in order to complete the
    proof [p] *)
 
 let list_pf p = fst (frontier p)
 
-let rec nb_unsolved_goals pf = 
-  if is_complete pf then 
-    0 
-  else if is_leaf_proof pf then 
-    1 
-  else 
-    let lpf = children_of_proof pf in 
-    List.fold_left (fun n pf1 -> n + nb_unsolved_goals pf1) 0 lpf
+let rec nb_unsolved_goals pf = pf.open_subgoals
 
 (* leaf g is the canonical incomplete proof of a goal g *)
 
 let leaf g = {
-  status = Incomplete_proof;
+  open_subgoals = 1;
   goal = g;
   ref = None }
 
@@ -163,7 +201,7 @@ let abstract_tactic_expr te tacfun gls =
   (sgl_sigma,
    fun spfl ->
      assert (check_subproof_connection sgl_sigma.it spfl);
-     { status = and_status (List.map pf_status spfl);
+     { open_subgoals = and_status (List.map pf_status spfl);
        goal = gls.it;
        ref = Some(Tactic(te,hidden_proof),spfl) })
 
@@ -175,7 +213,7 @@ let refiner = function
 	 ({it=sgl; sigma = goal_sigma.sigma},
           (fun spfl ->
 	     assert (check_subproof_connection sgl spfl);
-             { status = and_status (List.map pf_status spfl);
+             { open_subgoals = and_status (List.map pf_status spfl);
                goal = goal_sigma.it;
                ref = Some(r,spfl) })))
 
@@ -192,7 +230,7 @@ let refiner = function
 	       ({it=[ngl];sigma=goal_sigma.sigma},
                 (fun spfl -> 
 	          assert (check_subproof_connection [ngl] spfl);
-                  { status = (List.hd spfl).status;
+                  { open_subgoals = (List.hd spfl).open_subgoals;
                     goal = gl;
                     ref = Some(r,spfl) }))
            (* if the evar change does not affect the goal, leave the
@@ -570,21 +608,6 @@ let tactic_list_tactic tac gls =
 
 
 
-(* solve_subgoal :
-     (evar_map ref * goal list * validation -> 
-         evar_map ref * goal list * validation) -> 
-      (proof_tree sigma -> proof_tree sigma)
-   solve_subgoal tac pf_sigma applies the tactic tac at the nth subgoal of
-   pf_sigma *)
-let solve_subgoal tacl pf_sigma =
-  let (sigr,pf) = unpackage pf_sigma in
-  let gl,p = frontier pf in
-  let r = tacl (sigr,gl,p) in
-  let (sigr,gll,pl) =
-    if !sigr == pf_sigma.sigma then r
-    else then_tac norm_evar_tac r in
-  repackage sigr (pl (List.map leaf gll))
-
 (* The type of proof-trees state and a few utilities 
    A proof-tree state is built from a proof-tree, a set of global
    constraints, and a stack which allows to navigate inside the
@@ -631,9 +654,9 @@ let descend n p =
                        let pf'       = List.hd pfl' in
                        let spfl      = left@(pf'::right) in
                        let newstatus = and_status (List.map pf_status spfl) in
-                       { status   = newstatus;
-			 goal     = p.goal;
-			 ref      = Some(r,spfl) }
+                       { open_subgoals = newstatus;
+			 goal          = p.goal;
+			 ref           = Some(r,spfl) }
                      else 
 		       error "descend: validation"))
 	     | _ -> assert false)
@@ -662,17 +685,23 @@ let traverse n pts = match n with
         tpfsigma = pts.tpfsigma;
         tstack = (n,v):: pts.tstack }
 
-let change_constraints_pftreestate newgc pts = 
-  { tpf = pts.tpf; tpfsigma = newgc; tstack = pts.tstack }
+let change_constraints_pftreestate newgc pts = { pts with tpfsigma = newgc }
+
+let app_tac sigr tac p =
+  let (gll,v) = tac {it=p.goal;sigma= !sigr} in
+  sigr := gll.sigma;
+  v (List.map leaf gll.it)
 
 (* solve the nth subgoal with tactic tac *)
 let solve_nth_pftreestate n tac pts =
- let rslts =
-   solve_subgoal (theni_tac n tac) {it = pts.tpf;sigma = pts.tpfsigma}
- in
- { tpf      = rslts.it;
-   tpfsigma = rslts.sigma;
-   tstack   = pts.tstack }
+  let sigr = ref pts.tpfsigma in
+  let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in
+  let tpf'' =
+    if !sigr == pts.tpfsigma then tpf'
+    else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in
+  { tpf      = tpf'';
+    tpfsigma = !sigr;
+    tstack   = pts.tstack }
 
 let solve_pftreestate = solve_nth_pftreestate 1
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 2fa0b178c..c0d047edb 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -52,6 +52,16 @@ val unTAC : tactic -> goal sigma -> proof_tree sigma
 
 val local_Constraints : tactic
 
+(* [frontier_map f n p] applies f on the n-th open subgoal of p and
+   rebuilds proof-tree.
+   n=1 for first goal, n negative counts from the right *)
+val frontier_map :
+  (proof_tree -> proof_tree) -> int -> proof_tree -> proof_tree
+
+(* [frontier_mapi f p] applies (f i) on the i-th open subgoal of p. *)
+val frontier_mapi :
+  (int -> proof_tree -> proof_tree) -> proof_tree -> proof_tree
+
 (*s Tacticals. *)
 
 (* [tclIDTAC] is the identity tactic *)