get rid of closures in global/proof state

In some cases, an 'a -> 'b field is changed into an ('a -> b') option
field so that one can forget the closures and marshal the resulting
state

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

5 files changed, 54 insertions, 75 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ed1de75bc..d02711eeb 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -48,7 +48,6 @@ let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
 let set_end_tac tac =
-  let tac = Proofview.V82.tactic tac in
   Proof_global.set_endline_tactic tac
 
 let set_used_variables l =
@@ -117,7 +116,7 @@ open Decl_kinds
 let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
-  start_proof id goal_kind sign typ (fun _ _ -> ());
+  start_proof id goal_kind sign typ None;
   try
     by tac;
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ed9b55ae5..79929fd8d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -122,7 +122,7 @@ val get_all_proof_names : unit -> Id.t list
 (** [set_end_tac tac] applies tactic [tac] to all subgoal generate
     by [solve_nth] *)
 
-val set_end_tac : tactic -> unit
+val set_end_tac : Tacexpr.raw_tactic_expr -> unit
 
 (** {6 ... } *)
 (** [set_used_variables l] declares that section variables [l] will be
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 38886e9e1..c1a909aed 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -34,13 +34,15 @@ open Util
 type _focus_kind = int
 type 'a focus_kind = _focus_kind
 type focus_info = Obj.t
+type reason = NotThisWay | AlreadyNoFocus
 type unfocusable =
-  | Cannot of exn
+  | Cannot of reason
   | Loose
   | Strict
 type _focus_condition =
-    (_focus_kind -> Proofview.proofview -> unfocusable) *
-    (_focus_kind -> bool)
+  | CondNo       of bool * _focus_kind
+  | CondDone     of bool * _focus_kind
+  | CondEndStack of        _focus_kind (* loose_end is false here *)
 type 'a focus_condition = _focus_condition
 
 let next_kind = ref 0
@@ -49,51 +51,11 @@ let new_focus_kind () =
   incr next_kind;
   r
 
-(* Auxiliary function to define conditions. *)
-let check kind1 kind2 = Int.equal kind1 kind2
-
 (* 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
     of just one, if anyone needs it *)
-(* [no_cond] only checks that the unfocusing command uses the right
-    [focus_kind]. *)
-
-module Cond = struct
-  (* first attempt at an algebra of condition *)
-  (* semantics:
-     - [Cannot] means that the condition is not met
-     - [Strict] that the condition is met
-     - [Loose] that the condition is not quite met
-       but authorises to unfocus provided a condition
-       of a previous focus on the stack is (strictly)
-       met. [Loose] focuses are those, like bullets,
-       which do not have a closing command and
-       are hence closed by unfocusing actions unrelated
-       to their focus_kind.
-  *)
-  let bool e b =
-    if b then fun _ _ -> Strict
-    else fun _ _ -> Cannot e
-  let loose c k p = match c k p with
-    | Cannot _ -> Loose
-    | c -> c
-  let cloose l c =
-    if l then loose c
-    else c
-  let (&&&) c1 c2 k p=
-    match c1 k p , c2 k p with
-    | Cannot e , _
-    | _ , Cannot e -> Cannot e
-    | Strict, Strict -> Strict
-    | _ , _ -> Loose
-  let kind e k0 k p = bool e (Int.equal k0 k) k p
-  let pdone e k p = bool e (Proofview.finished p) k p
-end
 
-
-(* Unfocus command.
-   Fails if the proof is not focused. *)
 exception CannotUnfocusThisWay
 let _ = Errors.register_handler begin function
   | CannotUnfocusThisWay ->
@@ -101,18 +63,24 @@ let _ = Errors.register_handler begin function
   | _ -> raise Errors.Unhandled
 end
 
-open Cond
-let no_cond_gen e ~loose_end k0 =
-  cloose loose_end (kind e k0)
-let no_cond_gen e ?(loose_end=false) k = no_cond_gen e ~loose_end k , check k
-let no_cond ?loose_end = no_cond_gen CannotUnfocusThisWay ?loose_end
-(* [done_cond] checks that the unfocusing command uses the right [focus_kind]
-    and that the focused proofview is complete. *)
-let done_cond_gen e ~loose_end k0 =
-  (cloose loose_end (kind e k0)) &&& pdone e
-let done_cond_gen e ?(loose_end=false) k = done_cond_gen e ~loose_end k , check k
-let done_cond ?loose_end = done_cond_gen CannotUnfocusThisWay ?loose_end
-
+let check_cond_kind c k =
+  let kind_of_cond = function
+    | CondNo (_,k) | CondDone(_,k) | CondEndStack k -> k in
+  kind_of_cond c = k
+
+let test_cond c k1 pw =
+  match c with
+  | CondNo(_,     k) when k = k1 -> Strict
+  | CondNo(true,  _)             -> Loose
+  | CondNo(false, _)             -> Cannot NotThisWay
+  | CondDone(_,     k) when k = k1 && Proofview.finished pw -> Strict
+  | CondDone(true,  _)                                      -> Loose
+  | CondDone(false, _)                                      -> Cannot NotThisWay
+  | CondEndStack k when k = k1 -> Strict
+  | CondEndStack _             -> Cannot AlreadyNoFocus
+
+let no_cond ?(loose_end=false) k = CondNo (loose_end, k)
+let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
    are under control of the undo mechanism *)
