diff options
| -rw-r--r-- | proofs/proof.ml | 145 | ||||
| -rw-r--r-- | proofs/proof.mli | 23 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 6 |
3 files changed, 123 insertions, 51 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 7e5941025..c9b90ac38 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -34,8 +34,12 @@ open Term type _focus_kind = int type 'a focus_kind = _focus_kind type focus_info = Obj.t +type unfocusable = + | Cannot + | Loose + | Strict type _focus_condition = - (_focus_kind -> Proofview.proofview -> bool) * + (_focus_kind -> Proofview.proofview -> unfocusable) * (_focus_kind -> focus_info -> focus_info) type 'a focus_condition = _focus_condition @@ -59,12 +63,45 @@ let check kind1 kind2 inf = of just one, if anyone needs it *) (* [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 + +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 + but authorises to unfocus provided a condition + of a previous focus on the stack is (strictly) + met. + *) + let bool b = + if b then fun _ _ -> Strict + else fun _ _ -> Cannot + 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 , _ + | _ , Cannot -> Cannot + | Strict, Strict -> Strict + | _ , _ -> Loose + let kind k0 k p = bool (k0=k) k p + let pdone k p = bool (Proofview.finished p) k p +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 (* [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 +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 (* Subpart of the type of proofs. It contains the parts of the proof which @@ -145,6 +182,7 @@ let return p = else Proofview.return p.state.proofview + (*** The following functions implement the basic internal mechanisms of proofs, they are not meant to be exported in the .mli ***) @@ -244,6 +282,44 @@ let undo pr = let add_undo effect pr = push_undo (Effect effect) pr + + +(*** Transactions ***) + +let init_transaction pr = + pr.transactions <- []::pr.transactions + +let commit_stack pr stack = + let push s = push_undo s pr in + List.iter push (List.rev stack) + +(* Invariant: [commit] should be called only when a transaction + is open. It closes the current transaction. *) +let commit pr = + match pr.transactions with + | stack::trans' -> + pr.transactions <- trans'; + commit_stack pr stack + | [] -> assert false + +(* Invariant: [rollback] should be called only when a transaction + is open. It closes the current transaction. *) +let rec rollback pr = + try + undo pr; + rollback pr + with EmptyUndoStack -> + match pr.transactions with + | []::trans' -> pr.transactions <- trans' + | _ -> assert false + + +let transaction pr t = + init_transaction pr; + try t (); commit pr + with e -> rollback pr; raise e + + (* 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? *) @@ -253,14 +329,31 @@ let focus cond inf i pr = (* Unfocus command. Fails if the proof is not focused. *) -let unfocus kind pr = +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 - if fst cond kind pr.state.proofview then + match fst cond kind pr.state.proofview with + | Cannot -> raise CannotUnfocusThisWay + | Strict -> (_unfocus pr; push_undo starting_point pr) - else - Util.error "This proof is focused, but cannot be unfocused this way" + | Loose -> + begin try + _unfocus pr; + push_undo starting_point pr; + unfocus kind pr () + with FullyUnfocused -> raise CannotUnfocusThisWay + end + +let unfocus kind pr = + transaction pr (unfocus kind pr) let get_at_point kind ((_,get),inf,_) = get kind inf exception NoSuchFocus @@ -306,40 +399,6 @@ let run_tactic env tac pr = raise e -(*** Transactions ***) - -let init_transaction pr = - pr.transactions <- []::pr.transactions - -let commit_stack pr stack = - let push s = push_undo s pr in - List.iter push (List.rev stack) - -(* Invariant: [commit] should be called only when a transaction - is open. It closes the current transaction. *) -let commit pr = - match pr.transactions with - | stack::trans' -> - pr.transactions <- trans'; - commit_stack pr stack - | [] -> assert false - -(* Invariant: [rollback] should be called only when a transaction - is open. It closes the current transaction. *) -let rec rollback pr = - try - undo pr; - rollback pr - with EmptyUndoStack -> - match pr.transactions with - | []::trans' -> pr.transactions <- trans' - | _ -> assert false - - -let transaction pr t = - init_transaction pr; - try t (); commit pr - with e -> rollback pr; raise e (*** Compatibility layer with <=v8.2 ***) diff --git a/proofs/proof.mli b/proofs/proof.mli index cbde9244a..7de0a9fdf 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -85,11 +85,21 @@ val new_focus_kind : unit -> 'a focus_kind from it.*) type 'a focus_condition (* [no_cond] only checks that the unfocusing command uses the right - [focus_kind]. *) -val no_cond : 'a focus_kind -> 'a focus_condition + [focus_kind]. + If [loose_end] (default [false]) is [true], then if the [focus_kind] + doesn't match, then unfocusing can occur, provided it unfocuses + an earlier focus. + For instance bullets can be unfocused in the following situation + [{- solve_goal. }] because they use a loose-end condition. *) +val no_cond : ?loose_end:bool -> '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 : 'a focus_kind -> 'a focus_condition + and that the focused proofview is complete. + If [loose_end] (default [false]) is [true], then if the [focus_kind] + doesn't match, then unfocusing can occur, provided it unfocuses + an earlier focus. + For instance bullets can be unfocused in the following situation + [{ - solve_goal. }] because they use a loose-end condition. *) +val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition (* focus command (focuses on the [i]th subgoal) *) (* spiwack: there could also, easily be a focus-on-a-range tactic, is there @@ -97,8 +107,11 @@ val done_cond : 'a focus_kind -> 'a focus_condition val focus : 'a focus_condition -> 'a -> int -> proof -> unit exception FullyUnfocused +exception CannotUnfocusThisWay (* Unfocusing command. - Raises [FullyUnfocused] if the proof is not focused. *) + Raises [FullyUnfocused] if the proof is not focused. + Raises [CannotUnfocusThisWay] if the proof the unfocusing condition + is not met. *) val unfocus : 'a focus_kind -> proof -> unit (* [get_at_focus k] gets the information stored at the closest focus point diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 186472be2..a5e19e306 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -300,7 +300,7 @@ let maximal_unfocus k p = begin try while Proof.no_focused_goal p do Proof.unfocus k p done - with Proof.FullyUnfocused | Util.UserError _ -> () + with Proof.FullyUnfocused | Proof.CannotUnfocusThisWay -> () end @@ -335,7 +335,7 @@ module Bullet = struct module Strict = struct (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) let bullet_kind = Proof.new_focus_kind () - let bullet_cond = Proof.done_cond bullet_kind + let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind let (get_bullets,set_bullets) = let bullets = Store.field () in begin fun pr -> Option.default [] (bullets.get (Proof.get_proof_info pr)) end , @@ -364,7 +364,7 @@ module Bullet = struct let put p bul = if has_bullet bul p then - begin + Proof.transaction p begin fun () -> while bul <> pop p do () done; push bul p end |