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

4 files changed, 96 insertions, 30 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 44f1cce72..b932e95f9 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 ab1c0b834..bb651dea1 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 3e8c71482..bcd9d6e0d 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 a58973204..5f57c25ac 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