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

1 files changed, 31 insertions, 62 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 38886e9e1d..c1a909aedc 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