module Refiner

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

6 files changed, 688 insertions, 9 deletions

diff --git a/.depend b/.depend
index 27f9cef6f2..a44211446a 100644
--- a/.depend
+++ b/.depend
@@ -54,7 +54,7 @@ parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi
 proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi proofs/proof_trees.cmi \
     kernel/sign.cmi kernel/term.cmi 
 proofs/pfedit.cmi: library/declare.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    kernel/sign.cmi 
+    proofs/refiner.cmi kernel/sign.cmi 
 proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
     lib/util.cmi 
@@ -253,11 +253,13 @@ proofs/proof_trees.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \
     kernel/names.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \
     lib/util.cmx proofs/proof_trees.cmi 
 proofs/refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
-    proofs/logic.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \
-    lib/stamps.cmi kernel/term.cmi lib/util.cmi proofs/refiner.cmi 
+    kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
+    lib/util.cmi proofs/refiner.cmi 
 proofs/refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
-    proofs/logic.cmx lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx \
-    lib/stamps.cmx kernel/term.cmx lib/util.cmx proofs/refiner.cmi 
+    kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \
+    lib/util.cmx proofs/refiner.cmi 
 toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \
     toplevel/errors.cmi 
 toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \
diff --git a/lib/util.ml b/lib/util.ml
index 440acd6ba2..0f900ff923 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -127,6 +127,25 @@ let list_except x l = List.filter (fun y -> not (x = y)) l
 
 let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
 
+let list_map_i f = 
+  let rec map_i_rec i = function
+    | [] -> [] 
+    | x::l -> let v = f i x in v::map_i_rec (i+1) l
+  in 
+  map_i_rec
+
+let rec list_sep_last = function
+  | [] -> failwith "sep_last"
+  | hd::[] -> (hd,[])
+  | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
+
+let list_try_find_i f = 
+  let rec try_find_f n = function
+    | [] -> failwith "try_find_i"
+    | h::t -> try f n h with Failure _ -> try_find_f (n+1) t
+  in 
+  try_find_f
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index ef56afeb27..7998dde2a2 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -41,6 +41,9 @@ val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
 val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+val list_sep_last : 'a list -> 'a * 'a list
+val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 
 (*s Arrays. *)
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6c5cadd837..2473af0c5b 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,6 +6,7 @@ open Pp
 open Sign
 open Declare
 open Proof_trees
+open Refiner
 (*i*)
 
 val proof_prompt : unit -> string
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 4bd5836266..89aa184274 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -9,6 +9,8 @@ open Term
 open Sign
 open Evd
 open Environ
+open Reduction
+open Instantiate
 open Proof_trees
 open Logic
 
@@ -19,9 +21,6 @@ type 'a sigma = {
 type validation = (proof_tree list -> proof_tree)
 type tactic = goal sigma -> (goal list sigma * validation)
 type transformation_tactic = proof_tree -> (goal list * validation)
-type validation_list = proof_tree list -> proof_tree list
-
-type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
 
 let hypotheses gl = gl.evar_env
 let conclusion gl = gl.evar_concl
@@ -189,6 +188,23 @@ let refiner = function
                subproof = None;
                ref = Some(r,[pf]) })))
 
+
+let context ctxt = refiner (Context ctxt)
+let vernac_tactic texp = refiner (Tactic texp)
+
+(* hide_tactic s tac pr registers a tactic s under the name s *)
+
+let hide_tactic s tac =
+  add_tactic s tac;
+  (fun args -> vernac_tactic(s,args))
+
+(* overwriting_register_tactic s tac pr registers a tactic s under the
+   name s even if a tactic of the same name is already registered *)
+
+let overwrite_hidden_tactic s tac =
+  overwriting_add_tactic s tac;
+  (fun args -> vernac_tactic(s,args))
+
 (* rc_of_pfsigma : proof sigma -> readable_constraints *)
 let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
 
@@ -247,3 +263,565 @@ let extract_open_proof sign pf =
   let pfterm = proof_extractor (gLOB sign) pf in
   (pfterm, List.rev !open_obligations)
   
