diff options
| -rw-r--r-- | coq/coq-indent.el | 261 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 32 | ||||
| -rw-r--r-- | coq/coq.el | 46 | ||||
| -rw-r--r-- | coq/ex/indent.v | 163 |
4 files changed, 390 insertions, 112 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index ff94a669..1f7f353e 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -22,7 +22,7 @@ (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 @@ -37,11 +37,11 @@ (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(")) + "\\s(" "{|")) (defconst coq-indent-close-regexp - (proof-regexp-alt "\\s)" - (proof-ids-to-regexp '("EndSubproof" "end")) + (proof-regexp-alt "\\s)" "|}" "}" + (proof-ids-to-regexp '("end" "EndSubProof")) (proof-ids-to-regexp coq-keywords-save))) @@ -81,7 +81,7 @@ detect if they start something or not." (and (proof-string-match coq-goal-command-regexp str) (not - (and (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str) + (and (proof-string-match "\\`\\(Definition\\|Instance\\|Lemma\\|Module\\)\\>" str) (not (= letwith affect)))) (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) (not @@ -92,8 +92,11 @@ detect if they start something or not." ;; ". " and "... " are command endings, ".. " is not, same as in ;; proof-script-command-end-regexp in coq.el (defconst coq-end-command-regexp - "\\(?:[^.]\\|\\.\\.\\)\\(\\.\\)\\(?:\\s-\\|\\'\\)") -; "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\(\\.\\)\\(?:\\s-\\|\\'\\)") + "\\(?2:[^.]\\|\\.\\.\\)?\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\|\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\)\\(?1:}\\)" + "Regexp matching end of a command. There are 3 substrings: +* number 1 is the real coq ending string, +* 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") (defun coq-search-comment-delimiter-forward () @@ -177,7 +180,6 @@ Use this one for coq instead of the generic one." (defconst coq-end-command-or-comment-start-regexp (concat coq-comment-start-regexp "\\|" coq-end-command-regexp)) - (defun coq-find-not-in-comment-backward (reg &optional lim submatch) "Moves to the first not commented occurrence of REG found looking up. The point is @@ -190,7 +192,7 @@ found, go as far as possible and return nil." (while (and (not found) continue) (setq continue (re-search-backward regexp lim 'dummy)) (when continue - (if (looking-at coq-comment-end-regexp) + (if (coq-looking-at-comment) (progn (coq-skip-until-one-comment-backward)) (progn (when submatch (goto-char (match-beginning submatch))) (setq found t)) @@ -217,43 +219,107 @@ and return nil." (goto-char (match-beginning 0)) (if (looking-at coq-comment-start-regexp) (progn (forward-char 2) (coq-skip-until-one-comment-forward)) - (progn (when submatch (goto-char (match-beginning submatch))) + (progn (when (and submatch (match-beginning submatch)) (goto-char (match-beginning submatch))) (setq found t)) ))) (when found (point)))) -(defun coq-find-command-end-backward () + +(defun coq-is-on-ending-context () + (cond + ((looking-at "}") -1) + ((save-excursion + (ignore-errors + (forward-char -1) ; always nil, don't use "and" + (looking-at "{\\|\\."))) 1) + (t 0))) + +; 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 +(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 the ending token (but before matching +substring if present). If no end command is found, go as far as possible +and return nil. End of command appearing in comments are ignored." + (if (looking-at proof-script-comment-start-regexp) + ;; Handle comments + (if (proof-script-generic-parse-find-comment-end) 'comment) + ;; Handle non-comments: assumed to be commands + (if (< (coq-is-on-ending-context) 0) (ignore-errors (forward-char (coq-is-on-ending-context)))) + (let (foundend) + ;; Find end of command + (while (and (setq foundend + (progn + (and + (re-search-forward proof-script-command-end-regexp limit t) + (match-end 1)))) + (or (if (or (string-equal (match-string 1) "}") + (string-equal (match-string 1) "{")) + (save-excursion + ;; "{[^|]\\|[^|]}" matched, use length of match-string instead? + (goto-char (match-beginning 1)) + (not (coq-empty-command-p))) + nil) + (proof-buffer-syntactic-context))) + ;; inside a string or comment before the command end + ) + (if (and foundend + (goto-char foundend) ; move to command end + (not (proof-buffer-syntactic-context))) + ;; Found command end outside string/comment + 'cmd + ;; Didn't find command end + 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 +(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 \".\" of the ending token. -If no end command is found, go as far as possible and return -nil." - (ignore-errors (forward-char 1)); because regexp looks one char after last "." - (coq-find-not-in-comment-backward coq-end-command-regexp nil 1)) - - -(defun coq-find-command-end-forward () - "Move to the first end of command found looking down. -The point is put exactly before the last \".\" of the ending -token. If no end command is found, go as far as possible and -return nil." - (ignore-errors (backward-char 1)); because regexp looks one char before "." - (coq-find-not-in-comment-forward coq-end-command-regexp nil 1)) - - -(defun coq-find-command-end (direction) - "Move to the first end of command found looking at DIRECTION. -The point is put exactly before the last \".\" of the ending -token. If no end command is found, go as far as possible and -return nil." - (if (< direction 0) (coq-find-command-end-backward) - (coq-find-command-end-forward))) +Point is put exactly before the last ending token (before the last +\".\" if \"...\"). If no end command is found, go as far as possible +and return nil." + (if (looking-at proof-script-comment-start-regexp) + ;; Handle comments + (if (proof-script-generic-parse-find-comment-end) 'comment) ; start? + ;; Handle non-comments: assumed to be commands + ;; first shift if we are in the middle of a ending pattern + (if (> (coq-is-on-ending-context) 0) (ignore-errors(forward-char (coq-is-on-ending-context)))) + (let (foundend) + ;; Find end of command + (while (and (setq foundend + (progn + (and + (re-search-backward proof-script-command-end-regexp limit t) + (match-beginning 1)))) + (or (if (or (string-equal (match-string 1) "}") + (string-equal (match-string 1) "{")) + (save-excursion + (goto-char (match-beginning 1)) + (not (coq-empty-command-p))) + nil) + (proof-buffer-syntactic-context))) + ;; inside a string or comment before the command end + ) + (if (and foundend + (goto-char foundend) ; move to command end + (not (proof-buffer-syntactic-context))) + ;; Found command end outside string/comment + 'cmd + ;; Didn't find command end + nil)))) + (defun coq-find-current-start () "Move to the start of command at point. The point is put exactly after the end of previous command, or at the (point-min if there is no previous command)." - (coq-find-command-end-backward) - (if (proof-looking-at "\\.\\s-") (forward-char 1)) + (coq-script-parse-cmdend-backward) + (if (proof-looking-at "\\.\\s-\\|{\\|}") (forward-char 1)) ; else = no match found (point)) @@ -273,35 +339,29 @@ Can jump line if NOJUMPLINES = nil." (save-excursion (let* ((st (coq-find-real-start)) ; va chercher trop loin? OUI (linejumped (not (same-line initpos (point)))) - (nd (or (coq-find-command-end-forward) (- (point-max) 1)))) ; idem? + (xxx (goto-char (- (point) 1))) + (nd (or (if (coq-script-parse-cmdend-forward) (point) nil) (- (point-max) 1)))) ; idem? (if (and st (or (not nojumplines) (not linejumped))) (buffer-substring st (+ nd 1)) nil))))) -; -;(defun coq-command-at-point () -; "Return the string of the command at point." -; (save-excursion -; (let ((st (coq-find-real-start)) ; va chercher trop loin? -; (nd (or (coq-find-command-end-forward) (- (point-max) 1)))) ; idem? -; (if st (buffer-substring st (+ nd 1)))))) -; - - (defun coq-commands-at-line (&optional nojumplines) "Return the string of each command at current line." (save-excursion - (back-to-indentation) + ;; we must capture a "." or a "{" at start of the line. So we go at the end of + ;; previous line to have a left context to match (let ((initpoint (point)) + (forward-char (coq-is-on-ending-context)) (command-found (coq-command-at-point nojumplines)) res ) + (if command-found (coq-find-real-start)) (while (and command-found ;; need this second test even with nojumplines: (same-line (point) initpoint)) (setq res (cons command-found res)) - (if (and (coq-find-command-end-forward) + (if (and (coq-script-parse-cmdend-forward) (ignore-errors (forward-char 1) t);to fit in the "and" (coq-find-real-start)) (setq command-found (coq-command-at-point nojumplines)) @@ -362,26 +422,29 @@ not inside the {} of a record)." (setq topnotreached (= (forward-line -1) 0)) (end-of-line) (if (proof-looking-at-syntactic-context) - (coq-find-comment-start) ; (re-search-backward coq-comment-start-regexp nil 'dummy) + (re-search-backward coq-comment-start-regexp nil 'dummy) )) (back-to-indentation) (if (not topnotreached) 0 ;; returns nil if top of buffer was reached ;; if we are at end of a command (dot) find this command ; if there is a "." alone on the line (let ((pos (point))) - (ignore-errors (forward-char -1)) - (if (coq-indent-find-reg oldpt coq-end-command-regexp) - (progn (forward-char -2) + ;(ignore-errors (forward-char -1)) + (if (coq-script-parse-cmdend-forward oldpt) + (progn (forward-char -1) + ;; one more if "." found, no more if "{" or "}" + (when (proof-looking-at "\\.") (forward-char -1)) (coq-find-real-start) (back-to-indentation) 1) (goto-char pos) (if (save-excursion - (and (not (= (point) (point-min))) + (and + (not (= (point) (point-min))) (or (forward-char -1) t) (coq-find-real-start) - (proof-looking-at-safe "Record") - (coq-indent-find-reg oldpt "{"))) + (proof-looking-at-safe "Record\\|Class\\|Instance"); {struct} should not match this + (coq-indent-find-reg oldpt "{[^|]"))) 4 2))))))) @@ -530,41 +593,79 @@ Returns point if found." (defun coq-goal-count (l) (coq-add-iter l 'coq-indent-goal-command-p)) (defun coq-save-count (l) - (coq-add-iter l '(lambda (x) (or (coq-save-command-p nil x) - (eq (proof-string-match "\\<EndSubproof\\>" x) 0))))) + (coq-add-iter l '(lambda (x) + (or (coq-save-command-p nil x) + (eq (proof-string-match "\\<\\(?:EndSubproof\\)\\>\\|}" x) 0))))) (defun coq-proof-count (l) (coq-add-iter l '(lambda (x) - (eq (proof-string-match "\\<\\(?:Proof\\|BeginSubproof\\)\\>" x) 0)))) + (eq (proof-string-match "\\<\\(?:Proof\\|BeginSubproof\\)\\>\\|{" x) 0)))) ;; returns the difference between goal (and assimilate Proof and BeginSubproof) and ;; save commands in a commands list. This is to (defun coq-goal-save-diff-maybe-proof (l) (let ((proofs (coq-proof-count l)) + (saves (coq-save-count l)) (goals (coq-goal-count l))) - (if (= goals 0) (- (if (<= proofs 0) 0 1) (coq-save-count l)) - (- goals (coq-save-count l))))) +; (if (= goals 0) (- (if (<= proofs 0) 0 1) (coq-save-count l)) +; (- goals (coq-save-count l))) + (- (+ proofs goals) saves) + )) (defun coq-indent-command-offset (kind prevcol prevpoint) - "Returns the indentation offset of the current line. This function indents a *command* line (the first line of a command). Use `coq-indent-expr-offset' to indent a line belonging to an expression." - (let ((diff-goal-save-current (coq-goal-save-diff-maybe-proof (coq-commands-at-line t))) + "Returns the indentation offset of the current line. +This function indents a *command* line (the first line of a command). +Use `coq-indent-expr-offset' to indent a line belonging to an expression." + (let ((diff-goal-save-current + (coq-goal-save-diff-maybe-proof (coq-commands-at-line t))) (diff-goal-save-prev - (save-excursion (goto-char prevpoint) - (coq-goal-save-diff-maybe-proof (coq-commands-at-line t))))) + (save-excursion + (goto-char prevpoint) + (coq-goal-save-diff-maybe-proof (coq-commands-at-line t)))) + (prev-closing-beginning ; t if the closing is at start of the (prev) line + (save-excursion + (goto-char prevpoint) + (back-to-indentation) + ;(forward-char -1) + (looking-at coq-indent-close-regexp))) + (current-closing-beginning ; t if the closing is at start of the (current) line + (save-excursion + (back-to-indentation) + (looking-at coq-indent-close-regexp)))) + ;(message "currentkind,prevcol,prevpoint = %d , %d ,%d " kind prevcol prevpoint) (cond ((proof-looking-at-safe "\\<Proof\\>") 0);; no indentation at "Proof ..." - ;; we are at an end command -> one ident left unless previous line is a goal - ;; (if goal and save are consecutive, then no indentation at all) - ((and (< diff-goal-save-current 0) (<= diff-goal-save-prev 0)) (- proof-indent)) - - ;; previous command is a goal command -> one indent right unless the current one - ;; is an end (consecutive goal and save). - ((and (>= diff-goal-save-current 0) (> diff-goal-save-prev 0)) proof-indent) - - ;; otherwise -> same indent as previous command - (t 0)))) + (t (* proof-indent + (let ((res + (let ((a diff-goal-save-prev) (b diff-goal-save-current) + (a2 prev-closing-beginning) (b2 current-closing-beginning)) + ;(message "a,b,a2,b2 = %d,%d,%S,%S" a b a2 b2) + (cond + ((and (>= a 0) (>= b 0)) a) + ((and (>= a 0) (< b 0) b2) (+ a -1)) ; a + b + ((and (>= a 0) (< b 0) (not b2)) a) + ((and (< a 0) (< b 0) a2 b2) a) ; a +1 -1 + ((and (< a 0) (< b 0) a2 (not b2)) (+ a 1)) + ((and (< a 0) (< b 0) (not a2) b2) (+ a -1)) + ((and (< a 0) (< b 0) (not a2) (not b2)) a) + ((and (< a 0) (>= b 0) a2) (+ a 1)) + ((and (< a 0) (>= b 0) (not a2)) a) + (t (error "Muh?")))))) + ;(message "RES = %S" res) + ;(message "********************") + res)) + ) + ;; ;; we are at an end command -> one ident left unless previous line is a goal + ;; ;; (if goal and save are consecutive, then no indentation at all) + ;; ((and (< diff-goal-save-current 0) (<= diff-goal-save-prev 0)) (- proof-indent)) + ;; ;; previous command is a goal command -> one indent right unless the current one + ;; ;; is an end (consecutive goal and save). + ;; ((and (>= diff-goal-save-current 0) (> diff-goal-save-prev 0)) proof-indent) + ;; ;; otherwise -> same indent as previous command + ;; (t 0) + ))) @@ -583,6 +684,7 @@ Returns point if found." This function indents a *expression* line (a line inside of a command). Use `coq-indent-command-offset' to indent a line belonging to a command. The fourth argument must be t if inside the {}s of a record, nil otherwise." + ;(message "COQ-INDENT-EXPR-OFFSET") (let ((pt (point)) real-start) (save-excursion (setq real-start (coq-find-real-start))) @@ -660,8 +762,10 @@ argument must be t if inside the {}s of a record, nil otherwise." ;; just for side effect: jumps to end of previous line ((and (goto-char prevpoint) (or (and (end-of-line) nil) - (and (forward-char -1) t)) nil)) + (and (coq-find-not-in-comment-backward "[^[:space:]]") t)) nil)) + ;; TODO fix with new use of { for tactics enclosing + ;; should be ok if record is ok. ((and (proof-looking-at-safe ";") ;prev line has ";" at the end record) ; and we are inside {}s of a record (save-excursion @@ -683,6 +787,7 @@ argument must be t if inside the {}s of a record, nil otherwise." ;; There is a indent keyword (fun, forall etc) ;; and we are not in {}s of a record just after a ";" ((coq-find-at-same-level-zero prevpoint coq-indent-kw) + ;(message "COQ-INDENT-KW") (+ prevcol proof-indent)) ((and (goto-char prevpoint) nil)) ;; just for side effect: go back to previous line @@ -720,7 +825,7 @@ argument must be t if inside the {}s of a record, nil otherwise." ;;we were at the first line of a comment and the current line is the ;;previous one (t (goto-char oldpt) - (coq-find-command-end-backward) + (coq-script-parse-cmdend-backward) (coq-find-real-start) (current-column)))))))) @@ -731,7 +836,7 @@ argument must be t if inside the {}s of a record, nil otherwise." (setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert) prevcol (current-column) prevpoint (point))) - ;; (message "coq-indent-offset... kind = %s ; prevcol = %s; prevpoint = %s" kind prevcol prevpoint) + ;(message "coq-indent-offset... kind = %s ; prevcol = %s; prevpoint = %s" kind prevcol prevpoint) (cond ((= kind 0) 0 ; top of the buffer reached ) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index f4daaa0f..eb04e901 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -431,7 +431,7 @@ See also `coq-prog-env' to adjust the environment." ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Instance" nil "Instance #:#.\nProof.\n#End." t "Instance") + ("Instance" nil "Instance #:#.\nProof.\n#Defined." t "Instance") ("Program Instance" "pinstance" "Program Instance [ # ] => # where \n# := #;\n# := #." t "Program\\s-+Instance") ("Let" "Let" "Let # : # := #." t "Let") ("Ltac" "ltac" "Ltac # := #" t "Ltac") @@ -451,18 +451,25 @@ See also `coq-prog-env' to adjust the environment." ) ;; modules and section are indented like goal starters +;;; PC TODO: this category is used only for indentation, because +;;; scripting uses information from coq to decide if a goal is +;;; started. Since it is impossible for some commands to know +;;; syntactically if they start something (ex: Instance), the +;;; right thing to do would be to indent only on "Proof." and forget +;;; about this category for indentation. + (defvar coq-goal-starters-db '( - ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") - ("Add Parametric Morphism" nil "Add Parametric Morphism : " t "Add\\s-+Parametric\\s-+Morphism") - ("Add Parametric Relation" nil "Add Parametric Relation : " t "Add\\s-+Parametric\\s-+Relation") + ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") + ("Add Parametric Morphism" nil "Add Parametric Morphism : " t "Add\\s-+Parametric\\s-+Morphism") ("Chapter" "chp" "Chapter # : #." t "Chapter") ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) - ("Definition goal" "defg" "Definition #:#.\n#\nSave." t);; careful + ("Definition goal" "defg" "Definition #:#.\n#\nDefined." t);; careful ("Fact" "fct" "Fact # : #." t "Fact") ("Goal" nil "Goal #." t "Goal") + ("Instance goal" "instg" "Instance #:#.\n#\nDefined." t);; careful ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) @@ -482,6 +489,7 @@ See also `coq-prog-env' to adjust the environment." ;; command that are not declarations, definition or goal starters (defvar coq-other-commands-db '( + ("Add Parametric Relation" nil "Add Parametric Relation : " t "Add\\s-+Parametric\\s-+Relation") ("BeginSubproof" "bs" "BeginSubproof.\n#\nEndSubproof." t "BeginSubproof") ("EndSubproof" "es" "EndSubproof.#" t "EndSubproof") ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu @@ -749,15 +757,13 @@ Used by `coq-goal-command-p'" (coq-module-opening-p str)) ))) +;; TODO: rely on coq response nistead for span grouping (defvar coq-keywords-save-strict - '("Defined" - "Save" - "Qed" -; "EndSubproof" ;; care: this must happen before "End" - "End" - "Admitted" - "Abort" - )) + '("Defined" "Save" "Qed" "End" "Admitted" "Abort" ) + "This regexp must match *exactly* commands that close a goal/Module. +It is used: + 1) for grouping spans into one when scripting + 2) for indentation.") (defvar coq-keywords-save (append coq-keywords-save-strict '("Proof")) @@ -103,7 +103,7 @@ Set to t if you want this feature." (require 'coq-syntax) ;; FIXME: Even if we don't use coq-indent for indentation, we still need it for -;; coq-find-command-end-backward and coq-find-real-start. +;; coq-script-parse-cmdend-forward/backward and coq-find-real-start. (require 'coq-indent) (defcustom coq-prog-env nil @@ -288,6 +288,44 @@ SMIE is a navigation and indentation framework available in Emacs ≥ 23.3." ;; Auxiliary code for Coq modes ;; + + +;;;;;;;;;;; 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 +(setq coq-script-command-end-regexp coq-end-command-regexp) +; "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)") + + + +(defun coq-empty-command-p () + "Test if between point and previous command is empty. +Comments are ignored, of course." + (let ((end (point)) + (start (coq-find-not-in-comment-backward "[^[:space:]]"))) + ;; we must find a "." to be sure, because {O} {P} is allowed in definitions + ;; with implicits --> this function is recursive + (if (looking-at "{\\|}") (coq-empty-command-p) + (looking-at "\\.")))) + + +; 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 +(defun coq-script-parse-function () + "For `proof-script-parse-function' if `proof-script-command-end-regexp' set." + (coq-script-parse-cmdend-forward)) + +;;;;;;;;;;;;;;;;;;;;;;;;;; End of "{" and "} experiments ;;;;;;;;;;;; + + (defun coq-set-undo-limit (undos) (proof-shell-invisible-command (format "Set Undo %s . " undos))) @@ -743,8 +781,8 @@ This is specific to `coq-mode'." ;; Coq error messages are thrown off by TAB chars. (set (make-local-variable 'indent-tabs-mode) nil) (setq proof-terminal-string ".") - (setq proof-script-command-end-regexp - "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)") + (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 "(*") (setq proof-script-comment-end "*)") (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name @@ -1831,7 +1869,7 @@ Based on idea mentioned in Coq reference manual." ((str (string-match "<info type=\"infoH\">\\([^<]*\\)</info>" proof-shell-last-response-output)) (substr (match-string 1 proof-shell-last-response-output))) - (coq-find-command-end-backward) + (coq-script-parse-cmdend-backward) (let ((inhibit-read-only t)) (insert (concat " as " substr))))) diff --git a/coq/ex/indent.v b/coq/ex/indent.v index b06ae922..ce8e1edb 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -9,22 +9,151 @@ Function div2 (n : nat) {struct n}: nat := end. -Module toto. - Lemma l1: forall n:nat, n = n. - toto. - Qed. - Lemma l2: forall n:nat, n = n. - toto. Qed. - Lemma l3: forall n:nat, n <= n. intro. Qed. - Lemma l4: forall n:nat, n <= n. Proof. intro. Qed. - Lemma l5 : forall n:nat, n <= n. - Proof. intro. - Qed. - Lemma l6: forall n:nat, n = n. - toto. - Lemma l7: forall n:nat, n = n. - toto. +Module M1. + Module M2. + Lemma l1: forall n:nat, n = n. + auto. Qed. - Qed. -End toto. + Lemma l2: forall n:nat, n = n. + auto. Qed. + Lemma l3: forall n:nat, n <= n. auto. Qed. + (* Lemma l4: forall n:nat, n <= n. Proof. intro. Qed. *) + Lemma l5 : forall n:nat, n <= n. + Proof. auto. + Qed. + Lemma l6: forall n:nat, n = n. + intros. + Lemma l7: forall n:nat, n = n. + destruct n. + BeginSubproof. + auto. + EndSubproof. + BeginSubproof. + destruct n. + BeginSubproof. + auto. + EndSubproof. + auto. + EndSubproof. + Qed. + BeginSubproof. + destruct n. + BeginSubproof. + auto. EndSubproof. + BeginSubproof. auto. + EndSubproof. + EndSubproof. + Qed. + End M2. +End M1. + + +Module M1'. + Module M2'. + Lemma l6: forall n:nat, n = n. + intros. + Lemma l7: forall n:nat, n = n. + destruct n. + { + auto. + } + { + destruct n. + { + idtac;[ + auto + ]. + } + auto. + } + Qed. + {destruct n. + { + auto. } + {auto.} + } + Qed. + End M2'. +End M1'. + +Record rec:Set := { + fld1:nat; + fld2:nat; + fld3:bool +}. + +Class cla {X:Set}:Set := { + cfld1:nat; + cld2:nat; + cld3:bool +}. + + + + +Lemma l : + forall r:rec, + exists r':rec, + r'.(fld1) = r.(fld2) /\ r'.(fld2) = r.(fld1). +Proof. + intros r. + {exists + {| + fld1:=r.(fld2); + fld2:=r.(fld1); + fld3:=false + |}. + split. + {auto. } + {auto. } + } +Qed. + + +Lemma l2 : + forall r:rec, + exists r':rec, + r'.(fld1) = r.(fld2) /\ r'.(fld2) = r.(fld1). +Proof. + intros r. + { + idtac; + exists + {| + fld1:=r.(fld2); + fld2:=r.(fld1); + fld3:=false + |}. + (* ltac *) + match goal with + | _:rec |- ?a /\ ?b => split + | _ => fail + end. + {auto. } + {auto. } + } +Qed. + +Require Import Morphisms. +Generalizable All Variables. +Open Local Scope signature_scope. +Require Import RelationClasses. + +Module foo. +Instance: (@RewriteRelation nat) impl. +(* No goal created *) +Definition XX := 0. + + +Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R. +(* One goal created. Then the user MUST put "Proof." to help indentation *) +Proof. +firstorder. +Qed. + Program Fixpoint f (x:nat) {struct n} : nat := + match x with + | 0 => 0 + | S y => S (f y) + end. +End Foo. |