blob: 3f87d8b2646a929973adea696df00499d96b8941 (
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
|
;; pbp.el Major mode for proof by pointing
;; Subpackage of proof
;; Copyright (C) 1996 LFCS Edinburgh & INRIA Sophia Antipolis
;; Author: Yves Bertot < Yves.Bertot@sophia.inria.fr>
;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
;; Time-stamp: <05 Dec 96 tms /home/tms/elisp/pbp.el>
;; Reference: Yves Bertot and Laurent Théry
;; A Generic Approach to Building User Interfaces for
;; Theorem Provers
;; J. Symbolic Computation (1996)
;; Accepted for Publication
; The text structure is supposed to be given by annotations of the
; form %annotation text|annotated text@, The % and @ signs act as
; opening and closing parentheses, so that the annotated text may itself
; contain extra annotations. Analysing this structure yields the
; uncorrupted text (only "annotated text"), but the annotation are recorded
; into Emacs Extents that span over the text.
;To construct these extents, one scans the whole text for the characters
; % and @. When finding a %, its location is simply kept on a stack
; *location-stack*. When finding a @, one looks in the stack to get
; the position of the last % and creates an extent with these two positions.
; The annotation is then removed and stored in the extent's properties
; and the last bits are cleared.
(require 'proof)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Variables used by pbp, all auto-buffer-local ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(deflocal pbp-annotation-char ?@ "Annotation Mark")
(deflocal pbp-goal-char ?g "goal mark")
(deflocal pbp-start-char ?s "annotation start")
(deflocal pbp-end-char ?e "annotation end")
(deflocal pbp-field-char ?x "annotated field end")
(deflocal pbp-wakeup-character "\t"
"A character terminating the prompt in annotation mode")
(deflocal pbp-assumption-regexp nil
"A regular expression matching the name of assumptions.")
(deflocal pbp-goal-regexp nil
"A regular expressin matching the identifier of a goal.")
(deflocal pbp-annotated-prompt-string "Lego> \t"
"Annotated prompt pattern")
(deflocal pbp-start-goals-string "@s Start of Goals @e"
"String indicating the start of the proof state.")
(deflocal pbp-end-goals-string "@s End of Goals @e"
"String indicating the end of the proof state.")
(deflocal pbp-goal-command "Pbp %s;"
"Command informing the prover that `pbp-buttion-action' has been
requested on a goal.")
(deflocal pbp-hyp-command "PbpHyp %s;"
"Command informing the prover that `pbp-buttion-action' has been
requested on an assumption.")
(deflocal pbp-result-start "@s Pbp result @e"
"String indicating the start of an output from the prover following
a `pbp-goal-command' or a `pbp-hyp-command'.")
(deflocal pbp-result-end "@s End Pbp result @e"
"String indicating the end of an output from the prover following a
`pbp-goal-command' or a `pbp-hyp-command'.")
(deflocal pbp-script-buffer nil
"The buffer in which commands corresponding to proof-by-pointing
actions will be recorded. The proof process is responsible for
updating this variable")
(deflocal pbp-goals-buffer-name nil
"The name of the buffer in which goals are displayed in pbp mode")
(deflocal pbp-goals-buffer nil
"The buffer in which goals are displayed in pbp mode")
(deflocal pbp-regexp-noise-goals-buffer nil
"Unwanted information output from the proof process within
`pbp-start-goals-string' and `pbp-end-goals-string'.")
(deflocal pbp-keymap (make-keymap 'Pbp-keymap)
"Keymap for pbp mode")
(define-key pbp-keymap 'button2 'pbp-button-action)
(deflocal pbp-mode-is nil
"The actual mode for Proof-by-Pointing.")
(defun pbp-make-top-extent (start end)
(let (extent name)
(goto-char start)
(setq name (cond ((looking-at pbp-goal-regexp)
(cons 'goal (match-string 1)))
((looking-at pbp-assumption-regexp)
(cons 'hyp (match-string 1)))))
(beginning-of-line)
(setq start (point))
(goto-char end)
(beginning-of-line)
(backward-char)
(setq extent (make-extent start (point)))
(set-extent-property extent 'mouse-face 'highlight)
(set-extent-property extent 'keymap pbp-keymap)
(set-extent-property extent 'pbp-top-element name)))
(defun pbp-analyse-structure (string)
(save-excursion
(let* ((ip 0) (op 0) (l (length string)) (stack ()) (topl ()) ext n
(out (make-string l ?x )) )
(while (< ip l)
(if (not (char-equal (aref string ip) pbp-annotation-char))
(progn (aset out op (aref string ip))
(setq op (+ 1 op)))
(setq ip (+ 1 ip))
(cond
((char-equal (aref string ip) pbp-goal-char)
(setq topl (append topl (list (+ 1 op)) )))
((char-equal (aref string ip) pbp-start-char)
(setq n (setq ip (+ 1 ip)))
(while (not (char-equal (aref string ip) pbp-annotation-char))
(setq ip (+ 1 ip)))
(setq stack (cons op (cons (substring string n ip) stack)))
(setq ip (+ 1 ip)))
((char-equal (aref string ip) pbp-field-char)
(setq ext (make-extent (car stack) op out))
(set-extent-property ext 'mouse-face 'highlight)
(set-extent-property ext 'keymap pbp-keymap)
(set-extent-property ext 'pbp (cadr stack))
(set-extent-property ext 'duplicable t)
(setq stack (cddr stack)))))
(setq ip (+ 1 ip)))
(pop-to-buffer pbp-goals-buffer)
(erase-buffer)
(insert (substring out 0 op))
(while (setq ip (car topl)
topl (cdr topl))
(pbp-make-top-extent ip (car topl)))
(pbp-make-top-extent ip (point-max)))))
; Receiving the data from Lego is performed that a filter function
; added among the comint-output-filter-functions of the shell-mode.
(deflocal pbp-mark-ext nil "last mark")
(deflocal pbp-sanitise t "sanitise output?")
(defun pbp-sanitise-string (string)
(if pbp-sanitise
(let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x )))
(while (< ip l)
(if (char-equal (aref string ip) pbp-annotation-char)
(if (char-equal (aref string (setq ip (+ 1 ip)))
pbp-start-char)
(progn
(while (not (char-equal (aref string ip)
pbp-annotation-char))
(setq ip (+ 1 ip)))
(setq ip (+ 1 ip))))
(aset out op (aref string ip))
(setq op (+ 1 op)))
(setq ip (+ 1 ip)))
(substring out 0 op))
string))
(defun pbp-display-error (string)
(save-excursion
(pop-to-buffer pbp-goals-buffer)
(goto-char (point-max))
(if (re-search-backward proof-error-regexp nil t)
(delete-region (- (point) 2) (point-max)))
(newline 2)
(insert-string string)))
(defun pbp-send-and-remember (string)
(save-excursion
(proof-simple-send string)
(if (and (boundp 'pbp-script-buffer) pbp-script-buffer)
(progn (set-buffer pbp-script-buffer)
(end-of-buffer)
(insert-string string)))))
(defun pbp-process-string (string)
(let (start end)
(save-excursion
(cond
((string-match proof-error-regexp string)
(pbp-display-error
(pbp-sanitise-string (substring string (match-beginning 0)))))
((string-match proof-shell-abort-goal-regexp string)
(erase-buffer pbp-goals-buffer))
((string-match proof-shell-proof-completed-regexp string)
(erase-buffer pbp-goals-buffer)
(insert-string (concat "\n" (match-string 0 string)) pbp-goals-buffer))
((string-match pbp-start-goals-string string)
(while (progn (setq start (match-end 0))
(string-match pbp-start-goals-string string start)))
(string-match pbp-end-goals-string string start)
(setq end (match-beginning 0))
(pbp-analyse-structure (substring string start end)))
((string-match pbp-result-start string)
(setq start (+ 1 (match-end 0)))
(string-match pbp-result-end string)
(setq end (- (match-beginning 0) 1))
(pbp-send-and-remember (substring string start end)))))))
(defun pbp-filter (str)
(if (string-match pbp-wakeup-character str)
(save-excursion
(set-buffer (proof-shell-buffer))
(let (string mrk)
(while (progn (goto-char (extent-start-position pbp-mark-ext))
(setq mrk (point-marker))
(search-forward pbp-annotated-prompt-string nil t))
(set-extent-endpoints pbp-mark-ext (point) (point))
(backward-char (length pbp-annotated-prompt-string))
(setq string (buffer-substring mrk (point)))
(delete-region mrk (point))
(insert (pbp-sanitise-string string))
(goto-char (extent-start-position pbp-mark-ext))
(backward-delete-char 1)
(pbp-process-string string))))))
; Call after the shell is started
(defun pbp-goals-init ()
(save-excursion
(setq pbp-goals-buffer (get-buffer-create pbp-goals-buffer-name ))
(set-buffer pbp-goals-buffer)
(funcall pbp-mode-is)
(erase-buffer pbp-goals-buffer)
(add-hook 'comint-output-filter-functions 'pbp-filter t)
(set-buffer (proof-shell-buffer))
(setq pbp-mark-ext (make-extent (point-max) (point-max)))
(set-extent-property pbp-mark-ext 'detachable nil)
(set-extent-property pbp-mark-ext 'start-open nil)
(set-extent-property pbp-mark-ext 'end-open t)
(add-hook 'proof-shell-exit-hook
(lambda ()
(remove-hook 'comint-output-filter-functions 'pbp-filter)))))
; Now, using the extents in a mouse behavior is quite simple:
; from the mouse position, find the relevant extent, then get its annotation
; and produce a piece of text that will be inserted in the right buffer.
; Attaching this behavior to the mouse is simply done by attaching a keymap
; to all the extents.
(defun pbp-button-action (event)
(interactive "e")
(mouse-set-point event)
(pbp-construct-command))
(defun pbp-construct-command ()
(let ((ext (extent-at (point) () 'pbp))
(top-ext (extent-at (point) () 'pbp-top-element)))
(cond ((and (extentp top-ext) (extentp ext))
(let* ((top-info (extent-property top-ext 'pbp-top-element))
(path
(concat (cdr top-info) " " (extent-property ext 'pbp))))
(proof-command
(if (eq 'hyp (car top-info))
(format pbp-hyp-command path)
(format pbp-goal-command path)))))
((extentp top-ext)
(let ((top-info (extent-property top-ext 'pbp-top-element)))
(if (eq 'hyp (car top-info))
(proof-command (format pbp-hyp-command (cdr top-info)))
(pbp-send-and-remember
(format proof-shell-change-goal (cdr top-info)))))))))
(define-derived-mode pbp-mode fundamental-mode "Pbp" "Proof by Pointing"
(suppress-keymap pbp-mode-map))
(provide 'pbp)
|