aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
blob: d8dc585f3f2f88da03eba5d9fa1bd51ba02d1078 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Pp
open Util
open Names
open Nameops
open Sign
open Term
open Declarations
open Entries
open Environ
open Evd
open Typing
open Tacmach
open Proof_trees
open Tacexpr
open Proof_type
open Lib
open Safe_typing

(*********************************************************************)
(* Managing the proofs state                                         *)
(* Mainly contributed by C. Murthy                                   *)
(*********************************************************************)

type proof_topstate = {
  mutable top_end_tac : tactic option;
  top_hyps : named_context * named_context;
  top_goal : goal;
  top_strength : Decl_kinds.goal_kind;
  top_hook : declaration_hook }

let proof_edits =
  (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t)

let get_all_proof_names () = Edit.dom proof_edits

let msg_proofs use_resume =
  match Edit.dom proof_edits with
    | [] -> (spc () ++ str"(No proof-editing in progress).")
    | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
               (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++
	       str"." ++
               (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
              	else (mt ()))
)

let undo_default = 50
let undo_limit = ref undo_default

(*********************************************************************)
(*    Functions for decomposing and modifying the proof state        *)
(*********************************************************************)

let get_state () =
  match Edit.read proof_edits with
    | None -> errorlabstrm "Pfedit.get_state"
          (str"No focused proof" ++ msg_proofs true)
    | Some(_,pfs,ts) -> (pfs,ts)

let get_topstate ()    = snd(get_state())
let get_pftreestate () = fst(get_state())

let get_end_tac () = let ts = get_topstate () in ts.top_end_tac

let get_goal_context n =
  let pftree = get_pftreestate () in
  let goal = nth_goal_of_pftreestate n pftree in
  (project goal, pf_env goal)

let get_current_goal_context () = get_goal_context 1

let set_current_proof = Edit.focus proof_edits

let resume_proof (loc,id) = 
  try 
    Edit.focus proof_edits id
  with Invalid_argument "Edit.focus" ->
    user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false)

let suspend_proof () =
  try 
    Edit.unfocus proof_edits
  with Invalid_argument "Edit.unfocus" ->
    errorlabstrm "Pfedit.suspend_current_proof"
      (str"No active proof" ++ (msg_proofs true))
      
let resume_last_proof () =
  match (Edit.last_focused proof_edits) with
    | None ->
        errorlabstrm "resume_last" (str"No proof-editing in progress.")
    | Some p -> 
	Edit.focus proof_edits p
	  
let get_current_proof_name () =
  match Edit.read proof_edits with
    | None ->
        errorlabstrm "Pfedit.get_proof"
          (str"No focused proof" ++ msg_proofs true)
    | Some(na,_,_) -> na

let add_proof (na,pfs,ts) =
  Edit.create proof_edits (na,pfs,ts,!undo_limit+1)

let delete_proof_gen = Edit.delete proof_edits

let delete_proof (loc,id) =
  try 
    delete_proof_gen id
  with (UserError ("Edit.delete",_)) ->
    user_err_loc
      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
      
let init_proofs () = Edit.clear proof_edits
		       
let mutate f =
  try 
    Edit.mutate proof_edits (fun _ pfs -> f pfs)
  with Invalid_argument "Edit.mutate" ->
    errorlabstrm "Pfedit.mutate"
      (str"No focused proof" ++ msg_proofs true)

let start (na,ts) =
  let pfs = mk_pftreestate ts.top_goal in 
  add_proof(na,pfs,ts)
    
let restart_proof () =
  match Edit.read proof_edits with
    | None -> 
	errorlabstrm "Pfedit.restart"
          (str"No focused proof to restart" ++ msg_proofs true)
    | Some(na,_,ts) -> 
	delete_proof_gen na;
        start (na,ts);
        set_current_proof na

let proof_term () =
  extract_pftreestate (get_pftreestate())
    
(* Detect is one has completed a subtree of the initial goal *)
let subtree_solved () = 
  let pts = get_pftreestate () in
  is_complete_proof (proof_of_pftreestate pts) & 
  not (is_top_pftreestate pts)

(*********************************************************************)
(*                 Undo functions                                    *)
(*********************************************************************)

let set_undo = function
  | None -> undo_limit := undo_default
  | Some n -> 
      if n>=0 then 
	undo_limit := n
      else 
	error "Cannot set a negative undo limit"

let get_undo () = Some !undo_limit

let undo n =
  try 
    Edit.undo proof_edits n; 
       (* needed because the resolution of a subtree is done in 2 steps 
       then a sequence of undo can lead to a focus on a completely solved 
       subtree - this solution only works properly if undoing one step *)
    if subtree_solved() then  Edit.undo proof_edits 1
  with (Invalid_argument "Edit.undo") ->
    errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)

