diff options
-rw-r--r-- | coq/coq-smie.el | 76 | ||||
-rw-r--r-- | coq/coq-system.el | 2 | ||||
-rw-r--r-- | coq/ex/indent.v | 68 | ||||
-rw-r--r-- | generic/proof-utils.el | 2 |
4 files changed, 97 insertions, 51 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 1c0b9c67..c488e73f 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -185,6 +185,32 @@ the token of \".\" is simply \".\"." +;; A variant of smie-default-backward-token that recognize "." and ";" +;; as single token even if glued at the end of another symbols. + +(defun coq-backward-token-fast-nogluing-dot-friends () + (forward-comment (- (point))) + (let ((pt (point))) + (let* ((tok-punc (skip-syntax-backward ".")) + (str-punc (buffer-substring-no-properties pt (point))) + (tok-other (if (zerop tok-punc) (skip-syntax-backward "w_'")))) + ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token + (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc)) + (skip-syntax-forward ".") + (forward-char -1)) + (buffer-substring-no-properties pt (point))))) + +(defun coq-forward-token-fast-nogluing-dot-friends () + (forward-comment (point-max)) + (let ((pt (point))) + (let* ((tok-punc (skip-syntax-forward ".")) + (str-punc (buffer-substring-no-properties pt (point))) + (tok-other (if (zerop tok-punc) (skip-syntax-forward "w_'")))) + ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token + (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc)) + (forward-char -1)) + (buffer-substring-no-properties pt (point))))) + ;; ignore-between is a description of pseudo delimiters of blocks that ;; should be jumped when searching. There is a bad interaction when ;; tokens and ignore-bteween are not disjoint @@ -200,9 +226,7 @@ command (and inside parenthesis)." (catch 'found (while (< (point) end) ;; The default lexer is faster and is good enough for our needs. - (let* ((next2 (smie-default-forward-token)) - (is-dot-friend (coq-dot-friend-p next2)) - (next (if is-dot-friend "." next2)) + (let* ((next (coq-forward-token-fast-nogluing-dot-friends)) (parop (assoc next ignore-between))) ; if we find something to ignore, we directly jump to the ; corresponding closer @@ -231,6 +255,7 @@ command (and inside parenthesis)." ((member next tokens) (throw 'found next)))))))) (scan-error nil))) + ;; ignore-between is a description of pseudo delimiters of blocks that ;; should be jumped when searching. There is a bad interaction when ;; tokens and ignore-bteween are not disjoint @@ -246,9 +271,7 @@ command (and inside parenthesis). " (catch 'found (while (> (point) end) ;; The default lexer is faster and is good enough for our needs. - (let* ((next2 (smie-default-backward-token)) - (is-dot-friend (coq-dot-friend-p next2)) - (next (if is-dot-friend "." next2)) + (let* ((next (coq-backward-token-fast-nogluing-dot-friends)) (parop (rassoc next ignore-between))) ; if we find something to ignore, we directly jump to the ; corresponding openner @@ -266,8 +289,8 @@ command (and inside parenthesis). " (goto-char (point)) next)) ;; Do not consider "." when not followed by a space - ;(message "SPACE?: %S , %S , %S" next2 next (looking-at ".[[:space:]]")) - (when (or (not (equal next2 ".")) + ;(message "SPACE?: %S , %S , %S" next next (looking-at ".[[:space:]]")) + (when (or (not (equal next ".")) (looking-at "\\.[[:space:]]")) (cond ((and (zerop (length next)) @@ -350,7 +373,7 @@ The point should be at the beginning of the command name." (defun coq-smie-forward-token () - (let ((tok (smie-default-forward-token))) + (let ((tok (coq-forward-token-fast-nogluing-dot-friends))) (cond ;; @ may be ahead of an id, it is part of the id. ((and (equal tok "@") (looking-at "[[:alpha:]_]")) @@ -372,7 +395,7 @@ The point should be at the beginning of the command name." (concat tok newtok))) (t (save-excursion (coq-smie-backward-token))))) ;; recursive call ((or (string-match coq-bullet-regexp-nospace tok) - (member tok '("=>" ":=" "exists" "in" "as" "∀" "∃" "→" "∨" "∧" ";" + (member tok '("=>" ":=" "::=" "exists" "in" "as" "∀" "∃" "→" "∨" "∧" ";" "," ":" "eval"))) ;; The important lexer for indentation's performance is the backward ;; lexer, so for the forward lexer we delegate to the backward one when @@ -427,6 +450,8 @@ The point should be at the beginning of the command name." (goto-char (1+ (point))) "|}") ((member tok coq-smie-proof-end-tokens) "Proof End") ((member tok '("Obligation")) "Proof") + ;; FIXME: this case should be useless now that we replace + ;; smie-default-forward... by a smarter function. ((coq-dot-friend-p tok) ".") ;; Try to rely on backward-token for non empty tokens: bugs (hangs) ;; ((not (zerop (length tok))) (save-excursion (coq-smie-backward-token))) @@ -552,7 +577,7 @@ The point should be at the beginning of the command name." ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil)) ": ltacconstr") - ((equal tok ":=") + ((member tok '(":=" "::=")) (save-excursion (save-excursion (coq-smie-:=-deambiguate)))) @@ -905,6 +930,21 @@ Typical values are 2 or 4." ;; | Leaf => add x d l +;; Returns the column of the beginning of current atomic tactic (non +;; composed). Returns the command start column if not found. +(defun coq-find-with-related-backward() + (let ((cmd-start (save-excursion (coq-find-real-start)))) + (save-excursion + ;; no point in going further the start of the command + ;; let us find a tactical between it and point + (let ((tok (coq-smie-search-token-backward '(";" "||" "|" "+") cmd-start))) + ;; hopefully we found the start of the current (non composed)tactic + ;; move point after the token found (if not found it will not move) + (forward-char (length tok)) + (forward-comment (point-max)); skip spaces + ;; (coq-find-not-in-comment-forward "[^;+[:space:]|]") + (current-column))))) + (defun coq-is-at-first-line-of-def-decl () (let ((pt (point))) (save-excursion @@ -927,7 +967,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." (basic proof-indent))) (:close-all t) (:list-intro - (or (member token '("fun" "forall" "quantif exists")) + (or (member token '("fun" "forall" "quantif exists" "with")) ;; We include "." in list-intro for the ". { .. } \n { .. }" so the ;; second {..} is aligned with the first rather than being indented as ;; if it were an argument to the first. @@ -949,6 +989,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." 2) ((equal token "with match") coq-match-indent) + ((equal token "with") 2) ; add 2 to the column of "with" in the children ;;; the ";" tactical ;;; @@ -1010,6 +1051,12 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ; (smie-rule-parent 2) ; (smie-rule-parent))) + ;; "with" is also in the :list-intro rules and in :after. + ((equal token "with") + ;; Hack: We know that "with" is linked to the first word of + ;; the current atomic tactic. This tactic is the parent, not + ;; the "." of the previous command. + `(column . ,(+ 2 (coq-find-with-related-backward)))) ((equal token "with module") (if (smie-rule-parent-p "with module") @@ -1037,11 +1084,6 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." (smie-rule-parent 4))) - - - - - ;; This applies to forall located on the same line than "Lemma" ;; & co. This says that "if it *were* be on the beginning of ;; line" (which it is not) it would be indented of 2 wrt diff --git a/coq/coq-system.el b/coq/coq-system.el index 0b9b6c58..aad7d386 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -658,4 +658,4 @@ then be set using local file variables." "-emacs-U")) coq-prog-name)))) -;;; coq-compile-common.el ends here +;;; coq-system.el ends here diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 27b64942..411347f0 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -60,26 +60,33 @@ Let xxx (* Precedence of "else" w.r.t "," and "->"! *) 3). Module Y. - Lemma L : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x. + Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x. Proof with auto with arith. intros x. induction x;simpl;intros... Qed. - Lemma L2 : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x. + Lemma L2 : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x. Proof with auto with arith. idtac. (* "as" tactical *) induction x as [ | x IHx]. - - auto with arith. + - cbn. + apply Nat.le_trans + with + (n:=0) (* aligning the different closes of a "with". *) + (m:=0) + (p:=0). + + auto with arith. + + auto with arith. - simpl. intros. auto with arith. Qed. - Lemma L' : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x - with L'' : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x. + Lemma L' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x + with L'' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x. Proof with auto with arith. - induction x;simpl;intros... - induction x;simpl;intros... @@ -249,32 +256,29 @@ Module X. intros r. {{ idtac; - exists - {| - fld1:=r.(fld2); - fld2:=r.(fld1); - fld3:=false - |}. + exists + {| + fld1:=r.(fld2); + fld2:=r.(fld1); + fld3:=false + |}. (* ltac *) match goal with - | _:rec |- ?a /\ ?b => split - | _ => fail - end. - - match goal with _:rec |- ?a /\ ?b => split | _ => fail end. - lazymatch goal with - _:rec |- ?a /\ ?b => split - | _ => fail - end. + Fail + lazymatch goal with + _:rec |- ?a /\ ?b => split + | _ => fail + end. - multimatch goal with - _:rec |- ?a /\ ?b => split - | _ => fail - end. + Fail + multimatch goal with + _:rec |- ?a /\ ?b => split + | _ => fail + end. { simpl. auto. } { simpl. auto. }}} @@ -337,13 +341,13 @@ Section SET. Fixpoint setVecProd (T : Type) (n : nat) (v1:Vector.t (set T) n) {struct v1}: (Vector.t T n) -> Prop := match v1 with - Vector.nil => + Vector.nil _ => fun v2 => match v2 with - Vector.nil => True + Vector.nil _ => True | _ => False end - | (Vector.cons x n' v1') => + | (Vector.cons _ x n' v1') => fun v2 => (* indentation of dependen "match" clause. *) match v2 @@ -354,8 +358,8 @@ Section SET. return (Vector.t T (pred n'') -> Prop) -> Prop with - | Vector.nil => fun _ => False - | (Vector.cons y n'' v2') => fun v2'' => (x y) /\ (v2'' v2') + | Vector.nil _ => fun _ => False + | (Vector.cons _ y n'' v2') => fun v2'' => (x y) /\ (v2'' v2') end (setVecProd T n' v1') end. @@ -373,7 +377,7 @@ Module curlybracesatend. reflexivity. } exists (S (S n)). simpl. - rewrite NPeano.Nat.add_1_r. + rewrite Nat.add_1_r. reflexivity. Qed. @@ -388,7 +392,7 @@ Module curlybracesatend. exists (S (S n)). simpl. - rewrite NPeano.Nat.add_1_r. + rewrite Nat.add_1_r. reflexivity. Qed. @@ -402,7 +406,7 @@ Module curlybracesatend. reflexivity. } { exists (S (S n)). simpl. - rewrite NPeano.Nat.add_1_r. + rewrite Nat.add_1_r. reflexivity. } } idtac. diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 75ddbf69..dff19e76 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -411,7 +411,7 @@ or if the window is the only window of its frame." ;; weird test cases: ;; cur=45, max=23, desired=121, extraline=0 ;; current height - ;;; ((cur-height (window-height window)) + ;;; (cur-height (window-height window)) ;; Most window is allowed to grow to ((max-height (/ (frame-height (window-frame window)) |