blob: d03c23ab03151ec34c8dcdd660b3be2876bdae0e (
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
|
;;--------------------------------------------------------------------------;;
;;--------------------------------------------------------------------------;;
;; program extraction.
;;
;; note : program extraction is still experimental
;;--------------------------------------------------------------------------;;
(defun af2-compile-theorem(name)
"Interactive function :
ask for the name of a theorem and send a compile command to af2 for it."
(interactive "stheorem : ")
(proof-shell-invisible-command (concat "compile " name ".\n")))
(defun af2-compile-theorem-around-point()
"Interactive function :
send a compile command to af2 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)))
(af2-compile-theorem (buffer-substring start end))))
(setq
af2-forget-id-command "del %s.\n"
af2-forget-new-elim-command "edel elim %s.\n"
af2-forget-new-intro-command "edel intro %s.\n"
af2-forget-new-rewrite-command "edel rewrite %s.\n"
af2-forget-close-def-command "edel closed %s.\n"
af2-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*"
af2-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)"
af2-spaces-regexp "[ \n\t\r]*"
af2-sy-definition-regexp (concat
"\\(Cst\\|def\\)"
af2-comments-regexp
"\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)")
af2-definition-regexp (concat
"\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)"
af2-comments-regexp
af2-ident-regexp)
af2-new-elim-regexp (concat
"new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
af2-ident-regexp)
af2-new-intro-regexp (concat
"new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
af2-ident-regexp)
af2-new-rewrite-regexp (concat
"new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
af2-ident-regexp)
af2-close-def-regexp (concat
"close_def"
af2-comments-regexp
"\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]")
)
(defun af2-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 af2-forget-id-command
(span-property span 'name)) ans)))
((proof-string-match af2-new-elim-regexp str)
(setq ans
(concat (format af2-forget-new-elim-command
(match-string 3 str)) ans)))
((proof-string-match af2-new-intro-regexp str)
(setq ans
(concat (format af2-forget-new-intro-command
(match-string 3 str)) ans)))
((proof-string-match af2-new-rewrite-regexp str)
(setq ans
(concat (format af2-forget-new-rewrite-command
(match-string 3 str)) ans)))
((proof-string-match af2-close-def-regexp str)
(setq ans
(concat (format af2-forget-close-def-command
(match-string 4 str)) ans)))
((proof-string-match af2-sy-definition-regexp str)
(setq ans
(concat (format af2-forget-id-command
(concat "$" (match-string 7 str))) ans)))
((proof-string-match af2-definition-regexp str)
(setq ans (concat (format af2-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 af2-delete-symbol(symbol)
"Interactive function :
ask for a symbol and send a delete command to af2 for it."
(interactive "ssymbol : ")
(proof-shell-invisible-command (concat "del " symbol ".\n")))
(defun af2-delete-symbol-around-point()
"Interactive function :
send a delete command to af2 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)))
(af2-delete-symbol (buffer-substring start end))))
;;
;; Doing commands
;;
(defun af2-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 'af2-fun)
|
