diff options
author | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2000-09-15 13:04:04 +0000 |
---|---|---|
committer | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2000-09-15 13:04:04 +0000 |
commit | f2809edb93a7dcf06df6b5eb7dfb2452eaeb2136 (patch) | |
tree | f493761a02f32bb37822d5981c06c4b4ab07f37a /af2 | |
parent | eca97d0f816ea5aabd9f80e5c89bae8611fd58e0 (diff) |
usefull function definitions for af2
Diffstat (limited to 'af2')
-rw-r--r-- | af2/af2-fun.el | 159 |
1 files changed, 159 insertions, 0 deletions
diff --git a/af2/af2-fun.el b/af2/af2-fun.el new file mode 100644 index 00000000..3560c7fc --- /dev/null +++ b/af2/af2-fun.el @@ -0,0 +1,159 @@ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; 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-sy-definition-regexp "^[ \t\n\r]*\\(Cst\\|def\\)[ \t\n\r]*\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]*\"\\([^\"]*\\)\\)" + af2-definition-regexp "^[ \t\n\r]*\\(Cst\\|def\\|claim\\|Sort\\)[ \t\n\r]*\\([^ =\\[]*\\)" +) + +(defun string-search (sstr str &optional ipos) + (if str + (let + ((pos (if ipos ipos 0)) (len (length sstr)) (end (- (length str) (length sstr)))) + (if (not pos) (setq pos 0)) + (while (and (<= pos end) + (not (string= sstr (substring str pos (+ pos len))))) + (setq pos (+ pos 1))) + (if (> pos end) nil pos)))) + +(defun proof-remove-comment (str) + (if str (let + ((astr "") + (pos 0) + (lpos 0) + (spos -1) + (epos -1) + (lvl 0)) + (while (or spos epos) + (setq + spos (if (and spos (< spos lpos)) + (string-search proof-comment-start str lpos) spos) + epos (if (and epos (< epos lpos)) + (string-search proof-comment-end str lpos) epos)) + (message (format "pos: %d, spos: %d, epos: %d, astr: %s ///" + pos (if spos spos -1) (if epos epos -1) astr)) + (if (and spos (or (not epos) (< spos epos))) + (progn + (if (= lvl 0) (setq astr + (concat astr + (substring str pos spos)))) + (setq lpos (+ spos 1) lvl (+ lvl 1))) + (if (and epos (> lvl 0)) + (progn + (setq lpos (+ epos 1) lvl (- lvl 1)) + (if (= lvl 0) (setq pos (+ epos 2))))))) + (setq astr (concat astr (substring str pos))) + (message astr) + astr))) + +;(defun proof-string-match-ignore-comments (regexp str matchpos) +; (let +; (pos (proof-string-match regexp (proof-remove-comment str))) +; (if pos (string-match matchpos str) nil))) + +(defun af2-find-and-forget (span) + (let (str ans tmp) + (while span + (setq str (proof-remove-comment (span-property span 'cmd))) + (cond + + ((eq (span-property span 'type) 'comment)) + + ((eq (span-property span 'type) 'goalsave) + (setq ans (concat ans + (format af2-forget-id-command + (span-property span 'name))))) + + ((proof-string-match af2-sy-definition-regexp str) + (message "sy-definition:") + (message tmp) + (setq ans + (concat ans (format af2-forget-id-command + (concat "$" (match-string 4 str)))))) + + ((proof-string-match af2-definition-regexp str) + (message "definition:") + (message tmp) + (setq ans (concat ans (format af2-forget-id-command + (match-string 2 str)))))) + + + (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)))) + +;; retract current goal + +(defun proof-retract-current-goal () + "Retract the current proof, and move point to its start." + (interactive) + (proof-maybe-save-point + (let + ((span (proof-last-goal-or-goalsave))) + (if (and span (not (eq (span-property span 'type) 'goalsave)) + (< (span-end span) (proof-unprocessed-begin))) + (progn + (goto-char (span-start span)) + (proof-retract-until-point-interactive) + (proof-maybe-follow-locked-end)) + (error "Not proving"))))) + +(require 'proof-script) + +(proof-define-assistant-command-witharg proof-find-string-in-names + "Search for items containing a given string in their names." + proof-find-string-in-names-command + "Find item with name containing" + (proof-shell-invisible-command arg)) + +(provide 'af2-fun)
\ No newline at end of file |