diff options
Diffstat (limited to 'phox/phox-pbrpm.el')
-rw-r--r-- | phox/phox-pbrpm.el | 318 |
1 files changed, 0 insertions, 318 deletions
diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el deleted file mode 100644 index 544fa1c4..00000000 --- a/phox/phox-pbrpm.el +++ /dev/null @@ -1,318 +0,0 @@ -;; $State$ $Date$ $Revision$ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; the proof by rules popup menu part -;; -;; Note : program extraction is still experimental This file is very -;; dependant of the actual state of our developments -;;--------------------------------------------------------------------------;; - -(require 'pg-pbrpm) - -(declare-function phox-lang-absurd "nofile") -(declare-function phox-lang-suppress "nofile") -(declare-function phox-lang-instance "nofile") -(declare-function phox-lang-open-instance "nofile") -(declare-function phox-lang-opendef "nofile") -(declare-function phox-lang-unlock "nofile") -(declare-function phox-lang-lock "nofile") -(declare-function phox-lang-prove "nofile") -(declare-function phox-lang-let "nofile") -(declare-function int-char "nofile") -(declare-function char= "nofile") - -;;--------------------------------------------------------------------------;; -;; Syntactic functions -;;--------------------------------------------------------------------------;; -(setq - pg-pbrpm-start-goal-regexp "^goal \\([0-9]+\\)/[0-9]+\\( (new)\\)?$" - pg-pbrpm-start-goal-regexp-par-num 1 - pg-pbrpm-end-goal-regexp "^$" - pg-pbrpm-start-hyp-regexp "^\\([A-Za-z0-9_.']+\\) := " - pg-pbrpm-start-hyp-regexp-par-num 1 - pg-pbrpm-start-concl-regexp "^ *|- " - pg-pbrpm-auto-select-regexp "\\(\\(\\(['a-zA-Z0-9]+\\)\\|\\([][><=/~&+*^%!{}:-]+\\)\\)\\(_+\\(\\(['a-zA-Z0-9]+\\)\\|\\([][><=/~&+*^%!{}:-]+\\)\\)\\)*\\)\\|\\(\\?[0-9]+\\)" -) - - -; TODO : deal with future invisible parentheses (french guillemots) -(defun phox-pbrpm-left-paren-p (char) -"Retrun t if the character is a left parenthesis : '(' or a french guillemot '<<'" - (or - (char-equal char (int-char 40)) - (char-equal char (int-char 171))) -) - -(defun phox-pbrpm-right-paren-p (char) -"Retrun t if the character is a right parenthesis ')' or a french guillemot '>>'" - (or - (char-equal char (int-char 41)) - (char-equal char (int-char 187))) -) - - -(defun phox-pbrpm-menu-from-string (order str) - "build a menu from a string send by phox" - (setq str (proof-shell-invisible-cmd-get-result str)) - (if (string= str "") nil - (mapcar - (lambda (s) (append (list order) (split-string s "\\\\-") - (list 'phox-pbrpm-rename-in-cmd))) - (split-string str "\\\\\\\\")))) - -(defun phox-pbrpm-rename-in-cmd (cmd spans) - (let ((modified nil) (prev 0)) - (mapc (lambda (span) - (if (not (string= (span-property span 'original-text) - (span-string span))) - (setq modified (cons span modified)))) spans) - (setq modified (reverse modified)) - (if modified - (progn - (if (= 0 (span-property (car modified) 'goalnum)) - (progn - (while (and modified (= 0 (span-property (car modified) 'goalnum))) - (let ((span (pop modified))) - (setq cmd (concat cmd ";; rename " - (span-property span 'original-text) " " - (span-string span))))) - (if modified (setq cmd (concat "(" cmd ")"))))) - (if modified (setq cmd (concat cmd ";; "))) - (while modified - (let* ((span (pop modified)) - (goalnum (span-property span 'goalnum))) - (while (< (+ prev 1) goalnum) - (setq cmd (concat cmd "idt @+@ ")) - (setq prev (+ prev 1))) - (setq cmd (concat cmd "(rename " (span-property span 'original-text) " " - (span-string span))) - (setq prev goalnum) - (if (or (not modified) (< goalnum (span-property (car modified) 'goalnum))) - (setq cmd (concat cmd ") @+@ ")) - (setq cmd (concat cmd ";; "))))) - (if (> prev 0) (setq cmd (concat cmd "idt")))))) - cmd) - -(defun phox-pbrpm-get-region-name (region-info) - (if (= (nth 0 region-info) 1) (nth 1 region-info) (nth 2 region-info))) - -(defun phox-pbrpm-escape-string (str) - "add escape char '\'" - (concat "\"" (replace-regexp-in-string "\\\\" "\\\\\\\\" str) "\"")) - -(defun phox-pbrpm-generate-menu (click-infos region-infos) -"Use informations to build a list of (name , rule)" - ;click-infos = (goal-number, "whole"/hyp-name/"none", expression, depth-tree-list) - ;region-infos = idem if in the goal buffer, (0, "none", expression, nil ) if in another buffer, do not display if no region available. - - (let - ((pbrpm-rules-list nil) - (goal-prefix - (if (= (nth 0 click-infos) 1) "" - (concat "[" - (int-to-string (nth 0 click-infos)) - "] ")))) - - - ; the first goal is the selected one by default, so we prefer not to display it. - - ; if clicking in a conclusion with no selection - (if (and (string= (nth 1 click-infos) "none") (not region-infos)) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list - (list 4 (phox-lang-absurd) (concat goal-prefix "by_absurd;; elim False"))) - (phox-pbrpm-menu-from-string 0 - (concat "menu_intro " - (int-to-string (nth 0 click-infos)))) - (phox-pbrpm-menu-from-string 0 - (concat "menu_evaluate " - (int-to-string (nth 0 click-infos)))) - ); end append - );end setq - );end if - - ; if clicking a conclusion with a selection - (if (and (string= (nth 1 click-infos) "none") region-infos) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (phox-pbrpm-menu-from-string 0 - (concat "menu_intro " - (int-to-string (nth 0 click-infos)) - (let ((tmp "")) - (mapc (lambda (region-info) - (setq tmp - (concat tmp " " (phox-pbrpm-escape-string (nth 2 region-info))))) - region-infos) - tmp))) - (phox-pbrpm-menu-from-string 1 - (concat "menu_rewrite " - (int-to-string (nth 0 click-infos)) " " - (let ((tmp "")) - (mapc (lambda (region-info) - (setq tmp - (concat tmp " " (phox-pbrpm-escape-string (phox-pbrpm-get-region-name region-info))))) - region-infos) - tmp)))))) - - ; if clicking in an hypothesis with no selection - (if (and - (not (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole"))) - (or (string= "" (nth 2 click-infos)) (not (char= (string-to-char (nth 2 click-infos)) ??))) - (not region-infos)) - (let ((r (proof-shell-invisible-cmd-get-result (concat "is_hypothesis " - (int-to-string (nth 0 click-infos)) - " " - (phox-pbrpm-escape-string (nth 1 click-infos)))))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (if (char= (string-to-char r) ?t) - (list - (list 9 (phox-lang-suppress (nth 1 click-infos)) - (concat "[" (int-to-string (nth 0 click-infos)) "] " - "rmh " (nth 1 click-infos)))) - nil) - (phox-pbrpm-menu-from-string 1 - (concat "menu_elim " - (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos))) - (phox-pbrpm-menu-from-string 1 - (concat "menu_evaluate_hyp " - (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos))) - (phox-pbrpm-menu-from-string 0 - (concat "menu_left " - (int-to-string (nth 0 click-infos)) - " " - (nth 1 click-infos))))))) - - ; if clicking on an hypothesis with a selection - (if (and - (not (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole"))) - region-infos) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (phox-pbrpm-menu-from-string 1 - (concat "menu_apply " - (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos) - (let ((tmp "")) - (mapc (lambda (region-info) - (setq tmp - (concat tmp " " (phox-pbrpm-escape-string (nth 2 region-info))))) - region-infos) - tmp))) - (phox-pbrpm-menu-from-string 1 - (concat "menu_rewrite_hyp " - (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos) - (let ((tmp "")) - (mapc (lambda (region-info) - (setq tmp - (concat tmp " " (phox-pbrpm-escape-string (phox-pbrpm-get-region-name region-info))))) - region-infos) - tmp)))))) - - (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??) - region-infos (not (cdr region-infos))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (concat - (phox-lang-instance (nth 2 click-infos)) - (nth 2 (car region-infos))) - (concat - "instance " - (nth 2 click-infos) - " " - (nth 2 (car region-infos)))))))) - - (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??) - (not region-infos)) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (concat - (phox-lang-open-instance (nth 2 click-infos))) - (concat - "instance " - (nth 2 click-infos) - " ") - (lambda (cmd spans) - (let ((span (pop spans))) - (concat cmd " " (span-string span))))))))) - - ; is clicking on a token with no selection - (if (and (not region-infos) (not (string= (nth 2 click-infos) ""))) - (let ((r (proof-shell-invisible-cmd-get-result (concat "is_definition " - (int-to-string (nth 0 click-infos)) - " " - (phox-pbrpm-escape-string (nth 2 click-infos))))) - (ri (proof-shell-invisible-cmd-get-result (concat "is_definition " - (int-to-string (nth 0 click-infos)) - " " - (phox-pbrpm-escape-string (concat "$" (nth 2 click-infos))))))) - (if (or (char= (string-to-char r) ?t) (char= (string-to-char ri) ?t)) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 1 (concat - (phox-lang-opendef) - (nth 2 click-infos)) - (concat - goal-prefix - (if (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole")) - "unfold -ortho " - (concat "unfold_hyp " (nth 1 click-infos) " -ortho ")) - "$" - (nth 2 click-infos)))))) - (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??)) - (let ((r (proof-shell-invisible-cmd-get-result (concat "is_locked " - (nth 2 click-infos))))) - (if (char= (string-to-char r) ?t) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (phox-lang-unlock (nth 2 click-infos)) - (concat - goal-prefix - "unlock " - (nth 2 click-infos)))))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (phox-lang-lock (nth 2 click-infos)) - (concat - goal-prefix - "lock " - (nth 2 click-infos)))))))))))) - - (let ((arg (if (and region-infos (not (cdr region-infos))) (nth 2 (car region-infos)) " "))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list - (list 10 "Trivial ?" (concat goal-prefix "trivial")) - (list 10 (phox-lang-prove arg) (concat goal-prefix "prove") - (lambda (cmd spans) - (let ((span (pop spans))) - (concat cmd " " (span-string span))))) - (list 10 (phox-lang-let arg) (concat goal-prefix "local") - (lambda (cmd spans) - (let ((span1 (pop spans)) (span2 (pop spans))) - (concat cmd " " (span-string span1) " = "(span-string span2))))))))) - - pbrpm-rules-list -)) - - -;;--------------------------------------------------------------------------;; -;; phox specific functions -;;--------------------------------------------------------------------------;; - -(defalias 'proof-pbrpm-generate-menu 'phox-pbrpm-generate-menu) -(defalias 'proof-pbrpm-left-paren-p 'phox-pbrpm-left-paren-p) -(defalias 'proof-pbrpm-right-paren-p 'phox-pbrpm-right-paren-p) - -;;--------------------------------------------------------------------------;; - -(require 'phox-lang) -(provide 'phox-pbrpm) -;; phox-pbrpm ends here |