Skip to content

Commit

Permalink
Fix #514 + support for named goal selector.
Browse files Browse the repository at this point in the history 
It was hard to separate this too fixes (same regexps).
  • Loading branch information
@Matafou
Matafou committed Oct 16, 2020
1 parent eb6bba1 commit 0fdb1ae
Show file tree
Hide file tree
Showing 4 changed files with 109 additions and 140 deletions.
178 changes: 68 additions & 110 deletions coq/coq-indent.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 "\\_<match\\_>" str))
;; (with (coq-count-match "\\_<with\\_>" str))
;; (letwith (+ (coq-count-match "\\_<let\\_>" 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
Expand All @@ -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
Expand All @@ -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.
Expand All @@ -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):
Expand All @@ -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:}\\)\\)\\)")
Expand All @@ -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.
Expand Down Expand Up @@ -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.")


Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand All @@ -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) ".")
Expand All @@ -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
Expand All @@ -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
Expand Down
27 changes: 16 additions & 11 deletions coq/coq-smie.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
))
Expand Down Expand Up @@ -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 ?_))))
Expand Down Expand Up @@ -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
Expand Down
19 changes: 2 additions & 17 deletions coq/coq.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
Loading

0 comments on commit 0fdb1ae

Please sign in to comment.