Started to fix the declarative proof mode (C-zar).

Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported).
However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc.

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

9 files changed, 157 insertions, 65 deletions

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 232edda0fd..af6aa4bf59 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -66,7 +66,7 @@ type command_mode =
   | Mode_none
 
 let mode_of_pftreestate pts =
-  (* spiwack: it was "top_goal_..." but this should be fine *)
+  (* spiwack: it used to be "top_goal_..." but this should be fine *)
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
   let goal = List.hd goals in
     if info.get (Goal.V82.extra sigma goal) = None then
@@ -96,10 +96,25 @@ let get_stack pts =
   let info = get_info sigma (List.hd goals) in
   info.pm_stack
 
+
+let proof_focus = Proof.new_focus_kind ()
+let proof_cond = Proof.no_cond proof_focus
+
+let focus p =
+  let inf = get_stack p in
+  Proof.focus proof_cond inf 1 p
+
+let unfocus = Proof.unfocus proof_focus
+
+let maximal_unfocus = Proof_global.maximal_unfocus proof_focus
+
 let get_top_stack pts =
-  let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
-  let info = get_info sigma gl in
-  info.pm_stack
+  try
+    Proof.get_at_focus proof_focus pts
+  with Proof.NoSuchFocus ->
+    let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
+    let info = get_info sigma gl in
+    info.pm_stack
 
 let get_last env =
   try
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 72c46c7e7d..4e636598f9 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -70,3 +70,9 @@ val get_stack : Proof.proof -> stack_info list
 val get_top_stack : Proof.proof -> stack_info list
 
 val get_last:  Environ.env -> identifier
+
+val focus : Proof.proof -> unit
+
+val unfocus : Proof.proof -> unit
+
+val maximal_unfocus : Proof.proof -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index cee4d7271d..549b1f1465 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -111,17 +111,15 @@ let assert_postpone id t =
 
 (* start a proof *)
 
-let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
 
 let start_proof_tac gls=
   let info={pm_stack=[]} in
   tcl_change_info info gls
 
 let go_to_proof_mode () =
-  Pfedit.by start_proof_tac  ;
+  Pfedit.by start_proof_tac;
   let p = Proof_global.give_me_the_proof () in
-  Proof.focus proof_cond 1 p
+  Decl_mode.focus p
 
 (* closing gaps *)
 
@@ -154,12 +152,14 @@ let mark_rule_as_done = function
 
 (* post-instruction focus management *)
 
+(* spiwack: This used to fail if there was no focusing command
+   above, but I don't think it ever happened. I hope it doesn't mess
+   things up*)
 let goto_current_focus pts = 
-  Proof.unfocus proof_focus pts
+  Decl_mode.maximal_unfocus pts
 
 let goto_current_focus_or_top pts =
-  try goto_current_focus pts
-  with Util.UserError _ -> ()
+  goto_current_focus pts
 
 (* return *)
 
@@ -172,6 +172,7 @@ let close_tactic_mode pts =
       goto_current_focus pts2
 
 let return_from_tactic_mode () =
+  (* arnaud: la commande return ne fonctionne pas *)
   Util.anomaly "Todo: Decl_proof_instr.return_from_tactic_mode"
 
 (* end proof/claim *)
@@ -180,7 +181,12 @@ let close_block bt pts =
     if Proof.no_focused_goal pts then
       goto_current_focus pts
     else
-      let stack =get_stack pts in
+      let stack =
+	if Proof.is_done pts then
+	  get_top_stack pts
+	else
+	  get_stack pts 
+      in
       match bt,stack with
 	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
 	  (goto_current_focus pts)
@@ -197,7 +203,7 @@ let close_block bt pts =
 	      | ET_Induction ->  error "\"end induction\" expected."
 	  end
       | _,_ -> anomaly "Lonely suppose on stack."
-  
+
 
 (* utility for suppose / suppose it is *)
 
@@ -577,8 +583,8 @@ let instr_claim _thus st gls0 =
   let ninfo1 = {pm_stack=
       (if _thus then Focus_claim else Claim)::info.pm_stack} in
     tclTHENS (assert_postpone id st.st_it)
-      [tcl_change_info ninfo1;
-       thus_tac] gls0
+      [thus_tac;
+       tcl_change_info ninfo1] gls0
 
 (* tactics for assume *)
 
@@ -1294,12 +1300,9 @@ let understand_my_constr c gls =
   let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc ->  map_glob_constr frob rc in
     Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
 
