[nongnu] elpa/proof-general 0b3454492c 7/8: Merge pull request #647 from Matafou/fix-#646-indent-funargs

[ELPA Syncer]

branch: elpa/proof-general
commit 0b3454492ca0ac74a41efc8c9f50d66213ba0cbe
Merge: 1554eb7936 39911fe049
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #647 from Matafou/fix-#646-indent-funargs
    
    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 79bc3ab85e..6bd367e26b 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -767,7 +767,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)))
@@ -932,7 +932,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
@@ -1319,6 +1319,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 :=")
    ;; by default we pass the token name, but maybe it would be safer
    ;; to simply fail, so that we detect missing tokens in this function?
@@ -1365,6 +1366,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
@@ -1382,8 +1510,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)?
@@ -1396,7 +1523,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))
@@ -1431,7 +1558,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