branch: elpa/proof-general
commit 20028f74c4197eea6cc22c0093444e188959046f
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <mata...@users.noreply.github.com>
New smie grammar + indentation rules + tests.
Main design choice for this new version: the first word of a command
is now a token "Com start". Together with the "." token for ending a
command this makes the parsing much more "local".
Users may experience a few changes in the indentation. A few special
cases where the old indentation would reduce shifting to the right
have been removed.
Non regression testing have been added.
See comments in coq-smie.el at coq-smie-grammar for more details.
---
CHANGES | 10 +
ci/test-indent/.gitignore | 1 +
ci/test-indent/coq-test-indent.el | 96 +++++
ci/test-indent/coq-test-indent.sh | 37 ++
ci/test-indent/indent-commands-boxed.v | 268 ++++++++++++
ci/test-indent/indent-commands.v | 265 ++++++++++++
ci/test-indent/indent-inside-command-boxed.v | 104 +++++
ci/test-indent/indent-inside-command.v | 93 ++++
ci/test-indent/indent-tac-boxed.v | 164 +++++++
coq/ex/indent.v => ci/test-indent/indent-tac.v | 451 +++++++++++++-------
ci/test-indent/indent_equations.v | 79 ++++
ci/test-indent/indent_monadic.v | 44 ++
ci/test-indent/tests.sh | 8 +
coq/coq-indent.el | 2 +-
coq/coq-smie.el | 568 +++++++++++++------------
coq/coq-syntax.el | 2 +-
coq/ex/indent.v | 2 +-
17 files changed, 1771 insertions(+), 423 deletions(-)
diff --git a/CHANGES b/CHANGES
index 56232b3..56f3da1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -193,6 +193,16 @@ also https://wiki.ubuntu.com/Releases).
- 92: Compile before require from current directory failing
with 8.5
+*** indentation code refactored
+
+ A big refactoring of the code for indentation has been done. You
+ may experience a few changes in indentation results. Mostly small
+ shifts to the right.
+
+ Variable `coq-indent-box-style' only affects indentation after
+ quantifiers (used to affect script braces "{").
+
+
* Changes of Proof General 4.4 from Proof General 4.3
** ProofGeneral has moved to GitHub!
diff --git a/ci/test-indent/.gitignore b/ci/test-indent/.gitignore
new file mode 100644
index 0000000..8e2384a
--- /dev/null
+++ b/ci/test-indent/.gitignore
@@ -0,0 +1 @@
+indented_*
\ No newline at end of file
diff --git a/ci/test-indent/coq-test-indent.el
b/ci/test-indent/coq-test-indent.el
new file mode 100644
index 0000000..2320433
--- /dev/null
+++ b/ci/test-indent/coq-test-indent.el
@@ -0,0 +1,96 @@
+;;; Regression testing of indentation.
+
+;;; Initially the file is indented as it is supposed to be. Each line
+;;; is unindented, then indented. If the new indentation differ a
+;;; comment is added to signal it.
+
+;;; WARNING: there are relative path names, so this currently works
+;;; only frowhen the current directory is the one containin this file.
+
+(defun blank-line-p ()
+ (= (current-indentation)
+ (- (line-end-position) (line-beginning-position))))
+
+
+(defun line-fixindent ()
+ (save-excursion
+ (let ((end (line-end-position)))
+ (re-search-forward "fixindent" end t))))
+
+
+(defun test-indent-line (&optional nocomment)
+ (interactive)
+ (unless (or (blank-line-p) (line-fixindent))
+ (back-to-indentation)
+ (let ((init-col (current-column)))
+ ;; avoid moving comments
+ (unless (proof-inside-comment (point)) (delete-horizontal-space))
+ (indent-according-to-mode)
+ (let ((res (- (current-column) init-col)))
+ (unless (= 0 res)
+ (save-excursion
+ (end-of-line)
+ (unless nocomment
+ (insert (format " (*<=== %s%d INDENT CHANGED *)"
+ (if (< res 0) "" "+")
+ res))))
+ res)
+ 0))))
+
+
+(defun remove-previous-comment ()
+ (interactive)
+ (save-excursion
+ (end-of-line)
+ (let* ((com (re-search-backward " (\\*<===" (line-beginning-position) t))
+ (strt (and com (point)))
+ (end (and com (line-end-position))))
+ (when com (delete-region strt end)))))
+
+
+(defun test--indent-region (beg end boxed &optional nocomment)
+ (let ((line-move-visual nil)
+ ;; we store the last line number rather than the position
+ ;; since by inderting things we shift the end pos, but not the
+ ;; end line.
+ (last-line (line-number-at-pos end))
+ (stop nil))
+ (set (make-local-variable 'coq-indent-box-style) boxed)
+ (goto-char beg)
+ (while (and (<= (line-number-at-pos) last-line)
+ (not stop))
+ (remove-previous-comment)
+ (test-indent-line nocomment)
+ (setq stop (/= (forward-line) 0)))))
+
+(defun remove-comments-region (beg end)
+ (interactive "r")
+ (goto-char beg)
+ (let ((line-move-visual nil))
+ (while (< (point) end);; loops because end position changes.
+ (remove-previous-comment)
+ (forward-line))))
+
+
+(defun test-indent-region (beg end &optional boxed nocomment)
+ (interactive "r\nP")
+ (test--indent-region beg end boxed nocomment))
+
+
+(defun test-indent-region-boxed (beg end &optional nocomment)
+ (interactive "r")
+ (test--indent-region beg end t nocomment))
+
+
+(defun test-indent-buffer (&optional nocomment) (interactive)
+ (test--indent-region (point-min) (point-max) nil nocomment))
+
+(defun test-indent-buffer-boxed (&optional nocomment) (interactive)
+ (test--indent-region (point-min) (point-max) t nocomment))
+
+(defun launch-test (orig indented &optional boxed)
+ (load-file "../../generic/proof-site.el")
+ (find-file orig)
+ (write-file indented)
+ (if boxed (test-indent-buffer-boxed t) (test-indent-buffer t))
+ (write-file indented))
diff --git a/ci/test-indent/coq-test-indent.sh
b/ci/test-indent/coq-test-indent.sh
new file mode 100755
index 0000000..7204d00
--- /dev/null
+++ b/ci/test-indent/coq-test-indent.sh
@@ -0,0 +1,37 @@
+
+# This script should be launched from its own directory, so that file
+# coq-test-indent.el is accessible.
+
+GREEN='\033[1;32m'
+RED='\033[1;31m'
+MAGENTA='\033[1;35m'
+NC='\033[0m' # No Color
+
+TESTFILE=$1
+INDENTEDTESTFILE=indented_$1
+
+BOXED="nil"
+if [[ "$1" == *"boxed.v" ]];
+then
+ BOXED="t"
+fi
+
+echo "cp $TESTFILE $INDENTEDTESTFILE"
+cp $TESTFILE $INDENTEDTESTFILE
+
+emacs -q -batch --eval "(progn (load-file \"coq-test-indent.el\") (launch-test
\"$TESTFILE\" \"$INDENTEDTESTFILE\" $BOXED))"
+
+# echo "grep \"INDENT CHANGED\" $INDENTEDTESTFILE"
+# grep "INDENT CHANGED" $INDENTEDTESTFILE
+echo -n " diff -q $TESTFILE $INDENTEDTESTFILE..."
+diff -q $TESTFILE $INDENTEDTESTFILE > /dev/null
+if [[ $? == 1 ]] ;
+then echo " DIFFERENCES FOUND"
+ printf "${RED} TEST FAILURE ***${NC}\n"
+ echo " *** details can be seen with:"
+ echo " *** diff --side-by-side --suppress-common-lines $TESTFILE
$INDENTEDTESTFILE"
+ echo " *** or graphically: "
+ echo " *** meld $TESTFILE $INDENTEDTESTFILE"
+else echo "NO DIFFERENCE"
+ printf "${GREEN} TEST SUCCESS *** ${NC}\n"
+fi
diff --git a/ci/test-indent/indent-commands-boxed.v
b/ci/test-indent/indent-commands-boxed.v
new file mode 100644
index 0000000..f22bb50
--- /dev/null
+++ b/ci/test-indent/indent-commands-boxed.v
@@ -0,0 +1,268 @@
+
+Require Export Coq.Lists.List.
+
+Module Mod.
+
+ Module Foo.
+ Axiom X:Set.
+ Axiom Y:Set.
+ Axiom Z:Set.
+ End Foo.
+
+ Section Sec.
+ Axiom X:Set.
+ Axiom Y:Set.
+ Axiom Z:Set.
+ End Sec.
+
+ Definition a1 := 1.
+ Definition A2 := 1.
+ Definition arith1:=
+ 1.
+ Definition arith1
+ :=
+ 1.
+ Definition
+ arith1
+ :=
+ 1.
+
+ Let x := 1. Let y := 2.
+
+ Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+
+
+ Inductive test : nat -> Prop :=
+ C1 : forall n, test n
+ | C2 : forall n, test n
+ | C3 : forall n, test n
+ | C4 : forall n, test n.
+
+ Inductive testbar' : nat -> Prop :=
+ | Cbar1 : forall n, test n
+ | Cbar2 : forall n, test n
+ | Cbar3 : forall n, test n
+ | Cbar4 : forall n, test n.
+
+ Inductive test2 : nat -> Prop
+ := | C21 : forall n, test2 n
+ | C22 : forall n, test2 n
+ | C23 : forall n, test2 n
+ | C24 : forall n, test2 n.
+
+ Inductive test' : nat -> Prop :=
+ C1' : forall n, test' n
+ | C2' : forall n, test' n
+ | C3' : forall n, test' n
+ | C4' : forall n, test' n
+ with
+ test2' : nat -> Prop :=
+ C21' : forall n, test2' n
+ | C22' : forall n, test2' n
+ | C23' : forall n, test2' n
+ | C24' : forall n, test2' n
+ with test3' : nat -> Prop :=
+ C21' : forall n, test2' n
+ | C22' : forall n, test2' n
+ | C23' : forall n, test2' n
+ | C24' : forall n, test2' n
+ with test4' : nat -> Prop :=
+ | C21' : forall n, test2' n
+ | C22' : forall n, test2' n
+ | C23' : forall n, test2' n
+ | C24' : forall n, test2' n.
+
+
+ Inductive test3
+ : nat -> Prop
+ := C31 : forall n, test3 n
+ | C32 : forall n, test3 n
+ | C33 : forall n, test3 n .
+
+ (* Goal parenthesizing. *)
+ Lemma L : True.
+ Proof.
+ idtac.
+ idtac... (* special case of command ender. *)
+ idtac.
+ Qed.
+
+ (* Goal starter *)
+ Definition Foo:True.
+ exact I.
+ Defined.
+
+ (* Bullets. *)
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac. idtac.
+ idtac.
+ {
+ idtac.
+ idtac.
+ }
+ idtac. {
+ idtac.
+ idtac. }
+ { idtac.
+ idtac.
+ }
+ {
+ idtac.
+ idtac.
+ }
+ { idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+
+ { idtac . {
+ idtac.
+ idtac.
+ }
+ }
+ idtac.
+ }
+ idtac. { idtac. {
+ idtac.
+ idtac.
+ }
+ }
+ idtac.
+
+ { idtac . {
+ idtac.
+ idtac.
+ }
+ }
+ {
+ idtac.
+ idtac.
+ idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ Qed.
+
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ { idtac.
+ idtac. }
+ {
+ idtac.
+ idtac.
+ }
+ { idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ { idtac. idtac. { idtac.
+ idtac. }
+ idtac.
+ }
+ { idtac. { idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ }
+ { idtac. { idtac.
+ {
+ idtac.
+ idtac.
+ }
+ idtac.
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ {
+ idtac.
+ - idtac.
+ idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ Qed.
+
+
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ -
+ idtac.
+ idtac.
+ - idtac.
+ idtac.
+ + idtac.
+ idtac.
+ + idtac.
+ idtac.
+ * idtac.
+ - idtac.
+ Qed.
+
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ -
+ idtac.
+ idtac.
+ idtac.
+ idtac.
+ - idtac.
+ { idtac.
+ - idtac.
+ idtac.
+ - idtac.
+ idtac.
+ }
+ - idtac. idtac. {
+ idtac.
+ - idtac.
+ idtac.
+ - idtac.
+ idtac.
+ }
+ idtac.
+ - idtac.
+ Qed.
+
+
+ (* goal selectors. *)
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ 2:idtac.
+ 3-6:idtac.
+
+ 2:{ idtac.
+ idtac. }
+ {
+ idtac.
+ idtac.
+ }
+ [foo]:{
+ idtac.
+ - idtac.
+ idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ Qed.
+
+
+
+End Mod.
diff --git a/ci/test-indent/indent-commands.v b/ci/test-indent/indent-commands.v
new file mode 100644
index 0000000..9d1c52c
--- /dev/null
+++ b/ci/test-indent/indent-commands.v
@@ -0,0 +1,265 @@
+
+Require Export Coq.Lists.List.
+
+Module Mod.
+
+ Module Foo.
+ Axiom X:Set.
+ Axiom Y:Set.
+ Axiom Z:Set.
+ End Foo.
+
+ Section Sec.
+ Axiom X:Set.
+ Axiom Y:Set.
+ Axiom Z:Set.
+ End Sec.
+
+ Definition a1 := 1.
+ Definition A2 := 1.
+ Definition arith1:=
+ 1.
+ Definition arith1
+ :=
+ 1.
+ Definition
+ arith1
+ :=
+ 1.
+
+ Let x := 1. Let y := 2.
+
+ Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+
+
+ Inductive test : nat -> Prop :=
+ C1 : forall n, test n
+ | C2 : forall n, test n
+ | C3 : forall n, test n
+ | C4 : forall n, test n.
+
+ Inductive testbar' : nat -> Prop :=
+ | Cbar1 : forall n, test n
+ | Cbar2 : forall n, test n
+ | Cbar3 : forall n, test n
+ | Cbar4 : forall n, test n.
+
+ Inductive test2 : nat -> Prop
+ := | C21 : forall n, test2 n
+ | C22 : forall n, test2 n
+ | C23 : forall n, test2 n
+ | C24 : forall n, test2 n.
+
+ Inductive test' : nat -> Prop :=
+ C1' : forall n, test' n
+ | C2' : forall n, test' n
+ | C3' : forall n, test' n
+ | C4' : forall n, test' n
+ with
+ test2' : nat -> Prop :=
+ C21' : forall n, test2' n
+ | C22' : forall n, test2' n
+ | C23' : forall n, test2' n
+ | C24' : forall n, test2' n
+ with test3' : nat -> Prop :=
+ C21' : forall n, test2' n
+ | C22' : forall n, test2' n
+ | C23' : forall n, test2' n
+ | C24' : forall n, test2' n
+ with test4' : nat -> Prop :=
+ | C21' : forall n, test2' n
+ | C22' : forall n, test2' n
+ | C23' : forall n, test2' n
+ | C24' : forall n, test2' n.
+
+
+ Inductive test3
+ : nat -> Prop
+ := C31 : forall n, test3 n
+ | C32 : forall n, test3 n
+ | C33 : forall n, test3 n .
+
+ (* Goal parenthesizing. *)
+ Lemma L : True.
+ Proof.
+ idtac.
+ idtac... (* special case of command ender. *)
+ idtac.
+ Qed.
+
+ (* Goal starter *)
+ Definition Foo:True.
+ exact I.
+ Defined.
+
+ (* Bullets. *)
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac. idtac.
+ idtac.
+ {
+ idtac.
+ idtac.
+ }
+ idtac. {
+ idtac.
+ idtac. }
+ { idtac.
+ idtac.
+ }
+ {
+ idtac.
+ idtac.
+ }
+ { idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+
+ { idtac . {
+ idtac.
+ idtac.
+ }
+ }
+ idtac.
+ }
+ idtac. { idtac. {
+ idtac.
+ idtac.
+ }
+ }
+ idtac.
+
+ { idtac . {
+ idtac.
+ idtac.
+ }
+ }
+ {
+ idtac.
+ idtac.
+ idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ Qed.
+
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ { idtac.
+ idtac. }
+ {
+ idtac.
+ idtac.
+ }
+ { idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ { idtac. idtac. { idtac.
+ idtac. }
+ idtac.
+ }
+ { idtac. { idtac. {
+ idtac.
+ idtac.
+ }} }
+ { idtac. { idtac.
+ {
+ idtac.
+ idtac.
+ }
+ idtac.
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ {
+ idtac.
+ - idtac.
+ idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ Qed.
+
+
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ -
+ idtac.
+ idtac.
+ - idtac.
+ idtac.
+ + idtac.
+ idtac.
+ + idtac.
+ idtac.
+ * idtac.
+ - idtac.
+ Qed.
+
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ -
+ idtac.
+ idtac.
+ idtac.
+ idtac.
+ - idtac.
+ { idtac.
+ - idtac.
+ idtac.
+ - idtac.
+ idtac.
+ }
+ - idtac. idtac. {
+ idtac.
+ - idtac.
+ idtac.
+ - idtac.
+ idtac.
+ }
+ idtac.
+ - idtac.
+ Qed.
+
+
+ (* goal selectors. *)
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ 2:idtac.
+ 3-6:idtac.
+
+ 2:{ idtac.
+ idtac. }
+ {
+ idtac.
+ idtac.
+ }
+ [foo]:{
+ idtac.
+ - idtac.
+ idtac. {
+ idtac.
+ idtac.
+ }
+ idtac.
+ }
+ Qed.
+
+
+
+End Mod.
diff --git a/ci/test-indent/indent-inside-command-boxed.v
b/ci/test-indent/indent-inside-command-boxed.v
new file mode 100644
index 0000000..b5b0e93
--- /dev/null
+++ b/ci/test-indent/indent-inside-command-boxed.v
@@ -0,0 +1,104 @@
+
+Require Export
+ Coq.Lists.List.
+Require
+ Export
+ Arith.
+
+Module
+ Mod.
+
+ Module
+ Foo.
+ Axiom
+ X
+ :
+ Set.
+ Axiom Y
+ :
+ Set.
+ Axiom Z:
+ Set.
+ End
+ Foo.
+
+
+ Definition a1 :=
+ 1.
+ Definition A2
+ := 1.
+ Definition arith1
+ :=
+ 1.
+ Definition
+ arith1
+ :=
+ 1.
+
+ Let x := 1. Let y := 2.
+
+ Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+
+
+ Inductive test
+ : nat
+ ->
+ Prop :=
+ C1 : forall n,
+ test n
+ | C2 : forall n,
+ test
+ n
+ | C3 :
+ forall
+ n, test n
+ | C4 : forall n, test n.
+
+
+ (* Goal parenthesizing. *)
+ Lemma L :
+ True.
+ Proof.
+ idtac.
+ idtac... (* special case of command ender. *)
+ idtac.
+ Qed.
+
+
+ Lemma L4 : forall x:nat,
+ Nat.iter x (A:=nat)
+ (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ Qed.
+
+ Lemma L3 : forall x:nat,
+ Nat.iter
+ x
+ (A:=nat)
+ (plus 2)
+ 0 >= x.
+ Proof.
+ idtac.
+ Qed.
+
+ Lemma L1 : forall x:nat, Nat.iter x
+ (A:=nat)
+ (plus 2)
+ 0 >= x.
+ Proof.
+ idtac.
+ Qed.
+
+ Lemma L2 : forall x:nat, Nat.iter
+ x
+ (A:=nat)
+ (plus 2)
+ 0 >= x.
+ Proof.
+ idtac.
+ Qed.
+
+
+
+End Mod.
diff --git a/ci/test-indent/indent-inside-command.v
b/ci/test-indent/indent-inside-command.v
new file mode 100644
index 0000000..5ad50e6
--- /dev/null
+++ b/ci/test-indent/indent-inside-command.v
@@ -0,0 +1,93 @@
+
+Require Export
+ Coq.Lists.List.
+Require
+ Export
+ Arith.
+
+Module
+ Mod.
+
+ Module
+ Foo.
+ Axiom
+ X
+ :
+ Set.
+ Axiom Y
+ :
+ Set.
+ Axiom Z:
+ Set.
+ End
+ Foo.
+
+
+ Definition a1 :=
+ 1.
+ Definition A2
+ := 1.
+ Definition arith1
+ :=
+ 1.
+ Definition
+ arith1
+ :=
+ 1.
+
+ Let x := 1. Let y := 2.
+
+ Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+
+
+ Inductive test
+ : nat
+ ->
+ Prop :=
+ C1 : forall n,
+ test n
+ | C2 : forall n,
+ test
+ n
+ | C3 :
+ forall
+ n, test n
+ | C4 : forall n, test n.
+
+ Lemma L4 : forall x:nat,
+ Nat.iter x (A:=nat)
+ (plus 2) 0 >= x.
+ Proof.
+ idtac.
+ Qed.
+
+ Lemma L3 : forall x:nat,
+ Nat.iter
+ x
+ (A:=nat)
+ (plus 2)
+ 0 >= x.
+ Proof.
+ idtac.
+ Qed.
+
+ Lemma L1 : forall x:nat, Nat.iter x
+ (A:=nat)
+ (plus 2)
+ 0 >= x.
+ Proof.
+ idtac.
+ Qed.
+
+ Lemma L2 : forall x:nat, Nat.iter
+ x
+ (A:=nat)
+ (plus 2)
+ 0 >= x.
+ Proof.
+ idtac.
+ Qed.
+
+
+
+End Mod.
diff --git a/ci/test-indent/indent-tac-boxed.v
b/ci/test-indent/indent-tac-boxed.v
new file mode 100644
index 0000000..8c37d91
--- /dev/null
+++ b/ci/test-indent/indent-tac-boxed.v
@@ -0,0 +1,164 @@
+Module foo.
+ Lemma toto:nat.
+ Proof.
+ {{
+ exact 3.
+ }}
+ Qed.
+
+ Lemma foo: forall n: nat,
+ exists m:nat,
+ m = n + 1.
+ Proof.
+ intros n.
+ destruct n. {
+ exists 1.
+ reflexivity. }
+ exists (S (S n)).
+ simpl.
+ rewrite Nat.add_1_r.
+ reflexivity.
+ Qed.
+
+ 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...
+
+ induction x;
+ simpl ;
+ simpl ;
+ simpl ;
+ intros.
+ Qed.
+
+ Ltac foo:= intros x;
+ induction x;
+ simpl ;
+ intros.
+
+
+ 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.
+ idtacjqslkjd;[
+ intros x ;
+ induction x ;
+ simpl ;
+ intros].
+ 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.
+ Proof with auto with arith.
+ - induction x;simpl;intros...
+ - induction x;simpl;intros...
+ Qed.
+
+End foo.
+
+Section SET.
+ Definition set (T : Type) := Ensemble T.
+
+ Require Import Program.
+
+
+ Definition eq_n : forall A n (v:Vector.t A n) n',
+ n=n' ->
+ Vector.t A n'.
+ Proof.
+ intros A n v n' H.
+ rewrite <- H.
+ assumption.
+ Defined.
+
+End SET.
+
+Module curlybracesatend.
+
+
+ Lemma foo2: forall n: nat,
+ exists m:nat,
+ m = n + 1.
+ Proof.
+ intros n.
+ destruct n. {
+ exists 1.
+ reflexivity. }
+
+ exists (S (S n)).
+ simpl.
+ rewrite Nat.add_1_r.
+ reflexivity.
+ Qed.
+
+ Lemma foo3: forall n: nat,
+ forall n: nat,
+ forall n: nat,
+ forall n: nat, forall n: nat,
+ exists m:nat,
+ m = n + 1 ->
+ m = n + 1 ->
+ m = n + 1
+ -> m = n + 1
+ -> m = n + 1 ->
+ m = n + 1.
+ Proof.
+ intros n. cut (n = n). {
+ destruct n. {
+ exists 1.
+ reflexivity. } {
+ exists (S (S n)).
+ simpl.
+ rewrite Nat.add_1_r.
+ reflexivity. }
+ }
+ idtac.
+ reflexivity.
+ Qed.
+
+ Lemma foooooooooooooooo3: forall n: nat,
+ forall n: nat, forall n: nat,
+ f x ->
+ g y ->
+ f x -> forall n: nat,
+ forall n: nat,
+ forall n: nat,
+ exists m:nat,
+ m = n + 1 ->
+ m = n + 1 ->
+ m = n + 1
+ -> m = n + 1
+ -> m = n + 1 ->
+ m = n + 1 ->
+ True.
+ Proof.
+ intros n. cut (n = n).
+ {
+ destruct n. {
+ exists 1.
+ reflexivity. } {
+ exists (S (S n)).
+ simpl.
+ rewrite Nat.add_1_r.
+ reflexivity.
+ }
+ }
+ idtac.
+ reflexivity.
+ Qed.
+
+
+End curlybracesatend.
+
diff --git a/coq/ex/indent.v b/ci/test-indent/indent-tac.v
similarity index 57%
copy from coq/ex/indent.v
copy to ci/test-indent/indent-tac.v
index 2a0d5e4..7e474d4 100644
--- a/coq/ex/indent.v
+++ b/ci/test-indent/indent-tac.v
@@ -1,123 +1,206 @@
-(* First check that ".." is not considered as a command end. *)
-Require Export Coq.Lists.List.
-Notation "[ ]" := nil : list_scope.
-Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
-Require Import Arith.
-Open Scope nat_scope.
-Definition arith1:=
- 1 + 3 *
- 4.
+Module foo.
+ Lemma toto:nat.
+ Proof.
+ {{
+ exact 3.
+ }}
+ Qed.
-Definition arith2 :=
- 1 * 3 +
- 4.
+ 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...
-Definition logic1 :=
- True \/ False /\
- False.
+ induction x;
+ simpl ;
+ simpl ;
+ simpl ;
+ intros.
-Definition logic2 :=
- True /\ False \/
- False.
+ Ltac foo:=
+ intros x;
+ induction x;
+ simpl ;
+ simpl ;
+ simpl ;
+ intros.
-Definition logic3 :=
- let x := True /\ False in True \/
- False .
-Definition logic4 :=
- (let x := True /\ False in True) \/
- False .
+
+ induction x
+ ;
+ simpl
+ ;
+ intros
+ ;
+ intros
+ ;
+ intros
+ .
+
+
+ idtac
+ ;
+ [
+ induction x
+ ;
+ simpl
+ ;
+ intros
+ ].
+
+ Ltac foo
+ :=
+ intros x
+ ;
+ induction x
+ ;
+ simpl
+ ;
+ intros
+ ;
+ intros
+ .
+
-Record a : Type := make_a {
- aa : nat
- }.
+ idtac
+ ;
+ [
+ induction x
+ ;
+ simpl ;
+ simpl
+ | intros
+ ].
+
+ Ltac foo :=
+ intros x
+ ;
+ induction x
+ ;
+ simpl
+ ;
+ intros
+ ;
+ intros
+ .
+
-Module foo.
- Inductive test : nat -> Prop :=
- C1 : forall n, test n
- | C2 : forall n, test n
- | C3 : forall n, test n
- | C4 : forall n, test n.
-
- Inductive testbar' : nat -> Prop :=
- | Cbar1 : forall n, test n
- | Cbar2 : forall n, test n
- | Cbar3 : forall n, test n
- | Cbar4 : forall n, test n.
-
- Inductive test2 : nat -> Prop
- := | C21 : forall n, test2 n
- | C22 : forall n, test2 n
- | C23 : forall n, test2 n
- | C24 : forall n, test2 n.
-
- Inductive test' : nat -> Prop :=
- C1' : forall n, test' n
- | C2' : forall n, test' n
- | C3' : forall n, test' n
- | C4' : forall n, test' n
- with
- test2' : nat -> Prop :=
- C21' : forall n, test2' n
- | C22' : forall n, test2' n
- | C23' : forall n, test2' n
- | C24' : forall n, test2' n
- with test3' : nat -> Prop :=
- C21' : forall n, test2' n
- | C22' : forall n, test2' n
- | C23' : forall n, test2' n
- | C24' : forall n, test2' n
- with test4' : nat -> Prop :=
- | C21' : forall n, test2' n
- | C22' : forall n, test2' n
- | C23' : forall n, test2' n
- | C24' : forall n, test2' n.
-
- Let x := 1. Let y := 2.
-
- Let y2 := (1, 2, 3,
- 4, 5).
-
- Inductive test3 (* fixindent *)
- : nat -> Prop
- := C31 : forall n, test3 n
- | C32 : forall n, test3 n.
+
+
+ induction x ;
+ simpl ;
+ intros.
+
+ induction x
+ ;
+ simpl ;
+ intros.
+
+ induction x ;
+ simpl
+ ;
+ simpl ;
+ intros.
+
+
+ intros x
+ ; induction x
+ ; simpl
+ ; intros.
+
+ idtac;(intros x
+ ; induction x
+ ; simpl
+ ; intros).
+
+
+ idtac;( induction x;
+ simpl ;
+ intros ).
+
+ idtac;[ intros x
+ ; induction x
+ ; simpl
+ ; intros].
+
+ idtac
+ ;
+ [
+ induction x;
+ simpl ;
+ intros
+ | simpl
+ ; intros ].
+
+
+ idtac;[ intros x
+ ; induction x
+ | simpl
+ ; intros].
+
+
+ idtac;[ intros x ;
+ induction x
+ | simpl ;
+ intros
+ ].
+
+
+ idtac foobar;[ induction x;
+ simpl ;
+ intros ].
+
+ Qed.
+
+ Ltac foo:=
+ intros x;
+ induction x;
+ simpl ;
+ intros.
-End foo.
-
-Lemma toto:nat.
-Proof.
- {{
- exact 3.
- }}
-Qed.
-
-Let xxx (* Precedence of "else" w.r.t "," and "->"! *)
- : if true then nat * nat else nat ->
- nat
- := (if true then 1 else 2,
- 3).
-
-Module Y.
+
+ 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.
+ idtacjqslkjd;[
+ intros x ;
+ induction x ;
+ simpl ;
+ intros].
+ Qed.
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...
+ intros x;
+ [ induction x;
+ [
+ simpl;
+ intros...
+ ]
+ ]
Qed.
+
+
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].
+ [ | x IHx].
- cbn.
apply Nat.le_trans
with
- (n:=0) (* aligning the different closes of a "with". *)
- (m:=0)
- (p:=0).
+ (n:=0) (* aligning the different closes of a "with". *)
+ (m:=0)
+ (p:=0).
+ auto with arith.
+ auto with arith.
- simpl.
@@ -219,18 +302,23 @@ Module M1'.
intros.
Lemma l7: forall n:nat, n = n.
Proof.
- destruct n.
+ destruct n. intros.
{
auto.
}
{
- destruct n.
- {
- idtac;[
+ destruct n.
+ idtac a
+ ;
+ [
+ auto;
auto
+ |
+ auto;
+ auto.
].
- }
- auto.
+ }
+ auto.
}
Qed.
{destruct n.
@@ -254,8 +342,8 @@ Module M4'.
- auto.
- destruct n.
+ idtac;[
- auto
- ].
+ auto
+ ].
+ destruct n.
* auto.
* auto.
@@ -283,28 +371,30 @@ End M1''.
Record rec:Set := {
- fld1:nat;
- fld2:nat;
- fld3:bool
- }.
+ fld1:nat;
+ fld2:nat;
+ fld3:bool
+ }.
Class cla {X:Set}:Set := {
- cfld1:nat;
- cld2:nat;
- cld3:bool
- }.
+ cfld1:nat;
+ cld2:nat;
+ cld3:bool
+ }.
Module X.
- Lemma l
- :
+ Lemma l:
forall r:rec,
exists r':rec,
r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1).
Proof.
- intros r.
- { exists
+ idtac.
+ idtac.
+ idtac.
+ intros r. {
+ exists
{|
fld1:=r.(fld2);
fld2:=r.(fld1);
@@ -314,9 +404,20 @@ Module X.
{auto. }
{auto. }
}
+ auto.
+ auto.
Qed.
-
+ (* Issue #574 *)
+ Goal let x := 1 in True.
+ Proof.
+ intro.
+ match goal with
+ | y := _ : unit |- _ => idtac "unit"
+ | y := _ : nat |- _ => idtac "nat"
+ end.
+ Qed.
+
Lemma l2 :
forall r:rec,
exists r':rec,
@@ -342,7 +443,7 @@ Module X.
match goal with
| ?g := _:rec |- ?a /\ ?b => split
- | _ => fail
+ | _ => fail
end.
Fail
@@ -359,6 +460,27 @@ Module X.
{ simpl. auto. }
{ simpl. auto. }}}
+
+ - split.
+ match
+ goal
+ with
+ X => foo
+ end.
+ - split.
+ match goal with
+ X |- _ => foo
+ | H: X := Y |- _ => foo
+ end.
+ - split.
+ match H with
+ ?a = ?b |- _ => foo
+ | ?a < ?b |- _ => foo
+ end.
+ - split.
+ let x := f y in
+ let foo := idtac x in
+ idtac foo.
Qed.
End X.
@@ -419,25 +541,25 @@ Section SET.
(Vector.t T n) -> Prop :=
match v1 with
Vector.nil _ =>
- fun v2 =>
- match v2 with
- Vector.nil _ => True
- | _ => False
- end
+ fun v2 =>
+ match v2 with
+ Vector.nil _ => True
+ | _ => False
+ end
| (Vector.cons _ x n' v1') =>
- fun v2 =>
- (* indentation of dependen "match" clause. *)
- match v2
- as
- X
- in
- Vector.t _ n''
- return
- (Vector.t T (pred n'') -> Prop) -> Prop
- with
- | Vector.nil _ => fun _ => False
- | (Vector.cons _ y n'' v2') => fun v2'' => (x y) /\ (v2'' v2')
- end (setVecProd T n' v1')
+ fun v2 =>
+ (* indentation of dependen "match" clause. *)
+ match v2
+ as
+ X
+ in
+ Vector.t _ n''
+ return
+ (Vector.t T (pred n'') -> Prop) -> Prop
+ with
+ | Vector.nil _ => fun _ => False
+ | (Vector.cons _ y n'' v2') => fun v2'' => (x y) /\ (v2'' v2')
+ end (setVecProd T n' v1')
end.
End SET.
@@ -459,8 +581,8 @@ Module curlybracesatend.
Qed.
Lemma foo2: forall n: nat,
- exists m:nat, (* This is strange compared to the same line in the
previous lemma *)
- m = n + 1.
+ exists m:nat,
+ m = n + 1.
Proof.
intros n.
destruct n. {
@@ -473,9 +595,19 @@ Module curlybracesatend.
reflexivity.
Qed.
- Lemma foo3: forall n: nat,
- exists m:nat, (* This is strange compared to the same line in the
previous lemma *)
- m = n + 1.
+ Lemma foo3:
+ forall n: nat,
+ forall n: nat,
+ forall n: nat,
+ forall n: nat,
+ forall n: nat,
+ exists m:nat,
+ m = n + 1 ->
+ m = n + 1 ->
+ m = n + 1
+ -> m = n + 1
+ -> m = n + 1 ->
+ m = n + 1.
Proof.
intros n. cut (n = n). {
destruct n. {
@@ -490,6 +622,37 @@ Module curlybracesatend.
reflexivity.
Qed.
+ Lemma foooooooooooooooo3: forall n: nat,
+ forall n: nat, forall n: nat,
+ f x ->
+ g y ->
+ f x -> forall n: nat,
+ forall n: nat,
+ forall n: nat,
+ exists m:nat,
+ m = n + 1 ->
+ m = n + 1 ->
+ m = n + 1
+ -> m = n + 1
+ -> m = n + 1 ->
+ m = n + 1 ->
+ True.
+ Proof.
+ intros n. cut (n = n).
+ {
+ destruct n. {
+ exists 1.
+ reflexivity. } {
+ exists (S (S n)).
+ simpl.
+ rewrite Nat.add_1_r.
+ reflexivity.
+ }
+ }
+ idtac.
+ reflexivity.
+ Qed.
+
End curlybracesatend.
diff --git a/ci/test-indent/indent_equations.v
b/ci/test-indent/indent_equations.v
new file mode 100644
index 0000000..3e200b5
--- /dev/null
+++ b/ci/test-indent/indent_equations.v
@@ -0,0 +1,79 @@
+(* Needs Equations plugin to work. *)
+
+From Coq Require Import Arith Omega Program.
+From Equations Require Import Equations.
+Require Import Bvector.
+
+
+Module Equations.
+ Equations neg (b : bool) : bool :=
+ neg true := false ;
+ neg false := true.
+
+ Lemma neg_inv : forall b, neg (neg b) = b.
+ Proof.
+ intros b.
+ funelim (neg b); now simp neg.
+ Defined.
+
+
+ Inductive list {A} : Type := nil : list | cons : A -> list -> list.
+
+ Arguments list : clear implicits.
+ Notation "x :: l" := (cons x l).
+
+ Equations tail {A} (l : list A) : list A :=
+ | nil := nil ;
+ | (cons a v) := v.
+
+ Equations tail' {A} (l : list A) : list A :=
+ | nil :=
+ nil ;
+ | (cons a v)
+ := v.
+
+ (* The cases inside { } are recognized as record fields, which from
+ an indentation perspective is OK *)
+ 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 =>
+ {
+ | 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 ;
+ 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 ;
+ | false := filter'' l p };
+ filter'' nil p := nil.
+
+ Equations unzip {A B} (l : list (A * B)) : list A * list B :=
+ unzip nil := (nil, nil) ;
+ unzip (cons p l) with unzip l => {
+ unzip (cons (pair a b) l) (pair la lb) := (a :: la, b :: lb) }.
+
+
+ Equations equal (n m : nat) : { n = m } + { n <> m } :=
+ equal O O := left eq_refl ;
+ equal (S n) (S m) with equal n m :=
+ { equal (S n) (S ?(n)) (left eq_refl) := left eq_refl ;
+ equal (S n) (S m) (right p) := right _ } ;
+ equal x y := right _.
+
+End Equations.
diff --git a/ci/test-indent/indent_monadic.v b/ci/test-indent/indent_monadic.v
new file mode 100644
index 0000000..1cc6e8c
--- /dev/null
+++ b/ci/test-indent/indent_monadic.v
@@ -0,0 +1,44 @@
+(* Needs ext-lib library to compile. *)
+
+Require Import Coq.ZArith.ZArith_base Coq.Strings.Ascii Coq.Strings.String.
+Require Import ExtLib.Data.Monads.StateMonad ExtLib.Structures.Monads.
+Import StringSyntax.
+Open Scope string_scope.
+Section StateGame.
+
+ Check Ascii.Space.
+
+ Import MonadNotation.
+ Local Open Scope Z_scope.
+ Local Open Scope char_scope.
+ Local Open Scope monad_scope.
+
+ Definition GameValue : Type := Z.
+ Definition GameState : Type := (prod bool Z).
+
+ Variable m : Type -> Type.
+ Context {Monad_m: Monad m}.
+ Context {State_m: MonadState GameState m}.
+
+ Print Grammar constr.
+
+ Fixpoint playGame (s: string) m' {struct s}: m GameValue :=
+ match s with
+ | EmptyString =>
+ v <- (if true then m' else get) ;;
+ let '(on, score) := v in ret score
+ | String x xs =>
+ v <- get ;;
+ let '(on, score) := v in
+ match x, on with
+ | "a"%char, true => put (on, score + 1)
+ | "b"%char, true => put (on, score - 1)
+ | "c"%char, _ => put (negb on, score)
+ | _, _ => put (on, score)
+ end ;;
+ playGame xs m'
+ end.
+
+ Definition startState: GameState := (false, 0).
+
+End StateGame.
diff --git a/ci/test-indent/tests.sh b/ci/test-indent/tests.sh
new file mode 100755
index 0000000..9dcd5c0
--- /dev/null
+++ b/ci/test-indent/tests.sh
@@ -0,0 +1,8 @@
+
+
+
+
+for i in $(find . -name "*.v" -exec basename '{}' \; | grep -v "indented_") ;
do
+ echo -n "Testing $i..."
+ ./coq-test-indent.sh $i 2>&1 | tee .$i.log | grep "\*\*\*"
+done
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 3a531e5..715c1e2 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -78,7 +78,7 @@ No context checking.")
(defconst coq-bullet-prefix-regexp-backward
(concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp-backward
"\\)\\(?:\\.\\s-+\\)"
"\\(?:\\(?:" coq-goal-selector-regexp "\\)?"
- "{\\|}\\|-\\|+\\|\\*\\)*\\)"))
+ "{\\|}\\|-\\|+\\|\\*\\s-\\)*\\)"))
;; matches regular command end (. and ... followed by a space or "}" or buffer
end)
;; ". " and "... " are command endings, ".. " is not, same as in
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 88e3375..b3357d0 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -162,7 +162,8 @@ attention to case differences."
(cmdstrt (save-excursion (coq-find-real-start)))
(enclosing (coq-is-inside-enclosing cmdstrt)))
(cond
- ((string-equal enclosing "{|") nil)
+ ((string-equal enclosing "{|") nil) ;; only records
+ ((and enclosing (string-match "{" enclosing)) nil) ;; more agressive:
record-like notations
(t (save-excursion
(goto-char cmdstrt)
(let ((case-fold-search nil))
@@ -486,13 +487,14 @@ The point should be at the beginning of the command name."
(t (save-excursion (coq-smie-backward-token))))) ;; recursive call
((or (string-match coq-bullet-regexp-nospace tok)
(member tok '("=>" ":=" "::=" "exists" "in" "as" "∀" "∃" "→" "∨" "∧"
";"
- "," ":" "eval")))
+ "," ":" "eval" "return")))
;; The important lexer for indentation's performance is the backward
;; lexer, so for the forward lexer we delegate to the backward one when
;; we can.
(save-excursion (coq-smie-backward-token)))
- ((member tok '("lazymatch" "lazy_match" "multimatch" "multi_match"))
"match")
+ ;; match needs to be catpured now to avoid being catpured by "Com start"
+ ((member tok '("match" "lazymatch" "lazy_match" "multimatch"
"multi_match")) "match")
;; detect "with signature", otherwies use coq-smie-backward-token
((equal tok "with")
@@ -547,6 +549,16 @@ The point should be at the beginning of the command name."
((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)))
+
+ ;; Com start is a token for the first word of a command (provided it is a
word)
+ ((save-excursion
+ (and (smie-default-backward-token)
+ (coq-is-at-command-real-start)
+ (> (length tok) 0)
+ (or (string= "Lu" (get-char-code-property (aref tok 0)
'general-category))
+ (string= "Ll" (get-char-code-property (aref tok 0)
'general-category)))))
+ "Com start")
+
;; return it.
(tok)
)))
@@ -556,6 +568,11 @@ The point should be at the beginning of the command name."
;; This is very approximate and should be used with care
(let ((case-fold-search nil)) (looking-at coq-command-defn-regexp)))
+(defun coq-is-at-def-or-decl ()
+ ;; This is very approximate and should be used with care
+ (let ((case-fold-search nil))
+ (or (looking-at coq-command-defn-regexp) (looking-at
coq-command-decl-regexp))))
+
;; ":= with module" is really to declare some sub-information ":=
;; with" is for mutual definitions where both sides are of the same
@@ -588,13 +605,11 @@ The point should be at the beginning of the command name."
((equal corresp "where") ":= inductive") ;; inductive or fixpoint,
nevermind
((or (eq ?\{ (char-before))) ":= record")
((equal (point) cmdstrt)
- (if (or (looking-at "Equations") ;; note: "[[]" is the regexp for a
single "["
- (not (coq-is-at-def))
- )
- ":="
- ":= def")) ; := outside of any parenthesis
- (t ":=")
- ))) ; a parenthesis stopped the search
+ ;; we reached the command start: either we were in an Equation,
+ ;; or the ":=" was inpatter of an Ltac match (pattern the form
+ ;; "| H: T := t |- _"). Toherwise we are probably in a Definition.
+ (if (or (looking-at "Equations\\|match\\|let")) ":=" ":= def"))
+ (t ":="))))
(defun coq-smie-semicolon-deambiguate ()
@@ -631,6 +646,8 @@ The point should be at the beginning of the command name."
(cond
;; Distinguish between "," from quantification and other uses of
;; "," (tuples, tactic arguments)
+ ;; we cannot distinguish between tuples and tac args, because of:
+ ;; an term (f x , v) and a tactic expecting a tuple (tac x , v)
((equal tok ",")
(save-excursion
(let ((backtok (coq-smie-search-token-backward
@@ -702,7 +719,8 @@ The point should be at the beginning of the command name."
;(coq-find-real-start)
(coq-smie-module-deambiguate)))
- ((member tok '("lazy_?match" "multi_?match")) "match")
+ ;; match needs to be catpured now to avoid being catpured by "Com start"
+ ((member tok '("match" "lazy_match" "lazymatch" "multi_match"
"multimatch")) "match")
((equal tok "tryif") "if")
@@ -737,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)))
@@ -817,6 +835,17 @@ The point should be at the beginning of the command name."
((member prev-interesting '("Morphism" "Relation")) "as morphism")
(t tok)))))
+ ((equal tok "return")
+ (save-excursion
+ (let ((prev-interesting
+ (coq-smie-search-token-backward
+ '("match" "lazymatch" "multimatch" "lazy_match" "multi_match"
"Morphism" "Relation" "." ". proofstart")
+ nil
+ '((("match" "lazy_match" "multi_match" "let") . "with") ("with"
. "signature")))))
+ (cond
+ ((member prev-interesting '("match" "lazymatch" "multimatch"
"lazy_match" "mult_match")) "return match")
+ (t tok)))))
+
((equal tok "by")
(let ((p (point)))
(if (and (equal (smie-default-backward-token) "proved")
@@ -883,11 +912,26 @@ The point should be at the beginning of the command name."
(let ((newtok (coq-smie-backward-token))) ; recursive call
(concat newtok "." tok)))
- ;; easier to return directly than calling coq-smie-backward-token
((member tok '("lazymatch" "lazy_match" "multimatch" "multi_match"))
"match")
-
((coq-dot-friend-p tok) ".")
+
+ ;; Default fallback for words at command start position: We use a
+ ;; 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
+ ;; 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
+ ;; recognized as such by the grammar.
+ ((and (coq-is-at-command-real-start)
+ (> (length tok) 0)
+ (not (member tok '("match" "lazymatch" "let"))) ;; match are
already captured
+ (or (string= "Lu" (get-char-code-property (aref tok 0)
'general-category))
+ (string= "Ll" (get-char-code-property (aref tok 0)
'general-category))))
+ "Com start")
+
(tok))))
@@ -905,6 +949,9 @@ Lemma foo: forall n,
:type 'boolean
:group 'coq)
+(make-variable-buffer-local 'coq-indent-box-style)
+
+
(defun coq-indent-safep (indent)
(>= indent 0))
@@ -970,14 +1017,71 @@ Typical values are 2 or 4."
:group 'coq
:safe #'coq-indent-safep)
-;; - TODO: remove tokens "{ subproof" and "} subproof" but they are
-;; needed by the lexers at a lot of places.
-;; - FIXME: This does not know about Notations.
-;; - TODO Actually there are two grammars: one at script level, for
-;; indenting each command with respect to the previous commands, and
-;; a standard one inside commands. Separating the two grammars would
-;; greatly simplify this file. We should ask Stefan Monnier how to
-;; have two grammars with smie.
+
+
+;; smie grammar. General Remarks.
+
+;; 1. One oddity (a standard one IIUC) is that the "command end token"
+;; is considerd a separator. So any command is the child of the
+;; previous one. This may lead to strange things wrt to indentation if
+;; we don't take care. For instance the following script
+;:;
+;; Com1 .(1)
+;; Definition foo := bar .(2)
+;; ...
+;; could easily lead to the grammar tree
+;;
+;; __.(2)
+;; .(1) \
+;; / \ ...
+;; / \
+;; Com1 :=
+;; / \
+;; Def foo bar
+;;
+;; which means that "(1)" is the parent of ":=", which is the parent
+;; of "Def foo". This leads to hell. We need Def to be the parent. But
+;; there are hundreds of commands in coq. so we adopt the policy below.
+;;
+;; 2. the lexer tries to always treat the first word of a command as a
+;; dstinguished token "Com start". And a command is of the form ("Com
+;; start" exp) in smie grammar. This way the top-node of a command is
+;; always this token.
+;;
+;; This way the above script is parsed as:
+;;
+;; __.(2)
+;; .(1) \
+;; / \ ...
+;; / \
+;; Com1 Com start
+;; |
+;; :=
+;; / \
+;; foo bar
+;;
+;; which is much better. Indenting *inside* a command never looks
+;; above its own "Com start". This makes indentation rules much
+;; simpler, and hopefully speeds up things too since in practice it
+;; means indentation never inspect too far.
+;;
+;; 3. The only exception to "Com start" token at command start is
+;; structuring commands like "Proof" "Module", "{ subproof", bullets,
+;; goal selectors.
+;;
+;; 4. All non-word tokens (in particular bullets) are also not seen as
+;; "Com start". Thus user-defined commands (or tactics) starting with
+;; a non-word token will probably break indentation.
+;;
+;; 5. KNOWN BUGS: This does not know about Notations, but users can
+;; add new syntax for already defined tokens.
+;;
+;; 6. BUGS: probably dozens of.
+;;
+;; TODO: factorize infix operators into a series of "opxx" where "xx"
+;; is the coq grammar priority. users could then add there own infix
+;; operators in a consistent way.
+
(defconst coq-smie-grammar
(smie-prec2->grammar
(smie-bnf->prec2
@@ -994,7 +1098,6 @@ Typical values are 2 or 4."
("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp)
("quantif exists" exp ", quantif" exp)
("forall" exp ", quantif" exp)
-;;;
(exp "<- monadic" exp) (exp ";; monadic" exp)
("(" exp ")") ("{|" exps "|}") ("{" exps "}")
(exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp)
@@ -1008,11 +1111,14 @@ Typical values are 2 or 4."
(exp "+" exp) (exp "-" exp)
(exp "*" exp) (exp "&&" exp)
(exp "^" exp)
- (exp ": ltacconstr" exp)(exp ". selector" exp))
+ (exp ": ltacconstr" exp)(exp ". selector" exp)
+ ("Com start" exp)
+ )
+
;; Having "return" here rather than as a separate rule in `exp' causes
;; it to be indented at a different level than "with".
(matchexp (exp) (exp "as match" exp) (exp "in match" exp)
- (exp "return" exp) )
+ (exp "return match" exp) )
(exps (affectrec) (exps "; record" exps))
(affectrec (exp ":= record" exp))
(assigns (exp ":= let" exp) (exp "<- monadic" exp))
@@ -1065,29 +1171,33 @@ Typical values are 2 or 4."
(assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet")
(assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet")
(assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet")
- (assoc ".")
+ (left ".")
(assoc "with inductive" "with fixpoint" "where"))
- '((assoc ":= equations") (assoc ":= def" ":= inductive")
- (assoc "|") (assoc "; equations") (assoc "=>") (assoc ":=")
- (assoc "xxx provedby")
- (assoc "as morphism") (assoc "with signature") (assoc "with match")
+ '((nonassoc "Com start") (assoc ":= equations")
+ (assoc ":= def" ":= inductive")
+ (left "|") (assoc "; equations") (assoc "=>") (assoc ":=")
+ (assoc "as morphism") (assoc "xxx provedby")
+ (assoc "with signature") (assoc "with match")
(assoc "in let" "in monadic")
- (assoc "in eval") (assoc "=> fun") (assoc ", quantif") (assoc "then")
+ (assoc "in eval") (left "=> fun") (left ", quantif") (assoc "then")
(assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems
impossible
- (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
- (assoc "|-") (assoc ":" ":<") (assoc ",")
+ (left "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
+ (assoc "|-") (assoc ":" ":<") (left ",")
(assoc "else")
(assoc "->") (assoc "<->")
- (assoc "\\/") (assoc "&") (assoc "/\\")
- (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>")
+ (left "\\/") (left "&" "/\\")
+ ;; FTR: left (instead of assoc) for "<" makes the hoare triple notation
+ ;; <{ .. }>\n exp \n<{ ... }> indent the two assertions at the same
column.
+ (assoc "==") (assoc "=") (left "<" ">" "<=" ">=" "<>")
(assoc "=?") (assoc "<=?") (assoc "<?")
(assoc ";; monadic") (assoc "<- monadic")
(assoc "^")
(assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems
impossible
- (assoc "+") (assoc "-") (assoc "*")(assoc "&&")
+ ;; this make indentation as expected.
+ (left "+" "-") (left "*") (left "&&")
(assoc ": ltacconstr") (assoc ". selector"))
- '((assoc ":" ":<") (assoc "<"))
- '((assoc ". modulestart" "." ". proofstart") (assoc "Module def")
+ '((assoc ":" ":<") (left "<"))
+ '((assoc "Module def")
(assoc "with module" "module nodecl") (assoc ":= module")
(assoc ":= with module") (assoc ":" ":<"))
'((assoc ":= def") (assoc "; record") (assoc ":= record"))))
@@ -1143,17 +1253,38 @@ Typical values are 2 or 4."
"Return non-nil if PARENT-POS is on same line as CHILD-POS."
(= (line-number-at-pos parent-pos) (line-number-at-pos child-pos)))
-(defcustom coq-indent-basic nil
+(defcustom coq-indent-basic 2
"Basic indentation step.
If nil, default to `proof-indent' if it exists or to `smie-indent-basic'."
:group 'coq-mode
:type '(choice (const :tag "Fallback on global settings" nil)
integer))
-
-;; Debugging smie parent token, needs the highlight library
-;;and something like this in .emacs:
-;; (require 'highlight)
+;; otherwise there are some glitches
+(setq smie-indent-basic coq-indent-basic)
+
+;;;;;;;;;; DEBUG CODE ;;;;;;
+;; smie-config-show-indent is sufficient most of the time.
+
+(defun coq-debug-smie--parent (point parent &optional num)
+ ;;refresh highlighting? Not a good idea since this is called several times.
+ ;;(hlt-unhighlight-region)
+ (let* ((beg (if (listp (car parent)) (caar parent) (car parent)))
+ (end (cadr parent))
+ (regi (list (list beg end)))
+ (tok (caddr parent))
+ (face (cond
+ ((equal num 1) 'hlt-regexp-level-1)
+ ((equal num 2) 'hlt-regexp-level-2)
+ (t 'hlt-regexp-level-1))))
+ ;; uncomment to see visually the region
+ ;;(and parent (hlt-highlight-regions regi face))
+ ;;(when end (hlt-highlight-regions (list (list end (+ end 1)))
'hlt-regexp-level-1))
+ ;; and the point considered
+ (hlt-highlight-regions (list (list point (+ point 1))) 'holiday)))
+
+;; Debugging smie rules calls, needs the highlight library and
+;; something like this in .emacs: (require 'highlight)
;; (custom-set-faces '(highlight ((((type x) (class color) (background light))
(:background "Wheat")))))
(defun coq-show-smie--parent (parent token parent-token &optional num msg)
(ignore-errors
@@ -1167,248 +1298,133 @@ If nil, default to `proof-indent' if it exists or to
`smie-indent-basic'."
((equal num 2) 'hlt-regexp-level-2)
(t 'hlt-regexp-level-1))))
(and parent (hlt-highlight-regions regi face)))))
+;;;;;;;;;; END DEBUG CODE ;;;;;;;;;;;;
+
+(defun coq-indent-categorize-token-after (tk)
+ "Factorize tokens behaving the same \"smie-rules\"-wise (kind:after)."
+ (cond
+ ((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"
+ ((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
+ ;; to simply fail, so that we detect missing tokens in this function?
+ (t tk)))
+
+(defun coq-indent-categorize-token-before (tk)
+ "Factorize tokens behaving the same \"smie-rules\"-wise (kind:after)."
+ (cond
+ ((member tk '(". proofstart" ". modulestart")) "dot script parent open")
+ ((member tk '(":" "by" "in tactic" "as" "with" ",")) "tactic infix")
+ ((string-prefix-p ":= " tk) "before :=")
+
+ ;; 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?
+ (t tk)))
+
+
+;; ";" is a usual operator, with no indentation
+;; it would be like this;
+;; foo.
+;; foo ;
+;; bar ;
+;; bar.
+;; foo.
+;; which is confusing. So we indent the first ";" of a sequence
+;; if not already inside an ltacdef of parenthesized tactic:
+;; foo ;
+;; tac ; <--- indented
+;; tac ; <--- no indent
+;; [ tac2 ;
+;; tac1 ; <-- no indentation here
+;; now ( tac3 ; <- neither here
+;; tac5) ;
+;; ]
+(defun coq-smie-ltac-semicol-indent-first (parent-semicol)
+ (and coq-indent-semicolon-tactical (not parent-semicol)
+ (not (coq-smie-is-ltacdef))
+ (not (coq-smie-is-inside-parenthesized-tactic))))
+
+
+;; this should be called if we already know that parent is a quantif.
+(defun coq--prev-quantif-at-indent-p ()
+ (save-excursion
+ (coq-smie-search-token-backward '("forall" "quantif exists"))
+ (equal (current-column) (current-indentation))))
-
+;; 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
+;; treated like this either.
(defun coq-smie-rules (kind token)
"Indentation rules for Coq. See `smie-rules-function'.
KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
- (pcase kind
- (`:elem (pcase token
- (`basic (or coq-indent-basic
- (bound-and-true-p proof-indent)
- smie-indent-basic))))
- (`:close-all t)
- (`:list-intro
- (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.
- ;; FIXME: this gives a strange indentation for ". { \n .. } \n { .. }"
-; (when (or (coq-is-bullet-token token)
-; (coq-is-dot-token token)
-; (member token '("{ subproof")))
-; (forward-char 1) ; skip de "."
-; (equal (coq-smie-forward-token) "{ subproof"))
- ))
- (`:after
- ;;(coq-show-smie--parent smie--parent smie--token (smie-indent--parent)
1 "AFTER")
- (cond
- ;; Override the default indent step added because of their presence
- ;; in smie-closer-alist.
- ((or (coq-is-bullet-token token)
- (member token '(":" ":=" ":= with" ":= def" ":= equations"
- "by" "in tactic" "<:" "<+" ":= record"
- "with module" "as" ":= inductive" ":= module" )))
- 2)
-
- ((equal token "with match") coq-match-indent)
-
- ;; Inductive foo ...
- ;; ...
- ;; with
- ;; bar <-- indent this by 2
- ;; TODO: have this optional?
- ((equal token "with inductive")
- (if (smie-rule-parent-p "with inductive")
- 0
- 2))
-
- ((equal token "with") 2) ; add 2 to the column of "with" in the
children
-
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;XXXXXXXXXXXXXXXXXXXXXXXx
- ((and (member token '("{" "{|"))
- (smie-rule-prev-p ":=" ":= def")
- (not coq-indent-box-style))
- (save-excursion
- (smie-backward-sexp t)
- (cons 'column (+ 2 (smie-indent-virtual)))))
-
-
- ;;; the ";" tactical ;;;
- ;; ";" is a usual operator, with no indentation
- ;; it would be like this;
- ;; foo.
- ;; foo ;
- ;; bar ;
- ;; bar.
- ;; foo.
- ;; which is confusing. So we indent the first ";" of a sequence
- ;; if not already inside an ltacdef of parenthesized tactic:
- ;; foo ;
- ;; tac ; <--- indented
- ;; tac ; <--- no indent
- ;; [ tac2 ;
- ;; tac1 ; <-- no indentation here
- ;; now ( tac3 ; <- neither here
- ;; tac5) ;
- ;; ]
- ((equal token "; tactic")
- (if (and (smie-rule-hanging-p)
- coq-indent-semicolon-tactical
- (not (coq-smie-is-ltacdef))
- (not (coq-smie-is-inside-parenthesized-tactic))
- (or (not (smie-rule-parent-p "; tactic"))
- ;; FIXME: Don't depend on SMIE's internals!
- (and (boundp 'smie--parent)
- smie--parent
- (coq-smie--same-line-as-parent
- (nth 1 smie--parent) (point)))))
- coq-indent-semicolon-tactical
- nil))
-
- ((member token '("in let" "in monadic")) (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
- ;; parenthesis, hence the current command (C) ending with "."
- ;; is not recognized as correctly terminated. The "parent"
- ;; computed by smie is therefore wrong and default indetation
- ;; is broken. We fix this by indenting from the real-start of
- ;; the command terminated by ". proofstart".
- ((equal token ". proofstart")
- (save-excursion (forward-char -1) (coq-find-real-start)
- `(column . ,(+ coq-indent-proofstart
(current-column)))))
- ((equal token ". modulestart")
- (save-excursion (forward-char -1) (coq-find-real-start)
- `(column . ,(+ coq-indent-modulestart
(current-column)))))))
-
- (`:before
- ;(coq-show-smie--parent smie--parent smie--token (smie-indent--parent) 2
"BEFORE")
- (cond
+ (let ((boxed coq-indent-box-style))
+ ;; smie-rule... short synonyms
+ (cl-flet ((parent-p (&rest x) (apply 'smie-rule-parent-p x))
+ (parent (&optional x) (smie-rule-parent x))(hang-p ()
(smie-rule-hanging-p)))
+ (pcase (cons kind token)
+ (`(,_ . (or "; record")) (smie-rule-separator kind)) ;; see also the
"before" rule
+ (`(:elem . basic) (or coq-indent-basic (bound-and-true-p proof-indent)
2))
+ (`(:elem . arg) nil)
+ (`(:close-all . ,_) t)
+ (`(: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)?
+ ;; decrement indentation when hanging
+ ((and (or "tactic infix" "after :=") (guard (or (hang-p)
(smie-rule-bolp)))) 0)
+ ((and "->" (guard (hang-p))) 0) ((or ":=" "with inductive") 2)
+ ((or "." "; equations" "in let" "in monadic" ";; monadic") 0)
+ ((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)
+ ))
+ (`(:before . ,_) ; indent token at point itself
+ (let* ((cat (coq-indent-categorize-token-before token))
+ (real-start-col (save-excursion (coq-find-real-start)
(current-column))))
+ (pcase cat
+ ;; indenting the ". modulestart" itself, which is a prenthesizing
cmd
+ ("dot script parent open" `(column . ,real-start-col))
+ ;; special case for equations, so that "| xxx\n :=" is indented
nicely
+ ((and ":=" (guard (and (not (hang-p)) (parent-p "|")))) 4)
+ ("before :=" (parent 2)) ;; ":= xxx" always introduced by a parent
+ ("tactic infix" (parent 2))
+ ("|" (cond ((parent-p ":= inductive" ":= equations") -2)
+ (t 0)));((parent-p "|") 0)
+ ;; align quantifiers with the previous one
+ ((and(or "forall" "quantif exists")(guard (parent-p "forall"
"quantif exists")))
+ (parent))
+ ((and(or "fun")(guard (parent-p "fun"))) (parent))
+ ;; indent on level after a ";" but only at command level.
+ ((and "; tactic" (guard (parent-p "Com start"))) (parent))
+ ("; record" 0); is also a smie-rule-separator
+ ;; VIRTUAL INDENTATION for "unboxed" indentation: we are in the
"before"
+ ;; section, but we compute the indentation for a token NOT
appearing at
+ ;; beginning of line. This happens when not indenting the token
itself but
+ ;; rather querying its virtual indentation to compute indentation
of another
+ ;; (child) token. unbox ==> indent relative to parent.
+ ;; unboxed indent for "{" not at bol:
+ ((and (or "{ subproof" "[" "{") (guard (not (smie-rule-bolp))))
+ (cond
+ ((smie-rule-prev-p "} subproof" "]" "}") (parent 0))
+ (t (parent 2))))
+ ;; unboxed indent for quantifiers (if coq-indent-box-style non
nil)
+ ((and (or "forall" "quantif exists") (guard (not boxed))
+ (guard (not (smie-rule-bolp))) )
+ (parent coq-smie-after-bolp-indentation))
+ ;;((guard (and (message "DEFAULTING") nil)) nil)
+ )))))))
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;XXXXXXXXXXXXXXXXXXXXXXXx;;;;;;;;;;;;;;
- ;; trying to indent "{" at the end of line for records, but the
- ;; parent is not what I think.
- ;; ((and (member token '("{" "{|"))
- ;; (not coq-indent-box-style))
- ;; (if (smie-rule-bolp) 2 0))
- ;(and (zerop (length tok)) (member (char-before) '(?\{ ?\})))
- ((and (zerop (length token))
- (looking-back "}" (1- (point))) ;; "|}" useless when looking
backward
- (not coq-indent-box-style))
- (smie-backward-sexp)
- (smie-backward-sexp t)
- (smie-indent-virtual)
- )
-
- ;; "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")
- (smie-rule-parent)
- (smie-rule-parent 2)))
-
- ((member token '("in tactic" "as" "by"))
- (cond
- ((smie-rule-parent-p "- bullet" "+ bullet" "* bullet"
- "-- bullet" "++ bullet" "** bullet"
- "--- bullet" "+++ bullet" "*** bullet"
- "---- bullet" "++++ bullet" "**** bullet"
- "{ subproof" ". proofstart")
- (smie-rule-parent 4))
- ((smie-rule-parent-p "in tactic") (smie-rule-parent))
- (t (smie-rule-parent 2))))
-
- ((equal token "as")
- (if (smie-rule-parent-p "in tactic") (smie-rule-parent) 2))
-
- ((equal token "as morphism") (smie-rule-parent 2))
- ((member token '("xxx provedby" "with signature"))
- (if (smie-rule-parent-p "xxx provedby" "with signature")
- (smie-rule-parent)
- (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
- ;; "Lemma". This never applies directly to indent the forall,
- ;; but it is used to guess indentation of the next line. This
- ;; allows fo the following indentation:
- ;; Lemma foo: forall x:nat,
- ;; x <= 0 -> x = 0.
- ;; which refer to:
- ;; Lemma foo:
- ;; forall x:nat, <--- if it where on its own line it would be on
column 2
- ;; x <= 0 -> x = 0. <--- therefore this is on column 4.
- ;; instead of:
- ;; Lemma foo: forall x:nat,
- ;; x <= 0 -> x = 0.
-
- ((and (member token '("forall" "quantif exists"))
- (not coq-indent-box-style)
- (not (smie-rule-bolp)))
- (smie-rule-parent coq-smie-after-bolp-indentation))
-
-
-
- ((and (member token '("forall" "quantif exists"))
- (smie-rule-parent-p "forall" "quantif exists"))
- (if (save-excursion
- (coq-smie-search-token-backward '("forall" "quantif exists"))
- (equal (current-column) (current-indentation)))
- (smie-rule-parent)
- (smie-rule-parent 2)))
-
-
- ;; This rule allows "End Proof" to align with corresponding ".
- ;; proofstart" PARENT instead of ". proofstart" itself
- ;; Typically:
- ;; "Proof" ". proofstart"
- ;; "Qed" <- parent is ". proofstart" above
- ;; Align with the real command start of the ". xxxstart"
- ((member token '(". proofstart" ". modulestart"))
- (save-excursion (coq-find-real-start)
- `(column . ,(current-column))))
-
- ((or (member token '(":= inductive" ":= def" ":= equations" ":="))
- (and (equal token ":") (smie-rule-parent-p ".")))
- (let ((pcol
- (save-excursion
- ;; Indent relative to the beginning of the current command
- ;; rather than relative to the previous command.
- (smie-backward-sexp token)
- ;; special case: if this ":=" corresponds to a "with
- ;; foo", then the previous smie-backward-sexp stopped
- ;; between "with" and "foo" (because "with inductive"
- ;; and co are considered as ".", maybe this is the
- ;; problem), but we want to indent from the column of
- ;; "with" instead
- (let ((col1 (current-column)))
- (if (equal (coq-smie-backward-token) "with inductive")
- (current-column)
- col1)
- ))))
- `(column . ,(if (smie-rule-hanging-p) pcol (+ 2 pcol)))))
-
- ((equal token "|")
- (cond
- ;; ":= equations" and "; record" are for Equations plugin
- ((smie-rule-parent-p "with match" ":= equations" "; record")
- (- (funcall smie-rules-function :after "with match") 2))
- ;; This is also for Equations plugijns, but happens at first
- ;; line if a pattern matching and it is ugly to have the "|"
- ;; at the saem column than "{"
- ((smie-rule-parent-p "{")
- (funcall smie-rules-function :after "with match"))
- ((smie-rule-prev-p ":= inductive")
- (- (funcall smie-rules-function :after ":= inductive") 2))
- (t (smie-rule-separator kind))))))
- ))
;; No need of this hack anymore?
;; ((and (equal token "Proof End")
-;; (smie-rule-parent-p "Module" "Section" "goalcmd"))
+;; (parent-p "Module" "Section" "goalcmd"))
;; ;; ¡¡Major gross hack!!
;; ;; This typically happens when a Lemma had no "Proof" keyword.
;; ;; We should ideally find some other way to handle it (e.g. matching
Qed
@@ -1418,7 +1434,7 @@ KIND is the situation and TOKEN is the thing w.r.t which
the rule applies."
;; ;; when parsing backward.
;; ;; FIXME: This is fundamentally very wrong, but it seems to work
;; ;; OK in practice.
-;; (smie-rule-parent 2))
+;; (parent 2))
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index afcbd31..b8b498a 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1385,7 +1385,7 @@ different."
(defconst coq-command-prefix-regexp
"\\(Local\\s-\\|Global\\s-\\|#[[][^]]*[]]\\)")
;; FIXME: incomplete
-(defun coq-add-command-prefix (reg) (concat "\\(" coq-command-prefix-regexp
"\\)?" (mapconcat #'identity coq-keywords-defn "\\|")))
+(defun coq-add-command-prefix (reg) (concat "\\(" coq-command-prefix-regexp
"\\)?" (mapconcat #'identity reg "\\|")))
(defconst coq-command-decl-regexp (coq-add-command-prefix coq-keywords-decl))
(defconst coq-command-defn-regexp (coq-add-command-prefix coq-keywords-defn))
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 2a0d5e4..17bf481 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -342,7 +342,7 @@ Module X.
match goal with
| ?g := _:rec |- ?a /\ ?b => split
- | _ => fail
+ | _ => fail
end.
Fail