-let set_refine,my_refine =
-let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in
-((fun tac -> refine:= tac),
-(fun c gls -> 
-   let oc = understand_my_constr c gls in
-     !refine oc gls))
+let my_refine c gls =
+  let oc = understand_my_constr c gls in
+  Refine.refine oc gls
 
 (* end focus/claim *)
 
@@ -1438,12 +1441,16 @@ let rec postprocess pts instr =
     | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> ()
     | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _
-    | Pescape -> Proof.focus proof_cond 1 pts
+    | Pescape -> Decl_mode.focus pts
     | Pend (B_elim ET_Induction) ->
   	begin
 	  let pfterm = List.hd (Proof.partial_proof pts) in
 	  let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in
-	  let env =  Goal.V82.env sigma (List.hd gls) in
+	  let env =  try
+		       Goal.V82.env sigma (List.hd gls)
+	             with Failure "hd" ->
+		       Global.env ()
+	  in
 	    try
 	      Inductiveops.control_only_guard env pfterm;
 	      goto_current_focus_or_top pts
@@ -1469,7 +1476,10 @@ let do_instr raw_instr pts =
 	interp_proof_instr (get_its_info gl) sigma env glob_instr in
       Pfedit.by (tclTHEN (eval_instr instr) clean_tmp)
     else () end;
-  postprocess pts raw_instr.instr
+  postprocess pts raw_instr.instr;
+  (* spiwack: this should restore a compatible semantics with
+     v8.3 where we never stayed focused on 0 goal. *)
+  Decl_mode.maximal_unfocus pts
 
 let proof_instr raw_instr =
   let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index 0a2ab571ff..b27939b3ca 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -109,5 +109,3 @@ val init_tree:
      (int option * Declarations.recarg Rtree.t) array ->
      (Names.Idset.t * Decl_mode.split_tree) option) ->
     Decl_mode.split_tree
-
-val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 44f1cce723..b932e95f9a 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -31,8 +31,13 @@
 
 open Term
 
-type focus_kind = int
-type focus_condition = focus_kind -> Proofview.proofview -> bool
+type _focus_kind = int
+type 'a focus_kind = _focus_kind
+type focus_info = Obj.t
+type _focus_condition = 
+    (_focus_kind -> Proofview.proofview -> bool) *
+    (_focus_kind -> focus_info -> focus_info)
+type 'a focus_condition = _focus_condition
 
 let next_kind = ref 0
 let new_focus_kind () =
@@ -40,6 +45,13 @@ let new_focus_kind () =
   incr next_kind;
   r
 
+(* Auxiliary function to define conditions:
+   [check kind1 kind2 inf] returns [inf] if [kind1] and [kind2] match.
+   Otherwise it raises [CheckNext] *)
+exception CheckNext
+let check kind1 kind2 inf =
+  if kind1=kind2 then inf else raise CheckNext
+
 (* To be authorized to unfocus one must meet the condition prescribed by
     the action which focused.*)
 (* spiwack: we could consider having a list of authorized focus_kind instead
@@ -47,9 +59,11 @@ let new_focus_kind () =
 (* [no_cond] only checks that the unfocusing command uses the right
     [focus_kind]. *)
 let no_cond k0 k _ = k0 = k
+let no_cond k = no_cond k , check k
 (* [done_cond] checks that the unfocusing command uses the right [focus_kind]
     and that the focused proofview is complete. *)
 let done_cond k0 k p = k0 = k && Proofview.finished p
+let done_cond k = done_cond k , check k
 
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
@@ -58,9 +72,9 @@ type proof_state = {
   (* Current focused proofview *)
   proofview: Proofview.proofview;
   (* History of the focusings, provides information on how
-     to unfocus the proof.
+     to unfocus the proof and the extra information stored while focusing.
      The list is empty when the proof is fully unfocused. *)
-  focus_stack: (focus_condition*Proofview.focus_context) list;
+  focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list;
   (* Extra information which can be freely used to create new behaviours. *)
   intel: Store.t
 }
@@ -94,7 +108,7 @@ let start goals =
   }
 
 let rec unroll_focus pv = function
