From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- proofs/proof.ml | 134 ++++++++++++++++++++++++++++++-------------------------- 1 file changed, 72 insertions(+), 62 deletions(-) (limited to 'proofs/proof.ml') 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 -- cgit v1.2.3