path: root/coq/coq-smie.el

;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq

;; This file is part of Proof General.

;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017  Pierre Courtieu
;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
;; Portions © Copyright 2015-2017  Clément Pit-Claudel

;; Authors: Pierre Courtieu
;;          Stefan Monnier
;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>

;; License:     GPLv3+ (GNU GENERAL PUBLIC LICENSE version 3 or later)

;;; Commentary:

;; Lexer.

;; Due to the verycomplex grammar of Coq, and to the architecture of
;; smie, we deambiguate all kinds of tokens during lexing. This is a
;; complex piece of code but it allows for all smie goodies.
;; Some examples of deambigations:
;; - We distinguish ":=" from ":= inductive" to avoid the circular precedence
;;   constraint ":= < | < ; < :=" where ":= < |" is due to Inductive
;;   definitions, "| < ;" is due to tactics precedence, "; < :=" is due to
;;   "let x:=3; y:=4 in...".
;; - We distinguish the ".-selector" from the terminator "." for
;;   obvious reasons.
;; - We consider qualified.names as one single token for obvious reasons.
;; - We distinguish the "Module M." from "Module M := exp." since the first
;;   opens a new scope (closed by End) whereas the other doesn't.
;; - We drop "Program" because it's easier to consider "Program Function"
;;   as a single token (which behaves like "Function" w.r.t indentation and
;;   parsing) than to get the parser to handle it correctly.
;; - We identify the different types of bullets (First approximation).
;; - We distinguish "with match" from other "with".

;;; Code:

