From 31b9b0b06e3a692cc0a7907370919ad6270c303d Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 31 May 2011 15:24:26 +0000 Subject: Added indentation for BeginSubProof/EndSubProof. + added some tactics syntax. --- coq/coq-indent.el | 17 ++++++++++++----- coq/coq-syntax.el | 43 +++++++++++++++++++++++++++++++++++++------ 2 files changed, 49 insertions(+), 11 deletions(-) (limited to 'coq') diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 32e76015..48be8953 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -36,11 +36,14 @@ (concat coq-comment-start-regexp "\\|" coq-comment-end-regexp)) (defconst coq-indent-open-regexp (proof-regexp-alt ;(proof-regexp-alt-list coq-keywords-goal) goal-command-p instead - (proof-ids-to-regexp '("Cases" "match")) + (proof-ids-to-regexp '("Cases" "match" "BeginSubproof")) "\\s(")) (defconst coq-indent-close-regexp - (proof-regexp-alt-list (append coq-keywords-save '("end" "End" "\\s)")))) + (proof-regexp-alt "\\s)" + (proof-ids-to-regexp '("EndSubproof" "end")) + (proof-ids-to-regexp coq-keywords-save))) + (defconst coq-indent-closepar-regexp "\\s)") (defconst coq-indent-closematch-regexp (proof-ids-to-regexp '("end"))) @@ -510,12 +513,16 @@ Returns point if found." (defun coq-goal-count (l) (coq-add-iter l 'coq-indent-goal-command-p)) -(defun coq-save-count (l) (coq-add-iter l '(lambda (x) (coq-save-command-p nil x)))) +(defun coq-save-count (l) + (coq-add-iter l '(lambda (x) (or (coq-save-command-p nil x) + (proof-string-match "\\" x))))) (defun coq-proof-count (l) - (coq-add-iter l '(lambda (x) (proof-string-match "\\" x)))) + (coq-add-iter l '(lambda (x) + (proof-string-match "\\<\\(?:Proof\\|BeginSubproof\\)\\>" x)))) -;; returns the difference between goal and save commands in a commands list +;; returns the difference between goal (and assimilate Proof and BeginSubproof) and +;; save commands in a commands list. This is to (defun coq-goal-save-diff-maybe-proof (l) (let ((proofs (coq-proof-count l)) (goals (coq-goal-count l))) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index f11fed30..f4daaa0f 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -157,6 +157,7 @@ See also `coq-prog-env' to adjust the environment." ("change with" "chw" "change # with" t) ("change" "ch" "change " t "change") ("clear" "cl" "clear" t "clear") + ("clear dependent" "cldep" "clear dependent" t "clear\\s-+dependent") ("clearbody" "cl" "clearbody" t "clearbody") ("cofix" "cof" "cofix" t "cofix") ("coinduction" "coind" "coinduction" t "coinduction") @@ -168,6 +169,9 @@ See also `coq-prog-env' to adjust the environment." ("cut" "cut" "cut" t "cut") ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") ;; ("decide equality" "deg" "decide equality" t "decide\\s-+equality") + ("decide_right" "decr" "decide_right" t "decide\\s-+right") + ("decide_left" "decl" "decide_left" t "decide\\s-+left") + ("decide" nil "decide" t "decide") ("decompose record" "decr" "decompose record #" t "decompose\\s-+record") ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum") ("decompose" "dec" "decompose [#] #" t "decompose") @@ -177,9 +181,12 @@ See also `coq-prog-env' to adjust the environment." ("dependent inversion_clear with" "depinvw" "dependent inversion_clear # with #" t) ("dependent rewrite ->" "depr" "dependent rewrite -> @{id}" t "dependent\\s-+rewrite") ("dependent rewrite <-" "depr<" "dependent rewrite <- @{id}" t) + ("destr_eq" "deseq" "destr_eq " t "destr_eq") ("destruct as" "desa" "destruct # as #" t) ("destruct using" "desu" "destruct # using #" t) ("destruct" "des" "destruct " t "destruct") + ("destruct_with_eqn" "deswe" "destruct_with_eqn " t "destruct_with_eqn") + ("destruct_all" "desall" "destruct_all " t "destruct_all") ;; ("discriminate" "dis" "discriminate" t "discriminate") ("discrR" "discrR" "discrR" t "discrR") ("double induction" "dind" "double induction # #" t "double\\s-+induction") @@ -196,9 +203,11 @@ See also `coq-prog-env' to adjust the environment." ("eright" "erig" "eright" "eright") ("esplit" "esp" "esplit" t "esplit") ;; ("exact" "exa" "exact" t "exact") + ("exfalso" "exf" "exfalso" t "exfalso") ("exists" "ex" "exists #" t "exists") ;; ("fail" "fa" "fail" nil) ;; ("field" "field" "field" t "field") + ("false_hyp" nil "false_hyp @{H} @{G}" t "false_hyp") ("firstorder" "fsto" "firstorder" t "firstorder") ("firstorder with" "fsto" "firstorder with #" t) ("firstorder with using" "fsto" "firstorder # with #" t) @@ -232,6 +241,7 @@ See also `coq-prog-env' to adjust the environment." ("linear" "lin" "linear" t "linear") ("load" "load" "load" t "load") ("move after" "mov" "move # after #" t "move") + ("now_show" nil "now_show" t "now_show") ("omega" "o" "omega" t "omega") ("pattern" "pat" "pattern" t "pattern") ("pattern(s)" "pats" "pattern # , #" t) @@ -246,6 +256,10 @@ See also `coq-prog-env' to adjust the environment." ("rename into" "ren" "rename # into #" t "rename") ("replace with" "rep" "replace # with #" t "replace") ("replace with in" "repi" "replace # with # in #" t) + ("revert dependent" "r" "revert dependent" t "revert\\s-+dependent") + ("revert" "r" "revert" t "revert") + ("rewrite_all" nil "rewrite_all" t "rewrite_all") + ("rewrite_all <-" nil "rewrite_all" t "rewrite_all") ("rewrite <- in" "ri<" "rewrite <- # in #" t) ("rewrite <-" "r<" "rewrite <- #" t) ("rewrite in" "ri" "rewrite # in #" t) @@ -286,6 +300,7 @@ See also `coq-prog-env' to adjust the environment." ("unfold(s)" "us" "unfold # , #" t) ("unfold in" "unfi" "unfold # in #" t) ("unfold at" "unfa" "unfold # at #" t) + ("vm_compute" "vmc" "vm_compute." t "vm_compute") )) "Coq tactics information list. See `coq-syntax-db' for syntax. " ) @@ -295,8 +310,12 @@ See also `coq-prog-env' to adjust the environment." coq-user-solve-tactics-db '( ("assumption" "as" "assumption" t "assumption") + ("eassumption" "eas" "eassumption" t "eassumption") + ("easy" nil "easy" t "easy") + ("now" nil "now" t "now") ("by" "by" "by #" t "by") ("congruence" "cong" "congruence" t "congruence") + ("contradict" "contr" "contradict" t "contradict") ("contradiction" "contr" "contradiction" t "contradiction") ("decide equality" "deg" "decide equality" t "decide\\s-+equality") ("discriminate" "dis" "discriminate" t "discriminate") @@ -463,6 +482,8 @@ See also `coq-prog-env' to adjust the environment." ;; command that are not declarations, definition or goal starters (defvar coq-other-commands-db '( + ("BeginSubproof" "bs" "BeginSubproof.\n#\nEndSubproof." t "BeginSubproof") + ("EndSubproof" "es" "EndSubproof.#" t "EndSubproof") ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu ("About" nil "About #." nil "About") ; ("Add" nil "Add #." nil "Add" nil t) @@ -488,6 +509,7 @@ See also `coq-prog-env' to adjust the environment." ("Local Close Scope" "lclsc" "Local Close Scope #" t "Local\\s-+Close\\s-+Scope") ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") ("Comments" nil "Comments #." nil "Comments") + ("Declare" nil "Declare #." nil "Declare") ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) ("Eval" nil "Eval #." nil "Eval") ("Export" nil "Export #." t "Export") @@ -502,6 +524,7 @@ See also `coq-prog-env' to adjust the environment." ("Extraction" "extr" "Extraction @{id}." nil "Extraction") ("Focus" nil "Focus #." nil "Focus") ("Generalizable Variables" nil "Generalizable Variables #." t "Generalizable\\s-+Variables") + ("Generalizable All Variables" nil "Generalizable All Variables." t "Generalizable\\s-+All\\s-+Variables") ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") @@ -524,7 +547,8 @@ See also `coq-prog-env' to adjust the environment." ("Typeclasses Opaque" nil "Typeclasses Opaque #." nil "Typeclasses\\s-+Opaque") ("Opaque" nil "Opaque #." nil "Opaque") ("Obligation Tactic" nil "Obligation Tactic := #." t "Obligation\\s-+Tactic") - ("Local Open Scope" "lopsc" "Local Open Scope #" t "Local\\s-+Open\\s-+Scope") + ("Local Open Scope" nil "Local Open Scope #" t "Local\\s-+Open\\s-+Scope") + ("Open Local Scope" nil "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) @@ -729,6 +753,7 @@ Used by `coq-goal-command-p'" '("Defined" "Save" "Qed" +; "EndSubproof" ;; care: this must happen before "End" "End" "Admitted" "Abort" @@ -738,6 +763,7 @@ Used by `coq-goal-command-p'" (append coq-keywords-save-strict '("Proof")) ) + (defun coq-save-command-p (span str) "Decide whether argument is a Save command or not" (or (proof-string-match coq-save-command-regexp-strict str) @@ -814,10 +840,12 @@ Used by `coq-goal-command-p'" "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" "return" "struct" "else" "end" "if" "in" "into" "let" "then" "using" "with" "beta" "delta" "iota" "zeta" "after" "until" - "at" "Sort" "Time" "dest")) + "at" "Sort" "Time" "dest" "where")) "Reserved keywords of Coq.") -(defvar coq-reserved-regexp (proof-ids-to-regexp coq-reserved)) +(defvar coq-reserved-regexp + (concat "\\\\|" + (proof-ids-to-regexp coq-reserved) )) (defvar coq-state-changing-tactics (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) @@ -848,7 +876,7 @@ Used by `coq-goal-command-p'" (defun proof-regexp-alt-list-symb (args) (concat "\\_<\\(?:" (proof-regexp-alt-list args) "\\)\\_>")) -(defvar coq-keywords-regexp (proof-regexp-alt-list coq-keywords)) +(defvar coq-keywords-regexp (proof-regexp-alt-list-symb coq-keywords)) (defvar coq-symbols @@ -865,6 +893,9 @@ Used by `coq-goal-command-p'" "}" ":=" "=>" + "==>" + "++>" + "@" "->" ".") "Punctuation Symbols used by Coq.") @@ -912,13 +943,13 @@ Used by `coq-goal-command-p'" ;; recognizing global identifiers, see coq-global-p. (defconst coq-save-command-regexp-strict (proof-anchor-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-regexp-alt-list coq-keywords-save-strict) + (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict) "\\)"))) (defconst coq-save-command-regexp (proof-anchor-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-regexp-alt-list coq-keywords-save) + (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save) "\\)"))) (defconst coq-save-with-hole-regexp -- cgit v1.2.3