From 67f4332c9e802a0d272ac0670515d98d16cfebb4 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Tue, 3 Jun 2014 02:51:24 +0000 Subject: Rename coq-smie-lexer.el to coq-smie.el. --- coq/coq-smie-lexer.el | 825 ------------------------------------------------- coq/coq-smie.el | 841 ++++++++++++++++++++++++++++++++++++++++++++++++++ coq/coq.el | 2 +- coq/ex/indent.v | 17 +- 4 files changed, 854 insertions(+), 831 deletions(-) delete mode 100644 coq/coq-smie-lexer.el create mode 100644 coq/coq-smie.el diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el deleted file mode 100644 index eabc2ce6..00000000 --- a/coq/coq-smie-lexer.el +++ /dev/null @@ -1,825 +0,0 @@ -;; Lexer. -;; - 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". - -(require 'coq-indent) -(require 'smie nil 'noerror) - -;; 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)))) - - - - -(defun coq-smie-is-tactic () - (save-excursion - (coq-find-real-start) - (let ((cfs case-fold-search)) - (setq case-fold-search nil) - (let ((res (looking-at "[[:upper:]]"))) - (setq case-fold-search cfs) - (not res))))) - - -(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") ". proofstart" ".")) - ((or (looking-at "Next\\s-+Obligation\\>") - (coq-smie-detect-goal-command)) - (save-excursion - (goto-char (+ p 1)) - (if (equal (smie-default-forward-token) "Proof") - "." ". 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" ".")))) - (cond - ((null tok) nil) - ((equal tok ".") nil) - ((equal tok "match") t) - ((equal tok "with") - (coq-smie-find-unclosed-match-backward) - (coq-smie-find-unclosed-match-backward))))) - -(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") "with fixpoint") - ((looking-at "Module\\|Declare") "with module") - (t "with"))))) - - - -;; 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* ((next2 (smie-default-forward-token)) - (is-dot-friend (coq-dot-friend-p next2)) - (next (if is-dot-friend "." next2)) - (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 - (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* ((next2 (smie-default-backward-token)) - (is-dot-friend (coq-dot-friend-p next2)) - (next (if is-dot-friend "." next2)) - (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" next2 next (looking-at ".[[:space:]]")) - (when (or (not (equal next2 ".")) - (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)) (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-+") "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-smie-forward-token () - (let ((tok (smie-default-forward-token))) - (cond - ;; @ 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 - ((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))) - - ;; 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))) - - ((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") - ((coq-dot-friend-p tok) ".") - (tok)))) - - -(defun coq-is-at-command-real-start() - (equal (point) - (save-excursion (coq-find-real-start)))) - - -(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")) ":= inductive") - ((equal corresp "let") ":= let") - ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind - ((or (looking-back "{")) ":= record") - (t ":=")))) ; a parenthesis stopped the search - - -(defun coq-smie-backward-token () - (let ((tok (smie-default-backward-token))) - (cond - ((equal tok ",") - (save-excursion - (let ((backtok (coq-smie-search-token-backward - '("forall" "∀" "∃" "exists" "|" "match" ".")))) - (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))))) - ;; Distinguish between "," from quantification and other uses of - ;; "," (tuples, tactic arguments) - - ((equal tok ";") - (save-excursion - (let ((backtok (coq-smie-search-token-backward '("." "[" "{")))) - (cond - ((equal backtok ".") "; tactic") - ((equal backtok nil) - (if (or (looking-back "\\[") - (and (looking-back "{") - (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call - "; tactic" - "; record")))))) - - ((equal tok "Module") - (save-excursion - ;(coq-find-real-start) - (coq-smie-module-deambiguate))) - - ;; 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) - (member (coq-smie-backward-token) ;; recursive call - '("." ". proofstart" "{ subproof" "} subproof" - "- bullet" "+ bullet" "* bullet")))) - (forward-char -1) - (if (looking-at "{") "{ subproof" "} subproof")) - - ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\)")) - ": ltacconstr") - - ((equal tok ":=") - (save-excursion - (save-excursion (coq-smie-:=-deambiguate)))) - - ((equal tok "=>") - (save-excursion - (let ((corresp (coq-smie-search-token-backward - '("|" "match" "fun" ".") - nil '(("match" . "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 1) ".") - ; for "unfold in *|-*;" - ((member tok '("*;" "-*;" "|-*;" "*|-*;")) (forward-char 1) "; tactic") - ((and (member tok '("+" "-" "*")) - (save-excursion - (let ((prev (coq-smie-backward-token))) ;; recursive call - (member prev '("." ". proofstart" "{ subproof" "} subproof"))))) - (concat tok " bullet")) - - - - ((and (member tok '("exists" "∃")) - (save-excursion - (not (member - (coq-smie-backward-token) ;; recursive call looking at the ptoken immediately before - '("." ". proofstart" "; tactic" "[" "]" "|" "=>" ;; => may be wrong here but rare (h0ave "=> ltac"?) - "{ subproof" "} subproof" "- bullet" "+ bullet" - "* bullet"))))) - "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") ; "with" is a nightmare: at least 4 different uses - "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" "Morphism" "Relation" "." ". proofstart" - "{ subproof" "} subproof" "as") - nil - '((("match" "let") . "with") ("with" . "signature"))))) - (cond - ((equal prev-interesting "match") "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" ;"eval" should be "eval in" but this is not supported by search-token-backward - "." ) nil - '(("match" . "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 (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 looke like this: -Lemma foo: forall n, - n = n. - -instead of - -Lemma foo: forall n, - n = n. -" - :type 'boolean - :group 'coq) - - -;; - 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 "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 " 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 ".") - (assoc "with inductive" "with fixpoint" "where")) - '((assoc "|") (assoc "=>") - (assoc ":= def" ":= inductive") - (assoc ":=") (assoc "xxx provedby") - (assoc "as morphism") (assoc "with signature") (assoc "with match") - (assoc "in let") - (assoc "in eval") (assoc "=> fun") (assoc "then") (assoc "else") - (assoc ", quantif") - (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with") - (assoc "|-") (assoc ":" ":<") (assoc ",") (assoc "->") (assoc "<->") - (assoc "&") (assoc "/\\") (assoc "\\/") - (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>") - (assoc "=?") (assoc "<=?") (assoc " 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 - - -; This fixes a bug in smie that is not yet in regular emacs distribs?? -; To show the bug. Comment this and then try to indent the following: -; Module X. -; Module Y. <-- here --> Error: (wrong-type-argument integer-or-marker-p nil) -; No need anymore? -;; (defun smie-indent--parent () -;; (or smie--parent -;; (save-excursion -;; (let* ((pos (point)) -;; (tok (funcall smie-forward-token-function))) -;; (unless (numberp (cadr (assoc tok smie-grammar))) -;; (goto-char pos)) -;; (setq smie--parent -;; (or (smie-backward-sexp 'halfsexp) -;; (let (res) -;; (while (null (setq res (smie-backward-sexp)))) -;; (list nil (point) (nth 2 res))))))))) - -(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))) - (:list-intro - (or (member token '("fun" "forall" "quantif exists")) - ;; 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 (member token '("{ subproof" "- bullet" "+ bullet" "* bullet" - "." ". proofstart")) - (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. - ((member token '(":" ":=" ":= with" ":= def" "- bullet" "+ bullet" "* bullet" - "by" "in tactic" "<:" "<+" ":= record" - "with module" "as" ":= inductive" ":= module" )) 2) - - ((equal token "with match") 4) - - ((equal token "; tactic") - (cond - ((smie-rule-parent-p "; tactic") (smie-rule-separator kind)) - (t (smie-rule-parent 2)))) - - ; "as" tactical is not idented correctly - ((equal token "in let") (smie-rule-parent)))) - - (:before - (cond - ((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" - "{ 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))) - - - ((and (member token '("forall" "quantif exists")) - (smie-rule-parent-p "forall" "exists quantif")) - (smie-rule-parent)) - - ;; 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)))) - - ((member token '(":= module" ":= inductive" ":= def")) - (if (smie-rule-hanging-p) - (save-excursion (coq-find-real-start) - `(column . ,(current-column))) - (save-excursion (coq-find-real-start) - `(column . ,(+ 2 (current-column)))))) - - ((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-lexer) diff --git a/coq/coq-smie.el b/coq/coq-smie.el new file mode 100644 index 00000000..e9dd02fb --- /dev/null +++ b/coq/coq-smie.el @@ -0,0 +1,841 @@ +;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq + +;; Copyright (C) 2014 Free Software Foundation, Inc + +;; Authors: Pierre Courtieu +;; Stefan Monnier +;; Maintainer: Pierre Courtieu +;; License: GPLv3+ (GNU GENERAL PUBLIC LICENSE version 3 or later) + +;;; Commentary: + +;; Lexer. +;; - 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) + +;; 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)))) + + + + +(defun coq-smie-is-tactic () + (save-excursion + (coq-find-real-start) + (let ((cfs case-fold-search)) + (setq case-fold-search nil) + (let ((res (looking-at "[[:upper:]]"))) + (setq case-fold-search cfs) + (not res))))) + + +(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") ". proofstart" ".")) + ((or (looking-at "Next\\s-+Obligation\\>") + (coq-smie-detect-goal-command)) + (save-excursion + (goto-char (+ p 1)) + (if (equal (smie-default-forward-token) "Proof") + "." ". 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" ".")))) + (cond + ((null tok) nil) + ((equal tok ".") nil) + ((equal tok "match") t) + ((equal tok "with") + (coq-smie-find-unclosed-match-backward) + (coq-smie-find-unclosed-match-backward))))) + +(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") "with fixpoint") + ((looking-at "Module\\|Declare") "with module") + (t "with"))))) + + + +;; 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* ((next2 (smie-default-forward-token)) + (is-dot-friend (coq-dot-friend-p next2)) + (next (if is-dot-friend "." next2)) + (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 + (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* ((next2 (smie-default-backward-token)) + (is-dot-friend (coq-dot-friend-p next2)) + (next (if is-dot-friend "." next2)) + (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" next2 next (looking-at ".[[:space:]]")) + (when (or (not (equal next2 ".")) + (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)) (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-+") "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-smie-forward-token () + (let ((tok (smie-default-forward-token))) + (cond + ;; @ 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 + ((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))) + + ;; 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))) + + ((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") + ((coq-dot-friend-p tok) ".") + (tok)))) + + +(defun coq-is-at-command-real-start() + (equal (point) + (save-excursion (coq-find-real-start)))) + + +(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")) ":= inductive") + ((equal corresp "let") ":= let") + ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind + ((or (looking-back "{")) ":= record") + (t ":=")))) ; a parenthesis stopped the search + + +(defun coq-smie-backward-token () + (let ((tok (smie-default-backward-token))) + (cond + ((equal tok ",") + (save-excursion + (let ((backtok (coq-smie-search-token-backward + '("forall" "∀" "∃" "exists" "|" "match" ".")))) + (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))))) + ;; Distinguish between "," from quantification and other uses of + ;; "," (tuples, tactic arguments) + + ((equal tok ";") + (save-excursion + (let ((backtok (coq-smie-search-token-backward '("." "[" "{")))) + (cond + ((equal backtok ".") "; tactic") + ((equal backtok nil) + (if (or (looking-back "\\[") + (and (looking-back "{") + (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call + "; tactic" + "; record")))))) + + ((equal tok "Module") + (save-excursion + ;(coq-find-real-start) + (coq-smie-module-deambiguate))) + + ;; 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) + (member (coq-smie-backward-token) ;; recursive call + '("." ". proofstart" "{ subproof" "} subproof" + "- bullet" "+ bullet" "* bullet")))) + (forward-char -1) + (if (looking-at "{") "{ subproof" "} subproof")) + + ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\)")) + ": ltacconstr") + + ((equal tok ":=") + (save-excursion + (save-excursion (coq-smie-:=-deambiguate)))) + + ((equal tok "=>") + (save-excursion + (let ((corresp (coq-smie-search-token-backward + '("|" "match" "fun" ".") + nil '(("match" . "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 1) ".") + ; for "unfold in *|-*;" + ((member tok '("*;" "-*;" "|-*;" "*|-*;")) (forward-char 1) "; tactic") + ((and (member tok '("+" "-" "*")) + (save-excursion + (let ((prev (coq-smie-backward-token))) ;; recursive call + (member prev '("." ". proofstart" "{ subproof" "} subproof"))))) + (concat tok " bullet")) + + + + ((and (member tok '("exists" "∃")) + (save-excursion + (not (member + (coq-smie-backward-token) ;; recursive call looking at the ptoken immediately before + '("." ". proofstart" "; tactic" "[" "]" "|" "=>" ;; => may be wrong here but rare (h0ave "=> ltac"?) + "{ subproof" "} subproof" "- bullet" "+ bullet" + "* bullet"))))) + "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") ; "with" is a nightmare: at least 4 different uses + "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" "Morphism" "Relation" "." ". proofstart" + "{ subproof" "} subproof" "as") + nil + '((("match" "let") . "with") ("with" . "signature"))))) + (cond + ((equal prev-interesting "match") "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" ;"eval" should be "eval in" but this is not supported by search-token-backward + "." ) nil + '(("match" . "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 (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 looke like this: +Lemma foo: forall n, + n = n. + +instead of + +Lemma foo: forall n, + n = n. +" + :type 'boolean + :group 'coq) + + +;; - 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 "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 " 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 ".") + (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 "else") + (assoc ", quantif") + (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with") + (assoc "|-") (assoc ":" ":<") (assoc ",") (assoc "->") (assoc "<->") + (assoc "&") (assoc "/\\") (assoc "\\/") + (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>") + (assoc "=?") (assoc "<=?") (assoc " 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 + + +; This fixes a bug in smie that is not yet in regular emacs distribs?? +; To show the bug. Comment this and then try to indent the following: +; Module X. +; Module Y. <-- here --> Error: (wrong-type-argument integer-or-marker-p nil) +; No need anymore? +;; (defun smie-indent--parent () +;; (or smie--parent +;; (save-excursion +;; (let* ((pos (point)) +;; (tok (funcall smie-forward-token-function))) +;; (unless (numberp (cadr (assoc tok smie-grammar))) +;; (goto-char pos)) +;; (setq smie--parent +;; (or (smie-backward-sexp 'halfsexp) +;; (let (res) +;; (while (null (setq res (smie-backward-sexp)))) +;; (list nil (point) (nth 2 res))))))))) + +(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")) + ;; 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 (member token '("{ subproof" "- bullet" "+ bullet" "* bullet" + "." ". proofstart")) + (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. + ((member token '(":" ":=" ":= with" ":= def" "- bullet" "+ bullet" "* bullet" + "by" "in tactic" "<:" "<+" ":= record" + "with module" "as" ":= inductive" ":= module" )) + 2) + + ((equal token "with match") 4) + + ((equal token "; tactic") + (cond + ((smie-rule-parent-p "; tactic") (smie-rule-separator kind)) + (t (smie-rule-parent 2)))) + + ; "as" tactical is not idented correctly + ((equal token "in let") (smie-rule-parent)))) + + (:before + (cond + ((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" + "{ 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))) + + + ((and (member token '("forall" "quantif exists")) + (smie-rule-parent-p "forall" "exists quantif")) + (smie-rule-parent)) + + ;; 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)))) + + ((member token '(":= module" ":= inductive" ":= def")) + (if (smie-rule-hanging-p) + (save-excursion (coq-find-real-start) + `(column . ,(current-column))) + (save-excursion (coq-find-real-start) + `(column . ,(+ 2 (current-column)))))) + + ((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 diff --git a/coq/coq.el b/coq/coq.el index d85c20d0..e6c5e56c 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -332,7 +332,7 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3." :group 'coq) (require 'smie nil 'noerror) -(require 'coq-smie-lexer nil 'noerror) +(require 'coq-smie nil 'noerror) ;; diff --git a/coq/ex/indent.v b/coq/ex/indent.v index c574f715..b524d956 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -9,12 +9,19 @@ Record a : Type := make_a { aa : nat }. -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 test : nat -> Prop := + | C1 : forall n, test n + | C2 : forall n, test n + | C3 : forall n, test n + | C4 : forall n, test n. + Inductive test2 : nat -> Prop + := C1 : forall n, test n + | C2 : forall n, test n + | C3 : forall n, test n + | C4 : forall n, test n. +} Lemma toto:nat. Proof. -- cgit v1.2.3