(require 'coq-indent)
(require 'smie nil 'noerror)

; debugging
;(defmacro measure-time (&rest body)
;  "Measure the time it takes to evaluate BODY."
;  `(let ((time (current-time)))
;     ,@body
;     (message "%.06f" (float-time (time-since time)))))

(defcustom coq-smie-user-tokens nil
  "Alist of (syntax . token) pairs to extend the coq smie parser.
These are user configurable additional syntax for smie tokens. It
allows to define alternative syntax for smie token. Typical
example: if you define a infix operator \"xor\" you may want to
define it as a new syntax for token \"or\" in order to have the
indentation rules of or applied to xor. Other exemple: if you
want to define a new notation \"ifb\" ... \"then\" \"else\" then
you need to declare \"ifb\" as a new syntax for \"if\" to make
indentation work well."
  :type '(alist :key-type string :value-type string)
  :group 'coq)


(defun coq-string-suffix-p (str1 str2 &optional ignore-case)
  "Return non-nil if STR1 is a prefix of STR2.
If IGNORE-CASE is non-nil, the comparison is done without paying
attention to case differences."
  (let ((begin2 (- (length str2) (length str1)))
	(end2 (length str2)))
    (when (< begin2 0) (setq begin2 0)) ; to avoid negative begin2
    (eq t (compare-strings str1 nil nil str2 begin2 end2 ignore-case))))

;; Replacement for emacs < 24.4, borrowed from sindikat at
;; stackoverflow efficient if bytecompiled, builtin version is
;; probably better when it exists
(unless (fboundp 'string-suffix-p)
  (fset 'string-suffix-p 'coq-string-suffix-p)
  (declare-function string-suffix-p "smie"))

;; As any user defined notation ending with "." will break
;; proofgeneral synchronization anyway, let us consider that any
;; combination of symbols ending with "." is an end of command for
;; indentation purposes. One noticeable exception is .. that may
;; happen inside notations and is dealt with by pg synchro.
(defun coq-dot-friend-p (s)
  (and (not (string-equal ".." s)) ;; string-equal because ... should return t.
       (string-match "[^[:word:]]\\.\\'" s)))

; for debuging
(defun coq-time-indent ()
  (interactive)
  (let ((deb (float-time)))
    (smie-indent-line)
    (message "time: %S"(- (float-time) deb))))

(defun coq-time-indent-region (beg end)
  (interactive "r")
  (let ((deb (float-time)))
    (indent-region beg end nil)
    (message "time: %S"(- (float-time) deb))))



;; Fragile: users can define tactics with uppercases...
(defun coq-smie-is-tactic ()
  (save-excursion
    (coq-find-real-start)
    (let ((case-fold-search nil))
      (not (looking-at "[[:upper:]]")))))

(defun coq-smie-is-ltacdef ()
  (let ((case-fold-search nil))
    (save-excursion       
      (coq-find-real-start)
      (looking-at "\\(\\(Local\\|Global\\)\\s-+\\)?\\(Ltac\\|Tactic\\s-+Notation\\)\\s-"))))

(defun coq-smie-is-inside-parenthesized-tactic ()
  (and (coq-smie-is-tactic) ;; fragile (uppercase test only)
       (save-excursion
	 (let ((pt (point))
	       ;; we need to go one character forwardto avoid the
	       ;; coq-smie-search-token-backward below to fail on "{"
	       (strt (and (coq-script-parse-cmdend-backward)
			  (+ 1 (point)))))
	   (goto-char pt)
	   ;; looking for a dummy token to see if we fail before reaching
	   ;; strt, which means that we were in a prenthesized expression.
	   (coq-smie-search-token-backward '("#dummy#") strt)
	   (> (point) strt)))))

(defun coq-smie-.-deambiguate ()
  "Return the token of the command terminator of the current command.
For example in:

Proof.       or        Proof with ... .

the token of the \".\" is \". proofstart\".

But in

intros.      or        Proof foo.

the token of \".\" is simply \".\"."
  (save-excursion
    (let ((p (point)) (beg (coq-find-real-start))) ; moves to real start of command
      (cond
       ((looking-at "BeginSubproof\\>") ". proofstart")
       ((looking-at "Proof\\>")
	(forward-char 5)
	(coq-find-not-in-comment-forward "[^[:space:]]") ;; skip spaces and comments
	(if (looking-at "\\.\\|with\\|using") ". proofstart" "."))
       ((or (looking-at "Next\\s-+Obligation\\>")
	    (coq-smie-detect-goal-command))
	(save-excursion
	  (goto-char (+ p 1))
          (let ((tok (smie-default-forward-token)))
            (cond
             ;; If the next token is "Proof", then the current command does
             ;; introduce a proof, but the user opted to use the explicit
             ;; "Proof" command, so the current command doesn't itself start
             ;; the proof.
             ((equal tok "Proof") ".")
             ;; If the next command is a new definition, then the current
             ;; command didn't actually start a proof!
             ((member tok '("Let" "Definition" "Inductive" "Fixpoint")) ".")
             (t ". proofstart")))))
       ((equal (coq-smie-module-deambiguate) "Module start")
	". modulestart")
       (t ".")))))


(defun coq-smie-complete-qualid-backward ()
  "Return the qualid finishing at the current point."
  (let ((p (point)))
    (re-search-backward "[^.[:alnum:]_@]")
    (forward-char 1)
    (buffer-substring (point) p)))


(defun coq-smie-find-unclosed-match-backward ()
  (let ((tok (coq-smie-search-token-backward '("with" "match" "lazymatch" "multimatch" "."))))
    (cond
     ((null tok) nil)
     ((equal tok ".") nil)
     ((equal tok "with")
      (coq-smie-find-unclosed-match-backward)
      (coq-smie-find-unclosed-match-backward))
     (t t) ;; all variants of match
     )))

;; point supposed to be at start of the "with"
(defun coq-smie-with-deambiguate()
  (let ((p (point)))
    (if (coq-smie-find-unclosed-match-backward)
	"with match"
      (goto-char p)
      (coq-find-real-start)
      (cond
       ((looking-at "\\(Co\\)?Inductive") "with inductive")
       ((looking-at "\\(Co\\)?Fixpoint\\|Function\\|Program\\|Lemma") "with fixpoint")
       ((looking-at "Module\\|Declare") "with module")
       (t "with")))))



;; A variant of smie-default-backward-token that recognize "." and ";"
;; as single token even if glued at the end of another symbols.

(defun coq-backward-token-fast-nogluing-dot-friends ()
  (forward-comment (- (point)))
  (let ((pt (point)))
    (let* ((tok-punc (skip-syntax-backward "."))
           (str-punc (buffer-substring-no-properties pt (point)))
           (tok-other (if (zerop tok-punc) (skip-syntax-backward "w_'"))))
      ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token
      (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
        (skip-syntax-forward ".")
        (forward-char -1))
      (buffer-substring-no-properties pt (point)))))

(defun coq-forward-token-fast-nogluing-dot-friends ()
  (forward-comment (point-max))
  (let ((pt (point)))
    (let* ((tok-punc (skip-syntax-forward "."))
           (str-punc (buffer-substring-no-properties pt (point)))
           (tok-other (if (zerop tok-punc) (skip-syntax-forward "w_'"))))
     ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token
     (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
       (forward-char -1))
     (buffer-substring-no-properties pt (point)))))

;; ignore-between is a description of pseudo delimiters of blocks that
;; should be jumped when searching. There is a bad interaction when
;; tokens and ignore-bteween are not disjoint
(defun coq-smie-search-token-forward (tokens &optional end ignore-between)
  "Search for one of TOKENS between point and END.
If some enclosing parenthesis is reached, stop there and return
nil. Token \".\" is considered only if followed by a space.
optional IGNORE-BETWEEN defines opener/closer to ignore during
search. Careful: the search for a opener stays inside the current
command (and inside parenthesis)."
  (unless end (setq end (point-max)))
  (condition-case nil
      (catch 'found
	(while (< (point) end)
	  ;; The default lexer is faster and is good enough for our needs.
	  (let* ((next (coq-forward-token-fast-nogluing-dot-friends))
		 (parop (assoc next ignore-between)))
	    ; if we find something to ignore, we directly jump to the
	    ; corresponding closer
	    (if parop
		(let ((parops ; corresponding matcher may be a list
		       (if (listp parop) (cdr parop)
			 (cons (cdr parop) nil)))) ; go to corresponding closer
		  (when (member
			 (coq-smie-search-token-forward
			  (append parops (cons "." nil))
			  end ignore-between)
			 (cons "." nil))
		  (goto-char (point))
		  next))
	      ;; Do not consider "." when not followed by a space
	      (when (or (not (equal next ".")) ; see backward version
			(looking-at "[[:space:]]"))
		(cond
		 ((and (zerop (length next))
		       (or (equal (point) (point-max)) ; protecting char-after next line
			   (equal (char-syntax ?\)) (char-syntax (char-after)))))
		  (throw 'found nil))
		 ((zerop (length next)) ;; capture other characters than closing parent
		  ;; don't use smmie-forward-sexp here
		  (let ((forward-sexp-function nil)) (forward-sexp 1)))
		 ((member next tokens) (throw 'found next))))))))
    (scan-error nil)))


;; ignore-between is a description of pseudo delimiters of blocks that
;; should be jumped when searching. There is a bad interaction when
;; tokens and ignore-bteween are not disjoint
(defun coq-smie-search-token-backward (tokens &optional end ignore-between)
  "Search for one of TOKENS between point and END.
If some enclosing parenthesis is reached, stop there and return
nil. Token \".\" is considered only if followed by a space.
optional IGNORE-BETWEEN defines opener/closer to ignore during
search. Careful: the search for a opener stays inside the current
command (and inside parenthesis). "
  (unless end (setq end (point-min)))
    (condition-case nil
	(catch 'found
	  (while (> (point) end)
	    ;; The default lexer is faster and is good enough for our needs.
	    (let* ((next (coq-backward-token-fast-nogluing-dot-friends))
		   (parop (rassoc next ignore-between)))
	      ; if we find something to ignore, we directly jump to the
	      ; corresponding openner
	      (if parop
		  (let ((p (point))
			(parops ; corresponding matcher may be a list
			 (if (listp (car parop)) (car parop) (cons (car parop) nil))))
		    ; go to corresponding closer or meet "."
		    ;(message "newpatterns = %S" (append parops (cons "." nil)))
		    (when (member
			   (coq-smie-search-token-backward
			    (append parops (cons "." nil))
			    end ignore-between)
			   (cons "." nil))
		      (goto-char (point))
		      next))
		;; Do not consider "." when not followed by a space
		;(message "SPACE?: %S , %S , %S" next next (looking-at ".[[:space:]]"))
		(when (or (not (equal next "."))
			  (looking-at "\\.[[:space:]]"))
		  (cond
		   ((and (zerop (length next))
			 (or (equal (point) (point-min)) ; protecting char-before next line
			     (equal (char-syntax ?\() (char-syntax (char-before)))))
		    (throw 'found nil))
		   ((zerop (length next))
		    ;; don't use smmie-forward-sexp here
		    (let ((forward-sexp-function nil)) (forward-sexp -1)))
		   ((member next tokens) (throw 'found next))))))))
      (scan-error nil)))

(defun coq-lonely-:=-in-this-command ()
  "Return t if there is a lonely \":=\" from (point) to end of command.
Non lonely \":=\" are those corresponding to \"let\" or
\"with\" (module declaration) or those inside parenthesis. this
function is used to detect whether a command is a definition or a
proof-mode starter in Coq."
  (equal (coq-smie-search-token-forward
	  '("." ":=") nil
	  '(("with" . (":=" "signature")) ("let" . "in")))
	 "."))

;; Heuristic to detect a goal opening command: there must be a lonely
;; ":=" until command end.
;; \\|\\(Declare\\s-+\\)?Instance is not detected as it is not
;; syntactically decidable to know if some goals are created. Same for
;; Program Fixpoint but with Program Next Obligation is mandatory for
;; each goal anyway.
(defun coq-smie-detect-goal-command ()
  "Return t if the next command is a goal starting to be indented.
The point should be at the beginning of the command name. As
false positive are more annoying than false negative, return t
only if it is FOR SURE a goal opener. Put a \"Proof.\" when you want to
force indentation."
  (save-excursion ; FIXME add other commands that potentialy open goals
    (when (proof-looking-at "\\(Local\\|Global\\)?\
\\(Definition\\|Lemma\\|Theorem\\|Fact\\|Let\\|Class\
\\|Proposition\\|Remark\\|Corollary\\|Goal\
\\|Add\\(\\s-+Parametric\\)?\\s-+Morphism\
\\|Fixpoint\\)\\>") ;; Yes Fixpoint can start a proof like Definition
	(coq-lonely-:=-in-this-command))))


;; Heuristic to detect a goal opening command: there must be a lonely ":="
(defun coq-smie-module-deambiguate ()
  "Return t if the next command is a goal starting command.
The point should be at the beginning of the command name."
  (save-excursion ; FIXME Is there other module starting commands?
    (cond
     ((looking-back "with\\s-+" nil) "module") ; lowecase means Module that is not a declaration keyword (like in with Module) 
     ((proof-looking-at "\\(Module\\|Section\\)\\>")
      (if (coq-lonely-:=-in-this-command) "Module start" "Module def")))))


;(defun coq-smie-detect-module-or-section-start-command ()
;  "Return t if the next command is a goal starting command.
;The point should be at the beginning of the command name."
;  (save-excursion ; FIXME Is there other module starting commands?
;    (when (and (looking-back "with")
;	       (proof-looking-at "\\(\\(?:Declare\\s-+\\)?Module\\|Section\\)\\>"))
;      (coq-lonely-:=-in-this-command))))


(defconst coq-smie-proof-end-tokens
  ;; '("Qed" "Save" "Defined" "Admitted" "Abort")
  (cons "EndSubproof" (remove "End" coq-keywords-save-strict)))


(defun coq-is-at-command-real-start()
  (equal (point)
	 (save-excursion (coq-find-real-start))))

(defun coq-is-bullet-token (tok) (string-suffix-p "bullet" tok))
(defun coq-is-subproof-token (tok) (string-suffix-p "subproof" tok))
(defun coq-is-dot-token (tok) (or (string-suffix-p "proofstart" tok)
			       (string-equal "." tok)))
(defun coq-is-cmdend-token (tok)
  (or (coq-is-bullet-token tok) (coq-is-subproof-token tok) (coq-is-dot-token tok)))


(defun coq-smie-forward-token ()
  (let ((tok (smie-default-forward-token)))
    (cond
     ((assoc tok coq-smie-user-tokens)
      (let ((res (assoc tok coq-smie-user-tokens)))
        (cdr res)))
     ;; @ may be  ahead of an id, it is part of the id.
     ((and (equal tok "@") (looking-at "[[:alpha:]_]"))
      (let ((newtok (coq-smie-forward-token))) ;; recursive call
	(concat tok newtok)))
     ;; detecting if some qualification (dot notation) follows that id and
     ;; extend it if yes. Does not capture other alphanumerical token (captured
     ;; below)
     ((and (string-match "@?[[:alpha:]_][[:word:]]*" tok)
	   (looking-at "\\.[[:alpha:]_]")
	   (progn (forward-char 1)
		  (let ((newtok (coq-smie-forward-token))) ; recursive call
		    (concat tok "." newtok)))))
     ((member tok '("." "..."))
      ;; swallow if qualid, call backward-token otherwise
      (cond
       ((member (char-after) '(?w ?_))  ;(looking-at "[[:alpha:]_]") ;; extend qualifier
	(let ((newtok (coq-smie-forward-token))) ;; recursive call
	  (concat tok newtok)))
       (t (save-excursion (coq-smie-backward-token))))) ;; recursive call
     ((or (string-match coq-bullet-regexp-nospace tok)
	  (member tok '("=>" ":=" "::=" "exists" "in" "as" "∀" "∃" "→" "∨" "∧" ";"
			"," ":" "eval")))
      ;; 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)))

     ;; easier to return directly than calling coq-smie-backward-token
     ((member tok '("lazymatch" "multimatch")) "match")

     ;; detect "with signature", otherwies use coq-smie-backward-token
     ((equal tok "with")
      (let ((p (point)))
	(if (equal (smie-default-forward-token) "signature")
	    "with signature"
	  (goto-char p)
	  (save-excursion (coq-smie-backward-token)))))

     ((member tok '("transitivity" "symmetry" "reflexivity"))
      (let ((p (point)))
	(if (and (equal (smie-default-forward-token) "proved")
		 (equal (smie-default-forward-token) "by"))
	    "xxx provedby"
	  (goto-char p)
	  tok))) ; by tactical

     ((member tok '("Module")) ; TODO: Declare
      (let ((pos (point))
	    (next (smie-default-forward-token)))
	(unless (equal next "Type") (goto-char pos))
	(save-excursion (coq-smie-backward-token))))

     ((member tok '("End"))
      (save-excursion (coq-smie-backward-token)))

     ; empty token if a prenthesis is met.
     ((and (zerop (length tok)) (looking-at "{|")) (goto-char (match-end 0)) "{|")

     ;; this must be after detecting "{|":
     ((and (zerop (length tok)) (eq (char-after) ?\{))
      (if (equal (save-excursion (forward-char 1) (coq-smie-backward-token))
		 "{ subproof")
	  (progn (forward-char 1) "{ subproof")
	tok))

     ((and (zerop (length tok)) (eq (char-after) ?\}))
      (if (equal (save-excursion (forward-char 1)
				 (coq-smie-backward-token))
		 "} subproof")
	  (progn (forward-char 1) "} subproof")
	tok))
     ((and (equal tok "|") (eq (char-after) ?\}))
      (goto-char (1+ (point))) "|}")
     ((member tok coq-smie-proof-end-tokens) "Proof End")
     ((member tok '("Obligation")) "Proof")
     ;; FIXME: this case should be useless now that we replace
     ;; smie-default-forward... by a smarter function.
     ((coq-dot-friend-p tok) ".")
     ;; Try to rely on backward-token for non empty tokens: bugs (hangs)
     ;; ((not (zerop (length tok))) (save-excursion (coq-smie-backward-token)))
     ;; return it.
     (tok)
     )))




(defun coq-smie-:=-deambiguate ()
  (let ((corresp (coq-smie-search-token-backward
		  '("let" "Inductive" "CoInductive" "{|" "." "with" "Module" "where")
		  nil '((("let" "with") . ":=")))))
    (cond
     ((equal corresp "with")
      (let ((corresptok (coq-smie-with-deambiguate)))
	(cond ;; recursive call if the with found is actually et with match
	 ((equal corresptok "with match") (coq-smie-:=-deambiguate))
	 ((equal corresptok "with inductive") ":= inductive")
	 (t ":=")
	 )))
     ((equal corresp ".") ":= def") ; := outside of any parenthesis
     ((equal corresp "Module")
      (let ((p (point)))
	(if (equal (smie-default-backward-token) "with")
	    ":= with"
	  (goto-char p)
	  ":= module")))
     ((member corresp '("Inductive" "CoInductive" "Variant")) ":= inductive")
     ((equal corresp "let") ":= let")
     ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind
     ((or (looking-back "{" nil)) ":= record")
     (t ":=")))) ; a parenthesis stopped the search



(defun coq-smie-backward-token ()
  (let* ((tok (smie-default-backward-token)))
    (cond
     ((assoc tok coq-smie-user-tokens)
      (let ((res (assoc tok coq-smie-user-tokens)))
        (cdr res)))
     ;; Distinguish between "," from quantification and other uses of
     ;; "," (tuples, tactic arguments)
     ((equal tok ",")
      (save-excursion
	(let ((backtok (coq-smie-search-token-backward
			'("forall" "∀" "∃" "exists" "|" "match" "lazymatch" "multimatch" "."))))
	  (cond
	   ((member backtok '("forall" "∀" "∃")) ", quantif")
	   ((equal backtok "exists") ; there is a tactic called exists
	    (if (equal (coq-smie-forward-token) ;; recursive call
		       "quantif exists")
		", quantif" tok))
	   (t tok)))))

     ; Same for ";" : record field separator, tactic combinator, etc
     ((equal tok ";")
      (save-excursion
	(let ((backtok (coq-smie-search-token-backward '("." "[" "{" "Ltac"))))
	  (cond
	   ((member backtok '("." "Ltac")) "; tactic")
	   ((equal backtok nil)
	    (if (or (looking-back "(" nil) (looking-back "\\[")
		    (and (looking-back "{" nil)
			 (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call
		"; tactic"
	      "; record"))))))

     ;; trying to discriminate between bollean operator || and tactical ||.
     ((equal tok "||")
      (save-excursion
	(let ((backtok (coq-smie-search-token-backward '("." ";" "Ltac" "(" "[" "{"))))
	  (cond
	   ((member backtok '("." "Ltac")) "|| tactic")
	   ((and (equal backtok ";")
		 (or (forward-char) t)
		 (equal (coq-smie-backward-token) "; tactic")) ;; recursive
	    "|| tactic")
	   ;; this is wrong half of the time but should not harm indentation
	   ((and (equal backtok nil) (looking-back "(" nil)) "||") 
	   ((equal backtok nil)
	    (if (or (looking-back "\\[" nil)
		    (and (looking-back "{" nil)
			 (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call
		"|| tactic"
	      "||"))))))


     ; Same for "->" : rewrite or intro arg or term's implication
     ; FIXME: user defined arrows will be considered a term
     ((equal tok "->")
      (save-excursion
	(let ((backtok (coq-smie-search-token-backward '("intro" "intros" "rewrite" "."))))
	  (cond
	   ((equal backtok ".") "->")
	   ((equal backtok nil) "->")
	   (t "-> tactic")))))


     ((equal tok "Module")
      (save-excursion
	;(coq-find-real-start)
	(coq-smie-module-deambiguate)))

     ((member tok '("lazymatch" "multimatch")) "match")

     ((equal tok "tryif") "if")

     ;; rhaaa... Some peolple use "End" as a id...
     ((equal tok "End")
      (if (coq-is-at-command-real-start) "end module" tok))

     ((and (equal tok "|") (eq (char-before) ?\{))
      (goto-char (1- (point))) "{|")

     ((and (zerop (length tok)) (member (char-before) '(?\{ ?\}))
           (save-excursion
             (forward-char -1)
             (if (and (looking-at "{")
                      (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t))
                 (goto-char (match-beginning 0)))
             (let ((nxttok (coq-smie-backward-token))) ;; recursive call
               (coq-is-cmdend-token nxttok))))
      (forward-char -1)
      (if (looking-at "}") "} subproof"
        (if (and (looking-at "{")
                 (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t))
            (goto-char (match-beginning 0)))
        "{ subproof"
        ))

     ;; ((and (zerop (length tok)) (member (char-before) '(?\{ ?\}))
     ;;       (save-excursion
     ;;         (forward-char -1)
     ;;         (let ((nxttok (coq-smie-backward-token))) ;; recursive call
     ;;           (coq-is-cmdend-token nxttok))))
     ;;  (forward-char -1)
     ;;  (if (looking-at "{") "{ subproof" "} subproof"))

     ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil))
      ": ltacconstr")

     ((member tok '(":=" "::="))
      (save-excursion
	(save-excursion (coq-smie-:=-deambiguate))))

     ((equal tok "=>")
      (save-excursion
	(let ((corresp (coq-smie-search-token-backward
			'("|" "match" "lazymatch" "multimatch" "fun" ".")
			nil '((("match" "lazymatch" "multimatch") . "end") ("fun" . "=>")))))
	  (cond
	   ((member corresp '("fun")) "=> fun") ; fun
	   (t tok)))))

     ;; FIXME: no token should end with "." except "." itself
     ; for "unfold in *|-*."
     ((member tok '("*." "-*." "|-*." "*|-*."))
      (forward-char (- (length tok) 1))
      (coq-smie-.-deambiguate))
     ; for "unfold in *|-*;"
     ((member tok '("*;" "-*;" "|-*;" "*|-*;"))
      ;; FIXME; can be "; ltac" too
      (forward-char (- (length tok) 1)) "; tactic")
     ;; bullet detected, is it really a bullet? we have to traverse
     ;; recursively any other bullet or "n:{" "}". this is the work of
     ;; coq-empty-command-p
     ((and (string-match coq-bullet-regexp-nospace tok)
	   (save-excursion (coq-empty-command-p)))
      (concat tok " bullet"))

     ((and (member tok '("exists" "∃"))
	   (save-excursion
	     ;; recursive call looking at the ptoken immediately before
	     (let ((prevtok (coq-smie-backward-token)))
	       ;; => may be wrong here but rare (have "=> ltac"?)
	       (not (or (coq-is-cmdend-token prevtok)
			(member prevtok '("; tactic" "[" "]" "|" "=>")))))))
      "quantif exists")

     ((equal tok "∀") "forall")
     ((equal tok "→") "->")
     ((equal tok "∨") "\\/")
     ((equal tok "∧") "/\\")

     ((equal tok "with") ; "with" is a nightmare: at least 4 different uses
      (save-excursion (coq-smie-with-deambiguate)))
     ((equal tok "where")
      "where")

     ((and (equal tok "signature")
	   (equal (smie-default-backward-token) "with"))
      "with signature")

     ((equal tok "by")
      (let ((p (point)))
	(if (and (equal (smie-default-backward-token) "proved")
		 (member (smie-default-backward-token)
			 '("transitivity" "symmetry" "reflexivity")))
	    "xxx provedby"
	  (goto-char p)
	  tok))) ; by tactical

     ((equal tok "as")
      (save-excursion
	(let ((prev-interesting
	       (coq-smie-search-token-backward
		'("match" "lazymatch" "multimatch" "Morphism" "Relation" "." ". proofstart"
		  "{ subproof" "} subproof" "as")
		nil
		'((("match" "lazymatch" "multimatch" "let") . "with") ("with" . "signature")))))
	  (cond
	   ((member prev-interesting '("match" "lazymatch" "multimatch")) "as match")
	   ((member prev-interesting '("Morphism" "Relation")) "as morphism")
	   (t tok)))))

     ((equal tok "by")
      (let ((p (point)))
	(if (and (equal (smie-default-backward-token) "proved")
		 (member (smie-default-backward-token)
			 '("transitivity" "symmetry" "reflexivity")))
	    "xxx provedby"
	  (goto-char p)
	  tok))) ; by tactical


     ((equal tok "eval")
      (if (member (save-excursion
		    (forward-char 4)
		    (smie-default-forward-token))
		  '("red" "hnf" "compute" "simpl" "cbv" "lazy" "unfold" "fold" "pattern"))
	  "eval in" tok))
     

     ((equal tok "in")
      (save-excursion
	(let ((prev-interesting
	       (coq-smie-search-token-backward
		'("let" "match" "lazymatch" "multimatch" ;"eval" should be "eval in" but this is not supported by search-token-backward
		  "." ) nil
		'((("match" "lazymatch" "multimatch") . "with") (("let" ;"eval"
				       ) . "in")))))
	  (cond
	   ((member prev-interesting '("." nil)) "in tactic")
	   ((equal prev-interesting "let") "in let")
	   ;((equal prev-interesting "eval in") "in eval"); not detectable by coq-smie-search-token-backward
	   ((equal prev-interesting "match") "in match")
	   (t "in tactic")))))

     ((and (eq (char-before) ?@) (member (char-syntax (char-after)) '(?w ?_)))
      (forward-char -1)
      (concat "@" tok))

     ((member tok coq-smie-proof-end-tokens) "Proof End")

     ((member tok '("." "..."))
      ;; Distinguish field-selector "." from terminator "." from module
      ;; qualifier.
      (let ((nxtnxt (char-after (+ (point) (length tok)))))
	(if (eq nxtnxt ?\() ". selector"
	  (if (or (null nxtnxt) (eq (char-syntax nxtnxt) ?\ ))
	      ;; command terminator: ". proofstart" et al
	      (save-excursion (forward-char (- (length tok) 1))
			      (coq-smie-.-deambiguate))
	    (if (eq (char-syntax nxtnxt) ?w)
		(let ((newtok (coq-smie-complete-qualid-backward)))
		  ;; qualified name
		  (concat newtok tok))
	      ". selector")))))  ;; probably a user defined syntax

     ((and (and (eq (char-before) ?.) (member (char-syntax (char-after))
					      '(?w ?_))))
      (forward-char -1)
      (let ((newtok (coq-smie-backward-token))) ; recursive call
	(concat newtok "." tok)))

     ((coq-dot-friend-p tok) ".")

     (tok))))


(defcustom coq-indent-box-style nil
  "If non-nil, Coq mode will try to indent with a box style (SMIE code only).
Box style looks like this:

Lemma foo: forall n,
             n = n.

instead of:

Lemma foo: forall n,
  n = n.
"
  :type 'boolean
  :group 'coq)

(defun coq-indent-safep (indent)
  (>= indent 0))

(defcustom coq-indent-proofstart 2
  "Number of spaces used to indent after a proof start."
  :type 'integer
  :group 'coq
  :safe #'coq-indent-safep)

(defcustom coq-indent-semicolon-tactical 2
  "Number of spaces used to indent after the first tactical semi colon of a serie.
  If set to 0, indetation is as follows:
   tac1;
   tac2;
   tac3;
   tac4.

   if set to 2 (default):

   tac1;
     tac2;
     tac3;
     tac4."
  :type 'integer
  :group 'coq
  :safe #'coq-indent-safep)

(defcustom coq-indent-modulestart 2
  "Number of spaces used to indent after a module or section start."
  :type 'integer
  :group 'coq
  :safe #'coq-indent-safep)

(defcustom coq-smie-after-bolp-indentation 2
  "Number of spaces used to indent after a quantifier *not* on its own line.

the number of space is meant \"from the column on which the quantifier
would be if it were on its own line\".
for example, if set to 0 the indentation is as follows:

   Lemma foo: forall x:nat,
     x <= 0 -> x = 0.

If it is set to 2 (default) it is as follows:

   Lemma foo: forall x:nat,
       x <= 0 -> x = 0.
"
  :type 'integer
  :group 'coq
  :safe #'coq-indent-safep)

(defcustom coq-match-indent 2
  "Number of space used to indent cases of a match expression.
If the \"|\" separator is used, indentation will be reduced by 2.
For example the default value 2 makes indetation like this:

match n with
  O => ...
| S n => ...
end

Typical values are 2 or 4."
  :type 'integer
  :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.
(defconst coq-smie-grammar
  (when (fboundp 'smie-prec2->grammar)
    (smie-prec2->grammar
     (smie-bnf->prec2
      '((exp
	 (exp ":= def" exp)
	 (exp ":=" exp) (exp ":= inductive" exp)
	 (exp "||" exp) (exp "|" exp) (exp "=>" exp)
	 (exp "xxx provedby" exp) (exp "as morphism" exp)
	 (exp "with signature" exp)
	 ("match" matchexp "with match" exp "end");expssss
	 ("let" assigns "in let" exp) ;("eval in" assigns "in eval" exp) disabled
	 ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp)
	 ("quantif exists" exp ", quantif" exp)
	 ("forall" exp ", quantif" exp)
	 ;;;
	 ("(" exp ")") ("{|" exps "|}") ("{" exps "}")
	 (exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp)
	 (exp "by" exp) (exp "with" exp) (exp "|-" exp)
	 (exp ":" exp) (exp ":<" exp) (exp "," exp)
	 (exp "->" exp) (exp "<->" exp) (exp "&" exp)
	 (exp "/\\" exp) (exp "\\/" exp)
	 (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp)
	 (exp "<" exp) (exp ">=" exp) (exp ">" exp)
	 (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp)
	 (exp "^" exp)
	 (exp "+" exp) (exp "-" exp)
	 (exp "*" exp)
	 (exp ": ltacconstr" exp)(exp ". selector" 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) )
	(exps (affectrec) (exps "; record" exps))
	(affectrec (exp ":= record" exp))
	(assigns  (exp ":= let" exp)) ;(assigns "; record" assigns)

	(moduledef (moduledecl ":= module" exp))
	(moduledecl (exp) (exp ":" moduleconstraint)
		    (exp "<:" moduleconstraint))
	(moduleconstraint
	 (exp) (exp ":= with" exp)
	 (moduleconstraint "with module" "module" moduleconstraint))

	;; To deal with indentation inside module declaration and inside
	;; proofs, we rely on the lexer. The lexer detects "." terminator of
	;; goal starter and returns the ". proofstart" and ". moduelstart"
	;; tokens.
	(bloc ("{ subproof" commands "} subproof")
	      (". proofstart" commands  "Proof End")
	      (". modulestart" commands  "end module" exp)
	      (moduledecl) (moduledef)
	      (exp))

	(commands (commands "." commands)
		  (commands "- bullet" commands)
		  (commands "+ bullet" commands)
		  (commands "* bullet" commands)
		  (commands "-- bullet" commands)
		  (commands "++ bullet" commands)
		  (commands "** bullet" commands)
		  (commands "--- bullet" commands)
		  (commands "+++ bullet" commands)
		  (commands "*** bullet" commands)
		  (commands "---- bullet" commands)
		  (commands "++++ bullet" commands)
		  (commands "**** bullet" commands)
		  ;; "with" of mutual definition should act like "."
		  ;; same for "where" (introduction of a notation
		  ;; after a inductive or fixpoint)
		  (commands "with inductive" commands)
		  (commands "with fixpoint" commands)
		  (commands "where" commands)
		  (bloc)))


      ;; Resolve the "trailing expression ambiguity" as in "else x -> b".
      ;; each line orders tokens by increasing priority
      ;; | C x => fun a => b | C2 x => ...
      ;;'((assoc "=>") (assoc "|")  (assoc "|-" "=> fun")) ; (assoc ", quantif")
      '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet")
	(assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet")
	(assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet")
	(assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet")
	(assoc ".")
	(assoc "with inductive" "with fixpoint" "where"))
      '((assoc ":= def" ":= inductive")
	(assoc "|") (assoc "=>")
	(assoc ":=")	(assoc "xxx provedby")
	(assoc "as morphism") (assoc "with signature") (assoc "with match")
	(assoc "in let")
	(assoc "in eval") (assoc "=> fun") (assoc "then") (assoc ", quantif")
	(assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
	(assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
	(assoc "|-") (assoc ":" ":<") (assoc ",")
        (assoc "else")
        (assoc "->") (assoc "<->")
	(assoc "&") (assoc "/\\") (assoc "\\/")
	(assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>")
	(assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^")
	(assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
	(assoc "+") (assoc "-") (assoc "*")
	(assoc ": ltacconstr") (assoc ". selector"))
      '((assoc ":" ":<")  (assoc "<"))
      '((assoc ". modulestart" "." ". proofstart") (assoc "Module def")
	(assoc "with module" "module") (assoc ":= module")
	(assoc ":= with")  (assoc ":" ":<"))
      '((assoc ":= def") (assoc "; record") (assoc ":= record")))))
  "Parsing table for Coq.  See `smie-grammar'.")
;; FIXME:
; Record rec:Set :=     {
;                   fld1:nat;
;                   fld2:nat;
;                   fld3:bool
;                 }.
; FIXME: as is sometimes a "as morphism" but not detected as such
;; Add Parametric Morphism (A : Type) : (mu (A:=A))
;;     with signature Oeq ==> Oeq
;;                    as mu_eq_morphism.

;; FIXME: have a different token for := corresponding to a "fix" (not
;; Fixpoint)
;;Definition join l : key -> elt -> t -> t :=
;;      match l with
;;        | Leaf => add
;;        | Node ll lx ld lr lh => fun x d =>
;;                                   fix join_aux (r:t) : t
;;        := match r with   <---- ??
;;             | Leaf =>  add x d l


;; Returns the column of the beginning of current atomic tactic (non
;; composed). Returns the command start column if not found.
(defun coq-find-with-related-backward()
  (let ((cmd-start (save-excursion (coq-find-real-start))))
    (save-excursion
      ;; no point in going further the start of the command
      ;; let us find a tactical between it and point
      (let ((tok (coq-smie-search-token-backward '(";" "||" "|" "+") cmd-start)))
        ;; hopefully we found the start of the current (non composed)tactic
        ;; move point after the token found (if not found it will not move)
        (forward-char (length tok))
        (forward-comment (point-max)); skip spaces
        ;; (coq-find-not-in-comment-forward "[^;+[:space:]|]")
        (current-column)))))

(defun coq-is-at-first-line-of-def-decl ()
  (let ((pt (point)))
    (save-excursion
      (and
       (member (coq-smie-backward-token) '(":" ":="))
       (equal (line-number-at-pos) (line-number-at-pos pt))
       (or (back-to-indentation) t)
       (looking-at "Lemma\\|Defintion\\|Theorem\\|Corollary")))))

;; copied from elixir-smie.el
(defun coq-smie--same-line-as-parent (parent-pos child-pos)
  "Return non-nil if `child-pos' is on same line as `parent-pos'."
  (= (line-number-at-pos parent-pos) (line-number-at-pos child-pos)))

(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."
  (case kind
     (:elem (case token
	      (basic proof-indent)))
     (: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
      (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"
			    "by" "in tactic" "<:" "<+" ":= record"
			    "with module" "as" ":= inductive" ":= module" )))
	2)

       ((equal token "with match") coq-match-indent)
       ((equal token "with") 2)  ; add 2 to the column of "with" in the children


       ;;; 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"))
		     (and smie--parent
			  (coq-smie--same-line-as-parent
			   (nth 1 smie--parent) (point)))))
	    coq-indent-semicolon-tactical
	  nil))

       ; "as" tactical is not idented correctly
       ((equal token "in let") (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
      (cond

;       ((and (member token '("{ subproof"))
;	     (not coq-indent-box-style)
;	     (not (smie-rule-bolp)))
;	(if (smie-rule-parent-p "Proof")
;	    (smie-rule-parent 2)
;	  (smie-rule-parent)))

       ;; "with" is also in the :list-intro rules and in :after.
       ((equal token "with")
        ;; Hack: We know that "with" is linked to the first word of
        ;; the current atomic tactic. This tactic is the parent, not
        ;; the "." of the previous command.
        `(column . ,(+ 2 (coq-find-with-related-backward))))

       ((equal token "with module")
	(if (smie-rule-parent-p "with module")
	    (smie-rule-parent)
	  (smie-rule-parent 4)))

       ((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))

       ;; 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)
;	     (not (smie-rule-bolp)))
;	(smie-rule-parent))


       ((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 '(":= module" ":= inductive" ":= def"))
            (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)
                 (current-column))))
          `(column . ,(if (smie-rule-hanging-p) pcol (+ 2 pcol)))))

       ((equal token "|")
	(cond ((smie-rule-parent-p "with match")
	       (- (funcall smie-rules-function :after "with match") 2))
	      ((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"))
;;        ;; ¡¡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
;;        ;; not with Proof but with any of the keywords like Lemma that can
;;        ;; start a new proof), but we can workaround the problem here, because
;;        ;; SMIE happened to decide arbitrarily that Qed will stop before Module
;;        ;; when parsing backward.
;;        ;; FIXME: This is fundamentally very wrong, but it seems to work
;;        ;; OK in practice.
;;        (smie-rule-parent 2))




(provide 'coq-smie)
;;; coq-smie.el ends here