+(* extracts a constr from a proof, and raises an error if the proof is
+   incomplete *)
+
+let extract_proof sign pf =
+  match extract_open_proof sign pf with
+    | t,[] -> t
+    | _ -> errorlabstrm "extract_proof"
+	  [< 'sTR "Attempt to save an incomplete proof" >]
+
+(* whd_evar goes through existential variables when they are defined *)
+
+let rec whd_evar env sigma k = 
+  let (ev,_) = destEvar k in
+  if Evd.is_defined sigma ev then 
+    whd_evar env sigma (existential_value sigma k)
+  else 
+    k
+
+(* expanses every existential constant and compute the normal form
+   through beta iota reduction *)
+
+let rec expand_evars env sigma c = 
+  nf_betaiota env sigma (strong whd_evar env sigma c)
+
+
+(*********************)
+(*   Tacticals       *)
+(*********************)
+
+(* unTAC : tactic -> goal sigma -> proof sigma *)
+
+let unTAC tac g =
+  let (gl_sigma,v) = tac g in 
+  { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma }
+
+let unpackage glsig = (ref (glsig.sigma)),glsig.it
+
+let repackage r v = {it=v;sigma = !r}
+
+let apply_sig_tac r tac g =
+  let glsigma,v = tac (repackage r g) in 
+  r := glsigma.sigma;
+  (glsigma.it,v)
+
+(* the identity tactic *)
+
+let tclIDTAC gls = 
+  { it = [gls.it]; sigma = gls.sigma },
+  (function 
+     | [pf] -> pf 
+     | _ -> anomalylabstrm "Refiner.tclIDTAC"
+	   [< 'sTR "tclIDTAC validation is applicable only to"; 'sPC;
+	      'sTR "a one-proof list" >])
+
+(* solve_subgoal n tac pf_sigma applies the tactic tac at the nth subgoal of
+   pf_sigma *)
+
+let non_existent_goal n =
+  errorlabstrm ("No such goal: "^(string_of_int n))
+    [< 'sTR"Trying to apply a tactic to a non existent goal" >]
+
+let solve_subgoal n tac pf_sigma =
+  let (sigr,pf) = unpackage pf_sigma in
+  let gl,p = frontier pf in
+  if gl = [] then errorlabstrm "solve_subgoal" [< 'sTR"No more subgoals.">];
+  if List.length gl < n then non_existent_goal n;
+  let tac2 i = if i = n then tac else tclIDTAC in
+  let gll,pl = 
+    List.split (list_map_i (fun n -> apply_sig_tac sigr (tac2 n)) 1 gl)
+  in 
+  repackage sigr (compose p (mapshape (List.map List.length gll) pl) 
+                    (List.map leaf (List.flatten gll)))
+
+(* tclTHEN tac1 tac2 gls applies the tactic tac1 to gls and applies tac2 to
+   every resulting subgoals *)
+
+let tclTHEN (tac1:tactic) (tac2:tactic) (gls:goal sigma) =
+  let (sigr,g) = unpackage gls in
+  let gl,p = apply_sig_tac sigr tac1 g in
+  let gll,pl = List.split(List.map (apply_sig_tac sigr tac2) gl) in
+  (repackage sigr (List.flatten gll), 
+   compose p (mapshape(List.map List.length gll)pl))
+
+(* 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:tactic) (tac2:(int -> tactic)) n (gls:goal sigma) =
+  let (sigr,g) = unpackage gls in
+  let gl,p = apply_sig_tac sigr tac1 g in
+  let gll,pl = 
+    List.split (list_map_i (fun k -> apply_sig_tac sigr (tac2 k)) n gl) 
+  in
+  (repackage sigr (List.flatten gll), 
+   compose p (mapshape(List.map List.length gll)pl))
+
+(* 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:tactic) (tac2l:tactic list) (gls:goal sigma) =
+  let (sigr,g) = unpackage gls in
+  let gl,p = apply_sig_tac sigr tac1 g  in
+  let tac2gl = 
+    try List.combine tac2l gl
+    with Invalid_argument _ -> errorlabstrm "Refiner.tclTHENS"
+        [<'sTR "Wrong number of tactics.">]
+  in
+  let gll,pl = 
+    List.split (List.map (fun (tac2,g) -> apply_sig_tac sigr tac2 g) tac2gl)
+  in
+  (repackage sigr (List.flatten gll), 
+   compose p (mapshape(List.map List.length gll)pl))
+
+(* 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) =
+  let (sigr,g) = unpackage gls in
+  let gl,p = apply_sig_tac sigr tac1 g in 
+  if List.length gl = 0 then
+    errorlabstrm "Refiner.tclTHENL" [< 'sTR"No resulting subgoal.">];
+  let g,rest = list_sep_last gl in
+  let tac2l = (List.map (fun _ -> tclIDTAC) rest)@[tac2] in
+  let tac2gl = 
+    try List.combine tac2l gl
+    with Invalid_argument _ -> errorlabstrm "Refiner.tclTHENL"
+        [<'sTR "Wrong number of tactics.">]
+  in
+  let gll,pl = 
+    List.split (List.map (fun (tac2,g) -> apply_sig_tac sigr tac2 g) tac2gl)
+  in
+  (repackage sigr (List.flatten gll), 
+   compose p (mapshape(List.map List.length gll)pl))
+
+(* Completes by Idtac if there is not tactic enough for tac1;[t1|...|tn] *)
+
+let idtac_completion lac gl=
+  let nl = ref lac
+  and lthlac = List.length lac
+  and lthgl = List.length gl in
+  if lthlac > lthgl then failwith "idtac_completion";
+  for i = 0 to lthgl-lthlac-1 do
+    nl := !nl @ [tclIDTAC]
+  done;
+  !nl
+
+(* Same as tclTHENS but completes with Idtac if the number resulting
+  subgoals is strictly less than n *)
+
+let tclTHENSI (tac1:tactic) (tac2l:tactic list) (gls:goal sigma) =
+  let (sigr,g) = unpackage gls in
+  let gl,p = apply_sig_tac sigr tac1 g  in
+  let ntac2l=
+    try (idtac_completion tac2l gl)
+    with
+	Failure "idtac_completion" ->
+          errorlabstrm "Refiner.tclTHENSI" 
+	    [<'sTR "Too many tactics for the generated subgoals.">]
+  in
+  let tac2gl = List.combine ntac2l gl in
+  let gll,pl = 
+    List.split (List.map (fun (tac2,g) -> apply_sig_tac sigr tac2 g) tac2gl)
+  in
+  (repackage sigr (List.flatten gll), 
+   compose p (mapshape(List.map List.length gll)pl))
+
+(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
+   the goal unchanged *)
+
+let tclPROGRESS (tac:tactic) (ptree : goal sigma) =
+  let rslt = tac ptree in 
+  if (List.length (fst rslt).it) = 1 then begin
+    let subgoal = List.hd (fst rslt).it in 
+    if (hypotheses subgoal) = (hypotheses ptree.it) &&
+       (conclusion subgoal) = (conclusion ptree.it) &&
+       (subgoal.evar_info = ptree.it.evar_info) &&
+       ts_eq ptree.sigma (fst rslt).sigma then
+         errorlabstrm "Refiner.PROGRESS" [< 'sTR"Failed to progress.">];
+    rslt
+  end else 
+    rslt
+
+(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails 
+   if tac leaves the goal unchanged, possibly modifying sigma *)
+
+let tclWEAK_PROGRESS (tac:tactic) (ptree : goal sigma) =
+  let rslt = tac ptree in 
+  if (List.length (fst rslt).it) = 1 then begin
+    let subgoal = List.hd (fst rslt).it in 
+    if (hypotheses subgoal) = (hypotheses ptree.it) &&
+       eq_constr (conclusion subgoal) (conclusion ptree.it) &&
+       (subgoal.evar_info = ptree.it.evar_info) then
+         errorlabstrm "Refiner.tclWEAK_PROGRESS" 
+	   [< 'sTR"Failed to progress.">];
+    rslt
+  end else 
+    rslt
+
+(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
+   one of them being identical to the original goal *)
+
+let tclNOTSAMEGOAL (tac:tactic) (ptree : goal sigma) =
+  let rslt = tac ptree in 
+  let gls = (fst rslt).it in 
+  let same_goal subgoal = 
+    (hypotheses subgoal) = (hypotheses ptree.it) &
+    eq_constr (conclusion subgoal) (conclusion ptree.it) &
+    (subgoal.evar_info = ptree.it.evar_info)
+  in 
+  if List.exists same_goal gls then 
+    errorlabstrm "Refiner.tclNOTSAMEGOAL" 
+      [< 'sTR"Tactic generated a subgoal identical to the original goal.">];
+  rslt
+
+(* ORELSE f1 f2 tries to apply f1 and if it fails, applies f2 *)
+
+let tclORELSE (f1:tactic) (f2:tactic) (g:goal sigma) =
+  try 
+    (tclPROGRESS f1) g
+  with UserError _ | Stdpp.Exc_located(_,UserError _) -> 
+    f2 g 
+
+(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
+
+let tclTRY (f:tactic) = (tclORELSE f tclIDTAC)
+
+let tclTHENTRY (f:tactic) (g:tactic) = (tclTHEN f (tclTRY g))
+
+let tclCOMPLETE (tac:tactic) goal =
+  let achievement = tac goal in 
+  if (fst achievement).it <> [] then
+    errorlabstrm "Refiner.COMPLETE" [< 'sTR "Proof is not complete" >];
+  achievement
+
+(* Beware: call by need of CAML, g is needed *)
+
+let rec tclREPEAT = fun t g ->
+  (tclORELSE (tclTHEN t (tclREPEAT t)) tclIDTAC) g
+
+(*Try the first tactic that does not fail in a list of tactics*)
+
+let rec tclFIRST = fun tacl g ->
+  match tacl with
+    | [] -> errorlabstrm "Refiner.tclFIRST" [< 'sTR"No applicable tactic.">]
+    |  t::rest -> (try t g with UserError _ -> tclFIRST rest g)
+
+(*Try the first thats solves the current goal*)
+
+let tclSOLVE=fun tacl gls ->
+  let (sigr,gl)=unpackage gls in
+  let rec solve=function
+    | [] -> errorlabstrm "Refiner.tclSOLVE" [< 'sTR"Cannot solve the goal.">]
+    | e::tail ->
+        (try
+           let (ngl,p)=apply_sig_tac sigr e gl in
+           if ngl = [] then
+             (repackage sigr ngl,p)
+           else
+             solve tail
+         with UserError _ -> 
+	   solve tail)
+  in
+  solve tacl
+  
+let tclTRY t = (tclORELSE t tclIDTAC)
+		 
+let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
+			   
+let (tclFAIL:tactic) = 
+  fun _ -> errorlabstrm "Refiner.tclFAIL" [< 'sTR"Failtac always fails.">]
+
+(* Iteration tactical *)
+
+let tclDO n t = 
+  let rec dorec k = 
+    if k < 0 then errorlabstrm "Refiner.tclDO"
+      [<'sTR"Wrong argument : Do needs a positive integer.">];
+    if k = 0 then tclIDTAC
+    else if k = 1 then t else (tclTHEN t (dorec (k-1)))
+  in 
+  dorec n 
+
+
+(*s Tactics handling a list of goals. *)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+(* first_goal : goal list sigma -> goal sigma *)
+
+let first_goal gls = 
+  let gl = gls.it and sig_0 = gls.sigma in 
+  if gl = [] then error "first_goal"; 
+  { it = List.hd gl; sigma = sig_0 }
+
+(* goal_goal_list : goal sigma -> goal list sigma *)
+
+let goal_goal_list gls = 
+  let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 }
+
+(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
+
+let apply_tac_list tac glls = 
+  let (sigr,lg) = unpackage glls in
+  match lg with 
+    | g1::rest ->
+	let (gl,p) = apply_sig_tac sigr tac g1 in
+	let n = List.length gl in 
+        repackage sigr (gl@rest), 
+        (function pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest)
+    | _ -> error "apply_tac_list"
+	  
+let then_tactic_list tacl1 tacl2 glls = 
+  let (sigr,gl) = unpackage glls in
+  let gll1,pl1 = apply_sig_tac sigr tacl1 gl in
+  let gll2,pl2 = apply_sig_tac sigr tacl2 gll1 in
+  (repackage sigr gll2, compose pl1 pl2)
+
+(* Transform a tactic_list into a tactic *)
+
+let tactic_list_tactic tac gls = 
+  let glit = gls.it 
+  and glsig = gls.sigma in 
+  let (glres,vl) = tac {it=[glit];sigma=glsig} in 
+  (glres, 
+   fun pfl -> match (vl pfl) with [p] -> p | _ -> error "tactic_list_tactic")
+
+(* Functions working on goal list for correct backtracking in Prolog *)
+
+let tclFIRSTLIST = tclFIRST
+let tclIDTAC_list gls = (gls, fun x -> x)
+
+
+(* 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
+   proof-tree remembering how to rebuild the global proof-tree
+   possibly after modification of one of the focused children proof-tree.
+   The number in the stack corresponds to 
+   either the selected subtree and the validation is a function from a
+   proof-tree list consisting only of one proof-tree to the global
+   proof-tree 
+   or -1 when the move is done behind a registered tactic in which
+   case the validation corresponds to a constant function giving back 
+   the original proof-tree. *)
+
+type pftreestate = {
+  tpf      : proof_tree ;
+  tpfsigma : global_constraints;
+  tstack   : (int * validation) list }
+
+let proof_of_pftreestate pts = pts.tpf
+let is_top_pftreestate pts = pts.tstack = [] 
+let cursor_of_pftreestate pts = List.map fst pts.tstack
+let evc_of_pftreestate pts = pts.tpfsigma
+
+let top_goal_of_pftreestate pts = 
+  { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
+
+let nth_goal_of_pftreestate n pts =
+  let goals = fst (frontier pts.tpf) in
+  try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
+  with Failure "nth" -> non_existent_goal n
+
+let descend n p =
+  match p.ref with
+    | None        -> error "It is a leaf."
+    | Some(r,pfl) ->
+    	if List.length pfl >= n then
+	  (match list_chop (n-1) pfl with 
+	     | left,(wanted::right) ->
+		 (wanted,
+		  (fun pfl' ->
+                     if (List.length pfl' = 1) 
+		       & (List.hd pfl').goal = wanted.goal 
+		     then
+                       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;
+			 subproof = p.subproof;
+			 ref      = Some(r,spfl) }
+                     else 
+		       error "descend: validation"))
+	     | _ -> assert false)
+    	else 
+	  error "Too few subproofs"
+
+let traverse n pts = match n with 
+  | 0 -> (* go to the parent *)
+      (match  pts.tstack with
+	 | [] -> error "traverse: no ancestors"
+	 | (_,v)::tl ->
+	     { tpf = v [pts.tpf];
+	       tstack = tl;
+	       tpfsigma = pts.tpfsigma })
+  | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
+      (match pts.tpf.subproof with
+	 | None -> error "traverse: not a tactic-node"
+	 | Some spf ->
+	     let v = (fun pfl -> pts.tpf) in 
+	     { tpf = spf;
+               tstack = (-1,v)::pts.tstack;
+               tpfsigma = pts.tpfsigma })
+  | n -> (* when n>0, go to the nth child *)
+      let (npf,v) = descend n pts.tpf in 
+      { tpf = npf;
+        tpfsigma = pts.tpfsigma;
+        tstack = (n,v):: pts.tstack }
+
+let change_constraints_pftreestate newgc pts = 
+  { tpf = pts.tpf; tpfsigma = newgc; tstack = pts.tstack }
+
+(* solve the nth subgoal with tactic tac *)
+let solve_nth_pftreestate n tac pts =
+  let pf = pts.tpf in
+  let rslts = solve_subgoal n tac {it = pts.tpf;sigma = pts.tpfsigma} in
+  { tpf      = rslts.it;
+    tpfsigma = rslts.sigma;
+    tstack   = pts.tstack }
+
+let solve_pftreestate = solve_nth_pftreestate 1
+
+(* This function implements a poor man's undo at the current goal.
+   This is a gross approximation as it does not attempt to clean correctly
+   the global constraints given in tpfsigma. *)
+
+let weak_undo_pftreestate pts =
+  let pf = leaf pts.tpf.goal in
+  { tpf = pf;
+    tpfsigma = pts.tpfsigma;
+    tstack = pts.tstack }
+
+(* Gives a new proof (a leaf) of a goal gl *)
+let mk_pftreestate g =
+  { tpf      = leaf g;
+    tstack   = [];
+    tpfsigma = ts_mk Evd.empty }
+
+(* Extracts a constr from a proof-tree state ; raises an error if the
+   proof is not complete or the state does not correspond to the head
+   of the proof-tree *)
+
+let extract_pftreestate pts =
+  if pts.tstack <> [] then
+    errorlabstrm "extract_pftreestate"
+      [< 'sTR"Cannot extract from a proof-tree in which we have descended;" ;
+         'sPC; 'sTR"Please ascend to the root" >];
+  let env = pts.tpf.goal.evar_env in
+  let hyps = get_globals (Environ.context env) in
+  strong whd_betadeltatiota env (ts_it pts.tpfsigma)
+    (extract_proof hyps pts.tpf)
+
+
+(* Focus on the first leaf proof in a proof-tree state *)
+
+let rec first_unproven pts =
+  let pf = (proof_of_pftreestate pts) in 
+  if is_complete_proof pf then
+    errorlabstrm "first_unproven" [< 'sTR"No unproven subgoals" >];
+  if is_leaf_proof pf then
+    pts
+  else
+    let childnum =
+      list_try_find_i 
+	(fun n pf -> 
+	   if not(is_complete_proof pf) then n else failwith "caught")
+	1 (children_of_proof pf)
+    in 
+    first_unproven (traverse childnum pts)
+
+(* Focus on the last leaf proof in a proof-tree state *)
+
+let rec last_unproven pts =
+  let pf = proof_of_pftreestate pts in 
+  if is_complete_proof pf then
+    errorlabstrm "last_unproven" [< 'sTR"No unproven subgoals" >];
+  if is_leaf_proof pf then
+    pts
+  else 
+    let children = (children_of_proof pf) in
+    let nchilds = List.length children in
+    let childnum =
+      list_try_find_i 
+        (fun n pf ->
+           if not(is_complete_proof pf) then n else failwith "caught")
+        1 (List.rev children)
+    in 
+    last_unproven (traverse (nchilds-childnum+1) pts)
+      
+let rec nth_unproven n pts =
+  let pf = proof_of_pftreestate pts in 
+  if is_complete_proof pf then
+    errorlabstrm "nth_unproven" [< 'sTR"No unproven subgoals" >];
+  if is_leaf_proof pf then
+    if n = 1 then 
+      pts 
+    else
+      errorlabstrm "nth_unproven" [< 'sTR"Not enough unproven subgoals" >]
+  else 
+    let children = children_of_proof pf in
+    let rec process i k = function
+      | [] -> 
+	  errorlabstrm "nth_unproven" [< 'sTR"Not enough unproven subgoals" >]
+      | pf1::rest -> 
+	  let k1 = nb_unsolved_goals pf1 in 
+	  if k1 < k then 
+	    process (i+1) (k-k1) rest
+	  else 
+	    nth_unproven k (traverse i pts)
+    in 
+    process 1 n children
+
+let rec node_prev_unproven loc pts =
+  let pf = proof_of_pftreestate pts in 
+  match cursor_of_pftreestate pts with
+    | [] -> last_unproven pts
+    | n::l ->
+	if is_complete_proof pf or loc = 1 then
+          node_prev_unproven n (traverse 0 pts)
+	else 
+	  let child = List.nth (children_of_proof pf) (loc - 2) in
+	  if is_complete_proof child then
+	    node_prev_unproven (loc - 1) pts
+	  else 
+	    first_unproven (traverse (loc - 1) pts)
+
+let rec node_next_unproven loc pts =
+  let pf = proof_of_pftreestate pts in 
+  match cursor_of_pftreestate pts with
+    | [] -> first_unproven pts
+    | n::l ->
+	if is_complete_proof pf ||
+           loc = (List.length (children_of_proof pf)) then
+             node_next_unproven n (traverse 0 pts)
+	else if is_complete_proof (List.nth (children_of_proof pf) loc) then
+	  node_next_unproven (loc + 1) pts
+	else 
+	  last_unproven(traverse (loc + 1) pts)
+
+let next_unproven pts =
+  let pf = proof_of_pftreestate pts in 
+  if is_leaf_proof pf then
+    match cursor_of_pftreestate pts with
+      | [] -> error "next_unproven"
+      | n::_ -> node_next_unproven n (traverse 0 pts)
+  else 
+    node_next_unproven (List.length (children_of_proof pf)) pts
+
+let prev_unproven pts =
+  let pf = proof_of_pftreestate pts in 
+  if is_leaf_proof pf then
+    match cursor_of_pftreestate pts with
+      | [] -> error "prev_unproven"
+      | n::_ -> node_prev_unproven n (traverse 0 pts)
+  else 
+    node_prev_unproven 1 pts
+
+let rec top_of_tree pts = 
+  if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 871c43a3ee..def87ba038 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -38,5 +38,81 @@ val overwrite_hidden_tactic :
   string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
 
 val refiner : rule -> tactic
+val context : ctxtty -> tactic
+val vernac_tactic : tactic_expression -> tactic
+val frontier : transformation_tactic
+val list_pf : proof_tree -> goal list
+val unTAC : tactic -> goal sigma -> proof_tree sigma
 
-val extract_open_proof : context -> proof_tree -> constr * (int * constr) list
+val extract_open_proof : 
+  typed_type signature -> proof_tree -> constr * (int * constr) list
+
+
+(*s Tacticals. *)
+
+val tclIDTAC         : tactic
+val tclORELSE        : tactic -> tactic -> tactic
+val tclTHEN          : tactic -> tactic -> tactic
+val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
+val tclTHENL         : tactic -> tactic -> tactic
+val tclTHENS         : tactic -> tactic list -> tactic
+val tclTHENSI        : tactic -> tactic list -> tactic
+val tclREPEAT        : tactic -> tactic
+val tclFIRST         : tactic list -> tactic
+val tclSOLVE         : tactic list -> tactic
+val tclTRY           : tactic -> tactic
+val tclTHENTRY       : tactic -> tactic -> tactic
+val tclCOMPLETE      : tactic -> tactic
+val tclAT_LEAST_ONCE : tactic -> tactic
+val tclFAIL          : tactic
+val tclDO            : int -> tactic -> tactic
+val tclPROGRESS      : tactic -> tactic
+val tclWEAK_PROGRESS : tactic -> tactic
+val tclNOTSAMEGOAL   : tactic -> tactic
+
+
+(*s Tactics handling a list of goals. *)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+val tclFIRSTLIST       : tactic_list list -> tactic_list
+val tclIDTAC_list      : tactic_list
+val first_goal         : 'a list sigma -> 'a sigma
+val apply_tac_list     : tactic -> tactic_list
+val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
+val tactic_list_tactic : tactic_list -> tactic
+val goal_goal_list     : 'a sigma -> 'a list sigma
+
+
+(*s Functions for handling the state of the proof editor. *)
+
+type pftreestate
+
+val proof_of_pftreestate : pftreestate -> proof_tree
+val cursor_of_pftreestate : pftreestate -> int list
+val is_top_pftreestate : pftreestate -> bool
+val evc_of_pftreestate : pftreestate -> global_constraints
+val top_goal_of_pftreestate : pftreestate -> goal sigma
+val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
+
+val traverse : int -> pftreestate -> pftreestate
+val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
+val solve_pftreestate : tactic -> pftreestate -> pftreestate
+(* a weak version of logical undoing, that is really correct only *)
+(* if there are no existential variables.                         *)
+val weak_undo_pftreestate : pftreestate -> pftreestate
+
+val mk_pftreestate : goal -> pftreestate
+val extract_pftreestate : pftreestate -> constr
+val first_unproven : pftreestate -> pftreestate
+val last_unproven : pftreestate -> pftreestate
+val nth_unproven : int -> pftreestate -> pftreestate
+val node_prev_unproven : int -> pftreestate -> pftreestate
+val node_next_unproven : int -> pftreestate -> pftreestate
+val next_unproven : pftreestate -> pftreestate
+val prev_unproven : pftreestate -> pftreestate
+val top_of_tree : pftreestate -> pftreestate
+val change_constraints_pftreestate 
+  : global_constraints -> pftreestate -> pftreestate