@@ -207,8 +175,9 @@ let focus cond inf i pr =
 
 let rec unfocus kind pr () =
   let cond = cond_of_focus pr in
-  match fst cond kind pr.proofview with
-  | Cannot e -> raise e
+  match test_cond cond kind pr.proofview with
+  | Cannot NotThisWay -> raise CannotUnfocusThisWay
+  | Cannot AlreadyNoFocus -> raise FullyUnfocused
   | Strict ->
      let pr = _unfocus pr in
      pr
@@ -223,16 +192,16 @@ exception NoSuchFocus
 (* no handler: should not be allowed to reach toplevel. *)
 let rec get_in_focus_stack kind stack =
   match stack with
-  | ((_,check),inf,_)::stack ->
-      if check kind then inf
+  | (cond,inf,_)::stack ->
+      if check_cond_kind cond kind then inf
       else get_in_focus_stack kind stack
   | [] -> raise NoSuchFocus
 let get_at_focus kind pr =
   Obj.magic (get_in_focus_stack kind pr.focus_stack)
 
 let is_last_focus kind pr =
-  let ((_,check),_,_) = List.hd pr.focus_stack in
-  check kind
+  let (cond,_,_) = List.hd pr.focus_stack in
+  check_cond_kind cond kind
 
 let no_focused_goal p =
   Proofview.finished p.proofview
@@ -247,7 +216,7 @@ let rec maximal_unfocus k p =
 
 (* [end_of_stack] is unfocused by return to close every loose focus. *)
 let end_of_stack_kind = new_focus_kind ()
-let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind
+let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 470d19b71..1f5ee7f75 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -65,13 +65,13 @@ type lemma_possible_guards = int list list
 
 type pstate = {
   pid : Id.t;
-  endline_tactic : unit Proofview.tactic;
+  endline_tactic : Tacexpr.raw_tactic_expr option;
   section_vars : Context.section_context option;
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
   compute_guard : lemma_possible_guards;
   hook : unit Tacexpr.declaration_hook;
-  mode : proof_mode;
+  mode : proof_mode option;
 }
 
 (* The head of [!pstates] is the actual current proof, the other ones are
@@ -84,7 +84,7 @@ let current_proof_mode = ref !default_proof_mode
 (* combinators for proof modes *)
 let update_proof_mode () =
   match !pstates with
-  | { mode = m } :: _ ->
+  | { mode = Some m } :: _ ->
       !current_proof_mode.reset ();
       current_proof_mode := m;
       !current_proof_mode.set ()
@@ -141,18 +141,25 @@ let cur_pstate () =
 let give_me_the_proof () = (cur_pstate ()).proof
 let get_current_proof_name () = (cur_pstate ()).pid
 
+let interp_tac = ref (fun _ _ -> assert false)
+let set_interp_tac f = interp_tac := f
+
 let with_current_proof f =
   match !pstates with
   | [] -> raise NoCurrentProof
   | p :: rest ->
-      let p = { p with proof = f p.endline_tactic p.proof } in
+      let et =
+        match p.endline_tactic with
+        | None -> Proofview.tclUNIT ()
+        | Some tac -> Proofview.V82.tactic (!interp_tac tac) in
+      let p = { p with proof = f et p.proof } in
       pstates := p :: rest
 
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
 let set_endline_tactic tac =
   match !pstates with
   | [] -> raise NoCurrentProof
-  | p :: rest -> pstates := { p with endline_tactic = tac } :: rest
+  | p :: rest -> pstates := { p with endline_tactic = Some tac } :: rest
 
 (* spiwack: it might be considered to move error messages away.
     Or else to remove special exceptions from Proof_global.
@@ -201,7 +208,7 @@ let set_proof_mode m id =
   update_proof_mode ()
 
 let set_proof_mode mn =
-  set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
+  set_proof_mode (Some (find_proof_mode mn)) (get_current_proof_name ())
 
 let activate_proof_mode mode = (find_proof_mode mode).set ()
 let disactivate_proof_mode mode = (find_proof_mode mode).reset ()
@@ -225,12 +232,12 @@ let start_proof id str goals ?(compute_guard=[]) hook =
   let initial_state = {
     pid = id;
     proof = Proof.start goals;
-    endline_tactic = Proofview.tclUNIT ();
+    endline_tactic = None;
     section_vars = None;
     strength = str;
     compute_guard = compute_guard;
     hook = hook;
-    mode = ! default_proof_mode } in
+    mode = None } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 61bb5c0dd..4462255dd 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -82,7 +82,10 @@ val with_current_proof :
   (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : unit Proofview.tactic -> unit
+val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit
+val set_interp_tac :
+  (Tacexpr.raw_tactic_expr -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma)
+    -> unit
 
 (** Sets the section variables assumed by the proof *)
 val set_used_variables : Names.Id.t list -> unit
@@ -136,7 +139,8 @@ module Bullet : sig
 end
 
 module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+  val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
+  Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
 end
 
 type state