[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 39911fe049 2/8: Fix #646. Indentation of fun
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general 39911fe049 2/8: Fix #646. Indentation of function arguments. |
Date: |
Tue, 29 Mar 2022 02:58:41 -0400 (EDT) |
branch: elpa/proof-general
commit 39911fe04921798656e0e95d5210274242172396
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Fix #646. Indentation of function arguments.
---
CHANGES | 13 +++
ci/test-indent/indent-equations.v | 37 +++++++
ci/test-indent/indent-inside-command-boxed.v | 19 ++--
ci/test-indent/indent-inside-command.v | 24 +++--
ci/test-indent/indent-tac.v | 23 ++++-
coq/coq-mode.el | 1 +
coq/coq-smie.el | 139 +++++++++++++++++++++++++--
7 files changed, 233 insertions(+), 23 deletions(-)
diff --git a/CHANGES b/CHANGES
index e615731182..40ed9e9bdf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -204,6 +204,19 @@ also https://wiki.ubuntu.com/Releases).
Variable `coq-indent-box-style' only affects indentation after
quantifiers (used to affect script braces "{").
+ Variable `coq-indent-align-with-first-arg` governs between these
+ two indentation behaviours:
+
+ (setq 'coq-indent-align-with-first-arg t) gives
+
+ somefunciton x y
+ z t u
+ v
+ (setq 'coq-indent-align-with-first-arg nil) give (default):
+
+ somefunciton x y
+ z t u
+ v
* Changes of Proof General 4.4 from Proof General 4.3
diff --git a/ci/test-indent/indent-equations.v
b/ci/test-indent/indent-equations.v
index 3e200b5f2a..4d00809a30 100644
--- a/ci/test-indent/indent-equations.v
+++ b/ci/test-indent/indent-equations.v
@@ -10,6 +10,13 @@ Module Equations.
neg true := false ;
neg false := true.
+ Equations neg' (b : bool) : bool :=
+ neg' true
+ :=
+ false ;
+ neg' false :=
+ true.
+
Lemma neg_inv : forall b, neg (neg b) = b.
Proof.
intros b.
@@ -41,6 +48,16 @@ Module Equations.
| false := filter l p
}.
+ Equations filter_ {A} (l : list A) (p : A -> bool) : list A :=
+ filter nil p := nil;
+ filter (cons a l) p with p a => {
+ | true :=
+ a :: filter l p ;
+ | false
+ :=
+ filter l p
+ }.
+
Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
filter' (cons a l) p with p a =>
{
@@ -49,6 +66,16 @@ Module Equations.
};
filter' nil p := nil.
+ Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
+ filter' (cons a l) p with p a =>
+ {
+ | true :=
+ a :: filter' l p ;
+ | false
+ := filter' l p
+ };
+ filter' nil p := nil.
+
Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
filter' (cons a l) p with p a =>
{
@@ -57,6 +84,16 @@ Module Equations.
};
filter' nil p := nil.
+ Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
+ filter' (cons a l) p with p a =>
+ {
+ true :=
+ a :: filter' l p ;
+ false
+ := filter' l p
+ };
+ filter' nil p := nil.
+
Equations filter'' {A} (l : list A) (p : A -> bool) : list A :=
filter'' (cons a l) p with p a =>
{ | true := a :: filter'' l p ;
diff --git a/ci/test-indent/indent-inside-command-boxed.v
b/ci/test-indent/indent-inside-command-boxed.v
index b5b0e9330a..621f18fd3b 100644
--- a/ci/test-indent/indent-inside-command-boxed.v
+++ b/ci/test-indent/indent-inside-command-boxed.v
@@ -1,9 +1,9 @@
Require Export
- Coq.Lists.List.
+ Coq.Lists.List.
Require
Export
- Arith.
+ Arith.
Module
Mod.
@@ -38,7 +38,12 @@ Module
Let x := 1. Let y := 2.
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
-
+ Definition foo :=
+ foo x (y
+ a b)
+ z t (* align with function foo + 2. *)
+ u v. (* align with arg z on bol of previous line *)
+
Inductive test
: nat
@@ -67,7 +72,7 @@ Module
Lemma L4 : forall x:nat,
Nat.iter x (A:=nat)
- (plus 2) 0 >= x.
+ (plus 2) 0 >= x.
Proof.
idtac.
Qed.
@@ -83,9 +88,9 @@ Module
Qed.
Lemma L1 : forall x:nat, Nat.iter x
- (A:=nat)
- (plus 2)
- 0 >= x.
+ (A:=nat)
+ (plus 2)
+ 0 >= x.
Proof.
idtac.
Qed.
diff --git a/ci/test-indent/indent-inside-command.v
b/ci/test-indent/indent-inside-command.v
index 5ad50e6eec..9566ca3108 100644
--- a/ci/test-indent/indent-inside-command.v
+++ b/ci/test-indent/indent-inside-command.v
@@ -1,9 +1,9 @@
Require Export
- Coq.Lists.List.
+ Coq.Lists.List.
Require
Export
- Arith.
+ Arith.
Module
Mod.
@@ -35,6 +35,18 @@ Module
:=
1.
+ Definition arith1 a
+ (b:nat) c
+ d e
+ :=
+ 1.
+ Definition
+ arith1
+ (b:nat) c
+ d e
+ :=
+ 1.
+
Let x := 1. Let y := 2.
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
@@ -56,7 +68,7 @@ Module
Lemma L4 : forall x:nat,
Nat.iter x (A:=nat)
- (plus 2) 0 >= x.
+ (plus 2) 0 >= x.
Proof.
idtac.
Qed.
@@ -72,9 +84,9 @@ Module
Qed.
Lemma L1 : forall x:nat, Nat.iter x
- (A:=nat)
- (plus 2)
- 0 >= x.
+ (A:=nat)
+ (plus 2)
+ 0 >= x.
Proof.
idtac.
Qed.
diff --git a/ci/test-indent/indent-tac.v b/ci/test-indent/indent-tac.v
index 19aede3707..4a27e7038b 100644
--- a/ci/test-indent/indent-tac.v
+++ b/ci/test-indent/indent-tac.v
@@ -280,16 +280,16 @@ Module GoalSelectors.
[aa]:{ auto. }
2:{ auto. }
[ee]:auto.
- { 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.}
+ [aa]:{ auto. }
+ 2:{ auto. }
[ee]:auto.
- { auto.}
+ { auto. }
Qed.
@@ -404,6 +404,21 @@ Module X.
{auto. }
{auto. }
}
+ intros r. {
+ exists
+ {|
+ fld1:=
+ r.(fld2);
+ fld2
+ :=r.(fld1);
+ fld3
+ :=
+ false
+ |}.
+ split.
+ {auto. }
+ {auto. }
+ }
auto.
auto.
Qed.
diff --git a/coq/coq-mode.el b/coq/coq-mode.el
index 16140caf13..abb614a389 100644
--- a/coq/coq-mode.el
+++ b/coq/coq-mode.el
@@ -214,6 +214,7 @@ Near here means PT is either inside or just aside of a
comment."
(smie-setup coq-smie-grammar #'coq-smie-rules
:forward-token #'coq-smie-forward-token
:backward-token #'coq-smie-backward-token)
+ (add-hook 'smie-indent-functions #'coq-smie--args nil t)
;; old indentation code.
;; (require 'coq-indent)
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 00c1fd5e38..5dc6f872ff 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -755,7 +755,7 @@ The point should be at the beginning of the command name."
;; (let ((nxttok (coq-smie-backward-token))) ;; recursive call
;; (coq-is-cmdend-token nxttok))))
;; (forward-char -1)
- ;; (if (looking-at "{") "{ subproof" "} subproof")))
+ ;; (if (looking-at "{") "{ subproof" "} subproof"))
((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac2?\\|uconstr\\)"
(- (point) 7)))
@@ -920,7 +920,7 @@ The point should be at the beginning of the command name."
;; generic "Com start" token, so that everything in the command
;; is considered a child of this token. This makes indentation
;; never look above the current command start (unless indenting
- ;; the first line of the command. For now we only apply this to
+ ;; the first line of the command). For now we only apply this to
;; things starting with a letter, because the grammar makes use
;; of non letters token and this would hide them. Other
;; exception: Ltac things like "match" and "let' that need to be
@@ -1307,6 +1307,7 @@ If nil, default to `proof-indent' if it exists or to
`smie-indent-basic'."
((coq-is-bullet-token tk) "after bullet")
((member tk '("with" ":" "by" "in tactic" "as" ",")) "tactic infix")
((member tk '("<:" "<+" "with module")) "modulespec infix") ;; ":=
inductive" ":= module" and other ":= xxx"
+ ((member tk '(":= record")) tk) ;; avoids capture by next case
((string-prefix-p ":= " tk) "after :=")
((member tk '(". proofstart" ". modulestart")) "dot script parent open")
;; by default we pass the token name, but maybe it would be safer
@@ -1354,6 +1355,133 @@ If nil, default to `proof-indent' if it exists or to
`smie-indent-basic'."
(coq-smie-search-token-backward '("forall" "quantif exists"))
(equal (current-column) (current-indentation))))
+
+
+(defcustom coq-indent-align-with-first-arg nil
+ "Non-nil if indentation should try to align arguments on the first one.
+With a non-nil value you get
+
+ let x = List.map (fun x -> 5)
+ my list
+
+whereas with a nil value you get
+
+ let x = List.map (fun x -> 5)
+ my list"
+ :type 'boolean)
+
+;; to be added to smie-indent-functions: this function deals with
+;; arguemtns of functions. Explanation: it is hardcoded in SMIE that a
+;; list of expressions (with no separator) is actually a single
+;; expression. Thus we need an adhoc treatment to deal with the indentation
+;; of arguments if they are not on the same line as the function.
+
+;; Definition foo :=
+;; foo x y
+;; z t (* align with function foo + 2. *)
+;; u v. (* align with arg z on bol of previous line *)
+
+;; More complex:
+;; Definition foo :=
+;; foo x (y
+;; a b)
+;; z t (* align with function foo + 2. *)
+;; u v. (* align with arg z on bol of previous line *)
+
+;; This function examines these case. The generic situation is this:
+;; we want to indent token (tk)
+
+;;
+;; ... other sexps? ...
+;; (sexp) (se
+;; ^ xp) (sexp)
+;; | tk
+;; | ^
+;; | token to indent (tk)
+;; |
+;; last skipped token (lstk)
+
+;; The function examines the list of sexps on the left of
+;; (point) until reaching a beginning of line. Then it tries to
+;; determine what the last token skipped (lstk) is:
+
+;; - if none was skipped it means that (tk) is not an argument, so we
+;; give up and let the regular indentation do the job.
+
+;; - if (lstk) is still an argument of something above, indentation
+;; should align (tk) with (lstk).
+
+;; - if (lstk) is really a function (no more sexp before it) then we
+;; should indent from it (+2 in the example above).
+;; Remark: Stefan Monier may make this less adhoc some day.
+(defun coq-smie--args ()
+ ;; PG specifics: some token are like parenthesis in the grammar but
+ ;; are not paren-characters in the syntax table. ". proofstart" and
+ ;; ". module start" mainly. These tokens need a special treatment.
+ ;; We use coq-find-real-start to avoid crossing them
+ (let ((limit (save-excursion (coq-find-real-start))))
+ (unless
+ (or coq-indent-align-with-first-arg
+ (nth 8 (syntax-ppss))
+ (looking-at comment-start-skip)
+ (looking-at "[ \t]*$") ; tuareg bug #179
+ ;; the current token is a special token corresponding to
+ ;; an ends of command, but it is not recognized as such in
+ ;; the grammar, and the 2 tests below wrongly succeed:
+ ;; this token cannot be an argument of anything.
+ (member (nth 0 (save-excursion (smie-indent-forward-token)))
+ '(". proofstart" ". modulestart" "{|" "{|"))
+ (numberp (nth 1 (save-excursion (smie-indent-forward-token))))
+ (numberp (nth 2 (save-excursion (smie-indent-backward-token)))))
+ (save-excursion
+ (let ((positions nil)
+ arg)
+ (while (and (null (car (smie-backward-sexp)))
+ ;; never go beyond the current command start.
+ ;; otherwise things like this:
+ ;; { tac1. }
+ ;; { tac2. }
+ ;; would be detected as function applications.
+ (>= (point) limit)
+ (push (point) positions)
+ (not (smie-indent--bolp))))
+ (save-excursion
+ ;; Figure out if the atom we just skipped is an argument rather
+ ;; than a function.
+ (setq arg
+ (let ((left (smie-backward-sexp)))
+ (or (null (car left))
+ (funcall smie-rules-function :list-intro
+ (funcall smie-backward-token-function))))))
+ (cond
+ ((null positions)
+ ;; We're the first expression of the list. In that case, the
+ ;; indentation should be (have been) determined by its context.
+ nil)
+ (arg ;; There's a previous element, and it's not special
+ ;; (it's not the function), so let's just align with that one.
+ (goto-char (car positions))
+ (if (fboundp 'smie-indent--current-column)
+ (smie-indent--current-column)
+ (current-column)))
+ (t ;; There's no previous arg at BOL. Align with the function.
+ ;; TODO: obey boxed style? this was for quantifiers.
+ (goto-char (car positions))
+ ;; Special case: the function we found is actually next to a
command start.
+ ;; We prefer to indent from it.
+ (when (not (= (save-excursion (back-to-indentation) (point))
(point)))
+ (let ((left (save-excursion (smie-backward-sexp))))
+ (if (equal (nth 2 left) "Com start")
+ (goto-char (nth 1 left)))))
+ (+ (smie-indent--offset 'args)
+ ;; We used to use (smie-indent-virtual), but that
+ ;; doesn't seem right since it might then indent args less
than
+ ;; the function itself.
+ (if (fboundp 'smie-indent--current-column)
+ (smie-indent--current-column)
+ (current-column))))))))))
+
+
;; Reminder: (smie-rule-separator kind) only works for *parenthesized*
enumerations.
;; and ":= inductive" is not considered a parenthesis so "|" needs special hack
;; below. "," for tuples and for tac args cannot be distinguished, so it
cannot be
@@ -1371,8 +1499,7 @@ KIND is the situation and TOKEN is the thing w.r.t which
the rule applies."
(`(:elem . basic) (or coq-indent-basic (bound-and-true-p proof-indent)
2))
(`(:elem . arg) (if (smie-rule-prev-p "} subproof") 0 nil)) ;; hack:
"{} {}"" not an application
(`(:close-all . ,_) t)
- (`(:list-intro . ,_) (member token '("fun" "forall" "quantif exists"
- "with" "Com start")))
+ (`(:list-intro . ,_) (member token '("fun" "forall" "quantif exists"
"with"))) ;; "Com start"
(`(:after . ,_) ;; indent relative to token (parent of token at point).
(pcase (coq-indent-categorize-token-after token)
("} subproof" 0) ;;shouldn't be captured by (:elem . args)?
@@ -1383,7 +1510,7 @@ KIND is the situation and TOKEN is the thing w.r.t which
the rule applies."
((and "; tactic" (guard (hang-p)) (guard (not (parent-p "Com
start")))) 0)
("; tactic" 2);; only applies "after" so when ";" is alone at its
line
((guard (string-match "^[^][:alnum:](){}\[]" token)) 2); guessing
infix operator.
- ;;((guard (and (message "DEFAULTING") nil)) nil)
+ ;;((guard (and (message "################### RULES
AFTER:DEFAULTING") nil)) nil)
))
(`(:before . ,_) ; indent token at point itself
(let* ((cat (coq-indent-categorize-token-before token))
@@ -1418,7 +1545,7 @@ KIND is the situation and TOKEN is the thing w.r.t which
the rule applies."
((smie-rule-prev-p "} subproof") (parent))
((smie-rule-prev-p "{ subproof") (coq-smie-backward-token) (+ 2
(smie-indent-virtual)))
((smie-rule-prev-p ".") (smie-backward-sexp 'half)
(smie-indent-virtual)))))))))))
-
+;;((guard (and (message "################### RULES BEFORE: DEFAULTING") nil))
nil)
(provide 'coq-smie)
;;; coq-smie.el ends here
- [nongnu] elpa/proof-general updated (40c40d229e -> e1e29acb04), ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 3c9bed7061 1/8: Add an option to stop proof-shell-kill-function from killing buffers., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 39911fe049 2/8: Fix #646. Indentation of function arguments.,
ELPA Syncer <=
- [nongnu] elpa/proof-general 1554eb7936 6/8: Merge pull request #648 from Matafou/fix-#599-Proof-using-bad-detection, ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general e1e29acb04 8/8: Merge pull request #639 from Chobbes/save-frames, ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 24da4f5593 3/8: Fix #599, bad detection of "Proof" in "Proof using" suggestions., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 17a4cc00d6 5/8: Merge pull request #649 from Matafou/fix-#618-missing-keyword-derive, ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general ce033327e3 4/8: Support for command "Derive SuchThat As"., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 0b3454492c 7/8: Merge pull request #647 from Matafou/fix-#646-indent-funargs, ELPA Syncer, 2022/03/29