aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/decl_mode/decl_mode.ml23
-rw-r--r--plugins/decl_mode/decl_mode.mli6
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml50
-rw-r--r--plugins/decl_mode/decl_proof_instr.mli2
-rw-r--r--proofs/proof.ml57
-rw-r--r--proofs/proof.mli36
-rw-r--r--proofs/proof_global.ml15
-rw-r--r--proofs/proof_global.mli18
-rw-r--r--toplevel/vernacentries.ml15
9 files changed, 157 insertions, 65 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 232edda0fd..af6aa4bf59 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -66,7 +66,7 @@ type command_mode =
| Mode_none
let mode_of_pftreestate pts =
- (* spiwack: it was "top_goal_..." but this should be fine *)
+ (* spiwack: it used to be "top_goal_..." but this should be fine *)
let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
let goal = List.hd goals in
if info.get (Goal.V82.extra sigma goal) = None then
@@ -96,10 +96,25 @@ let get_stack pts =
let info = get_info sigma (List.hd goals) in
info.pm_stack
+
+let proof_focus = Proof.new_focus_kind ()
+let proof_cond = Proof.no_cond proof_focus
+
+let focus p =
+ let inf = get_stack p in
+ Proof.focus proof_cond inf 1 p
+
+let unfocus = Proof.unfocus proof_focus
+
+let maximal_unfocus = Proof_global.maximal_unfocus proof_focus
+
let get_top_stack pts =
- let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
- let info = get_info sigma gl in
- info.pm_stack
+ try
+ Proof.get_at_focus proof_focus pts
+ with Proof.NoSuchFocus ->
+ let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
+ let info = get_info sigma gl in
+ info.pm_stack
let get_last env =
try
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 72c46c7e7d..4e636598f9 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -70,3 +70,9 @@ val get_stack : Proof.proof -> stack_info list
val get_top_stack : Proof.proof -> stack_info list
val get_last: Environ.env -> identifier
+
+val focus : Proof.proof -> unit
+
+val unfocus : Proof.proof -> unit
+
+val maximal_unfocus : Proof.proof -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index cee4d7271d..549b1f1465 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -111,17 +111,15 @@ let assert_postpone id t =
(* start a proof *)
-let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
let start_proof_tac gls=
let info={pm_stack=[]} in
tcl_change_info info gls
let go_to_proof_mode () =
- Pfedit.by start_proof_tac ;
+ Pfedit.by start_proof_tac;
let p = Proof_global.give_me_the_proof () in
- Proof.focus proof_cond 1 p
+ Decl_mode.focus p
(* closing gaps *)
@@ -154,12 +152,14 @@ let mark_rule_as_done = function
(* post-instruction focus management *)
+(* spiwack: This used to fail if there was no focusing command
+ above, but I don't think it ever happened. I hope it doesn't mess
+ things up*)
let goto_current_focus pts =
- Proof.unfocus proof_focus pts
+ Decl_mode.maximal_unfocus pts
let goto_current_focus_or_top pts =
- try goto_current_focus pts
- with Util.UserError _ -> ()
+ goto_current_focus pts
(* return *)
@@ -172,6 +172,7 @@ let close_tactic_mode pts =
goto_current_focus pts2
let return_from_tactic_mode () =
+ (* arnaud: la commande return ne fonctionne pas *)
Util.anomaly "Todo: Decl_proof_instr.return_from_tactic_mode"
(* end proof/claim *)
@@ -180,7 +181,12 @@ let close_block bt pts =
if Proof.no_focused_goal pts then
goto_current_focus pts
else
- let stack =get_stack pts in
+ let stack =
+ if Proof.is_done pts then
+ get_top_stack pts
+ else
+ get_stack pts
+ in
match bt,stack with
B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
(goto_current_focus pts)
@@ -197,7 +203,7 @@ let close_block bt pts =
| ET_Induction -> error "\"end induction\" expected."
end
| _,_ -> anomaly "Lonely suppose on stack."
-
+
(* utility for suppose / suppose it is *)
@@ -577,8 +583,8 @@ let instr_claim _thus st gls0 =
let ninfo1 = {pm_stack=
(if _thus then Focus_claim else Claim)::info.pm_stack} in
tclTHENS (assert_postpone id st.st_it)
- [tcl_change_info ninfo1;
- thus_tac] gls0
+ [thus_tac;
+ tcl_change_info ninfo1] gls0
(* tactics for assume *)
@@ -1294,12 +1300,9 @@ let understand_my_constr c gls =
let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc -> map_glob_constr frob rc in
Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
-let set_refine,my_refine =
-let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in
-((fun tac -> refine:= tac),
-(fun c gls ->
- let oc = understand_my_constr c gls in
- !refine oc gls))
+let my_refine c gls =
+ let oc = understand_my_constr c gls in
+ Refine.refine oc gls
(* end focus/claim *)
@@ -1438,12 +1441,16 @@ let rec postprocess pts instr =
| Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
| Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> ()
| Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _
- | Pescape -> Proof.focus proof_cond 1 pts
+ | Pescape -> Decl_mode.focus pts
| Pend (B_elim ET_Induction) ->
begin
let pfterm = List.hd (Proof.partial_proof pts) in
let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in
- let env = Goal.V82.env sigma (List.hd gls) in
+ let env = try
+ Goal.V82.env sigma (List.hd gls)
+ with Failure "hd" ->
+ Global.env ()
+ in
try
Inductiveops.control_only_guard env pfterm;
goto_current_focus_or_top pts
@@ -1469,7 +1476,10 @@ let do_instr raw_instr pts =
interp_proof_instr (get_its_info gl) sigma env glob_instr in
Pfedit.by (tclTHEN (eval_instr instr) clean_tmp)
else () end;
- postprocess pts raw_instr.instr
+ postprocess pts raw_instr.instr;
+ (* spiwack: this should restore a compatible semantics with
+ v8.3 where we never stayed focused on 0 goal. *)
+ Decl_mode.maximal_unfocus pts
let proof_instr raw_instr =
let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index 0a2ab571ff..b27939b3ca 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -109,5 +109,3 @@ val init_tree:
(int option * Declarations.recarg Rtree.t) array ->
(Names.Idset.t * Decl_mode.split_tree) option) ->
Decl_mode.split_tree
-
-val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 44f1cce723..b932e95f9a 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 ab1c0b8345..bb651dea11 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 3e8c71482a..bcd9d6e0d3 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 a589732046..5f57c25ac5 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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f4fc8714be..ccbaa6d306 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -670,7 +670,7 @@ let pop_bullet pr =
b
| [] -> Util.anomaly "Tried to pop bullet from an empty stack"
let push_bullet b pr =
- Proof.focus bullet_cond 1 pr ;
+ Proof.focus bullet_cond () 1 pr ;
set_bullets (b::get_bullets pr) pr
let put_bullet p bul =
@@ -690,10 +690,7 @@ let vernac_solve n bullet tcom b =
solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b;
(* in case a strict subtree was completed,
go back to the top of the prooftree *)
- begin try while Proof.no_focused_goal p do
- Proof.unfocus command_focus p
- done
- with Util.UserError _ -> () end;
+ Proof_global.maximal_unfocus command_focus p;
print_subgoals();
if !pcoq <> None then (Option.get !pcoq).solve n
@@ -1252,8 +1249,8 @@ let vernac_backtrack snum pnum naborts =
let vernac_focus gln =
let p = Proof_global.give_me_the_proof () in
match gln with
- | None -> Proof.focus focus_command_cond 1 p; print_subgoals ()
- | Some n -> Proof.focus focus_command_cond n p; print_subgoals ()
+ | None -> Proof.focus focus_command_cond () 1 p; print_subgoals ()
+ | Some n -> Proof.focus focus_command_cond () n p; print_subgoals ()
(* Unfocuses one step in the focus stack. *)
@@ -1273,8 +1270,8 @@ let subproof_cond = Proof.done_cond subproof_kind
let vernac_subproof gln =
let p = Proof_global.give_me_the_proof () in
begin match gln with
- | None -> Proof.focus subproof_cond 1 p
- | Some n -> Proof.focus subproof_cond n p
+ | None -> Proof.focus subproof_cond () 1 p
+ | Some n -> Proof.focus subproof_cond () n p
end ;
print_subgoals ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 06:56:34 +0000