1 files changed, 150 insertions, 0 deletions
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
new file mode 100644
index 00000000..58771057
--- /dev/null
+++ b/phox/phox-fun.el
@@ -0,0 +1,150 @@
+;;--------------------------------------------------------------------------;;
+;;--------------------------------------------------------------------------;;
+;; 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 "[ \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)
+