1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: pfedit.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
29
(*********************************************************************)
30
(* Managing the proofs state *)
31
(* Mainly contributed by C. Murthy *)
32
(*********************************************************************)
34
type proof_topstate = {
35
mutable top_end_tac : tactic option;
36
top_init_tac : tactic option;
37
top_compute_guard : bool;
39
top_strength : Decl_kinds.goal_kind;
40
top_hook : declaration_hook }
43
(Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t)
45
let get_all_proof_names () = Edit.dom proof_edits
47
let msg_proofs use_resume =
48
match Edit.dom proof_edits with
49
| [] -> (spc () ++ str"(No proof-editing in progress).")
50
| l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
51
(prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++
53
(if use_resume then (fnl () ++ str"Use \"Resume\" first.")
58
let undo_limit = ref undo_default
60
(*********************************************************************)
61
(* Functions for decomposing and modifying the proof state *)
62
(*********************************************************************)
65
match Edit.read proof_edits with
66
| None -> errorlabstrm "Pfedit.get_state"
67
(str"No focused proof" ++ msg_proofs true)
68
| Some(_,pfs,ts) -> (pfs,ts)
70
let get_topstate () = snd(get_state())
71
let get_pftreestate () = fst(get_state())
73
let get_end_tac () = let ts = get_topstate () in ts.top_end_tac
75
let get_goal_context n =
76
let pftree = get_pftreestate () in
77
let goal = nth_goal_of_pftreestate n pftree in
78
(project goal, pf_env goal)
80
let get_current_goal_context () = get_goal_context 1
82
let set_current_proof = Edit.focus proof_edits
84
let resume_proof (loc,id) =
86
Edit.focus proof_edits id
87
with Invalid_argument "Edit.focus" ->
88
user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false)
90
let suspend_proof () =
92
Edit.unfocus proof_edits
93
with Invalid_argument "Edit.unfocus" ->
94
errorlabstrm "Pfedit.suspend_current_proof"
95
(str"No active proof" ++ (msg_proofs true))
97
let resume_last_proof () =
98
match (Edit.last_focused proof_edits) with
100
errorlabstrm "resume_last" (str"No proof-editing in progress.")
102
Edit.focus proof_edits p
104
let get_current_proof_name () =
105
match Edit.read proof_edits with
107
errorlabstrm "Pfedit.get_proof"
108
(str"No focused proof" ++ msg_proofs true)
111
let add_proof (na,pfs,ts) =
112
Edit.create proof_edits (na,pfs,ts,!undo_limit+1)
114
let delete_proof_gen = Edit.delete proof_edits
116
let delete_proof (loc,id) =
119
with (UserError ("Edit.delete",_)) ->
121
(loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
125
Edit.mutate proof_edits (fun _ pfs -> f pfs)
126
with Invalid_argument "Edit.mutate" ->
127
errorlabstrm "Pfedit.mutate"
128
(str"No focused proof" ++ msg_proofs true)
131
let pfs = mk_pftreestate ts.top_goal in
132
let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
135
let restart_proof () =
136
match Edit.read proof_edits with
138
errorlabstrm "Pfedit.restart"
139
(str"No focused proof to restart" ++ msg_proofs true)
146
extract_pftreestate (get_pftreestate())
148
(* Detect is one has completed a subtree of the initial goal *)
149
let subtree_solved () =
150
let pts = get_pftreestate () in
151
is_complete_proof (proof_of_pftreestate pts) &
152
not (is_top_pftreestate pts)
155
let pts = get_pftreestate () in
156
is_complete_proof (proof_of_pftreestate pts)
158
let top_tree_solved () =
159
let pts = get_pftreestate () in
160
is_complete_proof (proof_of_pftreestate (top_of_tree pts))
162
(*********************************************************************)
164
(*********************************************************************)
166
let set_undo = function
167
| None -> undo_limit := undo_default
172
error "Cannot set a negative undo limit"
174
let get_undo () = Some !undo_limit
178
Edit.undo proof_edits n;
179
(* needed because the resolution of a subtree is done in 2 steps
180
then a sequence of undo can lead to a focus on a completely solved
181
subtree - this solution only works properly if undoing one step *)
182
if subtree_solved() then Edit.undo proof_edits 1
183
with (Invalid_argument "Edit.undo") ->
184
errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
186
(* Undo current focused proof to reach depth [n]. This is used in
187
[vernac_backtrack]. *)
190
Edit.undo_todepth proof_edits n
191
with (Invalid_argument "Edit.undo") ->
192
errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
194
(* Return the depth of the current focused proof stack, this is used
195
to put informations in coq prompt (in emacs mode). *)
196
let current_proof_depth() =
198
Edit.depth proof_edits
199
with (Invalid_argument "Edit.depth") -> -1
201
(*********************************************************************)
203
(*********************************************************************)
205
let xml_cook_proof = ref (fun _ -> ())
206
let set_xml_cook_proof f = xml_cook_proof := f
209
let (pfs,ts) = get_state()
210
and ident = get_current_proof_name () in
211
let {evar_concl=concl} = ts.top_goal
212
and strength = ts.top_strength in
213
let pfterm = extract_pftreestate pfs in
214
!xml_cook_proof (strength,pfs);
217
({ const_entry_body = pfterm;
218
const_entry_type = Some concl;
219
const_entry_opaque = true;
220
const_entry_boxed = false},
221
ts.top_compute_guard, strength, ts.top_hook))
223
let current_proof_statement () =
224
let ts = get_topstate() in
225
(get_current_proof_name (), ts.top_strength,
226
ts.top_goal.evar_concl, ts.top_hook)
228
(*********************************************************************)
229
(* Abort functions *)
230
(*********************************************************************)
232
let refining () = [] <> (Edit.dom proof_edits)
234
let check_no_pending_proofs () =
236
errorlabstrm "check_no_pending_proofs"
237
(str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
238
str"Use \"Abort All\" first or complete proof(s).")
240
let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
242
let delete_all_proofs () = Edit.clear proof_edits
244
(*********************************************************************)
245
(* Modifying the end tactic of the current profftree *)
246
(*********************************************************************)
247
let set_end_tac tac =
248
let top = get_topstate () in
249
top.top_end_tac <- Some tac
251
(*********************************************************************)
252
(* Modifying the current prooftree *)
253
(*********************************************************************)
255
let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook =
256
let top_goal = mk_goal sign concl None in
259
top_init_tac = init_tac;
260
top_compute_guard = compute_guard;
268
let solve_nth k tac =
269
let pft = get_pftreestate () in
270
if not (List.mem (-1) (cursor_of_pftreestate pft)) then
271
mutate (solve_nth_pftreestate k tac)
273
error "cannot apply a tactic when we are descended behind a tactic-node"
275
let by tac = mutate (solve_pftreestate tac)
277
let instantiate_nth_evar_com n c =
278
mutate (Evar_refiner.instantiate_pf_com n c)
280
let traverse n = mutate (traverse n)
282
(* [traverse_to path]
284
Traverses the current proof to get to the location specified by
287
ALGORITHM: The algorithm works on reversed paths. One just has to remove
288
the common part on the reversed paths.
292
let common_ancestor l1 l2 =
293
let rec common_aux l1 l2 =
295
| a1::l1', a2::l2' when a1 = a2 -> common_aux l1' l2'
296
| _, _ -> List.rev l1, List.length l2
298
common_aux (List.rev l1) (List.rev l2)
300
let rec traverse_up = function
301
| 0 -> (function pf -> pf)
302
| n -> (function pf -> Refiner.traverse 0 (traverse_up (n - 1) pf))
304
let rec traverse_down = function
305
| [] -> (function pf -> pf)
306
| n::l -> (function pf -> Refiner.traverse n (traverse_down l pf))
308
let traverse_to path =
309
let up_and_down path pfs =
310
let cursor = cursor_of_pftreestate pfs in
311
let down_list, up_count = common_ancestor path cursor in
312
traverse_down down_list (traverse_up up_count pfs)
314
mutate (up_and_down path)
316
(* traverse the proof tree until it reach the nth subgoal *)
317
let traverse_nth_goal n = mutate (nth_unproven n)
319
let traverse_prev_unproven () = mutate prev_unproven
321
let traverse_next_unproven () = mutate next_unproven
323
(* The goal focused on *)
325
let make_focus n = focus_n := n
326
let focus () = !focus_n
327
let focused_goal () = let n = !focus_n in if n=0 then 1 else n
329
let reset_top_of_tree () =
332
let reset_top_of_script () =
335
up_until_matching_rule is_proof_instr pts
336
with Not_found -> top_of_tree pts)
added
removed
proofs/pfedit.ml
