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
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Coq
open Ideutils
type flag = [ `COMMENT | `UNSAFE ]
module SentenceId : sig
type sentence = private {
start : GText.mark;
stop : GText.mark;
mutable flags : flag list;
id : int;
}
val mk_sentence :
start:GText.mark -> stop:GText.mark -> flag list -> sentence
val set_flags : sentence -> flag list -> unit
end = struct
type sentence = {
start : GText.mark;
stop : GText.mark;
mutable flags : flag list;
id : int;
}
let id = ref 0
let mk_sentence ~start ~stop flags = decr id; {
start = start;
stop = stop;
flags = flags;
id = !id;
}
let set_flags s f = s.flags <- f
end
open SentenceId
let prefs = Preferences.current
let log msg : unit task =
Coq.lift (fun () -> Minilib.log msg)
class type ops =
object
method go_to_insert : unit task
method tactic_wizard : string list -> unit task
method process_next_phrase : unit task
method process_until_end_or_error : unit task
method handle_reset_initial : Coq.reset_kind -> unit task
method raw_coq_query : string -> unit task
method show_goals : unit task
method backtrack_last_phrase : unit task
method initialize : unit task
end
class coqops
(_script:Wg_ScriptView.script_view)
(_pv:Wg_ProofView.proof_view)
(_mv:Wg_MessageView.message_view)
(_ct:Coq.coqtop)
get_filename =
object(self)
val script = _script
val buffer = (_script#source_buffer :> GText.buffer)
val proof = _pv
val messages = _mv
val cmd_stack = Stack.create ()
initializer
Coq.set_feedback_handler _ct self#process_feedback;
Wg_Tooltip.set_tooltip_callback (script :> GText.view)
method private get_start_of_input =
buffer#get_iter_at_mark (`NAME "start_of_input")
method private get_insert =
buffer#get_iter_at_mark `INSERT
method show_goals =
Coq.PrintOpt.set_printing_width proof#width;
Coq.bind Coq.goals (function
| Interface.Fail (l, str) ->
messages#set ("Error in coqtop:\n"^str);
Coq.return ()
| Interface.Good goals ->
Coq.bind Coq.evars (function
| Interface.Fail (l, str)->
messages#set ("Error in coqtop:\n"^str);
Coq.return ()
| Interface.Good evs ->
proof#set_goals goals;
proof#set_evars evs;
proof#refresh ();
Coq.return ()
)
)
(* This method is intended to perform stateless commands *)
method raw_coq_query phrase =
let action = log "raw_coq_query starting now" in
let display_error s =
if not (Glib.Utf8.validate s) then
flash_info "This error is so nasty that I can't even display it."
else messages#add s;
in
let query =
Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in
let next = function
| Interface.Fail (_, err) -> display_error err; Coq.return ()
| Interface.Good msg ->
messages#add msg; Coq.return ()
in
Coq.bind (Coq.seq action query) next
(** [fill_command_queue until q] fills a command queue until the [until]
condition returns true; it is fed with the number of phrases read and the
iters enclosing the current sentence. *)
method private fill_command_queue until queue =
let rec loop len iter =
match Sentence.find buffer iter with
| None -> raise Exit
| Some (start, stop) ->
if until len start stop then raise Exit;
buffer#apply_tag Tags.Script.to_process ~start ~stop;
(* Check if this is a comment *)
let is_comment =
stop#backward_char#has_tag Tags.Script.comment_sentence
in
let sentence =
mk_sentence
~start:(`MARK (buffer#create_mark start))
~stop:(`MARK (buffer#create_mark stop))
(if is_comment then [`COMMENT] else []) in
Queue.push sentence queue;
if not stop#is_end then loop (succ len) stop
in
try loop 0 self#get_start_of_input with Exit -> ()
method private discard_command_queue queue =
while not (Queue.is_empty queue) do
let sentence = Queue.pop queue in
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
buffer#remove_tag Tags.Script.to_process ~start ~stop;
buffer#delete_mark sentence.start;
buffer#delete_mark sentence.stop;
done
method private mark_as_needed sentence =
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
let tag =
if List.mem `UNSAFE sentence.flags then Tags.Script.unjustified
else Tags.Script.processed in
buffer#apply_tag tag ~start ~stop
method private attach_tooltip sentence loc text =
let pre_chars, post_chars = Loc.unloc loc in
let start_sentence = buffer#get_iter_at_mark sentence.start in
let stop_sentence = buffer#get_iter_at_mark sentence.stop in
let phrase = start_sentence#get_slice ~stop:stop_sentence in
let pre = Ideutils.glib_utf8_pos_to_offset phrase ~off:pre_chars in
let post = Ideutils.glib_utf8_pos_to_offset phrase ~off:post_chars in
let start = start_sentence#forward_chars pre in
let stop = start_sentence#forward_chars post in
let markup = lazy text in
Wg_Tooltip.apply_tooltip_tag buffer ~start ~stop ~markup
method private process_feedback msg =
let id = msg.Interface.edit_id in
if id = 0 || Stack.is_empty cmd_stack then () else
let sentence =
let last_sentence = Stack.top cmd_stack in
if last_sentence.id = id then Some last_sentence else None in
match msg.Interface.content, sentence with
| Interface.AddedAxiom, Some sentence ->
set_flags sentence (CList.add_set `UNSAFE sentence.flags);
self#mark_as_needed sentence
| Interface.Processed, Some sentence -> self#mark_as_needed sentence
| Interface.GlobRef(loc, filepath, modpath, ident, ty), Some sentence ->
self#attach_tooltip sentence loc
(Printf.sprintf "%s %s %s" filepath ident ty)
| _ ->
if sentence = None then
Minilib.log "Coqide/Coq is really asynchronous now!"
(* In this case we shoud look for (exec_)id into cmd_stack *)
else Minilib.log "Unsupported feedback message"
method private commit_queue_transaction sentence =
(* A queued command has been successfully done, we push it to [cmd_stack].
We reget the iters here because Gtk is unable to warranty that they
were not modified meanwhile. Not really necessary but who knows... *)
self#mark_as_needed sentence;
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
buffer#move_mark ~where:stop (`NAME "start_of_input");
buffer#remove_tag Tags.Script.to_process ~start ~stop
method private process_error queue phrase loc msg =
Coq.bind (Coq.return ()) (function () ->
let position_error = function
| None -> ()
| Some (start, stop) ->
let soi = self#get_start_of_input in
let start =
soi#forward_chars (byte_offset_to_char_offset phrase start) in
let stop =
soi#forward_chars (byte_offset_to_char_offset phrase stop) in
buffer#apply_tag Tags.Script.error ~start ~stop;
buffer#place_cursor ~where:start
in
let sentence = Stack.pop cmd_stack in
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
buffer#remove_tag Tags.Script.to_process ~start ~stop;
self#discard_command_queue queue;
pop_info ();
position_error loc;
messages#clear;
messages#push Interface.Error msg;
self#show_goals)
(** Compute the phrases until [until] returns [true]. *)
method private process_until until verbose =
let push_msg lvl msg = if verbose then messages#push lvl msg in
let action = Coq.lift (fun () ->
let queue = Queue.create () in
(* Lock everything and fill the waiting queue *)
push_info "Coq is computing";
messages#clear;
script#set_editable false;
self#fill_command_queue until queue;
(* Now unlock and process asynchronously. Since [until]
may contain iterators, it shouldn't be used anymore *)
script#set_editable true;
Minilib.log "Begin command processing";
queue)
in
Coq.bind action (fun queue ->
let rec loop () =
if Queue.is_empty queue then
let () = pop_info () in
let () = script#recenter_insert in
self#show_goals
else
let sentence = Queue.pop queue in
Stack.push sentence cmd_stack;
if List.mem `COMMENT sentence.flags then
(self#commit_queue_transaction sentence; loop ())
else
(* If the line is not a comment, we interpret it. *)
let phrase =
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
start#get_slice ~stop
in
let commit_and_continue msg =
push_msg Interface.Notice msg;
self#commit_queue_transaction sentence;
loop ()
in
let query = Coq.interp ~logger:push_msg ~verbose sentence.id phrase in
let next = function
| Interface.Good msg -> commit_and_continue msg
| Interface.Fail (loc, msg) -> self#process_error queue phrase loc msg
in
Coq.bind query next
in
loop ())
method process_next_phrase =
let until len start stop = 1 <= len in
let next () =
buffer#place_cursor ~where:self#get_start_of_input; Coq.return ()
in
Coq.bind (self#process_until until true) next
method private process_until_iter iter =
let until len start stop =
if prefs.Preferences.stop_before then stop#compare iter > 0
else start#compare iter >= 0
in
self#process_until until false
method process_until_end_or_error =
self#process_until_iter buffer#end_iter
(** Clear the command stack until [until] returns [true].
Returns the number of commands sent to Coqtop to backtrack. *)
method private prepare_clear_zone until zone =
let merge_zone phrase zone =
match zone with
| None -> Some (phrase.start, phrase.stop)
| Some (start,stop) ->
(* phrase should be just before the current clear zone *)
buffer#delete_mark phrase.stop;
buffer#delete_mark start;
Some (phrase.start, stop)
in
let rec loop len real_len zone =
if Stack.is_empty cmd_stack then real_len, zone
else
let phrase = Stack.top cmd_stack in
let is_comment = List.mem `COMMENT phrase.flags in
if until len real_len phrase.start phrase.stop then
real_len, zone
else
(* [until] has not been reached, so we'll clear this command *)
let _ = Stack.pop cmd_stack in
let zone = merge_zone phrase zone in
loop (succ len) (if is_comment then real_len else succ real_len) zone
in
loop 0 0 zone
method private commit_clear_zone = function
| None -> ()
| Some (start_mark, stop_mark) ->
let start = buffer#get_iter_at_mark start_mark in
let stop = buffer#get_iter_at_mark stop_mark in
buffer#remove_tag Tags.Script.processed ~start ~stop;
buffer#remove_tag Tags.Script.unjustified ~start ~stop;
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#move_mark ~where:start (`NAME "start_of_input");
buffer#delete_mark start_mark;
buffer#delete_mark stop_mark
(** Actually performs the undoing *)
method private undo_command_stack n clear_zone =
let next = function
| Interface.Good n ->
let until _ len _ _ = n <= len in
(* Coqtop requested [n] more ACTUAL backtrack *)
let _, zone = self#prepare_clear_zone until clear_zone in
self#commit_clear_zone zone;
Coq.return ()
| Interface.Fail (l, str) ->
messages#set
("Error while backtracking: " ^ str ^
"\nCoqIDE and coqtop may be out of sync," ^
"you may want to use Restart.");
Coq.return ()
in
Coq.bind (Coq.rewind n) next
(** Wrapper around the raw undo command *)
method private backtrack_until until =
let action () =
push_info "Coq is undoing";
messages#clear
in
Coq.bind (Coq.lift action) (fun () ->
(* Instead of locking the whole buffer, we now simply remove
read-only tags *after* the actual backtrack *)
let to_undo, zone = self#prepare_clear_zone until None in
let next () = pop_info (); Coq.return () in
Coq.bind (self#undo_command_stack to_undo zone) next
)
method private backtrack_to_iter iter =
let until _ _ _ stop =
iter#compare (buffer#get_iter_at_mark stop) >= 0
in
Coq.seq (self#backtrack_until until)
(* We may have backtracked too much: let's replay *)
(self#process_until_iter iter)
method backtrack_last_phrase =
let until len _ _ _ = 1 <= len in
Coq.bind (self#backtrack_until until)
(fun () ->
buffer#place_cursor ~where:self#get_start_of_input;
self#show_goals)
method go_to_insert =
Coq.bind (Coq.return ()) (fun () ->
let point = self#get_insert in
if point#compare self#get_start_of_input >= 0
then self#process_until_iter point
else self#backtrack_to_iter point)
method tactic_wizard l =
let insert_phrase phrase tag =
let stop = self#get_start_of_input in
let phrase' = if stop#starts_line then phrase else "\n"^phrase in
buffer#insert ~iter:stop phrase';
Sentence.tag_on_insert buffer;
let start = self#get_start_of_input in
buffer#move_mark ~where:stop (`NAME "start_of_input");
buffer#apply_tag tag ~start ~stop;
if self#get_insert#compare stop <= 0 then
buffer#place_cursor ~where:stop;
let sentence =
mk_sentence
~start:(`MARK (buffer#create_mark start))
~stop:(`MARK (buffer#create_mark stop))
[] in
Stack.push sentence cmd_stack;
messages#clear;
self#show_goals
in
let display_error (loc, s) =
if not (Glib.Utf8.validate s) then
flash_info "This error is so nasty that I can't even display it."
else messages#add s
in
let try_phrase phrase stop more =
let action = log "Sending to coq now" in
let query = Coq.interp ~verbose:false 0 phrase in
let next = function
| Interface.Fail (l, str) ->
display_error (l, str);
messages#add ("Unsuccessfully tried: "^phrase);
more
| Interface.Good msg ->
messages#add msg;
stop Tags.Script.processed
in
Coq.bind (Coq.seq action query) next
in
let rec loop l = match l with
| [] -> Coq.return ()
| p :: l' ->
try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l')
in
loop l
method handle_reset_initial why =
let action () =
if why = Coq.Unexpected then warning "Coqtop died badly. Resetting.";
(* clear the stack *)
while not (Stack.is_empty cmd_stack) do
let phrase = Stack.pop cmd_stack in
buffer#delete_mark phrase.start;
buffer#delete_mark phrase.stop
done;
(* reset the buffer *)
buffer#move_mark ~where:buffer#start_iter (`NAME "start_of_input");
Sentence.tag_all buffer;
(* clear the views *)
messages#clear;
proof#clear ();
clear_info ();
push_info "Restarted";
(* apply the initial commands to coq *)
in
Coq.seq (Coq.lift action) self#initialize
method private include_file_dir_in_path =
let query f =
let dir = Filename.dirname f in
let loadpath = Coq.inloadpath dir in
let next = function
| Interface.Fail (_, s) ->
messages#set
("Could not determine lodpath, this might lead to problems:\n"^s);
Coq.return ()
| Interface.Good true -> Coq.return ()
| Interface.Good false ->
let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
let cmd = Coq.interp 0 cmd in
let next = function
| Interface.Fail (l, str) ->
messages#set ("Couln't add loadpath:\n"^str);
Coq.return ()
| Interface.Good _ ->
Coq.return ()
in
Coq.bind cmd next
in
Coq.bind loadpath next
in
let next () = match get_filename () with
| None -> Coq.return ()
| Some f -> query f
in
Coq.bind (Coq.return ()) next
method initialize =
let next () = Coq.PrintOpt.enforce in
Coq.bind self#include_file_dir_in_path next
end
|