diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 13:13:58 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 13:13:58 +0000 |
commit | 636a83078ec5271a07ba78fd5d02ce5e9f1f4a86 (patch) | |
tree | aa1e8021d55c2711f0d067949ff0360d2901f976 /coq | |
parent | d35efd03218733c5b45ca064fcd889af6fd61676 (diff) |
Fix compilation problems and rearrange startup settings for coq-prog-name,coq-prog-args
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq-abbrev.el | 20 | ||||
-rw-r--r-- | coq/coq-autotest.el | 1 | ||||
-rw-r--r-- | coq/coq-db.el | 10 | ||||
-rw-r--r-- | coq/coq-syntax.el | 1963 | ||||
-rw-r--r-- | coq/coq.el | 65 |
5 files changed, 1032 insertions, 1027 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 31ee58d6..c91911fb 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -54,16 +54,16 @@ ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete -(unless (noninteractive) - (if (and (boundp 'coq-mode-abbrev-table) - (not (equal coq-mode-abbrev-table (make-abbrev-table)))) - (message "Coq abbrevs already exists, default not loaded") - (message "Coq default abbrevs loaded") - (define-abbrev-table 'coq-mode-abbrev-table - (append coq-tactics-abbrev-table coq-tacticals-abbrev-table - coq-commands-abbrev-table coq-terms-abbrev-table)) - ;; if we use default coq abbrev, never ask to save it - (setq save-abbrevs nil))) +;; (unless (noninteractive) +;; (if (and (boundp 'coq-mode-abbrev-table) +;; (not (equal coq-mode-abbrev-table (make-abbrev-table)))) +;; (message "Coq abbrevs already exists, default not loaded") +;; (message "Coq default abbrevs loaded") +;; (define-abbrev-table 'coq-mode-abbrev-table +;; (append coq-tactics-abbrev-table coq-tacticals-abbrev-table +;; coq-commands-abbrev-table coq-terms-abbrev-table)) +;; ;; if we use default coq abbrev, never ask to save it +;; (setq save-abbrevs nil))) ;;;;; diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 160efdcb..a5b35ba4 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -17,4 +17,3 @@ (pg-autotest-quit-prover) (pg-autotest-finished)) - diff --git a/coq/coq-db.el b/coq/coq-db.el index 5d9e0d65..95b32bd9 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -2,7 +2,7 @@ ;; ;; Author: Pierre Courtieu <courtieu@lri.fr> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) - +;; ;;; We store all information on keywords (tactics or command) in big ;; tables (ex: `coq-tactics-db') From there we get: menus including @@ -15,6 +15,10 @@ ;; ;;; Code: + +;(require 'proof-config) ; for proof-face-specs, a macro + + (defconst coq-syntax-db nil "Documentation-only variable, for coq keyword databases. Each element of a keyword database contains the definition of a \"form\", of the @@ -211,8 +215,8 @@ See `coq-syntax-db' for DB structure." (defface coq-solve-tactics-face (proof-face-specs (:foreground "red" t) ; pour les fonds clairs - (:forground "red" t) ; pour les fond foncés - t) ; pour le noir et blanc + (:foreground "red" t) ; pour les fond foncés + ()) ; pour le noir et blanc "Face for names of closing tactics in proof scripts." :group 'proof-faces) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 87f587a1..ca8c36ee 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -10,1020 +10,1023 @@ (require 'coq-db) (defcustom coq-prog-name ;; da: moved from coq.el since needed here - "coqtop" -;; On Windows with latest Coq package you might need something like: -;; "C:/Program Files/Coq/bin/coqtop.opt.exe" -;; instead of just "coqtop". See also coq-prog-env below. - "*Name of program to run as Coq. Important: See `proof-prog-name'." - :type 'string - :group 'coq) - -;; Pierre: we will have both versions V8.0 and V8.1 during a while the -;; test with "coqtop -v" can be skipped if one of the variables -;; coq-version-is-V8-0/1 is already set (useful for people dealing -;; with several version of coq). - -;; DA: please ensure this file compiles! top-level forms need to be delayed -;; during compile explicitly so they are evaluated during load. - -; this one is temporary, for compatibility -(defvar coq-version-is-V8 nil "Obsolete, use `coq-version-is-V8-0' instead.") - -(defvar coq-version-is-V8-0 nil -"This variable can be set to t to force ProofGeneral to coq version -coq-8.0. To do that, put (setq coq-version-is-V8-0 t) in your .emacs and -restart emacs. This variable cannot be true simultaneously with -coq-version-is-V8-1. If none of these 2 variables is set to t, then -ProofGeneral guesses the version of coq by doing 'coqtop -v'." ) - -(defvar coq-version-is-V8-1 nil - "This variable can be set to t to force ProofGeneral to coq version -coq-8.1 and above(use it for coq-8.0cvs after january 2005). To do -that, put \(setq coq-version-is-V8-1 t) in your .emacs and restart -emacs. This variable cannot be true simultaneously with -coq-version-is-V8-0. If none of these 2 variables is set to t, then -ProofGeneral guesses the version of coq by doing 'coqtop -v'." ) - - -(defun coq-determine-version () - "Intuit the version of Coq we're using and configure accordingly." - ;; post-cond: one of the variables is set to t - (let* - ( - (seedoc (concat " (to force another version, see for example" - " C-h v `coq-version-is-V8-0)'.")) - (v80 (concat "proofgeneral is in coq 8.0 mode" seedoc)) - (v81 (concat "proofgeneral is in coq 8.1 mode" seedoc)) - (err (concat "Both config variables coq-version-is-V8-1 and" - " coq-version-is-V8-0 are set to true. This is" - "contradictory."))) - (cond - ((and coq-version-is-V8-1 coq-version-is-V8-0) (error err)) - (coq-version-is-V8-1 (message v81)) - (coq-version-is-V8-0 (message v80)) - (coq-version-is-V8 (setq coq-version-is-V8-0 nil coq-version-is-V8-1 t) - (message v80)) - (t;; otherwise do coqtop -v and see which version we have - (let* ((str (shell-command-to-string (concat "cd ~; " coq-prog-name " -v"))) - ;; this match sets match-string below - (ver (string-match "version v?\\([.0-9]*\\)" str))) - (message str) - (let ((num (and ver (match-string 1 str)))) - (cond - ((and num (string-match "\\<8.0" num)) - (message v80) - (setq coq-version-is-V8-0 t)) - ((and num (string-match "\\<8.1" num)) - (message v81) - (setq coq-version-is-V8-1 t)) - ((and num (string-match "\\<8.2" num)) - (message (concat "coq version is 8.2: " v81)) - (setq coq-version-is-V8-1 t)) - (t ; 8.1 by default now - (message (concat "Falling back to default: " v81)) - (setq coq-version-is-V8-1 t))))))))) - -(eval-when (load) - (coq-determine-version)) - - -;;; keyword databases + "coqtop" + "*Name of program to run as Coq. See `proof-prog-name', which is 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\". + This must be a single program name with no arguments; see `coq-prog-args' + to manually adjust the arguments to the Coq process. + See also `coq-prog-env' to adjust the environment." + :type 'string + :group 'coq) + + ;; Pierre: we will have both versions V8.0 and V8.1 during a while the + ;; test with "coqtop -v" can be skipped if one of the variables + ;; coq-version-is-V8-0/1 is already set (useful for people dealing + ;; with several version of coq). + + ;; DA: please ensure this file compiles! top-level forms need to be delayed + ;; during compile explicitly so they are evaluated during load. + + ; this one is temporary, for compatibility + (defvar coq-version-is-V8 nil "Obsolete, use `coq-version-is-V8-0' instead.") + + (defvar coq-version-is-V8-0 nil + "This variable can be set to t to force ProofGeneral to coq version + coq-8.0. To do that, put (setq coq-version-is-V8-0 t) in your .emacs and + restart emacs. This variable cannot be true simultaneously with + coq-version-is-V8-1. If none of these 2 variables is set to t, then + ProofGeneral guesses the version of coq by doing 'coqtop -v'." ) + + (defvar coq-version-is-V8-1 nil + "This variable can be set to t to force ProofGeneral to coq version + coq-8.1 and above(use it for coq-8.0cvs after january 2005). To do + that, put \(setq coq-version-is-V8-1 t) in your .emacs and restart + emacs. This variable cannot be true simultaneously with + coq-version-is-V8-0. If none of these 2 variables is set to t, then + ProofGeneral guesses the version of coq by doing 'coqtop -v'." ) + + + (defun coq-determine-version () + "Intuit the version of Coq we're using and configure accordingly." + ;; post-cond: one of the variables is set to t + (let* + ( + (seedoc (concat " (to force another version, see for example" + " C-h v `coq-version-is-V8-0)'.")) + (v80 (concat "proofgeneral is in coq 8.0 mode" seedoc)) + (v81 (concat "proofgeneral is in coq 8.1 mode" seedoc)) + (err (concat "Both config variables coq-version-is-V8-1 and" + " coq-version-is-V8-0 are set to true. This is" + "contradictory."))) + (cond + ((and coq-version-is-V8-1 coq-version-is-V8-0) (error err)) + (coq-version-is-V8-1 (message v81)) + (coq-version-is-V8-0 (message v80)) + (coq-version-is-V8 (setq coq-version-is-V8-0 nil coq-version-is-V8-1 t) + (message v80)) + (t;; otherwise do coqtop -v and see which version we have + (let* ((str (shell-command-to-string (concat "cd ~; " coq-prog-name " -v"))) + ;; this match sets match-string below + (ver (string-match "version v?\\([.0-9]*\\)" str))) + (message str) + (let ((num (and ver (match-string 1 str)))) + (cond + ((and num (string-match "\\<8.0" num)) + (message v80) + (setq coq-version-is-V8-0 t)) + ((and num (string-match "\\<8.1" num)) + (message v81) + (setq coq-version-is-V8-1 t)) + ((and num (string-match "\\<8.2" num)) + (message (concat "coq version is 8.2: " v81)) + (setq coq-version-is-V8-1 t)) + (t ; 8.1 by default now + (message (concat "Falling back to default: " v81)) + (setq coq-version-is-V8-1 t))))))))) + + (unless (noninteractive) + (coq-determine-version)) + + + ;;; keyword databases + + + (defcustom coq-user-tactics-db nil + "User defined tactic information. See `coq-syntax-db' for + syntax. It is not necessary to add your own tactics here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your tactics will be colorized by font-lock + + 2 your tactics will be added to the menu and to completion when + calling \\[coq-insert-tactic] + + 3 you may define an abbreviation for your tactic." + + :type '(repeat sexp) + :group 'coq) + + + (defcustom coq-user-commands-db nil + "User defined command information. See `coq-syntax-db' for + syntax. It is not necessary to add your own commands here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your commands will be colorized by font-lock + + 2 your commands will be added to the menu and to completion when + calling \\[coq-insert-command] + + 3 you may define an abbreviation for your command." + + :type '(repeat sexp) + :group 'coq) + + (defcustom coq-user-tacticals-db nil + "User defined tactical information. See `coq-syntax-db' for + syntax. It is not necessary to add your own commands here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your commands will be colorized by font-lock + + 2 your commands will be added to the menu and to completion when + calling \\[coq-insert-command] + + 3 you may define an abbreviation for your command." + + :type '(repeat sexp) + :group 'coq) + + (defcustom coq-user-solve-tactics-db nil + "User defined closing tactics. See `coq-syntax-db' for + syntax. It is not necessary to add your own commands here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your commands will be colorized by font-lock + + 2 your commands will be added to the menu and to completion when + calling \\[coq-insert-command] + + 3 you may define an abbreviation for your command." + + :type '(repeat sexp) + :group 'coq) + + + + (defcustom coq-user-reserved-db nil + "User defined reserved keywords information. See `coq-syntax-db' for + syntax. It is not necessary to add your own commands here (it is not + needed by the synchronizing/backtracking system). You may however do + so for the following reasons: + + 1 your commands will be colorized by font-lock + + 2 your commands will be added to the menu and to completion when + calling \\[coq-insert-command] + + 3 you may define an abbreviation for your command." + + :type '(repeat sexp) + :group 'coq) + + + + (defvar coq-tactics-db + (append + coq-user-tactics-db + '( + ("absurd " "abs" "absurd " t "absurd") + ("apply" "ap" "apply " t "apply") + ("assert by" "assb" "assert ( # : # ) by #" t "assert") + ("assert" "ass" "assert ( # : # )" t) + ;; ("assumption" "as" "assumption" t "assumption") + ("auto with arith" "awa" "auto with arith" t) + ("auto with" "aw" "auto with @{db}" t) + ("auto" "a" "auto" t "auto") + ("autorewrite with in using" "arwiu" "autorewrite with @{db,db...} in @{hyp} using @{tac}" t) + ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t) + ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t) + ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite") + ("case" "c" "case " t "case") + ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv") + ("change in" "chi" "change # in #" t) + ("change with in" "chwi" "change # with # in #" t) + ("change with" "chw" "change # with" t) + ("change" "ch" "change " t "change") + ("clear" "cl" "clear" t "clear") + ("clearbody" "cl" "clearbody" t "clearbody") + ("cofix" "cof" "cofix" t "cofix") + ("coinduction" "coind" "coinduction" t "coinduction") + ("compare" "cmpa" "compare # #" t "compare") + ("compute" "cmpu" "compute" t "compute") + ;; ("congruence" "cong" "congruence" t "congruence") + ("constructor" "cons" "constructor" t "constructor") + ;; ("contradiction" "contr" "contradiction" t "contradiction") + ("cut" "cut" "cut" t "cut") + ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") + ;; ("decide equality" "deg" "decide equality" t "decide\\s-+equality") + ("decompose record" "decr" "decompose record #" t "decompose\\s-+record") + ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum") + ("decompose" "dec" "decompose [#] #" t "decompose") + ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion") + ("dependent inversion with" "depinvw" "dependent inversion # with #" t) + ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear") + ("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) + ("destruct as" "desa" "destruct # as #" t) + ("destruct using" "desu" "destruct # using #" t) + ("destruct" "des" "destruct " t "destruct") + ;; ("discriminate" "dis" "discriminate" t "discriminate") + ("discrR" "discrR" "discrR" t "discrR") + ("double induction" "dind" "double induction # #" t "double\\s-+induction") + ("eapply" "eap" "eapply #" t "eapply") + ("eauto with arith" "eawa" "eauto with arith" t) + ("eauto with" "eaw" "eauto with @{db}" t) + ("eauto" "ea" "eauto" t "eauto") + ("econstructor" "econs" "econstructor" t "econstructor") + ("eexists" "eex" "eexists" t "eexists") + ("eleft" "eleft" "eleft" t "eleft") + ("elim using" "elu" "elim # using #" t) + ("elim" "e" "elim #" t "elim") + ("elimtype" "elt" "elimtype" "elimtype") + ("eright" "erig" "eright" "eright") + ("esplit" "esp" "esplit" t "esplit") + ;; ("exact" "exa" "exact" t "exact") + ("exists" "ex" "exists #" t "exists") + ;; ("fail" "fa" "fail" nil) + ;; ("field" "field" "field" t "field") + ("firstorder" "fsto" "firstorder" t "firstorder") + ("firstorder with" "fsto" "firstorder with #" t) + ("firstorder with using" "fsto" "firstorder # with #" t) + ("fold" "fold" "fold #" t "fold") + ;; ("fourier" "four" "fourier" t "fourier") + ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction") + ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent") + ("generalize" "g" "generalize #" t "generalize") + ("hnf" "hnf" "hnf" t "hnf") + ("idtac" "id" "idtac" nil "idtac") ; also in tacticals with abbrev id + ("idtac \"" "id\"" "idtac \"#\"") ; also in tacticals + ("induction" "ind" "induction #" t "induction") + ("induction using" "indu" "induction # using #" t) + ("injection" "inj" "injection #" t "injection") + ("instantiate" "inst" "instantiate" t "instantiate") + ("intro" "i" "intro" t "intro") + ("intro after" "ia" "intro # after #" t) + ("intros" "is" "intros #" t "intros") + ("intros! (guess names)" nil "intros #" nil nil coq-insert-intros) + ("intros until" "isu" "intros until #" t) + ("intuition" "intu" "intuition #" t "intuition") + ("inversion" "inv" "inversion #" t "inversion") + ("inversion in" "invi" "inversion # in #" t) + ("inversion using" "invu" "inversion # using #" t) + ("inversion using in" "invui" "inversion # using # in #" t) + ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") + ("lapply" "lap" "lapply" t "lapply") + ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy") + ("left" "left" "left" t "left") + ("linear" "lin" "linear" t "linear") + ("load" "load" "load" t "load") + ("move after" "mov" "move # after #" t "move") + ("omega" "o" "omega" t "omega") + ("pattern" "pat" "pattern" t "pattern") + ("pattern(s)" "pats" "pattern # , #" t) + ("pattern at" "pata" "pattern # at #" t) + ("pose" "po" "pose ( # := # )" t "pose") + ("prolog" "prol" "prolog" t "prolog") + ("quote" "quote" "quote" t "quote") + ("quote []" "quote2" "quote # [#]" t) + ("red" "red" "red" t "red") + ("refine" "ref" "refine" t "refine") + ;; ("reflexivity" "refl" "reflexivity #" t "reflexivity") + ("rename into" "ren" "rename # into #" t "rename") + ("replace with" "rep" "replace # with #" t "replace") + ("replace with in" "repi" "replace # with # in #" t) + ("rewrite <- in" "ri<" "rewrite <- # in #" t) + ("rewrite <-" "r<" "rewrite <- #" t) + ("rewrite in" "ri" "rewrite # in #" t) + ("rewrite" "r" "rewrite #" t "rewrite") + ("right" "rig" "right" t "right") + ;; ("ring" "ring" "ring #" t "ring") + ("set in * |-" "seth" "set ( # := #) in * |-" t) + ("set in *" "set*" "set ( # := #) in *" t) + ("set in |- *" "setg" "set ( # := #) in |- *" t) + ("set in" "seti" "set ( # := #) in #" t) + ("set" "set" "set ( # := #)" t "set") + ("setoid_replace with" "strep2" "setoid_replace # with #" t "setoid_replace") + ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace") + ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") + ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") + ("simpl" "s" "simpl" t "simpl") + ("simpl" "sa" "simpl # at #" t) + ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") + ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion") + ("simple induction" "sind" "simple induction" t "simple\\s-+induction") + ("simplify_eq" "simeq" "simplify_eq @{hyp}" t "simplify_eq") + ("specialize" "spec" "specialize" t "specialize") + ("split" "sp" "split" t "split") + ("split_Rabs" "spra" "splitRabs" t "split_Rabs") + ("split_Rmult" "sprm" "splitRmult" t "split_Rmult") + ("stepl" "stl" "stepl #" t "stepl") + ("stepl by" "stlb" "stepl # by #" t) + ("stepr" "str" "stepr #" t "stepr") + ("stepr by" "strb" "stepr # by #" t) + ("subst" "su" "subst #" t "subst") + ("symmetry" "sy" "symmetry" t "symmetry") + ("symmetry in" "syi" "symmetry in #" t) + ;; ("tauto" "ta" "tauto" t "tauto") + ("transitivity" "trans" "transitivity #" t "transitivity") + ("trivial" "t" "trivial" t "trivial") + ("trivial with" "tw" "trivial with @{db}" t) + ("unfold" "u" "unfold #" t "unfold") + ("unfold(s)" "us" "unfold # , #" t) + ("unfold in" "unfi" "unfold # in #" t) + ("unfold at" "unfa" "unfold # at #" t) + )) + "Coq tactics information list. See `coq-syntax-db' for syntax. " + ) + (defvar coq-solve-tactics-db + (append + coq-user-solve-tactics-db + '( + ("assumption" "as" "assumption" t "assumption") + ("by" "by" "by #" t "by") + ("congruence" "cong" "congruence" t "congruence") + ("contradiction" "contr" "contradiction" t "contradiction") + ("decide equality" "deg" "decide equality" t "decide\\s-+equality") + ("discriminate" "dis" "discriminate" t "discriminate") + ("exact" "exa" "exact" t "exact") + ("fourier" "four" "fourier" t "fourier") + ("fail" "fa" "fail" nil) + ("field" "field" "field" t "field") + ("omega" "o" "omega" t "omega") + ("reflexivity" "refl" "reflexivity #" t "reflexivity") + ("ring" "ring" "ring #" t "ring") + ("tauto" "ta" "tauto" t "tauto") + )) + "Coq tactic(al)s that solve a subgoal." + ) -(defcustom coq-user-tactics-db nil - "User defined tactic information. See `coq-syntax-db' for -syntax. It is not necessary to add your own tactics here (it is not -needed by the synchronizing/backtracking system). You may however do -so for the following reasons: - 1 your tactics will be colorized by font-lock + (defvar coq-tacticals-db + (append + coq-user-tacticals-db + '( + ("info" nil "info #" nil "info") + ("solve" nil "solve [ # | # ]" nil "solve") + ("first" nil "first [ # | # ]" nil "first") + ("abstract" nil "abstract @{tac} using @{name}." nil "abstract") + ("do" nil "do @{num} @{tac}" nil "do") + ("idtac" nil "idtac") ; also in tactics + ; ("idtac \"" nil "idtac \"#\"") ; also in tactics + ("fail" "fa" "fail" nil "fail") + ; ("fail \"" "fa\"" "fail" nil) ; + ; ("orelse" nil "orelse #" t "orelse") + ("repeat" nil "repeat #" nil "repeat") + ("try" nil "try #" nil "try") + ("progress" nil "progress #" nil "progress") + ("|" nil "[ # | # ]" nil) + ("||" nil "# || #" nil) + )) + "Coq tacticals information list. See `coq-syntax-db' for syntax.") + + + + + (defvar coq-decl-db + '( + ("Axiom" "ax" "Axiom # : #" t "Axiom") + ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") + ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern") + ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate") + ("Hint Resolve" "hr" "Hint Resolve # : @{db}." t "Hint\\s-+Resolve") + ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite") + ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t ) + ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold") + ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") + ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses") + ("Parameter" "par" "Parameter #: #" t "Parameter") + ("Parameters" "par" "Parameter #: #" t "Parameters") + ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") + ("Variable" "v" "Variable #: #." t "Variable") + ("Variables" "vs" "Variables # , #: #." t "Variables") + ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") + ) + "Coq declaration keywords information list. See `coq-syntax-db' for syntax." + ) - 2 your tactics will be added to the menu and to completion when - calling \\[coq-insert-tactic] + (defvar coq-defn-db + '( + ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint") + ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") + ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module") + ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful + ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t) + ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful + ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t) + ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful + ("Definition" "def" "Definition #:# := #." t "Definition");; careful + ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t) + ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t) + ("Definition (4 args)" "def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) + ("Program Definition" "pdef" "Program Definition #:# := #." t "Program\\s-+Definition");; careful ? + ("Program Definition (2 args)" "pdef2" "Program Definition # (# : #) (# : #):# := #." t) + ("Program Definition (3 args)" "pdef3" "Program Definition # (# : #) (# : #) (# : #):# := #." t) + ("Program Definition (4 args)" "pdef4" "Program Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) + ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t "Derive\\s-+Inversion") + ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # Sort #." t "Derive\\s-+Dependent\\s-+Inversion") + ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort #." t) + ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Fixpoint") + ("Program Fixpoint" "pfix" "Program Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Program\\s-+Fixpoint") + ("Program Fixpoint measure" "pfixm" "Program Fixpoint # (#:#) {measure @{arg} @{f}} : # :=\n#." t) + ("Program Fixpoint wf" "pfixwf" "Program Fixpoint # (#:#) {wf @{arg} @{f}} : # :=\n#." t) + ("Function" "func" "Function # (#:#) {struct @{arg}} : # :=\n#." t "Function") + ("Function measure" "funcm" "Function # (#:#) {measure @{f} @{arg}} : # :=\n#." t) + ("Function wf" "func wf" "Function # (#:#) {wf @{R} @{arg}} : # :=\n#." t) + ("Functional Scheme with" "fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." t ) + ("Functional Scheme" "fs" "Functional Scheme @{name} := Induction for @{fun}." t "Functional\\s-+Scheme") + ("Inductive" "indv" "Inductive # : # := # : #." t "Inductive") + ("Inductive (2 args)" "indv2" "Inductive # : # :=\n| # : #\n| # : #." t ) + ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) + ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) + ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) + ("Let" "Let" "Let # : # := #." t "Let") + ("Ltac" "ltac" "Ltac # := #" t "Ltac") + ("Module :=" "mo" "Module # : # := #." t ) ; careful + ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful + ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful + ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful + ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful + ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful + ("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record") + ("Scheme" "sc" "Scheme @{name} := #." t "Scheme") + ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) + ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) + ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") + ) + "Coq definition keywords information list. See `coq-syntax-db' for syntax. " + ) - 3 you may define an abbreviation for your tactic." + ;; modules and section are indented like goal starters + (defvar coq-goal-starters-db + '( + ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") + ("Chapter" "chp" "Chapter # : #." t "Chapter") + ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") + ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) + ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) + ("Definition" "def" "Definition #:# := #." t "Definition");; careful + ("Fact" "fct" "Fact # : #." t "Fact") + ("Goal" nil "Goal #." t "Goal") + ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") + ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") + ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) + ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful + ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful + ("Module <:" "moi2" "Module # <: #.\n#\nEnd #." t ) ; careful + ("Remark" "rk" "Remark # : #.\n#\nQed." t "Remark") + ("Section" "sec" "Section #." t "Section") + ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem") + ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem") + ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation") + ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") + ) + "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " + ) - :type '(repeat sexp) - :group 'coq) + (defvar coq-commands-db + (append + coq-user-commands-db + '( + ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu + ("About" nil "About #." nil "About") + ("Add" nil "Add #." nil "Add" nil t) + ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") + ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") + ("Add Field" nil "Add Field #." t "Add\\s-+Field") + ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") + ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") + ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") + ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") + ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") + ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") + ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") + ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") + ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") + ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") + ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") + ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") + ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") + ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") + ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") + ("Cd" nil "Cd #." nil "Cd") + ("Check" nil "Check" nil "Check") + ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope") + ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") + ("Comments" nil "Comments #." nil "Comments") + ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) + ("Eval" nil "Eval #." nil "Eval") + ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") + ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") + ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") + ("Extraction" "extr" "Extraction @{id}." nil "Extraction") + ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) + ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") + ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") + ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") + ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") + ("Focus" nil "Focus #." nil "Focus") + ("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") + ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") + ("Import" nil "Import #." t "Import") + ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") + ("Inspect" nil "Inspect #." nil "Inspect") + ("Locate" nil "Locate" nil "Locate") + ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") + ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") + ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) + ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) + ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) + ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) + ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) + ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t) + ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local") + ("Notation (simple)" "nots" "Notation # := #." t "Notation") + ("Opaque" nil "Opaque #." nil "Opaque") + ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic") + ("Open Local Scope" "oplsc" "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) + ("Print" "p" "Print #." nil "Print") + ("Qed" nil "Qed." nil "Qed") + ("Pwd" nil "Pwd." nil "Pwd") + ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") + ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") + ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") + ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") + ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") + ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") + ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") + ("Require Export" nil "Require Export #." t "Require\\s-+Export") + ("Require Import" nil "Require Import #." t "Require\\s-+Import") + ("Require" nil "Require #." t "Require") + ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") + ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") + ("Save" nil "Save." t "Save") + ("Search" nil "Search #" nil "Search") + ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") + ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") + ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") + ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") + ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") + ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") + ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit") + ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") + ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") + ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") + ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") + ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") + ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") + ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") + ("Show" nil "Show #." nil "Show") + ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations") + ("Test" nil "Test" nil "Test" nil t) + ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") + ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") + ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") + ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") + ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") + ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") + ("Transparent" nil "Transparent #." nil "Transparent") + ("Unfocus" nil "Unfocus." nil "Unfocus") + ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline") + ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize") + ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments") + ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit") + ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth") + ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard") + ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit") + ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All") + ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion") + ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") + ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") + ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") + ; ("print" "pr" "print #" "print") + ) + coq-decl-db coq-defn-db coq-goal-starters-db) + "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " + ) + (defvar coq-terms-db + '( + ("fun (1 args)" "f" "fun #:# => #" nil "fun") + ("fun (2 args)" "f2" "fun (#:#) (#:#) => #") + ("fun (3 args)" "f3" "fun (#:#) (#:#) (#:#) => #") + ("fun (4 args)" "f4" "fun (#:#) (#:#) (#:#) (#:#) => #") + ("forall" "fo" "forall #:#,#" nil "forall") + ("forall (2 args)" "fo2" "forall (#:#) (#:#), #") + ("forall (3 args)" "fo3" "forall (#:#) (#:#) (#:#), #") + ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #") + ("if" "if" "if # then # else #" nil "if") + ("let in" "li" "let # := # in #" nil "let") + ("match! (from type)" nil "" nil "match" coq-insert-match) + ("match with" "m" "match # with\n| # => #\nend") + ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend") + ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend") + ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") + ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") + ) + "Coq terms keywords information list. See `coq-syntax-db' for syntax. " + ) -(defcustom coq-user-commands-db nil - "User defined command information. See `coq-syntax-db' for -syntax. It is not necessary to add your own commands here (it is not -needed by the synchronizing/backtracking system). You may however do -so for the following reasons: - 1 your commands will be colorized by font-lock - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - 3 you may define an abbreviation for your command." - :type '(repeat sexp) - :group 'coq) -(defcustom coq-user-tacticals-db nil - "User defined tactical information. See `coq-syntax-db' for -syntax. It is not necessary to add your own commands here (it is not -needed by the synchronizing/backtracking system). You may however do -so for the following reasons: - 1 your commands will be colorized by font-lock + ;;; Goals (and module/sections) starters detection + + + ;; ----- keywords for font-lock. + + ;; FIXME da: this one function breaks the nice configuration of Proof General: + ;; would like to have proof-goal-regexp instead. + ;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, + ;; so it appears more difficult than just a proof-goal-regexp setting. + ;; Future improvement may simply to be allow a function value for + ;; proof-goal-regexp. + + ;; FIXME Pierre: the right way IMHO here would be to set a span + ;; property 'goalcommand when coq prompt says it (if the name of + ;; current proof has changed). + + ;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry + ;; for the french: + ;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de + ; module (donc pas de Definition truc:machin. Lemma, Theorem ... ) + ; + ; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable + ; uniquement hors d'un MT + ; - si :=MEXPR est absent, elle demarre un nouveau module interactif + ; - si :=MEXPR est present, elle definit un module + ; (la fonction vernac_define_module dans toplevel/vernacentries) + ; + ; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ] + ; est valable uniquement dans un MT + ; - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module + ; interactif + ; - si (:=MEXPR absent, :MTYP present) + ; ou (:=MEXPR present, :MTYP absent) + ; elle declare un module. + ; (la fonction vernac_declare_module dans toplevel/vernacentries) + + (defun coq-count-match (regexp strg) + "Count the number of (maximum, non overlapping) matching substring + of STRG matching REGEXP. Empty match are counted once." + (let ((nbmatch 0) (str strg)) + (while (and (proof-string-match regexp str) (not (string-equal str ""))) + (incf nbmatch) + (if (= (match-end 0) 0) (setq str (substring str 1)) + (setq str (substring str (match-end 0))))) + nbmatch)) + + ; This function is used for amalgamating a proof into a single + ; goal-save region (proof-goal-command-p used in + ; proof-done-advancing-save in generic/proof-script.el) for coq < + ; 8.0. It is the test when looking backward the start of the proof. + ; It is NOT used for coq > v8.1 + ; (coq-find-and-forget in coq.el uses state numbers, proof numbers and + ; lemma names given in the prompt) + + ; compatibility with v8.0, will delete it some day + (defun coq-goal-command-str-v80-p (str) + "See `coq-goal-command-p'." + (let* ((match (coq-count-match "\\<match\\>" str)) + (with (coq-count-match "\\<with\\>" str)) + (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) + (affect (coq-count-match ":=" str))) + + (and (proof-string-match coq-goal-command-regexp str) + (not ; + (and + (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str) + (not (= letwith affect)))) + (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) + ) + ) + ) - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] + ; Module and or section openings are detected syntactically. Module + ; *openings* are difficult to detect because there can be Module + ; ...with X := ... . So we need to count :='s to detect real openings. + + ; TODO: have opened section/chapter in the prompt too, and get rid of + ; syntactical tests everywhere + (defun coq-module-opening-p (str) + "Decide whether STR is a module or section opening or not. + Used by `coq-goal-command-p'" + (let* ((match (coq-count-match "\\<match\\>" str)) + (with (coq-count-match "\\<with\\>" str)) + (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) + (affect (coq-count-match ":=" str))) + (and (proof-string-match "\\`\\(Module\\)\\>" str) + (= letwith affect)) + )) - 3 you may define an abbreviation for your command." + (defun coq-section-command-p (str) + (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) - :type '(repeat sexp) - :group 'coq) -(defcustom coq-user-solve-tactics-db nil - "User defined closing tactics. See `coq-syntax-db' for -syntax. It is not necessary to add your own commands here (it is not -needed by the synchronizing/backtracking system). You may however do -so for the following reasons: + (defun coq-goal-command-str-v81-p (str) + "Decide syntactically whether STR is a goal start or not. Use + `coq-goal-command-p-v81' on a span instead if possible." + (coq-goal-command-str-v80-p str) + ) - 1 your commands will be colorized by font-lock + ;; This is the function that tests if a SPAN is a goal start. All it + ;; has to do is look at the 'goalcmd attribute of the span. + ;; It also looks if this is not a module start. + + ;; TODO: have also attributes 'modulecmd and 'sectioncmd. This needs + ;; something in the coq prompt telling the name of all opened modules + ;; (like for open goals), and use it to set goalcmd --> no more need + ;; to look at Modules and section (actually indentation will still + ;; need it) + (defun coq-goal-command-p-v81 (span) + "see `coq-goal-command-p'" + (or (span-property span 'goalcmd) + ;; module and section starts are detected here + (let ((str (or (span-property span 'cmd) ""))) + (or (coq-section-command-p str) + (coq-module-opening-p str)) + ))) + + ;; In coq > 8.1 This is used only for indentation. + (defun coq-goal-command-str-p (str) + "Decide whether argument is a goal or not. Use + `coq-goal-command-p' on a span instead if posible." + (cond + (coq-version-is-V8-1 (coq-goal-command-str-v81-p str)) + (coq-version-is-V8-0 (coq-goal-command-str-v80-p str)) + (t (coq-goal-command-str-v80-p str)) ;; this is temporary + )) + + ;; This is used for backtracking + (defun coq-goal-command-p (span) + "Decide whether argument is a goal or not." + (cond + (coq-version-is-V8-1 (coq-goal-command-p-v81 span)) + (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd))) + (t (coq-goal-command-str-v80-p (span-property span 'cmd))) ;; this is temporary + )) + + (defvar coq-keywords-save-strict + '("Defined" + "Save" + "Qed" + "End" + "Admitted" + "Abort" + )) + + (defvar coq-keywords-save + (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) + (and (proof-string-match "\\`Proof\\>" str) + (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str))) + ) + ) - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - 3 you may define an abbreviation for your command." + (defvar coq-keywords-kill-goal + '("Abort")) - :type '(repeat sexp) - :group 'coq) + ;; Following regexps are all state changing + (defvar coq-keywords-state-changing-misc-commands + (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing)) + (defvar coq-keywords-goal + (coq-build-regexp-list-from-db coq-goal-starters-db)) + (defvar coq-keywords-decl + (coq-build-regexp-list-from-db coq-decl-db)) -(defcustom coq-user-reserved-db nil - "User defined reserved keywords information. See `coq-syntax-db' for -syntax. It is not necessary to add your own commands here (it is not -needed by the synchronizing/backtracking system). You may however do -so for the following reasons: + (defvar coq-keywords-defn + (coq-build-regexp-list-from-db coq-defn-db)) - 1 your commands will be colorized by font-lock - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] + (defvar coq-keywords-state-changing-commands + (append + coq-keywords-state-changing-misc-commands + coq-keywords-decl ; all state changing + coq-keywords-defn ; idem + coq-keywords-goal)) ; idem - 3 you may define an abbreviation for your command." - :type '(repeat sexp) - :group 'coq) + ;; + (defvar coq-keywords-state-preserving-commands + (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving)) + ;; concat this is faster that redoing coq-build-regexp-list-from-db on + ;; whole commands-db + (defvar coq-keywords-commands + (append coq-keywords-state-changing-commands + coq-keywords-state-preserving-commands) + "All commands keyword.") + (defvar coq-solve-tactics + (coq-build-regexp-list-from-db coq-solve-tactics-db) + "Keywords for closing tactic(al)s.") -(defvar coq-tactics-db - (append - coq-user-tactics-db - '( - ("absurd " "abs" "absurd " t "absurd") - ("apply" "ap" "apply " t "apply") - ("assert by" "assb" "assert ( # : # ) by #" t "assert") - ("assert" "ass" "assert ( # : # )" t) -;; ("assumption" "as" "assumption" t "assumption") - ("auto with arith" "awa" "auto with arith" t) - ("auto with" "aw" "auto with @{db}" t) - ("auto" "a" "auto" t "auto") - ("autorewrite with in using" "arwiu" "autorewrite with @{db,db...} in @{hyp} using @{tac}" t) - ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t) - ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t) - ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite") - ("case" "c" "case " t "case") - ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv") - ("change in" "chi" "change # in #" t) - ("change with in" "chwi" "change # with # in #" t) - ("change with" "chw" "change # with" t) - ("change" "ch" "change " t "change") - ("clear" "cl" "clear" t "clear") - ("clearbody" "cl" "clearbody" t "clearbody") - ("cofix" "cof" "cofix" t "cofix") - ("coinduction" "coind" "coinduction" t "coinduction") - ("compare" "cmpa" "compare # #" t "compare") - ("compute" "cmpu" "compute" t "compute") -;; ("congruence" "cong" "congruence" t "congruence") - ("constructor" "cons" "constructor" t "constructor") -;; ("contradiction" "contr" "contradiction" t "contradiction") - ("cut" "cut" "cut" t "cut") - ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") -;; ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("decompose record" "decr" "decompose record #" t "decompose\\s-+record") - ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum") - ("decompose" "dec" "decompose [#] #" t "decompose") - ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion") - ("dependent inversion with" "depinvw" "dependent inversion # with #" t) - ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear") - ("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) - ("destruct as" "desa" "destruct # as #" t) - ("destruct using" "desu" "destruct # using #" t) - ("destruct" "des" "destruct " t "destruct") -;; ("discriminate" "dis" "discriminate" t "discriminate") - ("discrR" "discrR" "discrR" t "discrR") - ("double induction" "dind" "double induction # #" t "double\\s-+induction") - ("eapply" "eap" "eapply #" t "eapply") - ("eauto with arith" "eawa" "eauto with arith" t) - ("eauto with" "eaw" "eauto with @{db}" t) - ("eauto" "ea" "eauto" t "eauto") - ("econstructor" "econs" "econstructor" t "econstructor") - ("eexists" "eex" "eexists" t "eexists") - ("eleft" "eleft" "eleft" t "eleft") - ("elim using" "elu" "elim # using #" t) - ("elim" "e" "elim #" t "elim") - ("elimtype" "elt" "elimtype" "elimtype") - ("eright" "erig" "eright" "eright") - ("esplit" "esp" "esplit" t "esplit") -;; ("exact" "exa" "exact" t "exact") - ("exists" "ex" "exists #" t "exists") -;; ("fail" "fa" "fail" nil) -;; ("field" "field" "field" t "field") - ("firstorder" "fsto" "firstorder" t "firstorder") - ("firstorder with" "fsto" "firstorder with #" t) - ("firstorder with using" "fsto" "firstorder # with #" t) - ("fold" "fold" "fold #" t "fold") -;; ("fourier" "four" "fourier" t "fourier") - ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction") - ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent") - ("generalize" "g" "generalize #" t "generalize") - ("hnf" "hnf" "hnf" t "hnf") - ("idtac" "id" "idtac" nil "idtac") ; also in tacticals with abbrev id - ("idtac \"" "id\"" "idtac \"#\"") ; also in tacticals - ("induction" "ind" "induction #" t "induction") - ("induction using" "indu" "induction # using #" t) - ("injection" "inj" "injection #" t "injection") - ("instantiate" "inst" "instantiate" t "instantiate") - ("intro" "i" "intro" t "intro") - ("intro after" "ia" "intro # after #" t) - ("intros" "is" "intros #" t "intros") - ("intros! (guess names)" nil "intros #" nil nil coq-insert-intros) - ("intros until" "isu" "intros until #" t) - ("intuition" "intu" "intuition #" t "intuition") - ("inversion" "inv" "inversion #" t "inversion") - ("inversion in" "invi" "inversion # in #" t) - ("inversion using" "invu" "inversion # using #" t) - ("inversion using in" "invui" "inversion # using # in #" t) - ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") - ("lapply" "lap" "lapply" t "lapply") - ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy") - ("left" "left" "left" t "left") - ("linear" "lin" "linear" t "linear") - ("load" "load" "load" t "load") - ("move after" "mov" "move # after #" t "move") - ("omega" "o" "omega" t "omega") - ("pattern" "pat" "pattern" t "pattern") - ("pattern(s)" "pats" "pattern # , #" t) - ("pattern at" "pata" "pattern # at #" t) - ("pose" "po" "pose ( # := # )" t "pose") - ("prolog" "prol" "prolog" t "prolog") - ("quote" "quote" "quote" t "quote") - ("quote []" "quote2" "quote # [#]" t) - ("red" "red" "red" t "red") - ("refine" "ref" "refine" t "refine") -;; ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("rename into" "ren" "rename # into #" t "rename") - ("replace with" "rep" "replace # with #" t "replace") - ("replace with in" "repi" "replace # with # in #" t) - ("rewrite <- in" "ri<" "rewrite <- # in #" t) - ("rewrite <-" "r<" "rewrite <- #" t) - ("rewrite in" "ri" "rewrite # in #" t) - ("rewrite" "r" "rewrite #" t "rewrite") - ("right" "rig" "right" t "right") -;; ("ring" "ring" "ring #" t "ring") - ("set in * |-" "seth" "set ( # := #) in * |-" t) - ("set in *" "set*" "set ( # := #) in *" t) - ("set in |- *" "setg" "set ( # := #) in |- *" t) - ("set in" "seti" "set ( # := #) in #" t) - ("set" "set" "set ( # := #)" t "set") - ("setoid_replace with" "strep2" "setoid_replace # with #" t "setoid_replace") - ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace") - ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") - ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") - ("simpl" "s" "simpl" t "simpl") - ("simpl" "sa" "simpl # at #" t) - ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") - ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion") - ("simple induction" "sind" "simple induction" t "simple\\s-+induction") - ("simplify_eq" "simeq" "simplify_eq @{hyp}" t "simplify_eq") - ("specialize" "spec" "specialize" t "specialize") - ("split" "sp" "split" t "split") - ("split_Rabs" "spra" "splitRabs" t "split_Rabs") - ("split_Rmult" "sprm" "splitRmult" t "split_Rmult") - ("stepl" "stl" "stepl #" t "stepl") - ("stepl by" "stlb" "stepl # by #" t) - ("stepr" "str" "stepr #" t "stepr") - ("stepr by" "strb" "stepr # by #" t) - ("subst" "su" "subst #" t "subst") - ("symmetry" "sy" "symmetry" t "symmetry") - ("symmetry in" "syi" "symmetry in #" t) - ;; ("tauto" "ta" "tauto" t "tauto") - ("transitivity" "trans" "transitivity #" t "transitivity") - ("trivial" "t" "trivial" t "trivial") - ("trivial with" "tw" "trivial with @{db}" t) - ("unfold" "u" "unfold #" t "unfold") - ("unfold(s)" "us" "unfold # , #" t) - ("unfold in" "unfi" "unfold # in #" t) - ("unfold at" "unfa" "unfold # at #" t) - )) - "Coq tactics information list. See `coq-syntax-db' for syntax. " - ) + (defvar coq-tacticals + (coq-build-regexp-list-from-db coq-tacticals-db) + "Keywords for tacticals in a Coq script.") -(defvar coq-solve-tactics-db - (append - coq-user-solve-tactics-db - '( - ("assumption" "as" "assumption" t "assumption") - ("by" "by" "by #" t "by") - ("congruence" "cong" "congruence" t "congruence") - ("contradiction" "contr" "contradiction" t "contradiction") - ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("discriminate" "dis" "discriminate" t "discriminate") - ("exact" "exa" "exact" t "exact") - ("fourier" "four" "fourier" t "fourier") - ("fail" "fa" "fail" nil) - ("field" "field" "field" t "field") - ("omega" "o" "omega" t "omega") - ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("ring" "ring" "ring #" t "ring") - ("tauto" "ta" "tauto" t "tauto") - )) - "Coq tactic(al)s that solve a subgoal." - ) - - -(defvar coq-tacticals-db - (append - coq-user-tacticals-db - '( - ("info" nil "info #" nil "info") - ("solve" nil "solve [ # | # ]" nil "solve") - ("first" nil "first [ # | # ]" nil "first") - ("abstract" nil "abstract @{tac} using @{name}." nil "abstract") - ("do" nil "do @{num} @{tac}" nil "do") - ("idtac" nil "idtac") ; also in tactics -; ("idtac \"" nil "idtac \"#\"") ; also in tactics - ("fail" "fa" "fail" nil "fail") -; ("fail \"" "fa\"" "fail" nil) ; -; ("orelse" nil "orelse #" t "orelse") - ("repeat" nil "repeat #" nil "repeat") - ("try" nil "try #" nil "try") - ("progress" nil "progress #" nil "progress") - ("|" nil "[ # | # ]" nil) - ("||" nil "# || #" nil) - )) - "Coq tacticals information list. See `coq-syntax-db' for syntax.") - - - - -(defvar coq-decl-db - '( - ("Axiom" "ax" "Axiom # : #" t "Axiom") - ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") - ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern") - ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate") - ("Hint Resolve" "hr" "Hint Resolve # : @{db}." t "Hint\\s-+Resolve") - ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite") - ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t ) - ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold") - ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") - ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses") - ("Parameter" "par" "Parameter #: #" t "Parameter") - ("Parameters" "par" "Parameter #: #" t "Parameters") - ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") - ("Variable" "v" "Variable #: #." t "Variable") - ("Variables" "vs" "Variables # , #: #." t "Variables") - ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") - ) - "Coq declaration keywords information list. See `coq-syntax-db' for syntax." - ) - -(defvar coq-defn-db - '( - ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint") - ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") - ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module") - ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful - ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t) - ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful - ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t) - ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful - ("Definition" "def" "Definition #:# := #." t "Definition");; careful - ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t) - ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t) - ("Definition (4 args)" "def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Program Definition" "pdef" "Program Definition #:# := #." t "Program\\s-+Definition");; careful ? - ("Program Definition (2 args)" "pdef2" "Program Definition # (# : #) (# : #):# := #." t) - ("Program Definition (3 args)" "pdef3" "Program Definition # (# : #) (# : #) (# : #):# := #." t) - ("Program Definition (4 args)" "pdef4" "Program Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t "Derive\\s-+Inversion") - ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # Sort #." t "Derive\\s-+Dependent\\s-+Inversion") - ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort #." t) - ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Fixpoint") - ("Program Fixpoint" "pfix" "Program Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Program\\s-+Fixpoint") - ("Program Fixpoint measure" "pfixm" "Program Fixpoint # (#:#) {measure @{arg} @{f}} : # :=\n#." t) - ("Program Fixpoint wf" "pfixwf" "Program Fixpoint # (#:#) {wf @{arg} @{f}} : # :=\n#." t) - ("Function" "func" "Function # (#:#) {struct @{arg}} : # :=\n#." t "Function") - ("Function measure" "funcm" "Function # (#:#) {measure @{f} @{arg}} : # :=\n#." t) - ("Function wf" "func wf" "Function # (#:#) {wf @{R} @{arg}} : # :=\n#." t) - ("Functional Scheme with" "fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." t ) - ("Functional Scheme" "fs" "Functional Scheme @{name} := Induction for @{fun}." t "Functional\\s-+Scheme") - ("Inductive" "indv" "Inductive # : # := # : #." t "Inductive") - ("Inductive (2 args)" "indv2" "Inductive # : # :=\n| # : #\n| # : #." t ) - ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Let" "Let" "Let # : # := #." t "Let") - ("Ltac" "ltac" "Ltac # := #" t "Ltac") - ("Module :=" "mo" "Module # : # := #." t ) ; careful - ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful - ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful - ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful - ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful - ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful - ("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record") - ("Scheme" "sc" "Scheme @{name} := #." t "Scheme") - ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) - ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) - ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") - ) - "Coq definition keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; modules and section are indented like goal starters -(defvar coq-goal-starters-db - '( - ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") - ("Chapter" "chp" "Chapter # : #." t "Chapter") - ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") - ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) - ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) - ("Definition" "def" "Definition #:# := #." t "Definition");; careful - ("Fact" "fct" "Fact # : #." t "Fact") - ("Goal" nil "Goal #." t "Goal") - ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") - ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") - ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) - ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful - ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful - ("Module <:" "moi2" "Module # <: #.\n#\nEnd #." t ) ; careful - ("Remark" "rk" "Remark # : #.\n#\nQed." t "Remark") - ("Section" "sec" "Section #." t "Section") - ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem") - ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem") - ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation") - ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") - ) - "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " - ) -(defvar coq-commands-db - (append - coq-user-commands-db + ; From JF Monin: + (defvar coq-reserved + (append + coq-user-reserved-db '( - ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu - ("About" nil "About #." nil "About") - ("Add" nil "Add #." nil "Add" nil t) - ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") - ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") - ("Add Field" nil "Add Field #." t "Add\\s-+Field") - ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") - ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") - ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") - ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") - ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") - ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") - ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") - ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") - ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") - ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") - ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") - ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") - ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") - ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") - ("Cd" nil "Cd #." nil "Cd") - ("Check" nil "Check" nil "Check") - ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope") - ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") - ("Comments" nil "Comments #." nil "Comments") - ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) - ("Eval" nil "Eval #." nil "Eval") - ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") - ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") - ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") - ("Extraction" "extr" "Extraction @{id}." nil "Extraction") - ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) - ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") - ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") - ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") - ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") - ("Focus" nil "Focus #." nil "Focus") - ("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") - ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") - ("Import" nil "Import #." t "Import") - ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") - ("Inspect" nil "Inspect #." nil "Inspect") - ("Locate" nil "Locate" nil "Locate") - ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") - ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") - ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) - ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) - ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) - ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) - ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) - ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t) - ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local") - ("Notation (simple)" "nots" "Notation # := #." t "Notation") - ("Opaque" nil "Opaque #." nil "Opaque") - ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic") - ("Open Local Scope" "oplsc" "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) - ("Print" "p" "Print #." nil "Print") - ("Qed" nil "Qed." nil "Qed") - ("Pwd" nil "Pwd." nil "Pwd") - ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") - ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") - ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") - ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") - ("Require Export" nil "Require Export #." t "Require\\s-+Export") - ("Require Import" nil "Require Import #." t "Require\\s-+Import") - ("Require" nil "Require #." t "Require") - ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") - ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") - ("Save" nil "Save." t "Save") - ("Search" nil "Search #" nil "Search") - ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") - ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") - ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") - ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") - ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") - ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") - ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit") - ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") - ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") - ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") - ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") - ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") - ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") - ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") - ("Show" nil "Show #." nil "Show") - ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations") - ("Test" nil "Test" nil "Test" nil t) - ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") - ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") - ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") - ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") - ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") - ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") - ("Transparent" nil "Transparent #." nil "Transparent") - ("Unfocus" nil "Unfocus." nil "Unfocus") - ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline") - ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize") - ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments") - ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit") - ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth") - ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard") - ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit") - ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All") - ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion") - ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") - ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") - ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") -; ("print" "pr" "print #" "print") - ) - coq-decl-db coq-defn-db coq-goal-starters-db) - "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " - ) - -(defvar coq-terms-db - '( - ("fun (1 args)" "f" "fun #:# => #" nil "fun") - ("fun (2 args)" "f2" "fun (#:#) (#:#) => #") - ("fun (3 args)" "f3" "fun (#:#) (#:#) (#:#) => #") - ("fun (4 args)" "f4" "fun (#:#) (#:#) (#:#) (#:#) => #") - ("forall" "fo" "forall #:#,#" nil "forall") - ("forall (2 args)" "fo2" "forall (#:#) (#:#), #") - ("forall (3 args)" "fo3" "forall (#:#) (#:#) (#:#), #") - ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #") - ("if" "if" "if # then # else #" nil "if") - ("let in" "li" "let # := # in #" nil "let") - ("match! (from type)" nil "" nil "match" coq-insert-match) - ("match with" "m" "match # with\n| # => #\nend") - ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend") - ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend") - ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") + "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")) + "Reserved keywords of Coq.") + + + (defvar coq-state-changing-tactics + (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) + + (defvar coq-state-preserving-tactics + (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-preserving)) + + + (defvar coq-tactics + (append coq-state-changing-tactics coq-state-preserving-tactics)) + + (defvar coq-retractable-instruct + (append coq-state-changing-tactics coq-keywords-state-changing-commands)) + + (defvar coq-non-retractable-instruct + (append coq-state-preserving-tactics + coq-keywords-state-preserving-commands)) + + (defvar coq-keywords + (append coq-keywords-goal coq-keywords-save coq-keywords-decl + coq-keywords-defn coq-keywords-commands) + "All keywords in a Coq script.") + + + + (defvar coq-symbols + '("|" + "||" + ":" + ";" + "," + "(" + ")" + "[" + "]" + "{" + "}" + ":=" + "=>" + "->" + ".") + "Punctuation Symbols used by Coq.") + + ;; ----- regular expressions + (defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" + "A regexp indicating that the Coq process has identified an error.") + + (defvar coq-id proof-id) + (defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)") + + (defvar coq-ids (proof-ids coq-id " ")) + + (defun coq-first-abstr-regexp (paren end) + (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) + + (defvar coq-font-lock-terms + (list + ;; lambda binders + (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) + ;; forall binder + (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) + ; (list "\\<forall\\>" + ; (list 0 font-lock-type-face) + ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil + ; (list 0 font-lock-variable-name-face))) + ;; parenthesized binders + (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) ) - "Coq terms keywords information list. See `coq-syntax-db' for syntax. " - ) - - - - - - - -;;; Goals (and module/sections) starters detection - - -;; ----- keywords for font-lock. - -;; FIXME da: this one function breaks the nice configuration of Proof General: -;; would like to have proof-goal-regexp instead. -;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, -;; so it appears more difficult than just a proof-goal-regexp setting. -;; Future improvement may simply to be allow a function value for -;; proof-goal-regexp. - -;; FIXME Pierre: the right way IMHO here would be to set a span -;; property 'goalcommand when coq prompt says it (if the name of -;; current proof has changed). - -;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry -;; for the french: -;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de -; module (donc pas de Definition truc:machin. Lemma, Theorem ... ) -; -; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable -; uniquement hors d'un MT -; - si :=MEXPR est absent, elle demarre un nouveau module interactif -; - si :=MEXPR est present, elle definit un module -; (la fonction vernac_define_module dans toplevel/vernacentries) -; -; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ] -; est valable uniquement dans un MT -; - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module -; interactif -; - si (:=MEXPR absent, :MTYP present) -; ou (:=MEXPR present, :MTYP absent) -; elle declare un module. -; (la fonction vernac_declare_module dans toplevel/vernacentries) - -(defun coq-count-match (regexp strg) - "Count the number of (maximum, non overlapping) matching substring -of STRG matching REGEXP. Empty match are counted once." - (let ((nbmatch 0) (str strg)) - (while (and (proof-string-match regexp str) (not (string-equal str ""))) - (incf nbmatch) - (if (= (match-end 0) 0) (setq str (substring str 1)) - (setq str (substring str (match-end 0))))) - nbmatch)) - -; This function is used for amalgamating a proof into a single -; goal-save region (proof-goal-command-p used in -; proof-done-advancing-save in generic/proof-script.el) for coq < -; 8.0. It is the test when looking backward the start of the proof. -; It is NOT used for coq > v8.1 -; (coq-find-and-forget in coq.el uses state numbers, proof numbers and -; lemma names given in the prompt) - -; compatibility with v8.0, will delete it some day -(defun coq-goal-command-str-v80-p (str) - "See `coq-goal-command-p'." - (let* ((match (coq-count-match "\\<match\\>" str)) - (with (coq-count-match "\\<with\\>" str)) - (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) - (affect (coq-count-match ":=" str))) - - (and (proof-string-match coq-goal-command-regexp str) - (not ; - (and - (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str) - (not (= letwith affect)))) - (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) - ) - ) - ) - -; Module and or section openings are detected syntactically. Module -; *openings* are difficult to detect because there can be Module -; ...with X := ... . So we need to count :='s to detect real openings. - -; TODO: have opened section/chapter in the prompt too, and get rid of -; syntactical tests everywhere -(defun coq-module-opening-p (str) - "Decide whether STR is a module or section opening or not. -Used by `coq-goal-command-p'" - (let* ((match (coq-count-match "\\<match\\>" str)) - (with (coq-count-match "\\<with\\>" str)) - (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) - (affect (coq-count-match ":=" str))) - (and (proof-string-match "\\`\\(Module\\)\\>" str) - (= letwith affect)) - )) - -(defun coq-section-command-p (str) - (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) - - -(defun coq-goal-command-str-v81-p (str) - "Decide syntactically whether STR is a goal start or not. Use - `coq-goal-command-p-v81' on a span instead if possible." - (coq-goal-command-str-v80-p str) - ) - -;; This is the function that tests if a SPAN is a goal start. All it -;; has to do is look at the 'goalcmd attribute of the span. -;; It also looks if this is not a module start. - -;; TODO: have also attributes 'modulecmd and 'sectioncmd. This needs -;; something in the coq prompt telling the name of all opened modules -;; (like for open goals), and use it to set goalcmd --> no more need -;; to look at Modules and section (actually indentation will still -;; need it) -(defun coq-goal-command-p-v81 (span) - "see `coq-goal-command-p'" - (or (span-property span 'goalcmd) - ;; module and section starts are detected here - (let ((str (or (span-property span 'cmd) ""))) - (or (coq-section-command-p str) - (coq-module-opening-p str)) - ))) - -;; In coq > 8.1 This is used only for indentation. -(defun coq-goal-command-str-p (str) - "Decide whether argument is a goal or not. Use - `coq-goal-command-p' on a span instead if posible." - (cond - (coq-version-is-V8-1 (coq-goal-command-str-v81-p str)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p str)) - (t (coq-goal-command-str-v80-p str)) ;; this is temporary - )) - -;; This is used for backtracking -(defun coq-goal-command-p (span) - "Decide whether argument is a goal or not." - (cond - (coq-version-is-V8-1 (coq-goal-command-p-v81 span)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd))) - (t (coq-goal-command-str-v80-p (span-property span 'cmd))) ;; this is temporary - )) - -(defvar coq-keywords-save-strict - '("Defined" - "Save" - "Qed" - "End" - "Admitted" - "Abort" - )) - -(defvar coq-keywords-save - (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) - (and (proof-string-match "\\`Proof\\>" str) - (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str))) - ) - ) - - -(defvar coq-keywords-kill-goal - '("Abort")) - -;; Following regexps are all state changing -(defvar coq-keywords-state-changing-misc-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing)) - -(defvar coq-keywords-goal - (coq-build-regexp-list-from-db coq-goal-starters-db)) - -(defvar coq-keywords-decl - (coq-build-regexp-list-from-db coq-decl-db)) - -(defvar coq-keywords-defn - (coq-build-regexp-list-from-db coq-defn-db)) - - -(defvar coq-keywords-state-changing-commands - (append - coq-keywords-state-changing-misc-commands - coq-keywords-decl ; all state changing - coq-keywords-defn ; idem - coq-keywords-goal)) ; idem - - -;; -(defvar coq-keywords-state-preserving-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving)) - -;; concat this is faster that redoing coq-build-regexp-list-from-db on -;; whole commands-db -(defvar coq-keywords-commands - (append coq-keywords-state-changing-commands - coq-keywords-state-preserving-commands) - "All commands keyword.") - -(defvar coq-solve-tactics - (coq-build-regexp-list-from-db coq-solve-tactics-db) - "Keywords for closing tactic(al)s.") - -(defvar coq-tacticals - (coq-build-regexp-list-from-db coq-tacticals-db) - "Keywords for tacticals in a Coq script.") - - -; From JF Monin: -(defvar coq-reserved -(append - coq-user-reserved-db - '( - "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")) - "Reserved keywords of Coq.") - - -(defvar coq-state-changing-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) - -(defvar coq-state-preserving-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-preserving)) - - -(defvar coq-tactics - (append coq-state-changing-tactics coq-state-preserving-tactics)) - -(defvar coq-retractable-instruct - (append coq-state-changing-tactics coq-keywords-state-changing-commands)) - -(defvar coq-non-retractable-instruct - (append coq-state-preserving-tactics - coq-keywords-state-preserving-commands)) - -(defvar coq-keywords - (append coq-keywords-goal coq-keywords-save coq-keywords-decl - coq-keywords-defn coq-keywords-commands) - "All keywords in a Coq script.") - - - -(defvar coq-symbols - '("|" - "||" - ":" - ";" - "," - "(" - ")" - "[" - "]" - "{" - "}" - ":=" - "=>" - "->" - ".") - "Punctuation Symbols used by Coq.") - -;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" - "A regexp indicating that the Coq process has identified an error.") - -(defvar coq-id proof-id) -(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)") - -(defvar coq-ids (proof-ids coq-id " ")) - -(defun coq-first-abstr-regexp (paren end) - (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) - -(defvar coq-font-lock-terms - (list - ;; lambda binders - (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) - ;; forall binder - (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) -; (list "\\<forall\\>" -; (list 0 font-lock-type-face) -; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil -; (list 0 font-lock-variable-name-face))) - ;; parenthesized binders - (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - ) - "*Font-lock table for Coq terms.") - -;; According to Coq, "Definition" is both a declaration and a goal. -;; It is understood here as being a goal. This is important for -;; recognizing global identifiers, see coq-global-p. -(defconst coq-save-command-regexp-strict - (proof-anchor-regexp + "*Font-lock table for Coq terms.") + + ;; According to Coq, "Definition" is both a declaration and a goal. + ;; It is understood here as being a goal. This is important for + ;; recognizing global identifiers, see coq-global-p. + (defconst coq-save-command-regexp-strict + (proof-anchor-regexp + (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) + "\\)"))) + (defconst coq-save-command-regexp + (proof-anchor-regexp + (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save) + "\\)"))) + (defconst coq-save-with-hole-regexp (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)"))) -(defconst coq-save-command-regexp - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save) - "\\)"))) -(defconst coq-save-with-hole-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) - -(defconst coq-goal-command-regexp - (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) - -(defconst coq-goal-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) - "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) - -(defconst coq-decl-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) - "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) - -(defconst coq-defn-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) - "\\)\\s-+\\(" coq-id "\\)")) - -; must match: -; "with f x y :" (followed by = or not) -; "with f x y (z:" (not followed by =) -; BUT NOT: -; "with f ... (x:=" -; "match ... with .. => " -(defconst coq-with-with-hole-regexp - (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" - coq-id "\\s-*:[^=]\\)")) -; marche aussi a peu pres -; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) -;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" -(defvar coq-font-lock-keywords-1 - (append - coq-font-lock-terms - (list - (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) - (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) - (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) - (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) - (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) - (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) - (cons "============================" 'font-lock-keyword-face) - (cons "Subtree proved!" 'font-lock-keyword-face) - (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) - (list "^\\([^ \n]+\\) \\(is defined\\)" - (list 2 'font-lock-keyword-face t) - (list 1 'font-lock-function-name-face t)) - - (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face) - (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) - ;; Remove spurious variable and function faces on commas. - '(proof-zap-commas)))) -(defvar coq-font-lock-keywords coq-font-lock-keywords-1) - -(defun coq-init-syntax-table () - "Set appropriate values for syntax table in current buffer." - - (modify-syntax-entry ?\$ ".") - (modify-syntax-entry ?\/ ".") - (modify-syntax-entry ?\\ ".") - (modify-syntax-entry ?+ ".") - (modify-syntax-entry ?- ".") - (modify-syntax-entry ?= ".") - (modify-syntax-entry ?% ".") - (modify-syntax-entry ?< ".") - (modify-syntax-entry ?> ".") - (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "w") - (modify-syntax-entry ?\' "w") - (modify-syntax-entry ?\| ".") - -; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug - (modify-syntax-entry ?\. ".") - - (condition-case nil - ;; Try to use Emacs-21's nested comments. - (modify-syntax-entry ?\* ". 23n") - ;; Revert to non-nested comments if that failed. - (error (modify-syntax-entry ?\* ". 23"))) - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - - -(defconst coq-generic-expression - (mapcar (lambda (kw) - (list (capitalize kw) - (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) - 1)) - (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) - -(provide 'coq-syntax) -;;; coq-syntax.el ends here - -;;; Local Variables: *** -;;; indent-tabs-mode: nil *** -;;; End: *** + "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) + + (defconst coq-goal-command-regexp + (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) + + (defconst coq-goal-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) + "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) + + (defconst coq-decl-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) + "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) + + (defconst coq-defn-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) + "\\)\\s-+\\(" coq-id "\\)")) + + ; must match: + ; "with f x y :" (followed by = or not) + ; "with f x y (z:" (not followed by =) + ; BUT NOT: + ; "with f ... (x:=" + ; "match ... with .. => " + (defconst coq-with-with-hole-regexp + (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" + coq-id "\\s-*:[^=]\\)")) + ; marche aussi a peu pres + ; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) + ;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" + (defvar coq-font-lock-keywords-1 + (append + coq-font-lock-terms + (list + (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) + (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) + (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) + (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) + (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) + (cons "============================" 'font-lock-keyword-face) + (cons "Subtree proved!" 'font-lock-keyword-face) + (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) + (list "^\\([^ \n]+\\) \\(is defined\\)" + (list 2 'font-lock-keyword-face t) + (list 1 'font-lock-function-name-face t)) + + (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face) + (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face) + (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) + (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) + (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) + ;; Remove spurious variable and function faces on commas. + '(proof-zap-commas)))) + (defvar coq-font-lock-keywords coq-font-lock-keywords-1) + + (defun coq-init-syntax-table () + "Set appropriate values for syntax table in current buffer." + + (modify-syntax-entry ?\$ ".") + (modify-syntax-entry ?\/ ".") + (modify-syntax-entry ?\\ ".") + (modify-syntax-entry ?+ ".") + (modify-syntax-entry ?- ".") + (modify-syntax-entry ?= ".") + (modify-syntax-entry ?% ".") + (modify-syntax-entry ?< ".") + (modify-syntax-entry ?> ".") + (modify-syntax-entry ?\& ".") + (modify-syntax-entry ?_ "w") + (modify-syntax-entry ?\' "w") + (modify-syntax-entry ?\| ".") + + ; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug + (modify-syntax-entry ?\. ".") + + (condition-case nil + ;; Try to use Emacs-21's nested comments. + (modify-syntax-entry ?\* ". 23n") + ;; Revert to non-nested comments if that failed. + (error (modify-syntax-entry ?\* ". 23"))) + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4")) + + + (defconst coq-generic-expression + (mapcar (lambda (kw) + (list (capitalize kw) + (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) + 1)) + (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) + + (provide 'coq-syntax) + ;;; coq-syntax.el ends here + +; Local Variables: *** +; indent-tabs-mode: nil *** +; End: *** @@ -9,15 +9,14 @@ ;;; Commentary: ;; - - ;;; History: -;; (require 'proof) (require 'local-vars-list) ; in lib directory -(require 'coq-local-vars) ; in coq directory -;; coq-syntaxe is required below + +(require 'coq-local-vars) +(require 'coq-syntax) ; determines coq version + ;; ----- coq-shell configuration options ;;; Code: @@ -25,14 +24,28 @@ ;; (defun proofstack () (coq-get-span-proofstack (span-at (point) 'type))) ;; End debugging -;; List of arguments to pass to Coq process. Should contain -emacs. +;; coq-prog-args is the user-set list of arguments to pass to Coq process, +;; see 'defpacustom prog-args' in proof-config for documentation. + +;; For Coq, this should contain -emacs. ;; -translate will be added automatically to this list if `coq-translate-to-v8' -;; is set. -;; coq-prog-args is set by defpgcustom in proof-config -(defcustom coq-prog-args '("-emacs") - "The arguments passed to coqtop, important: see `proof-prog-name'." +;; is set. The list is not altered if the user has set this herself. + +(defcustom coq-translate-to-v8 nil + "*Whether to use -translate argument to Coq" + :type 'boolean :group 'coq) +(unless (or (noninteractive) ;; compiling + (not (equal + (default-value 'coq-prog-args) coq-prog-args))) + (setq coq-prog-args + (append coq-prog-args + (cond + (coq-version-is-V8-0 '("-emacs")) + (t '("-emacs-U"))) + (if coq-translate-to-v8 " -translate")))) + (defcustom coq-compile-file-command "coqc %s" "*Command to compile a coq file. This is called when `coq-auto-compile-vos' is set, unless a Makefile @@ -60,14 +73,11 @@ To disable coqc being called (and use only make), set this to nil." (defvar coq-utf-safe coq-version-is-V8-1 "Obsolete, coq >= 8.1 does not use special symbols for delimiting prompts.") -(if coq-version-is-V8-1 - (setq coq-prog-args '("-emacs-U")) - (setq coq-prog-args '("-emacs"))) - ;; utf-8 is not yet well accepted (especially by xemacs) -;Set to t in your .emacs to enable it. Needs to load library `un-define' to -;work on xemacs." -(or (boundp 'proof-shell-unicode) (setq proof-shell-unicode nil)) +;; Set to t in your .emacs to enable it. Needs to load library `un-define' to +;; work on xemacs." +;; (or (boundp 'proof-shell-unicode) (setq proof-shell-unicode nil)) +;; da: I think the default t setting now works fine, at least for me. (defcustom coq-prog-env nil "*List of environment settings d to pass to Coq process. @@ -85,7 +95,8 @@ On Windows you might need something like: ;; Pierre added the infos in the prompt, this is new in Coq v8-1 (defvar coq-shell-prompt-pattern - (if coq-version-is-V8-1 (concat "\\(?:\n\\(?:[^\n\371]+\371\\|<prompt>[^\n]+</prompt>\\)\\)") + (if coq-version-is-V8-1 + (concat "\\(?:\n\\(?:[^\n\371]+\371\\|<prompt>[^\n]+</prompt>\\)\\)") (concat "\\(?:\n" proof-id " < \371\\)")) "*The prompt pattern for the inferior shell running coq.") @@ -757,6 +768,7 @@ This is specific to `coq-mode'." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; To guess the command line options ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (defun coq-guess-command-line (filename) "Guess the right command line options to compile FILENAME using `make -n'." (let ((dir (file-name-directory filename))) @@ -780,12 +792,10 @@ This is specific to `coq-mode'." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun coq-pre-shell-start () - (setq proof-prog-name (concat coq-prog-name - (if coq-translate-to-v8 " -translate"))) + (setq proof-prog-name coq-prog-name) (setq proof-mode-for-shell 'coq-shell-mode) (setq proof-mode-for-goals 'coq-goals-mode) - (setq proof-mode-for-response 'coq-response-mode) - ) + (setq proof-mode-for-response 'coq-response-mode)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Configuring proof and pbp mode and setting up various utilities ;; @@ -1182,17 +1192,6 @@ Group number 1 matches the name of the library which is required.") ; proof-shell-process-file nil ; proof-shell-inform-file-retracted-cmd nil))) -;; da: what a shame -translate is a command line flag and not a -;; command in Coq. Otherwise we could enable/disable interactively. -;; As it is, this setting will only work between restarts. -;; Moreover, if we had collaborated on this we could easily have -;; implemented a hook to translate automatically in PG with some -;; extra markup. Scanning the whitespace as formatted presently -;; is messy. - -(defpacustom translate-to-v8 nil - "*Whether to use -translate argument to Coq" - :type 'boolean) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |