diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 57 | ||||
| -rw-r--r-- | proofs/proof.mli | 36 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 15 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 18 |
4 files changed, 96 insertions, 30 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 44f1cce72..b932e95f9 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -31,8 +31,13 @@ open Term -type focus_kind = int -type focus_condition = focus_kind -> Proofview.proofview -> bool +type _focus_kind = int +type 'a focus_kind = _focus_kind +type focus_info = Obj.t +type _focus_condition = + (_focus_kind -> Proofview.proofview -> bool) * + (_focus_kind -> focus_info -> focus_info) +type 'a focus_condition = _focus_condition let next_kind = ref 0 let new_focus_kind () = @@ -40,6 +45,13 @@ 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 +let check kind1 kind2 inf = + if kind1=kind2 then inf else raise CheckNext + (* 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 @@ -47,9 +59,11 @@ let new_focus_kind () = (* [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 (* [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 (* Subpart of the type of proofs. It contains the parts of the proof which @@ -58,9 +72,9 @@ type proof_state = { (* Current focused proofview *) proofview: Proofview.proofview; (* History of the focusings, provides information on how - to unfocus the proof. + to unfocus the proof and the extra information stored while focusing. The list is empty when the proof is fully unfocused. *) - focus_stack: (focus_condition*Proofview.focus_context) list; + focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list; (* Extra information which can be freely used to create new behaviours. *) intel: Store.t } @@ -94,7 +108,7 @@ let start goals = } let rec unroll_focus pv = function - | (_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk + | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk | [] -> pv (* spiwack: a proof is considered completed even if its still focused, if the focus @@ -126,15 +140,15 @@ let return p = of proofs, they are not meant to be exported in the .mli ***) (* An auxiliary function to push a {!focus_context} on the focus stack. *) -let push_focus kind context pr = - pr.state <- { pr.state with focus_stack = (kind,context)::pr.state.focus_stack } +let push_focus cond inf context pr = + pr.state <- { pr.state with focus_stack = (cond,inf,context)::pr.state.focus_stack } exception FullyUnfocused (* An auxiliary function to read the kind of the next focusing step *) let cond_of_focus pr = match pr.state.focus_stack with - | (cond,_)::_ -> cond + | (cond,_,_)::_ -> cond | _ -> raise FullyUnfocused (* An auxiliary function to pop and read the last {!Proofview.focus_context} @@ -159,16 +173,16 @@ let pop_undo pr = (* This function focuses the proof [pr] between indices [i] and [j] *) -let _focus cond i j pr = +let _focus cond inf i j pr = let (focused,context) = Proofview.focus i j pr.state.proofview in - push_focus cond context pr; + push_focus cond inf context pr; pr.state <- { pr.state with proofview = focused } (* This function unfocuses the proof [pr], it raises [FullyUnfocused], if the proof is already fully unfocused. This function does not care about the condition of the current focus. *) let _unfocus pr = - let (_,fc) = pop_focus pr in + let (_,_,fc) = pop_focus pr in pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview } @@ -214,9 +228,9 @@ let add_undo effect pr = (* 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? *) -let focus cond i pr = +let focus cond inf i pr = save pr; - _focus cond i i pr + _focus cond (Obj.repr inf) i i pr (* Unfocus command. Fails if the proof is not focused. *) @@ -224,7 +238,7 @@ let unfocus kind pr = let starting_point = save_state pr in try let cond = cond_of_focus pr in - if cond kind pr.state.proofview then + if fst cond kind pr.state.proofview then (_unfocus pr; push_undo starting_point pr) else @@ -232,6 +246,21 @@ let unfocus kind pr = with FullyUnfocused -> Util.error "This proof is not focused" +let get_at_point kind ((_,get),inf,_) = get kind inf +exception NoSuchFocus +exception GetDone of Obj.t +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 get_at_focus kind pr = + Obj.magic (get_in_focus_stack kind pr.state.focus_stack) + let no_focused_goal p = Proofview.finished p.state.proofview diff --git a/proofs/proof.mli b/proofs/proof.mli index ab1c0b834..bb651dea1 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -64,32 +64,44 @@ val add_undo : (unit -> unit) -> proof -> unit (*** Focusing actions ***) -(* [focus_kind] is the type used by focusing and unfocusing +(* ['a focus_kind] is the type used by focusing and unfocusing commands to synchronise. Focusing and unfocusing commands use - a particular focus_kind, and if they don't match, the unfocusing command - will fail. *) -type focus_kind -val new_focus_kind : unit -> focus_kind + a particular ['a focus_kind], and if they don't match, the unfocusing command + will fail. + When focusing with an ['a focus_kind], an information of type ['a] is + stored at the focusing point. An example use is the "induction" tactic + of the declarative mode where sub-tactics must be aware of the current + induction argument. *) +type 'a focus_kind +val new_focus_kind : unit -> 'a focus_kind (* To be authorized to unfocus one must meet the condition prescribed by - the action which focused.*) -type focus_condition + the action which focused. + Conditions always carry a focus kind, and inherit their type parameter + from it.*) +type 'a focus_condition (* [no_cond] only checks that the unfocusing command uses the right [focus_kind]. *) -val no_cond : focus_kind -> focus_condition +val no_cond : '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 : focus_kind -> focus_condition +val done_cond : 'a focus_kind -> 'a focus_condition (* focus command (focuses on the [i]th subgoal) *) -(* there could also, easily be a focus-on-a-range tactic, is there +(* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) -val focus : focus_condition -> int -> proof -> unit +val focus : 'a focus_condition -> 'a -> int -> proof -> unit exception FullyUnfocused (* Unfocusing command. Raises [FullyUnfocused] if the proof is not focused. *) -val unfocus : focus_kind -> proof -> unit +val unfocus : 'a focus_kind -> proof -> unit + +(* [get_at_focus k] gets the information stored at the closest focus point + of kind [k]. + Raises [NoSuchFocus] if there is no focus point of kind [k]. *) +exception NoSuchFocus +val get_at_focus : 'a focus_kind -> proof -> 'a (* returns [true] if there is no goal under focus. *) val no_focused_goal : proof -> bool diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3e8c71482..bcd9d6e0d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -281,6 +281,21 @@ let close_proof () = | Proof.HasUnresolvedEvar -> Util.error "Attempt to save a proof with existential variables still non-instantiated" + +(**********************************************************) +(* *) +(* Utility functions *) +(* *) +(**********************************************************) + +let maximal_unfocus k p = + begin try while Proof.no_focused_goal p do + Proof.unfocus k p + done + with Util.UserError _ -> (* arnaud: attention à ça si je fini par me décider à mettre une vrai erreur pour Proof.unfocus *) + () + end + module V82 = struct let get_current_initial_conclusions () = let p = give_me_the_proof () in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index a58973204..5f57c25ac 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -72,18 +72,28 @@ val suspend : unit -> unit val resume_last : unit -> unit val resume : Names.identifier -> unit -(** @raise NoSuchProof if it doesn't find *) +(** @raise NoSuchProof if it doesn't find one. *) -(* Runs a tactic on the current proof. Raises [NoCurrentProof] is there is +(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is no current proof. *) val run_tactic : unit Proofview.tactic -> unit -(* Sets the tactic to be used when a tactic line is closed with [...] *) +(** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : unit Proofview.tactic -> unit -(* Appends the endline tactic of the current proof to a tactic. *) +(** Appends the endline tactic of the current proof to a tactic. *) val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic +(**********************************************************) +(* *) +(* Utility functions *) +(* *) +(**********************************************************) + +(** [maximal_unfocus k p] unfocuses [p] until [p] has at least a + focused goal or that the last focus isn't of kind [k]. *) +val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit + module V82 : sig val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook) end |