-  | (_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
+  | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
 
 (* spiwack: a proof is considered completed even if its still focused, if the focus
@@ -126,15 +140,15 @@ let return p =
      of proofs, they are not meant to be exported in the .mli ***)
 
 (* An auxiliary function to push a {!focus_context} on the focus stack. *)
-let push_focus kind context pr =
-  pr.state <- { pr.state with focus_stack = (kind,context)::pr.state.focus_stack }
+let push_focus cond inf context pr =
+  pr.state <- { pr.state with focus_stack = (cond,inf,context)::pr.state.focus_stack }
 
 exception FullyUnfocused
 
 (* An auxiliary function to read the kind of the next focusing step *)
 let cond_of_focus pr =
   match pr.state.focus_stack with
-  | (cond,_)::_ -> cond
+  | (cond,_,_)::_ -> cond
   | _ -> raise FullyUnfocused
 
 (* An auxiliary function to pop and read the last {!Proofview.focus_context} 
@@ -159,16 +173,16 @@ let pop_undo pr =
 
 
 (* This function focuses the proof [pr] between indices [i] and [j] *)
-let _focus cond i j pr =
+let _focus cond inf i j pr =
   let (focused,context) = Proofview.focus i j pr.state.proofview in
-  push_focus cond context pr;
+  push_focus cond inf context pr;
   pr.state <- { pr.state with proofview = focused }
 
 (* This function unfocuses the proof [pr], it raises [FullyUnfocused],
    if the proof is already fully unfocused.
    This function does not care about the condition of the current focus. *)
 let _unfocus pr =
-  let (_,fc) = pop_focus pr in
+  let (_,_,fc) = pop_focus pr in
   pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview }
 
 
@@ -214,9 +228,9 @@ let add_undo effect pr =
 (* Focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
-let focus cond i pr =
+let focus cond inf i pr =
   save pr;
-  _focus cond i i pr
+  _focus cond (Obj.repr inf) i i pr
 
 (* Unfocus command.
    Fails if the proof is not focused. *)
@@ -224,7 +238,7 @@ let unfocus kind pr =
   let starting_point = save_state pr in
   try
     let cond = cond_of_focus pr in
-    if cond kind pr.state.proofview then
+    if fst cond kind pr.state.proofview then
       (_unfocus pr;
        push_undo starting_point pr)
     else
@@ -232,6 +246,21 @@ let unfocus kind pr =
   with FullyUnfocused -> 
     Util.error "This proof is not focused"
 
+let get_at_point kind ((_,get),inf,_) = get kind inf
+exception NoSuchFocus
+exception GetDone of Obj.t
+let get_in_focus_stack kind stack =
+  try
+    List.iter begin fun pt ->
+      try 
+	raise (GetDone (get_at_point kind pt))
+      with CheckNext -> ()
+    end stack;
+    raise NoSuchFocus
+  with GetDone x -> x
+let get_at_focus kind pr =
+  Obj.magic (get_in_focus_stack kind pr.state.focus_stack)
+
 let no_focused_goal p =
   Proofview.finished p.state.proofview
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index ab1c0b8345..bb651dea11 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -64,32 +64,44 @@ val add_undo : (unit -> unit) -> proof -> unit
 
 (*** Focusing actions ***)
 
-(* [focus_kind] is the type used by focusing and unfocusing
+(* ['a focus_kind] is the type used by focusing and unfocusing
     commands to synchronise. Focusing and unfocusing commands use
-    a particular focus_kind, and if they don't match, the unfocusing command
-    will fail. *)
-type focus_kind
-val new_focus_kind : unit -> focus_kind
+    a particular ['a focus_kind], and if they don't match, the unfocusing command
+    will fail.
+    When focusing with an ['a focus_kind], an information of type ['a] is
+    stored at the focusing point. An example use is the "induction" tactic
+    of the declarative mode where sub-tactics must be aware of the current
+    induction argument. *)
+type 'a focus_kind
+val new_focus_kind : unit -> 'a focus_kind
 
 (* To be authorized to unfocus one must meet the condition prescribed by
-    the action which focused.*)
-type focus_condition 
+    the action which focused.
+    Conditions always carry a focus kind, and inherit their type parameter
+    from it.*)
+type 'a focus_condition 
 (* [no_cond] only checks that the unfocusing command uses the right
     [focus_kind]. *)
-val no_cond : focus_kind -> focus_condition
+val no_cond : 'a focus_kind -> 'a focus_condition
 (* [done_cond] checks that the unfocusing command uses the right [focus_kind]
     and that the focused proofview is complete. *)
-val done_cond : focus_kind -> focus_condition
+val done_cond : 'a focus_kind -> 'a focus_condition
 
 (* focus command (focuses on the [i]th subgoal) *)
-(* there could also, easily be a focus-on-a-range tactic, is there 
+(* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
-val focus : focus_condition -> int -> proof -> unit
+val focus : 'a focus_condition -> 'a -> int -> proof -> unit
 
 exception FullyUnfocused
 (* Unfocusing command.
    Raises [FullyUnfocused] if the proof is not focused. *)
-val unfocus : focus_kind -> proof -> unit
+val unfocus : 'a focus_kind -> proof -> unit
+
+(* [get_at_focus k] gets the information stored at the closest focus point
+    of kind [k].
+    Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
+exception NoSuchFocus
+val get_at_focus : 'a focus_kind -> proof -> 'a
 
 (* returns [true] if there is no goal under focus. *)
 val no_focused_goal : proof -> bool
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3e8c71482a..bcd9d6e0d3 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -281,6 +281,21 @@ let close_proof () =
     | Proof.HasUnresolvedEvar ->
 	Util.error "Attempt to save a proof with existential variables still non-instantiated"
 
+
+(**********************************************************)
+(*                                                                                                  *)
+(*                              Utility functions                                          *)
+(*                                                                                                  *)
+(**********************************************************)
+
+let maximal_unfocus k p =
+  begin try while Proof.no_focused_goal p do
+    Proof.unfocus k p
+  done
+  with Util.UserError _ -> (* arnaud: attention à ça si je fini par me décider à mettre une vrai erreur pour Proof.unfocus *)
+    ()
+  end
+
 module V82 = struct
   let get_current_initial_conclusions () =
     let p = give_me_the_proof () in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index a589732046..5f57c25ac5 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -72,18 +72,28 @@ val suspend : unit -> unit
 val resume_last : unit -> unit
 
 val resume : Names.identifier -> unit
-(** @raise NoSuchProof if it doesn't find *)
+(** @raise NoSuchProof if it doesn't find one. *)
 
-(* Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
+(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
    no current proof. *)
 val run_tactic : unit Proofview.tactic -> unit
 
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
+(** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : unit Proofview.tactic -> unit
 
-(* Appends the endline tactic of the current proof to a tactic. *)
+(** Appends the endline tactic of the current proof to a tactic. *)
 val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
 
+(**********************************************************)
+(*                                                                                                  *)
+(*                              Utility functions                                          *)
+(*                                                                                                  *)
+(**********************************************************)
+
+(** [maximal_unfocus k p] unfocuses [p] until [p] has at least a
+    focused goal or that the last focus isn't of kind [k]. *)
+val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit
+
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook)
 end
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f4fc8714be..ccbaa6d306 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -670,7 +670,7 @@ let pop_bullet pr =
 		   b
   | [] -> Util.anomaly "Tried to pop bullet from an empty stack"
 let push_bullet b pr =
-  Proof.focus bullet_cond 1 pr ;
+  Proof.focus bullet_cond () 1 pr ;
   set_bullets (b::get_bullets pr) pr
 
 let put_bullet p bul =
@@ -690,10 +690,7 @@ let vernac_solve n bullet tcom b =
   solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b;
   (* in case a strict subtree was completed,
      go back to the top of the prooftree *)
-  begin try while Proof.no_focused_goal p do
-    Proof.unfocus command_focus p
-  done
-  with Util.UserError _ -> () end;
+  Proof_global.maximal_unfocus command_focus p;
   print_subgoals();
   if !pcoq <> None then (Option.get !pcoq).solve n
  
@@ -1252,8 +1249,8 @@ let vernac_backtrack snum pnum naborts =
 let vernac_focus gln =
   let p = Proof_global.give_me_the_proof () in
   match gln with
-    | None -> Proof.focus focus_command_cond 1 p; print_subgoals ()
-    | Some n -> Proof.focus focus_command_cond n p; print_subgoals ()
+    | None -> Proof.focus focus_command_cond () 1 p; print_subgoals ()
+    | Some n -> Proof.focus focus_command_cond () n p; print_subgoals ()
 
 
   (* Unfocuses one step in the focus stack. *)
@@ -1273,8 +1270,8 @@ let subproof_cond = Proof.done_cond subproof_kind
 let vernac_subproof gln =
   let p = Proof_global.give_me_the_proof () in
   begin match gln with
-  | None -> Proof.focus subproof_cond 1 p
-  | Some n -> Proof.focus subproof_cond n p
+  | None -> Proof.focus subproof_cond () 1 p
+  | Some n -> Proof.focus subproof_cond () n p
   end ;
   print_subgoals ()