From 0fdb1ae633baeb9afb07bbd8632bece5976f95f2 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 16 Oct 2020 09:14:11 +0200 Subject: Fix #514 + support for named goal selector. It was hard to separate this too fixes (same regexps). --- coq/coq-indent.el | 178 +++++++++++++++++++++--------------------------------- coq/coq-smie.el | 27 +++++---- coq/coq.el | 19 +----- coq/ex/indent.v | 25 +++++++- 4 files changed, 109 insertions(+), 140 deletions(-) (limited to 'coq') diff --git a/coq/coq-indent.el b/coq/coq-indent.el index a069ab07..6c1cdcae 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -32,107 +32,59 @@ ; ,@body ; (message "%.06f" (float-time (time-since time))))) -;; (defvar coq-script-indent) - -;; (defconst coq-any-command-regexp -;; (proof-regexp-alt-list coq-keywords)) - -;; (defconst coq-indent-inner-regexp -;; (proof-regexp-alt -;; "[[]()]" "[^{]|[^}]" -;; ;; forall with must not be enclosed by \\< and -;; ;;\\> . "~" forall but interacts with 'not' -;; (proof-ids-to-regexp -;; '("as" "Cases" "match" "else" "Fix" "forall" "fun" "if" "into" "let" "then" -;; "using" "after")))) -; "ALL" "True" "False" "EX" "end" "in" "of" "with" - (defconst coq-comment-start-regexp "(\\*") (defconst coq-comment-end-regexp "\\*)") (defconst coq-comment-start-or-end-regexp (concat coq-comment-start-regexp "\\|" coq-comment-end-regexp)) -;; (defconst coq-indent-open-regexp -;; (proof-regexp-alt ;(proof-regexp-alt-list coq-keywords-goal) goal-command-p instead -;; (proof-ids-to-regexp '("Cases" "match" "BeginSubproof")) -;; "\\s(" "{|")) - -;; (defconst coq-indent-close-regexp -;; (proof-regexp-alt "\\s)" "|}" "}" -;; (proof-ids-to-regexp '("end" "EndSubProof")) -;; (proof-ids-to-regexp coq-keywords-save))) - - -;; (defconst coq-indent-closepar-regexp "\\s)") -;; (defconst coq-indent-closematch-regexp (proof-ids-to-regexp '("end"))) -;; (defconst coq-indent-openpar-regexp "\\s(") -;; (defconst coq-indent-openmatch-regexp (proof-ids-to-regexp '("match" "Cases"))) -;; (defconst coq-tacticals-tactics-regex -;; (proof-regexp-alt (proof-regexp-alt-list (append coq-tacticals coq-tactics)))) -;; (defconst coq-indent-any-regexp -;; (proof-regexp-alt coq-indent-close-regexp coq-indent-open-regexp -;; coq-indent-inner-regexp coq-any-command-regexp -;; coq-tacticals-tactics-regex)) -;; (defconst coq-indent-kw -;; (proof-regexp-alt-list (cons coq-any-command-regexp -;; (cons coq-indent-inner-regexp -;; (append coq-tacticals coq-tactics))))) - -; pattern matching detection, will be tested only at beginning of a -; line (only white sapces before "|") must not match "|" followed by -; another symbol the following char must not be a symbol (tokens of coq -; are the biggest symbol cocateantions) - -;; (defconst coq-indent-pattern-regexp "\\(|\\(?:(\\|\\s-\\|\\w\\|\n\\)\\|with\\)") - -;;;; End of regexps - -;; (defun coq-indent-goal-command-p (str) -;; "Syntactical detection of a Coq goal opening. -;; Only used in indentation code and in v8.0 compatibility mode. -;; Module, Definition and Function need a special parsing to detect -;; if they start something or not." -;; (let* ((match (coq-count-match "\\_" str)) -;; (with (coq-count-match "\\_" str)) -;; (letwith (+ (coq-count-match "\\_" str) (- with match))) -;; (affect (coq-count-match ":=" str))) - -;; (and (proof-string-match coq-goal-command-regexp str) -;; (not -;; (and (proof-string-match "\\`\\(Definition\\|Instance\\|Lemma\\|Module\\)\\>" str) -;; (not (= letwith affect)))) -;; (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) -;; (not -;; (and (proof-string-match "\\`\\(Function\\|GenFixpoint\\)\\>" str) -;; (not (proof-string-match "{\\s-*\\(wf\\|measure\\)" str))))))) - - -(defconst coq-simple-cmd-ender-prefix-regexp "[^.]\\|\\=\\|\\.\\." - "Used internally. Matches the allowed prefixes of coq \".\" command ending.") (defconst coq-bullet-regexp-nospace "\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+" "Matches single bullet, WARNING: Lots of false positive. No context checking.") -;; Goal selector syntax -(defconst coq-goal-selector-regexp "[0-9]+\\s-*:\\s-*") - -;; We can detect precisely bullets (and curlies) by looking at there -;; prefix: the prefix should be a real "." then spaces then only -;; bullets and curlys and spaces). This is used when search backward. -;; This variable is the regexp of possible prefixes -(defconst coq-bullet-prefix-regexp - (concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp "\\)" - "\\(?:\\.\\)\\(?:\\s-\\)" - "\\(?:\\s-\\|" - "\\(?:" coq-goal-selector-regexp "\\)?" +;; goal selectors are of two forms; +;; 2: +;; [goalname]: +(defconst coq-goal-selector-regexp "\\(?:[0-9]+\\|\\[\\w+\\]\\)\\s-*:\\s-*" + "regexp of goal selector in coq.") + +;;;;;;;;;;;;;;; FORWARD / BACKWARD REGEXP ;;;;;;;;;;;;;;;;; +;; These regexp are used to split the buffer into commands. They make +;; use of the fact that the file is processed from top to bottom. At +;; each step the point is put just after the last recognized chunk, +;; then spaces are jumped, and THEN the regexp for command end is +;; searched. Since bullets are are command ends occurring at command +;; start, we use the "\\=" regexp to tell if we are at the beginning +;; of a command. We don't car for the presence of comments, as the +;; regexp search is launched once coments are passed. +;; On the contrary when going backward we cannot use this trick. + +;; NOTE: \\= here allows to fail when the user types a "." just after +;; an already played command with no space. +(defconst coq-simple-cmd-ender-prefix-regexp-forward "[^.]\\|\\=\\|\\.\\." + "Used internally. Matches the allowed prefixes of coq \".\" command ending.") + +(defconst coq-simple-cmd-ender-prefix-regexp-backward "[^.]\\|\\.\\." + "Used internally. Matches the allowed prefixes of coq \".\" command ending.") + + +;; bullets must appear after a command end. So when splitting a buffer +;; forward it is enough that they appear at cursor, maybe preceded by +;; a goal selector +(defconst coq-bullet-prefix-regexp-forward "\\=") + +;; when going backward, we need to check that the bullet is located +;; after a nother command end. +(defconst coq-bullet-prefix-regexp-backward + (concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp-backward "\\)\\(?:\\.\\s-+\\)" + "\\(?:\\(?:" coq-goal-selector-regexp "\\)?" "{\\|}\\|-\\|+\\|\\*\\)*\\)")) -;; matches regular command end (. and ... followed by a space or buffer end) +;; matches regular command end (. and ... followed by a space or "}" or buffer end) ;; ". " and "... " are command endings, ".. " is not, same as in ;; proof-script-command-end-regexp in coq.el (defconst coq-period-end-command - (concat "\\(?:\\(?2:" coq-simple-cmd-ender-prefix-regexp "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)") + (concat "\\(?:\\(?2:" coq-simple-cmd-ender-prefix-regexp-forward "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\}\\|\\'\\)\\)") "Matches coq regular syntax for ending a command (except bullets and curlies). This should match EXACTLY command ending syntax. No false @@ -144,11 +96,11 @@ There are 3 substrings (2 and 3 may be nil): * number 2 is the left context matched that is not part of the bullet * number 3 is the right context matched that is not part of the bullet") -;; captures a lot of false bullets, need to check that the commaand is -;; empty. When searching forward (typically when splitting the buffer -;; into commands commands) we can't do better than that. -(defconst coq-bullet-end-command - (concat "\\(?:\\(?2:\\s-\\|\\=\\)" "\\(?1:" coq-bullet-regexp-nospace "\\)\\)") +;; captures a lot of false bullets, unless called at the first non +;; space character of a command. The primary use of this variable is +;; to split the buffer into commands, from top to bottom. +(defconst coq-bullet-end-command-forward + (concat "\\(?:\\=\\(?1:" coq-bullet-regexp-nospace "\\)\\)") "Matches ltac bullets. WARNING: lots of false positive. This matches more than real bullets as - + and * may match this @@ -158,7 +110,7 @@ only when searching backward).") ;; Context aware detecting regexp, usefull when search backward. (defconst coq-bullet-end-command-backward - (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)") + (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp-backward "\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)") "Matches ltac bullets when searching backward. This should match EXACTLY bullets. No false positive should be accepted. @@ -167,9 +119,15 @@ There are 2 substrings: * number 2 is the left context matched that is not part of the bullet" ) (defconst coq-curlybracket-end-command - (concat "\\(?:\\(?1:" - "\\(?:" coq-bullet-prefix-regexp"\\)?" - "{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)") + (concat + "\\(?:" + "\\(?2:" + "\\(?:" coq-bullet-prefix-regexp-forward"\\)\\)" + "\\(?1:\\(?:" coq-goal-selector-regexp "\\)?{\\)" + "\\(?3:[^|]\\)" + "\\|" + ;; [^|]} + "\\(?2:[^|.]\\|\\=\\)\\(?1:}\\)\\)") "Matches ltac curlies when searching backward. Warning: False positive. There are 3 substrings (2 and 3 may be nil): @@ -182,7 +140,7 @@ This matches more than real ltac curlies. See only when searching backward).") (defconst coq-curlybracket-end-command-backward - (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)" + (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp-backward "\\)" "\\(?:\\(?:\\(?1:" "\\(?:" coq-goal-selector-regexp "\\)?{\\)" "\\(?3:[^|]\\)\\)" "\\|\\(?1:}\\)\\)\\)") @@ -195,9 +153,9 @@ There are 3 substrings (2 and 3 may be nil): * number 2 is the left context matched that is not part of the bullet * number 3 is the right context matched that is not part of the bullet") -(defconst coq-end-command-regexp +(defconst coq-end-command-regexp-forward (concat coq-period-end-command "\\|" - coq-bullet-end-command "\\|" + coq-bullet-end-command-forward "\\|" coq-curlybracket-end-command) "Matches end of commands (and ltac bullets and curlies). WARNING: False positive. @@ -230,7 +188,7 @@ There are 3 substrings (2 and 3 may be nil): * number 2 is the left context matched that is not part of the ending string * number 3 is the right context matched that is not part of the ending string -Remqrk: This regexp is much more precise than `coq-end-command-regexp' but only +Remqrk: This regexp is much more precise than `coq-end-command-regexp-forward' but only works when searching backward.") @@ -359,10 +317,12 @@ a comment, return nil and does not move the point." ;; ))) ;; (when found (point)))) - +;; check if we are in the middle of an command ender. Return the +;; number of shift needed to have to move one char to see the end of a +;; command. typically if we are ( >< is the cursor). intro.>< (defun coq-is-on-ending-context () (cond - ((looking-at "}") -1) + ((looking-at "}") 0) ((save-excursion (ignore-errors (forward-char -1) ; always nil, don't use "and" @@ -401,9 +361,9 @@ Comments are ignored, of course." ; slight modification of proof-script-generic-parse-cmdend (one of the -; candidate for proof-script-parse-function), to allow "{" and "}" to be -; command terminator when the command is empty. TO PLUG: swith the comment -; below and rename coq-script-parse-function2 into coq-script-parse-function +; candidate for proof-script-parse-function), to allow "{" and "}" to +; be command terminator when the command is empty. This function is +; used as coq-script-parse-function in coq.el. (defun coq-script-parse-cmdend-forward (&optional limit) "Move to the first end of command found looking forward from point. Point is put exactly after the ending token (but before matching @@ -421,7 +381,7 @@ regexp." ;; Find end of command (while (and (setq foundend (and - (re-search-forward coq-end-command-regexp limit t) + (re-search-forward coq-end-command-regexp-forward limit t) (match-end 1))) (or (and (not (or (string-equal (match-string 1) ".") @@ -441,7 +401,7 @@ regexp." (and (goto-char foundend) (nth 8 (syntax-ppss))))) - ;; Given the form of coq-end-command-regexp + ;; Given the form of coq-end-command-regexp-forward ;; match-end 1 is the right place to start again ;; to search backward, next time we start from just ;; there @@ -455,10 +415,8 @@ regexp." nil)))) -; slight modification of proof-script-generic-parse-cmdend (one of the -; candidate for proof-script-parse-function), to allow "{" and "}" to be -; command terminator when the command is empty. TO PLUG: swith the comment -; below and rename coq-script-parse-function2 into coq-script-parse-function +;; This is not used by generic pg, just by a few functions in here. +;; It is less trustable that itsforward version above. (defun coq-script-parse-cmdend-backward (&optional limit) "Move to the first end of command (not commented) found looking up. Point is put exactly before the last ending token (before the last diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 3f72634d..37dc390c 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -709,18 +709,19 @@ The point should be at the beginning of the command name." ((and (equal tok "|") (eq (char-before) ?\{)) (goto-char (1- (point))) "{|") + ;; curly braces can be beginproof/endproof or record stuff. ((and (zerop (length tok)) (member (char-before) '(?\{ ?\})) (save-excursion (forward-char -1) (if (and (looking-at "{") - (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t)) + (looking-back "\\(\\[?\\w+\\]?\\s-*:\\s-*\\)" nil t)) (goto-char (match-beginning 0))) (let ((nxttok (coq-smie-backward-token))) ;; recursive call (coq-is-cmdend-token nxttok)))) (forward-char -1) (if (looking-at "}") "} subproof" (if (and (looking-at "{") - (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t)) + (looking-back "\\(\\[?\\w+\\]?\\s-*:\\s-*\\)" nil t)) (goto-char (match-beginning 0))) "{ subproof" )) @@ -855,15 +856,18 @@ The point should be at the beginning of the command name." ;; qualifier. (let ((nxtnxt (char-after (+ (point) (length tok))))) (if (eq nxtnxt ?\() ". selector" - (if (or (null nxtnxt) (eq (char-syntax nxtnxt) ?\ )) - ;; command terminator: ". proofstart" et al - (save-excursion (forward-char (- (length tok) 1)) - (coq-smie-.-deambiguate)) - (if (eq (char-syntax nxtnxt) ?w) - (let ((newtok (coq-smie-complete-qualid-backward))) + (if (eq nxtnxt ?}) ;; dot immediately followed by closesubproof. + "." + (if (or (null nxtnxt) (eq (char-syntax nxtnxt) ?\ )) + ;; command terminator: ". proofstart" et al + (save-excursion (forward-char (- (length tok) 1)) + (coq-smie-.-deambiguate)) + (cond + ((eq (char-syntax nxtnxt) ?w) + (let ((newtok (coq-smie-complete-qualid-backward))) ;; qualified name - (concat newtok tok)) - ". selector"))))) ;; probably a user defined syntax + (concat newtok tok))) + (t ". selector"))))))) ;; probably a user defined syntax ((and (and (eq (char-before) ?.) (member (char-syntax (char-after)) '(?w ?_)))) @@ -1244,7 +1248,8 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((member token '("in let" "in monadic")) (smie-rule-parent)) - ((equal token "} subproof") (smie-rule-parent)) + ((equal token "} subproof") + (smie-rule-parent)) ;; proofstart is a special hack, since "." should be used as a ;; separator between commands, here it is recognized as an open diff --git a/coq/coq.el b/coq/coq.el index 663279cf..dc6fe529 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -457,20 +457,6 @@ This is a subroutine of `proof-shell-filter'." (pg-response-display-with-face strnotrailingspace))) ; face -;; Trying to accept { and } as terminator for empty commands. Actually -;; I am experimenting two new commands "{" and "}" (without no -;; trailing ".") which behave like BeginSubProof and EndSubproof. The -;; absence of a trailing "." makes it difficult to distinguish between -;; "{" of normal coq code (implicits, records) and this the new -;; commands. We therefore define a coq-script-parse-function to this -;; purpose. - -;; coq-end-command-regexp is ni coq-indent.el -(defconst coq-script-command-end-regexp coq-end-command-regexp) -;; "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)") - - - ;; slight modification of proof-script-generic-parse-cmdend (one of the ;; candidate for proof-script-parse-function), to allow "{" and "}" to be ;; command terminator when the command is empty. TO PLUG: swith the comment @@ -1913,7 +1899,8 @@ at `proof-assistant-settings-cmds' evaluation time.") ;; coq-mode colorize errors better than the generic mechanism (setq proof-script-color-error-messages nil) (setq proof-terminal-string ".") - (setq proof-script-command-end-regexp coq-script-command-end-regexp) + ;; superseded by coq-script-parse-function + ;;(setq proof-script-command-end-regexp coq-script-command-end-regexp) (setq proof-script-parse-function 'coq-script-parse-function) (setq proof-script-comment-start comment-start) (setq proof-script-comment-end comment-end) @@ -2783,8 +2770,6 @@ SPAN is the span of the whole theorem (statement + proof)." "Coq specific dependency mechanism. Used for automatic insertion of \"Proof using\" annotations.") -;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; - (defun coq-insert-as-in-next-command () (interactive) diff --git a/coq/ex/indent.v b/coq/ex/indent.v index e93616c8..72a3c201 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -4,8 +4,8 @@ Notation "[ ]" := nil : list_scope. Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope. Require Import Arith. - -Definition arith1: +Open Scope nat_scope. +Definition arith1:= 1 + 3 * 4. @@ -190,6 +190,27 @@ Module M1. End M2. End M1. +Module GoalSelectors. + Theorem lt_n_S : (True \/ True \/ True \/ True \/ True ) -> True. + Proof. + refine (or_ind ?[aa] (or_ind ?[bb] (or_ind ?[cc] (or_ind ?[dd] ?[ee])))). + [aa]:{ auto. } + 2:{ auto. } + [ee]:auto. + { auto.} + Qed. + (* Same without space between "." and "}". *) + Theorem lt_n_S2 : (True \/ True \/ True \/ True \/ True ) -> True. + Proof. + refine (or_ind ?[aa] (or_ind ?[bb] (or_ind ?[cc] (or_ind ?[dd] ?[ee])))). + [aa]:{ auto.} + 2:{ auto.} + [ee]:auto. + { auto.} + Qed. + + +End GoalSelectors. Module M1'. Module M2'. -- cgit v1.2.3