Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 72 insertions, 62 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 72730495..996a895f 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -35,12 +35,12 @@ type _focus_kind = int
 type 'a focus_kind = _focus_kind
 type focus_info = Obj.t
 type unfocusable =
-  | Cannot
+  | Cannot of exn
   | Loose
   | Strict
 type _focus_condition = 
     (_focus_kind -> Proofview.proofview -> unfocusable) *
-    (_focus_kind -> focus_info -> focus_info)
+    (_focus_kind -> bool)
 type 'a focus_condition = _focus_condition
 
 let next_kind = ref 0
@@ -49,13 +49,8 @@ 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
-(* no handler: confined to this module. *)
-let check kind1 kind2 inf =
-  if kind1=kind2 then inf else raise CheckNext
+(* Auxiliary function to define conditions. *)
+let check kind1 kind2 = kind1=kind2
 
 (* To be authorized to unfocus one must meet the condition prescribed by
     the action which focused.*)
@@ -68,40 +63,55 @@ module Cond = struct
   (* first attempt at an algebra of condition *)
   (* semantics:
      - [Cannot] means that the condition is not met
-     - [Strict] that the condition is meant
-     - [Loose] that the condition is not quite meant
+     - [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.
+       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 b =
+  let bool e b =
     if b then fun _ _ -> Strict
-    else fun _ _ -> Cannot
+    else fun _ _ -> Cannot e
   let loose c k p = match c k p with
-    | Cannot -> Loose
+    | 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 , _ 
-    | _ , Cannot -> Cannot
+    | Cannot e , _ 
+    | _ , Cannot e -> Cannot e
     | Strict, Strict -> Strict
     | _ , _ -> Loose
-  let kind k0 k p = bool (k0=k) k p 
-  let pdone k p = bool (Proofview.finished p) k p
+  let kind e k0 k p = bool e (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 ->
+    Util.error "This proof is focused, but cannot be unfocused this way"
+  | _ -> raise Errors.Unhandled
 end
 
 open Cond
-let no_cond ~loose_end k0 =
-  cloose loose_end (kind k0)
-let no_cond ?(loose_end=false) k = no_cond ~loose_end k , check k
+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 ~loose_end k0 =
-  (cloose loose_end (kind k0)) &&& pdone
-let done_cond ?(loose_end=false) k = done_cond ~loose_end k , check k
+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
 
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
@@ -249,13 +259,13 @@ let save pr =
   push_undo (save_state pr) pr
 
 (* This function restores a state, presumably from the top of the undo stack. *)
-let restore_state save pr = 
+let restore_state save pr =
   match save with
   | State save -> pr.state <- save
   | Effect undo -> undo ()
 
 (* Interpretes the Undo command. *)
-let undo pr = 
+let undo pr =
   (* On a single line, since the effects commute *)
   restore_state (pop_undo pr) pr
 
@@ -309,20 +319,11 @@ let focus cond inf i pr =
   save pr;
   _focus cond (Obj.repr inf) i i pr
 
-(* Unfocus command.
-   Fails if the proof is not focused. *)
-exception CannotUnfocusThisWay
-let _ = Errors.register_handler begin function
-  | CannotUnfocusThisWay ->
-    Util.error "This proof is focused, but cannot be unfocused this way"
-  | _ -> raise Errors.Unhandled
-end
-
 let rec unfocus kind pr () =
   let starting_point = save_state pr in
   let cond = cond_of_focus pr in
   match fst cond kind pr.state.proofview with
-  | Cannot -> raise CannotUnfocusThisWay
+  | Cannot e -> raise e
   | Strict -> 
     (_unfocus pr;
      push_undo starting_point pr)
@@ -336,34 +337,35 @@ let rec unfocus kind pr () =
 
 let unfocus kind pr =
   transaction pr (unfocus kind pr)
-      
-let get_at_point kind ((_,get),inf,_) = get kind inf
+
 exception NoSuchFocus
 (* no handler: should not be allowed to reach toplevel. *)
-exception GetDone of Obj.t
-(* no handler: confined to this module. *)
-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 rec get_in_focus_stack kind stack =
+  match stack with
+  | ((_,check),inf,_)::stack ->
+      if check 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.state.focus_stack)
 
+let is_last_focus kind pr =
+  let ((_,check),_,_) = List.hd pr.state.focus_stack in
+  check kind
+
 let no_focused_goal p =
   Proofview.finished p.state.proofview
 
 (*** Proof Creation/Termination ***)
 
+(* [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 end_of_stack_kind
+let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind
+
+let unfocused = is_last_focus end_of_stack_kind
 
 let start goals =
-  let pr = 
+  let pr =
     { state = { proofview = Proofview.init goals ;
 	        focus_stack = [] ;
 	        intel = Store.empty} ;
@@ -445,14 +447,22 @@ module V82 = struct
   let top_evars p =
     Proofview.V82.top_evars p.state.proofview
 
-  let instantiate_evar n com pr =
-    let starting_point = save_state pr in
-    let sp = pr.state.proofview in
-    try
-      let new_proofview = Proofview.V82.instantiate_evar n com sp in
-      pr.state <- { pr.state with proofview = new_proofview };
-      push_undo starting_point pr
-    with e -> 
-      restore_state starting_point pr;
-      raise e
+  let grab_evars p =
+    if not (is_done p) then
+      raise UnfinishedProof
+    else
+      save p;
+      p.state <- { p.state with proofview = Proofview.V82.grab p.state.proofview }
+    
+
+    let instantiate_evar n com pr =
+      let starting_point = save_state pr in
+      let sp = pr.state.proofview in
+      try
+	let new_proofview = Proofview.V82.instantiate_evar n com sp in
+	pr.state <- { pr.state with proofview = new_proofview };
+	push_undo starting_point pr
+      with e -> 
+	restore_state starting_point pr;
+	raise e
 end