From de92628f356fabdc5c1d59d85e0891b5f8969273 Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Thu, 18 Jan 2001 15:02:35 +0000 Subject: *** empty log message *** --- phox/phox-extraction.el | 170 ++++++++++++++++++++++++++++++++++++++++++++++++ phox/phox-fun.el | 83 ++++++++++++----------- phox/phox-tags.el | 40 +++++++++++- phox/phox.el | 39 +++++------ 4 files changed, 263 insertions(+), 69 deletions(-) create mode 100644 phox/phox-extraction.el (limited to 'phox') diff --git a/phox/phox-extraction.el b/phox/phox-extraction.el new file mode 100644 index 00000000..b488d43e --- /dev/null +++ b/phox/phox-extraction.el @@ -0,0 +1,170 @@ +;; $State$ $Date$ $Revision$ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; program extraction. +;; +;; note : program extraction is still experimental This file is very +;; dependant of the actual state of program extraction in phox. +;;--------------------------------------------------------------------------;; +;; configuration : + +(defvar phox-prog-orig "phox -pg" "original name of phox binary.") + +(defun phox-prog-flags-modify(option) +"ask for a string that are options to pass to phox binary" +(interactive "soption :") +; pas d'analyse de la réponse, +(let ((process)) + (if (and phox-prog-name + (progn (string-match " \\|$" phox-prog-name) + (setq process + (substring phox-prog-name 0 (match-beginning 0)) + ) + ) + (processp (get-process process)) + (eq (process-status process) 'run)) + (error "Error : exit phox process first !") + ) +(if (string-match "^ *$" option) + (progn + (message + "no option other than default ones will be passed to phox binary.") + (setq phox-prog-name phox-prog-orig)) + (progn + (message (format "option %s will be passed to phox binary." option )) + (setq phox-prog-name (concat phox-prog-orig " " option)) + ) + ) +) +) + + +(defun phox-prog-flags-extract() +"pass option -f to phox binary. A program can be extracted from +proof of theorem_name with : +compile theorem_name. +output." +(interactive) +(phox-prog-flags-modify "-f") +(message +"WARNING : program extraction is experimental and can disturb the prover !") +) + +(defun phox-prog-flags-erase() +"no option to phox binary." +(interactive) +(phox-prog-flags-modify "")) + +; encore une fonction qui devrait être redéfinie en cas d'autres +; options possibles que -f + +(defun phox-toggle-extraction() +"toggle between extraction mode and ordinary mode for phox process." +(interactive) +(cond ((string-equal phox-prog-name phox-prog-orig) ;; à améliorer (espaces) + (phox-prog-flags-extract)) + ((string-match "\-f$" phox-prog-name) (phox-prog-flags-erase)) + (t (error "option must be empty or -f, use phox-prog-flags-modify."))) +) + +;; commands + +; compilation +(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))) + +(defun phox-compile-theorem-on-cursor() +"Interactive function : +send a compile command to PhoX for the theorem which name is under the cursor." + (interactive) + (let (start end) + (save-excursion +; (modify-syntax-entry ?\. "w") + (forward-word 1) + (setq start (point)) + (forward-word -1) + (setq end (point))) + (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) + (phox-compile-theorem (buffer-substring start end)))) + +; extraction + +(defun phox-output () + +"Interactive function : +send output command to phox in order to obtain programs +extracted from proofs of all compiled theorems." + + +(interactive) +(proof-shell-invisible-command "output")) + +(defun phox-output-theorem (name) +"Interactive function : +ask for the name of a theorem and send an output command to PhoX for it +in order to obtain a programm extracted from the known proof of this theorem." + (interactive "stheorem : ") + (proof-shell-invisible-command (concat "output " name))) + +(defun phox-output-theorem-on-cursor() +"Interactive function : +send an output command to PhoX for the theorem which name is under the cursor +in order to obtain a programm extracted from the known proof of this theorem." + (interactive) + (let (start + end +; (syntax (char-to-string (char-syntax ?\.))) + ) + (save-excursion +; (modify-syntax-entry ?\. "w") ; à modifier globablement ? + (forward-word 1) + (setq start (point)) + (forward-word -1) + (setq end (point))) +; (modify-syntax-entry ?\. syntax) + (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) + (phox-output-theorem (buffer-substring start end)))) + +; Definitions of lambda-mu terms (tdef nom_de_term = terme.) and +; normalization (eval term.) have to be "visible" proof commands. + +;; menu + + (defvar phox-extraction-menu + '("Extraction" + ["Program extraction enabled" + phox-toggle-extraction + :style radio + :selected(string-match "\-f$" phox-prog-name) + ] + ["------------------------------" nil nil + ] + ["Compile theorem on cursor" phox-compile-theorem-on-cursor + :active(string-match "\-f$" phox-prog-name) + ] + ["Extraction for theorem on cursor" phox-output-theorem-on-cursor + :active(string-match "\-f$" phox-prog-name) + ] + ["Extraction for all compiled theorems" phox-output + :active(string-match "\-f$" phox-prog-name) + ] + ["------------------------------" nil nil + ] + ["Compile theorem : " phox-compile-theorem + :active(string-match "\-f$" phox-prog-name) + ] + ["Extraction for theorem : " phox-output-theorem + :active(string-match "\-f$" phox-prog-name) + ] + ) +"A list of menu items to deal with program extraction. +Warning, program extraction is still experimental +and can disturb the prover !" +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(provide 'phox-extraction) diff --git a/phox/phox-fun.el b/phox/phox-fun.el index 1c2735dd..f1ffa464 100644 --- a/phox/phox-fun.el +++ b/phox/phox-fun.el @@ -1,28 +1,5 @@ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; 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)))) - +;; $State$ $Date$ $Revision$ +;; syntax (setq phox-forget-id-command "del %s.\n" @@ -59,6 +36,23 @@ send a compile command to PhoX for the theorem which name is under the cursor." "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]") ) + +(defun phox-init-syntax-table () + "Set appropriate values for syntax table in current buffer." +;; useful for using forward-word + (modify-syntax-entry ?_ "w") + (modify-syntax-entry ?\. "w") +;; Configure syntax table for block comments + (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4") +;; à compléter éventuellement +) + + + + + (defun phox-find-and-forget (span) (let (str ans tmp (lsp -1)) (while span @@ -107,20 +101,37 @@ send a compile command to PhoX for the theorem which name is under the cursor." (or ans proof-no-command))) +;; +;; 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))) + + ;;--------------------------------------------------------------------------;; ;; ;; Deleting symbols ;; ;;--------------------------------------------------------------------------;; - +;; obsolète probablement, sinon à modifier pour en étendre la portée. (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"))) + (proof-shell-invisible-command (concat "del " symbol))) -(defun phox-delete-symbol-around-point() +(defun phox-delete-symbol-on-cursor() "Interactive function : send a delete command to PhoX for the symbol whose name is under the cursor." (interactive) @@ -133,21 +144,9 @@ send a delete command to PhoX for the symbol whose name is under the cursor." (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) + diff --git a/phox/phox-tags.el b/phox/phox-tags.el index f2b5959a..c983c347 100644 --- a/phox/phox-tags.el +++ b/phox/phox-tags.el @@ -1,3 +1,4 @@ +;; $State$ $Date$ $Revision$ ;;--------------------------------------------------------------------------;; ;;--------------------------------------------------------------------------;; ;; gestion des TAGS @@ -26,7 +27,7 @@ ; gnu emacs (if (member table tags-table-list) (message (concat table " already loaded.")) -; (make-local-variable 'tags-table-list) ; ne focntionne pas +; (make-local-variable 'tags-table-list) ; ne fonctionne pas (setq tags-table-list (cons table tags-table-list)) ) ) @@ -51,7 +52,7 @@ (defun phox-tags-add-lib-table() "Add tags in libraries." (interactive) - (phox-tags-add-table (concat phox-lib-dir "TAGS")) + (phox-tags-add-table (concat phox-lib-dir "/TAGS")) ) (defun phox-tags-add-local-table() @@ -70,8 +71,41 @@ (file-name-nondirectory (buffer-file-name)))) ) + +(defun phox-complete-tag() +"Complete symbol using tags table. Works with FSF emacs. + Problems with xemacs." +;; xemacs build a table for completion, tag-completion-table +;; this table donnot contains key words that use ".", probably a +;; problem with syntax table. + +(if proof-running-on-XEmacs + (complete-tag) + (tag-complete-symbol))) + +;; menu + +(defvar phox-tags-menu + '("Tags" + ["create a tags table for local buffer" phox-tags-create-local-table t] + ["------------------" nil nil] + ["add table" phox-tags-add-table t] + ["add local table" phox-tags-add-local-table t] + ["add table for libraries" phox-tags-add-lib-table t] + ["add table for text doc" phox-tags-add-doc-table t] + ["reset tags table list" phox-tags-reset-table t] + ["------------------" nil nil] + ["Find theorem, definition ..." find-tag t] + ["complete theorem, definition ..." phox-complete-tag t] + ) +"Phox menu for dealing with tags" +) + ;; default (if phox-tags-doc (add-hook 'phox-mode-hook 'phox-tags-add-doc-table)) -(provide 'phox-tags) \ No newline at end of file +(provide 'phox-tags) + + + diff --git a/phox/phox.el b/phox/phox.el index 0341b664..1a2ade5e 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -1,3 +1,5 @@ +;; $State$ $Date$ $Revision$ + (require 'proof) ; load generic parts ;; Adjust toolbar entries. (Must be done @@ -71,6 +73,7 @@ :type 'string :group 'phox-config) +(require 'phox-extraction) (require 'phox-tags) (require 'phox-outline) (require 'phox-font) @@ -79,25 +82,15 @@ ;; ----- PhoX specific menu (defpgdefault menu-entries - '( - ["Delete symbol around cursor" phox-delete-symbol-around-point t] - ["Delete symbol" phox-delete-symbol t] - ["Compile theorem under cursor" phox-compile-theorem-around-point t] - "----" - ("Tags" - ["create a tags table for local buffer" phox-tags-create-local-table t] - ["------------------" nil nil] -; ["load table" phox-tags-load-table t] - ["add table" phox-tags-add-table t] - ["add local table" phox-tags-add-local-table t] - ["add table for libraries" phox-tags-add-lib-table t] - ["add table for text doc" phox-tags-add-doc-table t] - ["reset tags table list" phox-tags-reset-table t] - ["------------------" nil nil] - ["Find theorem, definition ..." find-tag t] - ["complete theorem, definition ..." complete-tag t] - ) - )) + (cons + phox-tags-menu + (cons + phox-extraction-menu +;; not useful ? +; '(["Delete symbol around cursor" phox-delete-symbol-around-point t] +; ["Delete symbol" phox-delete-symbol t]) + nil)) + ) ;; ;; ======== Configuration of generic modes ======== @@ -139,6 +132,7 @@ proof-auto-multiple-files nil font-lock-keywords phox-font-lock-keywords ) + (phox-init-syntax-table) ) (defun phox-shell-config () @@ -177,11 +171,8 @@ ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed" (define-key phox-mode-map [(control c) (meta d)] - 'phox-delete-symbol-around-point) - ;; Configure syntax table for block comments - (modify-syntax-entry ?\* ". 23") - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) + 'phox-delete-symbol-on-cursor) +) (define-derived-mode phox-shell-mode proof-shell-mode "PhoX shell" nil -- cgit v1.2.3