diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-smie-lexer.el | 737 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 15 | ||||
| -rw-r--r-- | coq/coq.el | 493 |
3 files changed, 756 insertions, 489 deletions
diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el new file mode 100644 index 00000000..54ca855f --- /dev/null +++ b/coq/coq-smie-lexer.el @@ -0,0 +1,737 @@ +;; 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". + +(setq coq-smie-dot-friends '("*." "-*." "|-*." "*|-*.")) + +; for debuging +(defun coq-time-indent () + (interactive) + (let ((deb (time-to-seconds))) + (smie-indent-line) + (message "time: %S"(- (time-to-seconds) 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-search-token-forward (tokens &optional end ignore-between) + "Search for one of TOKENS between point and END. +Token \".\" is considered only if followed by a space." + (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 (smie-default-forward-token)) + (parop (assoc next ignore-between))) + (if parop ; if we find something to ignore, we directly + (let ((parops ; corresponding matcher may be a list + (if (listp parop) (cdr parop) + (cons (cdr parop) nil)))) ; go to corresponding closer + (coq-smie-search-token-forward parops + end ignore-between)) + ;; Do not consider "." when not followed by a space + (when (or (not (equal next ".")) + (looking-at "[[:space:]]")) + (cond + ((zerop (length next)) (forward-sexp 1)) + ((member next tokens) (throw 'found next)))))))) + (scan-error nil))) + +(defun coq-smie-search-token-backward (tokens &optional end ignore-between) + "Search for one of TOKENS between point and END. +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. " + (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)) + (next (if (member next2 coq-smie-dot-friends) "." next2)) + (parop (rassoc next ignore-between))) + ;(message "praop = %S" parop) + (if parop ; if we find something to ignore, we directly + (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)) ;coq-smie-dot-friends + end ignore-between) + (cons "." nil)) ;coq-smie-dot-friends + (goto-char (point)) + next)) + ;; Do not consider "." when not followed by a space + (when (or (not (equal next ".")) + (looking-at ".[[:space:]]")) + (cond + ((zerop (length next)) (forward-sexp -1)) + ((member next tokens) (throw 'found next)))))))) + (scan-error nil))) + +;; This avoids parenthesized expression containing := and let +;; .. := ... in. We consider any other occurrence of := as an +;; evidence of explicit definition by contrast to goal +;; opening. +(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. +(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\ +\\|Add\\(\\s-+Parametric\\)?\\s-+Morphism\\)\\>") + (coq-lonely-:=-in-this-command) + ))) + +;; Heuristic to detect a goal opening command: there must be a lonely ":=" +(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 (proof-looking-at "\\(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" "∀" "∃" "→" ";" "," ":")) + ;; 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 + + + ;; ((equal tok "Program") + ;; (let ((pos (point)) + ;; (next (smie-default-forward-token))) + ;; (if (member next '("Fixpoint" "Declaration" "Lemma" "Instance")) + ;; next + ;; (goto-char pos) + ;; tok))) + ;; ((member tok '("Definition" "Lemma" "Theorem" "Local" + ;; "Fact" "Let" "Program" + ;; "Class" "Instance")) + ;; (save-excursion (coq-smie-backward-token))) + + ((member tok '("Module")) + (let ((pos (point)) + (next (smie-default-forward-token))) + (unless (equal next "Type") (goto-char pos)) + (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)) (looking-at "{")) + (if (equal (save-excursion (forward-char 1) (coq-smie-backward-token)) + "{ subproof") + (progn (forward-char 1) "{ subproof") + tok)) + ((and (zerop (length tok)) (looking-at "}")) + (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") + ;; ((equal tok "Proof") ;; put point after with if present + ;; (let ((pos (point)) + ;; (next (smie-default-forward-token))) + ;; (if (equal next "with") + ;; "Proof" + ;; (goto-char pos) + ;; tok))) + ;; ((equal tok "Next") + ;; (let ((pos (point)) + ;; (next (smie-default-forward-token))) + ;; (if (equal next "Obligation") + ;; next + ;; (goto-char pos) + ;; tok))) + + + +; +; ((string-match "[[:alpha:]_]+" tok) +; (save-excursion +; (if (equal (coq-smie-backward-token) " upperkw") +; " upperkw" tok))) +; + + (tok)))) + +(defun coq-smie-.-desambiguate () + "Return the token of the command terminator of the current command." + (save-excursion + (let ((p (point)) (beg (coq-find-real-start))) ; moves to real start of command + (cond + ((looking-at "Proof\\>\\|BeginSubproof\\>") ". 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"))) + ((coq-smie-detect-module-or-section-start-command) + ". 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-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 "Type") + ;; (let ((pos (point)) + ;; (prev (smie-default-backward-token))) + ;; (if (equal prev "Module") + ;; prev + ;; (goto-char pos) + ;; tok))) + ((equal tok "Module") + (save-excursion + (coq-find-real-start) + (if (coq-smie-detect-module-or-section-start-command) + "Module start" "Module def"))) + ((and (equal tok "|") (eq (char-before) ?\{)) + (goto-char (1- (point))) "{|") + ;; ;; FIXME: bugs when { } { } happens for some other reason + ;; ;; FIXME: it seems to even loop sometime + ;; ;; ((and (equal tok "") (member (char-before) '(?\{ ?\})) + ;; ;; (save-excursion + ;; ;; (forward-char -1) + ;; ;; (let ((prev (smie-default-backward-token))) + ;; ;; (or (and (equal prev ".") (looking-at "\\.")) + ;; ;; (and (equal prev "") (member (char-before) '(?\{ ?\}))))))) + ;; ;; (forward-char -1) + ;; ;; (if (looking-at "{") "BeginSubproof" "EndSubproof")) + ;; ((and (equal tok "") (looking-back "|}" (- (point) 2))) + ;; (goto-char (match-beginning 0)) "|}") + + ((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 + (let ((corresp (coq-smie-search-token-backward + '("let" "Inductive" "Coinductive" "{|" "." "with") + nil '(("let" . ":=") ("match" . "with"))))) + (cond + ((member corresp '("Inductive" "CoInductive")) ":="); := inductive + ((equal corresp "let") ":= let") + ((equal corresp "with") ":= with") + ((or (looking-back "{")) ":= record") + (t tok))))) + + ((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 + '("." ". proofstart" "; tactic" "[" "]" "|" "{ subproof" "} subproof")))) + "quantif exists")) + ((equal tok "∀") "forall") + ((equal tok "→") "->") + ((and (equal tok "with") + (save-excursion + (equal (coq-smie-search-token-backward '("match" ".")) "match"))) + "with match") + ((and (equal tok "with") + (save-excursion + (equal (coq-smie-search-token-backward '("Module" ".")) "Module"))) + "with module") + + + ((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 "in") + (save-excursion + (let ((prev-interesting + (coq-smie-search-token-backward + '("let" "match" "eval" "." ) nil + '(("match" . "with") (("let" "eval") . "in"))))) + (cond + ((member prev-interesting '("." nil)) "in tactic") + ((equal prev-interesting "let") "in let") + ((equal prev-interesting "eval") "in eval") + ((equal prev-interesting "match") "in match") + (t "in tactic"))))) + + ;; Too slow + ((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. + ;; (if (looking-at "\\.(") ". selector" ;;Record selector. + ;; (if (looking-at "\\.[[:space:]]") ;; command terminator + ;; (coq-smie-.-desambiguate) + ;; (if (looking-at "\\.[[:alpha:]_]") ;; qualified id + ;; (let ((newtok (coq-smie-complete-qualid-backward))) + ;; (concat newtok tok)) + ;; ". selector")))) ;; probably a user defined syntax + + ((member tok '("." "...")) + ;; Distinguish field-selector "." from terminator "." from module + ;; qualifier. + (let ((nxtnxt (char-after (+ (point) (length tok))))) + (if (eq nxtnxt ?\() ". selector" ;(looking-at "\\.(") ". selector" ;;Record selector. + (if (eq (char-syntax nxtnxt) ?\ ) ;; command terminator + (save-excursion (forward-char (- (length tok) 1)) + (coq-smie-.-desambiguate)) + (if (eq (char-syntax nxtnxt) ?w) ;(looking-at "\\.[[:alpha:]_]") ;; qualified id + (let ((newtok (coq-smie-complete-qualid-backward))) + (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))) + + (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) + + +;; FIXME: This does not know about Notations. +(defconst coq-smie-grammar + (when (fboundp 'smie-prec2->grammar) + (smie-prec2->grammar + (smie-bnf->prec2 + '((exp(assoc "|") + (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" assigns "in eval" exp) + ("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 "|-" 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) ) + ;(expssss (exp) (expssss "|" expssss) (exp "=>" expssss)) ; (expssss "as" expssss) + (exps (exp) (exp ":= record" exp) (exps "; record" exps)) + (assigns (exp ":= let" exp)) ;(assigns "; record" assigns) + + (moduledecl (exp) + (exp ":" moduleconstraint)) + (moduleconstraint (exp) + (moduleconstraint "with module" moduleconstraint) + (exp ":= with" exp)) + + ;; 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") + (exp)) + (commands (commands "." commands) + (commands "- bullet" commands) + (commands "+ bullet" commands) + (commands "* bullet" 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 ".") (assoc "Module")) + '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet") (assoc ".")) + '((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") + (assoc "|-") (assoc ":" ":<") (assoc ",") (assoc "->") (assoc "<->") + (assoc "/\\") (assoc "\\/") + (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>") + (assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^") + (assoc "+") (assoc "-") (assoc "*") + (assoc ": ltacconstr") (assoc ". selector") (assoc "")) + '((assoc ":")(assoc "<")) + '((assoc "with module") (assoc ":= with") (nonassoc ":")) + '((assoc "; record"))))) + "Parsing table for Coq. See `smie-grammar'.") +;; FIXME: {|\n xx:=y; ...|} +;; FIXME: +; Record rec:Set := { +; fld1:nat; +; fld2:nat; +; fld3:bool +; }. +; FIXME: +; - Si Next Obligation suivi de Proof: pas d'indentation sur le Next +; Obligation +; FIXME: +; rewrite +; in +; H. +; FIXME: same thing with "as" +; FIXME: +; Instance x +; := <- should right shift +; FIXME: idem: +; Lemma x +; : <- should right shift +; FIXME: +;; Add Parametric Morphism (A : Type) : (mu (A:=A)) +;; with signature Oeq ==> Oeq +;; as mu_eq_morphism. +;; FIXME: +;; match x with +;; C1 => .. +;; | ... + + +; 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) +(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 '("." ". 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. + ((equal token "with match") 4) + ((member token '(":" ":=" ":= with")) +; (if (smie-rule-parent-p "Definition" "Lemma" "Theorem" "Fixpoint" +; "Inductive" "Function" "Let" "Record" +; "Instance" "Class" "Ltac" "Add" "goalcmd") +; (smie-rule-parent 2) 2) + 2) + + ((equal token ":= record") 2) +; ((equal token ". modulestart") 0) +; ((equal token ". proofstart") 0) + ((equal token "with module") 2) + + + ((equal token "- bullet") (smie-rule-parent 2)) + ((equal token "+ bullet") (smie-rule-parent 2)) + ((equal token "* bullet") (smie-rule-parent 2)) + + ((equal token "; tactic") ; "; tactic" maintenant!! + (cond + ((smie-rule-parent-p "; tactic") (smie-rule-separator kind)) + (t (smie-rule-parent 2)))) + + ; "as" tactical is not idented correctly + ((equal token "as") (smie-rule-parent 2)) + ((equal token "in let") (smie-rule-parent)) + + +;; ((equal token "in match") 2) +;; ((equal token "as match") 2) +;; ((equal token "return") 2) +;; ((equal token ":= inductive") 2) +;; ((equal token ",") +;; (cond +;; ;; FIXME: when using utf8 quantifiers, is is better to have 1 instead +;; ;; of 2 here, workaround: write "∀x" instead of "∀ x". +;; ((smie-rule-parent-p "forall" "quantif exists") (smie-rule-parent 2)) +;; (t (smie-rule-parent 2)))) +;; ((equal token "Proof") ;; ("BeginSubproof" "Module" "Section" "Proof") +;; (message "PROOF FOUND") +;; (smie-rule-parent 2)) + )) + + (:before + (cond + ((equal token "with module") + (if (smie-rule-parent-p "with module") + (smie-rule-parent) + (smie-rule-parent 4))) + + ((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)))) + + + +;; ((equal token "as") 2) +;; ((member token '("return" "in match" "as match")) +;; (if (smie-rule-parent-p "match") 3)) + ((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)))) +;; ((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)
\ No newline at end of file diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index fbaaebc4..2030d141 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -323,13 +323,20 @@ (defvar coq-solve-cheat-tactics-db (append coq-user-cheat-tactics-db - '( - ("admit" nil "admit" t "admit") - )) + '(("admit" nil "admit" t "admit") + ("Admitted" nil "Admitted" t "Admitted"))) "Coq tactic(al)s that solve a subgoal." ) - +(setq develock-coq-font-lock-keywords + '((develock-find-long-lines + (1 'develock-long-line-1 t) + (2 'develock-long-line-2 t)) + ("[^ \n ]\\([ ]+\\)$" + (1 'develock-whitespace-1 t)) + ("^[ ]+$" + (0 'develock-whitespace-2 append)) + ("\\.[{}]" 0 'develock-whitespace-2 nil nil))) (defvar coq-tacticals-db @@ -60,7 +60,7 @@ (defcustom coq-prog-name (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin")) - "*Name of program to run as Coq. See `proof-prog-name', set from this. + "*Name of program to run as Coq. See `proof-prog-name', set from this. On Windows with latest Coq package you might need something like: C:/Program Files/Coq/bin/coqtop.opt.exe instead of just \"coqtop\". @@ -157,7 +157,7 @@ On Windows you might need something like: (defun get-coq-library-directory () (let ((c (substring (shell-command-to-string "coqtop -where") 0 -1 ))) (if (string-match c "not found") - "/usr/local/lib/coq" + "/usr/local/lib/coq" c))) (defconst coq-library-directory (get-coq-library-directory) @@ -219,7 +219,7 @@ See also `coq-hide-additional-subgoals'." (defcustom coq-proof-tree-current-goal-regexp (concat "^[0-9]+ subgoal\\(?:s, subgoal 1\\)? " - "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)") + "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)") "Regexp for `proof-tree-current-goal-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -274,8 +274,10 @@ See also `coq-hide-additional-subgoals'." (defvar coq-outline-regexp ;; (concat "(\\*\\|" (concat "[ ]*" (regexp-opt - '( - "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal" "Definition" "Lemm" "Theo" "Fact" "Rema" "Mutu" "Fixp" "Func") t))) + '( + "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal" + "Definition" "Lemm" "Theo" "Fact" "Rema" + "Mutu" "Fixp" "Func") t))) ;;) (defvar coq-outline-heading-end-regexp "\\.[ \t\n]") @@ -332,488 +334,9 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3." :type 'boolean :group 'coq) -(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) - - - - (require 'smie nil 'noerror) +(require 'coq-smie-lexer nil 'noerror) -(defconst coq-smie-grammar - ;; FIXME: This does not know about Notations. - (when (fboundp 'smie-prec2->grammar) - (smie-prec2->grammar - (smie-bnf->prec2 - '((exp ("match" matchexp "with match" expssss "end") - ("let" assigns "in" exp) - ("eval" assigns "in" exp) - ("fun" exp "=>" exp) - ("if" exp "then" exp "else" exp) - ("quantif exists" exp "," exp) - ("forall" exp "," exp) - ("(" exps ")") ("{|" exps "|}") ("{" exps "}") ("[" expssss "]") - (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)) - ;; 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) ) - (assigns (exp ":= let" exp) (assigns "; record" assigns)) - (exps (exp) (exps "," exps)) - (expss (exps) (exps ":= record" exps) (expss ";" expss) - (expss "in tactic" expss) (expss "as" expss)) - (expssss (expss) (expssss "|" expssss) (exp "=>" expss)) - ;; The elements below are trying to capture the syntactic structure - ;; layered above the commands language. Bullets are all the same as a - ;; first approximation. - (subcmds (cmds) - (subcmds "- bullet" subcmds) - (subcmds "+ bullet" subcmds) - (subcmds "* bullet" subcmds) - ("BeginSubproof" subcmds "EndSubproof") ;captures also { and } - ("Proof" subcmds "Proof End") - ("Module" subcmds "End") - ("Section" subcmds "End")) - (cmds ("Add" exp ":=" exp) ; Not sure this exists - ("Add" exp) ; LoadPath etc - ("Lemma" exp ":=" exp) - ("Theorem" exp ":=" exp) - ("Instance" exp ":=" exp) - ("Class" exp ":=" exp) - ("Definition" exp ":=" exp) - ("Let" exp ":=" exp) - ("Function" exp ":=" exp) - ("Scheme" exp ":=" exp) - ("Function" "Scheme" exp ":=" exp) - ("Combine" "Scheme" exp ":=" exp) - ("with" exp ":=" exp) - ("Program Fixpoint" exp ":=" exp) ("Fixpoint" exp ":=" exp) - ("goalcmd" exp) - ("Inductive" exp ":= inductive" expssss) - ("CoInductive" exp ":= inductive" expssss) - ("Notation" exp ":=" exp) - ("Record" exp ":=" exp) - ("Ltac" exp ":=" exp) - (expss) ; tactics - ;; The above elements are far from the only ones terminated by - ;; "." (think of all the tactics). So we won't list them all, - ;; instead we'll use "." as separator rather than terminator. - ;; This has the downside that smie-forward-sexp on a "Definition" - ;; stops right before the "." rather than right after. - (cmds "." cmds))) - ;; Resolve the "trailing expression ambiguity" as in "else x -> b". - ;; each line orders tokens by increasing proprity - '((left ",") (assoc ":") - (assoc "->") (left "<->") (assoc "\\/") (assoc "/\\") - (assoc "<?") (assoc "<=?") (assoc "=?") (assoc ">") (assoc ">=") - (assoc "<") (assoc "<=") (left "<>") (left "=") (left "==") - (nonassoc "else") (nonassoc "in") (left "as") (left "in tactic") - (assoc ":= record") (left "; record") (left "=>") - (left "^") - (assoc "-")(assoc "+") (assoc "*")) - '((left ",")(left "|")(left ";") ; indent rule uses this left - (left "as") (left "in tactic")(left "=>")) - '((left "- bullet") (left "+ bullet") (left "* bullet")) - '((assoc "."))))) - "Parsing table for Coq. See `smie-grammar'.") - - -(defun coq-smie-search-token-forward (tokens &optional end ignore-between) - "Search for one of TOKENS between point and END. -Token \".\" is considered only if followed by a space." - (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 (smie-default-forward-token)) - (parop (assoc next ignore-between))) - (if parop ; if we find something to ignore, we directly - ; go to corresponding closer - (coq-smie-search-token-forward (cons (cdr parop) nil) - end ignore-between) - ;; Do not consider "." when not followed by a space - (when (or (not (equal next ".")) - (looking-at "[[:space:]]")) - (cond - ((zerop (length next)) (forward-sexp 1)) - ((member next tokens) (throw 'found next)))))))) - (scan-error nil))) - -(defun coq-smie-search-token-backward (tokens &optional end ignore-between) - "Search for one of TOKENS between point and END. -Token \".\" is considered only if followed by a space." - (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 (smie-default-backward-token)) - (parop (rassoc next ignore-between))) - (if parop ; if we find something to ignore, we directly - ; go to corresponding closer - (coq-smie-search-token-backward (cons (car parop) nil) - end ignore-between) - ;; Do not consider "." when not followed by a space - (when (or (not (equal next ".")) - (looking-at ".[[:space:]]")) - (cond - ((zerop (length next)) (forward-sexp -1)) - ((member next tokens) (throw 'found next)))))))) - (scan-error nil))) - -;; Heuristic to detect a goal opening command: there must be a lonely ":=" -(defun coq-smie-detect-goal-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 add other commands that potentialy open goals - (when (proof-looking-at "\\(Local\\|Definition\\|Lemma\\|Theorem\\|Fact\\|Add\\|Let\\|Program\\|Class\\|Instance\\)\\>") - (unless ; FIXME: there are probably other "Add xxx" that start goals - (save-excursion - (and (proof-looking-at "Add") - (or (forward-char 3) t) - (not (member (smie-default-forward-token) '("Parametric" "Morphism"))))) - ;; This avoids parenthesized expression containing := and let .. := ... - ;; in. We consider any other occurrence of := as an evidence of explicite - ;; definition by contrast to goal opening. - (equal (coq-smie-search-token-forward '("." ":=") nil '(("let" . "in"))) "."))))) - - -;; 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". - -(defconst coq-smie-proof-end-tokens - ;; '("Qed" "Save" "Defined" "Admitted" "Abort") - (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))) - (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))) - (concat tok "." newtok))))) - ((equal tok ".") - ;; detect what kind of dot this is: record selector, module qualification - ;; or command end - (cond - ((looking-at "(") ".-selector") - ((looking-at "[[:alpha:]]") ;; extend qualifier - (let ((newtok (coq-smie-forward-token))) - (concat tok newtok))) - (t tok))) - ((member tok - '(":=" "+" "-" "*" "with" "exists" "in" "as" "∀" "∃" "→" ";")) - ;; 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))) - ((equal tok "Program") - (let ((pos (point)) - (next (smie-default-forward-token))) - (if (member next '("Fixpoint" "Declaration" "Lemma" "Instance")) - next - (goto-char pos) - tok))) - ((member tok '("Definition" "Lemma" "Theorem" "Local" - "Fact" "Let" "Program" - "Class" "Instance")) - (save-excursion (coq-smie-backward-token))) - - ((member tok '("Module")) - (let ((pos (point)) - (next (smie-default-forward-token))) - (unless (equal next "Type") (goto-char pos)) - (save-excursion - (if (equal (coq-smie-search-token-forward '(":=" ".")) ":=") - "Module def" tok)))) - ((and (equal tok "") (looking-at "{|")) (goto-char (match-end 0)) "{|") - ;; this must be after detecting "{|": - ((and (equal tok "") (looking-at "{") - (save-excursion (forward-char 1) - (coq-smie-backward-token)))) - ((and (equal tok "") (looking-at "}") - (save-excursion (forward-char 1) - (coq-smie-backward-token)))) - ((and (equal tok "|") (eq (char-after) ?\})) - (goto-char (1+ (point))) "|}") - ((member tok coq-smie-proof-end-tokens) "Proof End") - ((member tok '("Obligation")) "Proof") - ((equal tok "Proof") ;; put point after with if present - (let ((pos (point)) - (next (smie-default-forward-token))) - (if (equal next "with") - "Proof" - (goto-char pos) - tok))) - ((equal tok "Next") - (let ((pos (point)) - (next (smie-default-forward-token))) - (if (equal next "Obligation") - next - (goto-char pos) - tok))) - (tok)))) - -(defun coq-smie-backward-token () - (let ((tok (smie-default-backward-token))) - (cond - ((and (looking-at "[[:alpha:]]") (looking-back "@")) - (forward-char -1) - (concat "@" tok)) - ;; extending on the left if this id is a module qualifier - ((and (looking-at "[[:alpha:]]") (looking-back "\\.")) - (forward-char -1) - (let ((newtok (coq-smie-backward-token))) - (concat newtok "." tok))) - ((equal tok ".") - ;; Distinguish field-selector "." from terminator "." from module - ;; qualifier. - (if (looking-at "\\.(") ".-selector" ;;Record selector. - (if (looking-at "\\.[[:space:]]") ;; command terminator - (let ((p (point)) - (prev (coq-smie-search-token-backward - '("." "Proof" "BeginSubproof" "Module" "Section")))) - (cond - ((null prev) (goto-char p) ".") - ((equal prev ".") - ;; This is a bit complex. We replace the "." by "Proof" if the - ;; previous command is detected as a goal starter and there is - ;; no "Proof" and the next command is not a "Proof". This way - ;; we insert missing "Proof" and avoid the major hack signalled - ;; in smie-rules. In particular this speeds up alot indentation - ;; on big files - (goto-char p) - (if (and (save-excursion - (coq-find-real-start) - (coq-smie-detect-goal-command)) - (save-excursion - (forward-char 1) - (not (equal (smie-default-forward-token) "Proof")))) - "Proof" - ".")) - (t prev))) - (if (looking-at "\\.[[:alpha:]]") ;; qualified id - (let ((newtok (coq-smie-backward-token))) - (concat newtok tok)) - ".-selector")))) ;; probably a user defined syntax - ((equal tok ";") - (save-excursion - (let ((backtok (coq-smie-search-token-backward '("." "[" "{")))) - (cond - ((equal backtok ".") tok) - ((equal backtok nil) - (if (looking-back "{") "; record" tok)))))) - - ((equal tok "Type") - (let ((pos (point)) - (prev (smie-default-backward-token))) - (if (equal prev "Module") - prev - (goto-char pos) - tok))) - ((equal tok "Module") - (save-excursion - (if (equal (coq-smie-search-token-forward '(":=" ".")) ":=") - "Module def" tok))) - ((and (equal tok "|") (eq (char-before) ?\{)) - (goto-char (1- (point))) "{|") - ;; FIXME: bugs when { } { } happens for some other reason - ;; FIXME: it seems to even loop sometime - ;; ((and (equal tok "") (member (char-before) '(?\{ ?\})) - ;; (save-excursion - ;; (forward-char -1) - ;; (let ((prev (smie-default-backward-token))) - ;; (or (and (equal prev ".") (looking-at "\\.")) - ;; (and (equal prev "") (member (char-before) '(?\{ ?\}))))))) - ;; (forward-char -1) - ;; (if (looking-at "{") "BeginSubproof" "EndSubproof")) - ((and (equal tok "") (looking-back "|}" (- (point) 2))) - (goto-char (match-beginning 0)) "|}") - ((equal tok ":=") - (save-excursion - (let ((corresp (coq-smie-search-token-backward - '("let" "Inductive" "Coinductive" "{|" ".") - nil '(("let" . ":="))))) - (cond - ((member corresp '("Inductive" "CoInductive")) ":= inductive") - ((equal corresp "let") ":= let") - ((or (looking-back "{")) ":= record") - (t tok))))) - ;; FIXME: no token should end with "." except "." itself - ((member tok '("*." "-*." "|-*." "*|-*.")) (forward-char 1) ".") ; for "unfold in *|-*." etc - ((and (member tok '("+" "-" "*")) - (save-excursion - (let ((prev (coq-smie-backward-token))) - (member prev '("." "BeginSubproof" "EndSubproof"))))) - (concat tok " bullet")) - ((member tok coq-smie-proof-end-tokens) "Proof End") - ((and (member tok '("exists" "∃")) - (save-excursion - (not (member - (coq-smie-backward-token) - '("." ";" "[" "]" "|" "BeginSubproof" "EndSubproof")))) - "quantif exists")) - ((equal tok "∀") "forall") - ((equal tok "→") "->") - ((and (equal tok "with") - (save-excursion - (equal (coq-smie-search-token-backward '("match" ".")) "match"))) - "with match") - ((and (equal tok "with") - (let ((pos (point)) - (next (smie-default-backward-token))) - (if (equal next "Proof") - next - (goto-char pos) - tok)))) - ((equal tok "Obligation") - (let ((pos (point)) - (prev (smie-default-backward-token))) - (unless (equal prev "Next") (goto-char pos)) - "Proof")) - ((equal tok "as") - (save-excursion - (let ((prev-interesting - (coq-smie-search-token-backward - ;; coq-smie-search... do not stop on the "." of qualified.names - '("match" "as" "." )))) - (cond - ((member prev-interesting '("." "as")) "as") - ((equal prev-interesting "match") "as match"))))) - ;; three uses of "in": let, match .. as .. in ... and tactics - ((equal tok "in") - (save-excursion - (let ((prev-interesting - (coq-smie-search-token-backward '("in" "let" "match" "." ) - nil '(("match" . "with"))))) - (cond - ((equal prev-interesting ".") "in tactic") - ((member prev-interesting '("in" "let")) "in") - ((equal prev-interesting "match") "in match"))))) -; ((member tok '("Fixpoint" "Declaration" "Lemma" "Instance")) -; (let ((pos (point)) -; (prev (smie-default-backward-token))) -; (unless (equal prev "Program") (goto-char pos)) -; tok)) - ((coq-smie-detect-goal-command) "goalcmd") - (tok)))) - -(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 (equal token ".") - (forward-char 1) ; skip de "." - (equal (coq-smie-forward-token) "BeginSubproof")))) - (:after - (cond - ;; Override the default indent step added because of their presence - ;; in smie-closer-alist. - ((equal token "with match") 4) - ((equal token ":") - (if (smie-rule-parent-p "Definition" "Lemma" "Theorem" "Fixpoint" - "Inductive" "Function" "Let" "Record" - "Instance" "Class" "Ltac" "Add" "goalcmd") - (smie-rule-parent 2) 2)) - ((equal token ":= record") 2) - ((equal token "in match") 2) - ((equal token "as match") 2) - ((equal token "return") 2) - ((equal token "as") 2) - ((equal token ";") - (cond - ((smie-rule-parent-p ";") (smie-rule-separator kind)) - (t (smie-rule-parent 2)))) - ((equal token ":= inductive") 2) - ((equal token ",") - (cond - ;; FIXME: when using utf8 quantifiers, is is better to have 1 instead - ;; of 2 here, workaround: write "∀x" instead of "∀ x". - ((smie-rule-parent-p "forall" "quantif exists") (smie-rule-parent 2)) - (t (smie-rule-parent 2)))) - ((equal token "Proof") ;; ("BeginSubproof" "Module" "Section" "Proof") - (message "PROOF FOUND") - (smie-rule-parent 2)))) - (:before - (cond - ((equal token "- bullet") 2) - ((equal token "+ bullet") 2) - ((equal token "* bullet") 2) - ((equal token "as") 2) - ((member token '("return" "in match" "as match")) - (if (smie-rule-parent-p "match") 3)) - ((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)))) - ((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)) - ;; CHECK: pc: Stefan, I don't understand this rule and replaced it by - ;; the next one to follow the coq usual indentation: - ;((and (equal token "forall" "exists") (smie-rule-prev-p ":") - ; (smie-rule-parent-p "Lemma")) - ; (smie-rule-parent)) - ((and (member token '("forall" "quantif exists")) - (smie-rule-parent-p "forall" "exists quantif")) - (smie-rule-parent)))))) ;; ;; Auxiliary code for Coq modes |