blob: 0e82b1d3cad6aa7c5992178709bb5ebfe0156ae7 (
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
|
;;--------------------------------------------------------------------------;;
;;--------------------------------------------------------------------------;;
;; program extraction.
;;
;; note : program extraction is still experimental
;;--------------------------------------------------------------------------;;
(defun phox-compile-theorem(name)
"Interactive function :
ask for the name of a theorem and send a compile command to PhoX for it."
(interactive "stheorem : ")
(proof-shell-invisible-command (concat "compile " name ".\n")))
(defun phox-compile-theorem-around-point()
"Interactive function :
send a compile command to PhoX for the theorem which name is under the cursor."
(interactive)
(let (start end)
(save-excursion
(forward-word 1)
(setq start (point))
(forward-word -1)
(setq end (point)))
(phox-compile-theorem (buffer-substring start end))))
(setq
phox-forget-id-command "del %s.\n"
phox-forget-new-elim-command "edel elim %s.\n"
phox-forget-new-intro-command "edel intro %s.\n"
phox-forget-new-rewrite-command "edel rewrite %s.\n"
phox-forget-close-def-command "edel closed %s.\n"
; phox-comments-regexp : a sequence of comments and white spaces
phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*"
; phox-strict-comments-regexp : a not empty sequence of comments and white spaces
phox-strict-comments-regexp "\\([ \n\t\r]+\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*\\|\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)+\\)"
phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)"
phox-spaces-regexp "[ \n\t\r]*"
phox-sy-definition-regexp (concat
"\\(Cst\\|def\\)"
phox-comments-regexp
"\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)")
phox-definition-regexp (concat
"\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)"
phox-comments-regexp
phox-ident-regexp)
phox-new-elim-regexp (concat
"new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
phox-ident-regexp)
phox-new-intro-regexp (concat
"new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
phox-ident-regexp)
phox-new-rewrite-regexp (concat
"new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
phox-ident-regexp)
phox-close-def-regexp (concat
"close_def"
phox-comments-regexp
"\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]")
)
(defun phox-find-and-forget (span)
(let (str ans tmp (lsp -1))
(while span
(setq str (span-property span 'cmd))
(cond
((eq (span-property span 'type) 'comment))
((eq (span-property span 'type) 'goalsave)
(setq ans (concat (format phox-forget-id-command
(span-property span 'name)) ans)))
((proof-string-match phox-new-elim-regexp str)
(setq ans
(concat (format phox-forget-new-elim-command
(match-string 3 str)) ans)))
((proof-string-match phox-new-intro-regexp str)
(setq ans
(concat (format phox-forget-new-intro-command
(match-string 3 str)) ans)))
((proof-string-match phox-new-rewrite-regexp str)
(setq ans
(concat (format phox-forget-new-rewrite-command
(match-string 3 str)) ans)))
((proof-string-match phox-close-def-regexp str)
(setq ans
(concat (format phox-forget-close-def-command
(match-string 4 str)) ans)))
((proof-string-match phox-sy-definition-regexp str)
(setq ans
(concat (format phox-forget-id-command
(concat "$" (match-string 7 str))) ans)))
((proof-string-match phox-definition-regexp str)
(setq ans (concat (format phox-forget-id-command
(match-string 6 str)) ans))))
(setq lsp (span-start span))
(setq span (next-span span 'type)))
(or ans proof-no-command)))
;;--------------------------------------------------------------------------;;
;;
;; Deleting symbols
;;
;;--------------------------------------------------------------------------;;
(defun phox-delete-symbol(symbol)
"Interactive function :
ask for a symbol and send a delete command to PhoX for it."
(interactive "ssymbol : ")
(proof-shell-invisible-command (concat "del " symbol ".\n")))
(defun phox-delete-symbol-around-point()
"Interactive function :
send a delete command to PhoX for the symbol whose name is under the cursor."
(interactive)
(let (start end)
(save-excursion
(forward-word -1)
(setq start (point))
(forward-word 1)
(setq end (point)))
(if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1)))
(phox-delete-symbol (buffer-substring start end))))
;;
;; Doing commands
;;
(defun phox-assert-next-command-interactive ()
"Process until the end of the next unprocessed command after point.
If inside a comment, just process until the start of the comment."
(interactive)
(message "test")
(if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n"))
(proof-with-script-buffer
(proof-maybe-save-point
(goto-char (proof-queue-or-locked-end))
(proof-assert-next-command))
(proof-maybe-follow-locked-end)))
(provide 'phox-fun)
|