(*********************************************************************)
(*                  Proof cooking                                    *)
(*********************************************************************)

let xml_cook_proof = ref (fun _ -> ())
let set_xml_cook_proof f = xml_cook_proof := f

let cook_proof () =
  let (pfs,ts) = get_state() 
  and ident = get_current_proof_name () in
  let {evar_concl=concl} = ts.top_goal 
  and strength = ts.top_strength in
  let pfterm = extract_pftreestate pfs in
  !xml_cook_proof pfs;
  (ident,
   ({ const_entry_body = pfterm;
      const_entry_type = Some concl;
      const_entry_opaque = true },
    strength, ts.top_hook))

let current_proof_statement () = 
  let ts = get_topstate() in
  (get_current_proof_name (), ts.top_strength, 
   ts.top_goal.evar_concl, ts.top_hook)

(*********************************************************************)
(*              Abort   functions                                    *)
(*********************************************************************)
 
let refining () = [] <> (Edit.dom proof_edits)

let check_no_pending_proofs () =
  if refining () then 
    errorlabstrm "check_no_pending_proofs"
      (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
         str"Use \"Abort All\" first or complete proof(s).")

let delete_current_proof () = delete_proof_gen (get_current_proof_name ())

let delete_all_proofs = init_proofs

(*********************************************************************)
(*   Modifying the end tactic of the current profftree               *)
(*********************************************************************)
let set_end_tac tac =
  let top = get_topstate () in
  top.top_end_tac <- Some tac

(*********************************************************************)
(*              Modifying the current prooftree                      *)
(*********************************************************************)

let start_proof na str sign concl hook =
  let top_goal = mk_goal sign concl in
  let ts = { 
    top_end_tac = None;
    top_hyps = (sign,empty_named_context);
    top_goal = top_goal;
    top_strength = str;
    top_hook = hook}
  in
  start(na,ts);
  set_current_proof na


let solve_nth k tac =
  let pft = get_pftreestate () in
  if not (List.mem (-1) (cursor_of_pftreestate pft)) then
    mutate (solve_nth_pftreestate k tac)
  else 
    error "cannot apply a tactic when we are descended behind a tactic-node"

let by tac = mutate (solve_pftreestate tac)

let instantiate_nth_evar_com n c =
  mutate (Evar_refiner.instantiate_pf_com n c)

let traverse n = mutate (traverse n)
 
(* [traverse_to path]

   Traverses the current proof to get to the location specified by
   [path].

   ALGORITHM: The algorithm works on reversed paths. One just has to remove
   the common part on the reversed paths.

*)

let common_ancestor l1 l2 =
  let rec common_aux l1 l2 =
    match l1, l2 with
      | a1::l1', a2::l2' when a1 = a2 -> common_aux l1' l2'
      | _, _ -> List.rev l1, List.length l2
  in
  common_aux (List.rev l1) (List.rev l2)
      
let rec traverse_up = function
  | 0 -> (function pf -> pf)
  | n -> (function pf -> Tacmach.traverse 0 (traverse_up (n - 1) pf))

let rec traverse_down = function
  | [] -> (function pf -> pf)
  | n::l -> (function pf -> Tacmach.traverse n (traverse_down l pf))

let traverse_to path =
  let up_and_down path pfs =
    let cursor = cursor_of_pftreestate pfs in
    let down_list, up_count = common_ancestor path cursor in
    traverse_down down_list (traverse_up up_count pfs)
  in
  mutate (up_and_down path)

(* traverse the proof tree until it reach the nth subgoal *)
let traverse_nth_goal n = mutate (nth_unproven n)

let traverse_prev_unproven () = mutate prev_unproven

let traverse_next_unproven () = mutate next_unproven


(* The goal focused on *)
let focus_n = ref 0
let make_focus n = focus_n := n
let focus () = !focus_n
let focused_goal () = let n = !focus_n in if n=0 then 1 else n

let reset_top_of_tree () = 
  let pts = get_pftreestate () in 
  if not (is_top_pftreestate pts) then mutate top_of_tree

(** Printers *)

let pr_subgoals_of_pfts pfts = 
  let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in 
  let sigma = project (top_goal_of_pftreestate pfts) in
  pr_subgoals_existential sigma gls

let pr_open_subgoals () =
  let pfts = get_pftreestate () in
  match focus() with
    | 0 -> 
	pr_subgoals_of_pfts pfts
    | n -> 
	let pf = proof_of_pftreestate pfts in
	let gls = fst (frontier pf) in 
	assert (n > List.length gls);
	if List.length gls < 2 then 
	  pr_subgoal n gls
	else 
	  v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
	  pr_subgoal n gls)

let pr_nth_open_subgoal n =
  let pf = proof_of_pftreestate (get_pftreestate ()) in
  pr_subgoal n (fst (frontier pf))