diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 148 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 41 | ||||
| -rw-r--r-- | coq/coq.el | 47 |
3 files changed, 89 insertions, 147 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 9e938a2a..14626227 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -4,64 +4,9 @@ ;(defvar coq-version-is-V7 nil) ;(defvar coq-version-is-V6 nil) +;#s are replaced by holes by holes-abbrev-complete (if (boundp 'holes-abbrev-complete) - (define-abbrev-table 'coq-mode-abbrev-table - '( - ("a" "auto" nil 0) - ("ab" "absurd" nil 0) - ("abs" "absurd" nil 0) - ("ao" "abstract omega" nil 0) - ("ap" "apply" nil 0) - ("as" "assumption" nil 0) - ("au" "auto" nil 0) - ("aw" "auto with" nil 0) - ("awa" "auto with arith" nil 0) - ("con" "constructor" nil 0) - ("dec" "decompose []" nil 0) - ("def" "Definition : :=." nil 0) - ("di" "discriminate" nil 0) - ("dis" "discriminate" nil 0) - ("e" "elim" nil 0) - ("ea" "eauto" nil 0) - ("eap" "eapply" nil 0) - ("eaw" "eauto with" nil 0) - ("eawa" "eauto with arith" nil 0) - ("el" "elim" nil 0) - ("ex" "exists" nil 0) - ("f" "forall #:#,#" nil 0) - ("f" "fun (:) => " nil 0) - ("fi" "functional induction" nil 0) - ("fix" "Fixpoint X (X : X) {struct X} : X := X." nil 0) - ("fs" "Functional Scheme xxx := Induction for yyy (opt:with ...)." nil 0) - ("g" "generalize" nil 0) - ("ge" "generalize" nil 0) - ("gen" "generalize" nil 0) - ("h" "Hints : ." nil 0) - ("hr" "Hint Resolve :." nil 0) - ("i" "intro" nil 0) - ("in" "intro" nil 0) - ("ind" "induction" nil 0) - ("indv" "Inductive" nil 0) - ("inv" "inversion" nil 0) - ("is" "intros" nil 0) - ("l" "Lemma :" nil 0) - ("o" "abstract omega" nil 0) - ("p" "Print" nil 0) - ("pr" "Print" nil 0) - ("r" "rewrite" nil 0) - ("r<" "rewrite <-" nil 0) - ("re" "rewrite" nil 0) - ("re<" "rewrite <-" nil 0) - ("s" "simpl" nil 0) - ("sc" "Scheme := Induction for Sort ." nil 0) - ("si" "simpl" nil 0) - ("sy" "symmetry" nil 0) - ("sym" "symmetry" nil 0) - ("t" "trivial" nil 0) - ("tr" "trivial" nil 0) - ("u" "unfold" nil 0) - ("un" "unfold" nil 0) - )) + () (define-abbrev-table 'coq-mode-abbrev-table '( ("a" "auto" holes-abbrev-complete 4) @@ -90,6 +35,10 @@ ("desu" "destruct # using #" holes-abbrev-complete 0) ("desa" "destruct # as #" holes-abbrev-complete 0) ("dis" "discriminate" holes-abbrev-complete 0) + ("dm" "Declare Module # : # := #." holes-abbrev-complete 0) + ("dm2" "Declare Module # <: # := #." holes-abbrev-complete 0) + ("dmi" "Declare Module # : #.\n#\nEnd #." holes-abbrev-complete 0) + ("dmi2" "Declare Module # <: #.\n#\nEnd #." holes-abbrev-complete 0) ("e" "elim #" holes-abbrev-complete 1) ("ea" "eauto" holes-abbrev-complete 0) ("eap" "eapply #" holes-abbrev-complete 0) @@ -104,7 +53,7 @@ ("f3" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) ("f4" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) ("fi" "functional induction #" holes-abbrev-complete 0) - ("fix" "Fixpoint # (#:#) {struct #} : # :=" holes-abbrev-complete 3) + ("fix" "Fixpoint # (#:#) {struct #} : # :=\n#." holes-abbrev-complete 3) ("fo" "forall #,#" holes-abbrev-complete 0) ("fo1" "forall #:#,#" holes-abbrev-complete 0) ("fo2" "forall (#:#) (#:#), #" holes-abbrev-complete 0) @@ -125,8 +74,13 @@ ("i" "intro #" holes-abbrev-complete 10) ("if" "if # then # else #" holes-abbrev-complete 1) ("in" "intro" holes-abbrev-complete 1) + ("inf" "infix \"#\" := # (at level #) : #." holes-abbrev-complete 1) ("ind" "induction #" holes-abbrev-complete 2) ("indv" "Inductive # : # := # : #." holes-abbrev-complete 0) + ("indv2" "Inductive # : # :=\n# : #\n| # : #." holes-abbrev-complete 0) + ("indv3" "Inductive # : # :=\n # : #\n| # : #\n| # : #." holes-abbrev-complete 0) + ("indv4" "Inductive # : # :=\n # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0) + ("indv5" "Inductive # : # :=\n # : #\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0) ("inj" "injection #" holes-abbrev-complete 2) ("inv" "inversion #" holes-abbrev-complete 9) ("intu" "intuition #" holes-abbrev-complete 9) @@ -134,6 +88,17 @@ ("ite" "if # then # else #" holes-abbrev-complete 1) ("l" "Lemma # : #." holes-abbrev-complete 4) ("li" "let # := # in #" holes-abbrev-complete 1) + ("m" "match # with\n# => #\nend" holes-abbrev-complete 1) + ("m2" "match # with\n # => #\n| # => #\nend" holes-abbrev-complete 1) + ("m3" "match # with\n # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1) + ("m4" "match # with\n# => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1) + ("m5" "match # with\n # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1) + ("mt" "Module Type # := #." holes-abbrev-complete 0) + ("mti" "Module Type #.\n#\nEnd #." holes-abbrev-complete 0) + ("mo" "Module # : # := #." holes-abbrev-complete 0) + ("mo2" "Module # <: # := #." holes-abbrev-complete 0) + ("moi" "Module # : #.\n#\nEnd #." holes-abbrev-complete 0) + ("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0) ("o" "omega" holes-abbrev-complete 0) ("om" "Omega" holes-abbrev-complete 0) ("p" "Print #" holes-abbrev-complete 3) @@ -166,71 +131,8 @@ ("ta" "tauto" holes-abbrev-complete 1) ("u" "unfold #" holes-abbrev-complete 1) ("un" "unfold #" holes-abbrev-complete 7) - - ("mt" "Module Type # := #." holes-abbrev-complete 0) - ("mti" "Module Type #. -# -End #." holes-abbrev-complete 0) - ("mo" "Module # : # := #." holes-abbrev-complete 0) - ("mo2" "Module # <: # := #." holes-abbrev-complete 0) - ("moi" "Module # : #. -# -End #." holes-abbrev-complete 0) - ("moi2" "Module # <: #. -# -End #." holes-abbrev-complete 0) - - - ("dm" "Declare Module # : # := #." holes-abbrev-complete 0) - ("dm2" "Declare Module # <: # := #." holes-abbrev-complete 0) - ("dmi" "Declare Module # : #. -# -End #." holes-abbrev-complete 0) - ("dmi2" "Declare Module # <: #. -# -End #." holes-abbrev-complete 0) - - - - - ("m" "match # with -# => #" holes-abbrev-complete 1) - ("m2" "match # with - # => # -| # => #" holes-abbrev-complete 1) - ("m3" "match # with - # => # -| # => # -| # => #" holes-abbrev-complete 1) - ("m4" "match # with - # => # -| # => # -| # => # -| # => #" holes-abbrev-complete 1) - ("m5" "match # with - # => # -| # => # -| # => # -| # => # -| # => #" holes-abbrev-complete 1) - ("indv2" "Inductive # : # := - # : # -| # : #." holes-abbrev-complete 0) - ("indv3" "Inductive # : # := - # : # -| # : # -| # : #." holes-abbrev-complete 0) - ("indv4" "Inductive # : # := - # : # -| # : # -| # : # -| # : #." holes-abbrev-complete 0) - ("indv5" "Inductive # : # := - # : # -| # : # -| # : # -| # : # -| # : #." holes-abbrev-complete 0) + ("v" "Variable # : #." holes-abbrev-complete 7) + ("vs" "Variables # : #." holes-abbrev-complete 7) ) ) ) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index d9f4d153..3922c7fd 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -127,19 +127,21 @@ version of coq by doing 'coqtop -v'." ) "CoInductive" "Definition" ;; careful: if not followed by :=, then it is a goal cmd "Fixpoint" + "CoInductive" "Inductive" "Inductive\\s-+Set" "Inductive\\s-+Prop" "Inductive\\s-+Type" "Mutual\\s-+Inductive" "Record" - "Functional\\s-+Scheme" "Scheme" + "Functional\\s-+Scheme" "Syntactic\\s-+Definition" - "Structure")) + "Structure" + "Ltac")) -;; Modules are like section in v74. -(if coq-version-is-V74 +;; Modules are like section in v > 7.4. +(if (or coq-version-is-V74 coq-version-is-V8) (defvar coq-keywords-goal '("Chapter" "Declare\\s-+Module";;only if not followed by:=(see coq-proof-mode-p in coq.el) @@ -169,7 +171,9 @@ version of coq by doing 'coqtop -v'." ) '("Defined" "Save" "Qed" - "End")) + "End" + "Admitted" + )) (defvar coq-keywords-kill-goal '("Abort")) @@ -201,7 +205,6 @@ Print and Check commands, put the following line in your .emacs: :group 'coq) ;; -;; Hint Rewrite/Resolve... ==> state-changing ;; Print Hint ==> state preserving (defvar coq-keywords-state-preserving-commands (append '("(*" ;;Pierre comments must not be undone @@ -217,7 +220,6 @@ Print and Check commands, put the following line in your .emacs: "Extraction Library" "Extraction Module" "Focus" ;; ??? - "Hint\\s-+Rewrite" "Inspect" "Locate" "Locate\\s-+File" @@ -225,8 +227,7 @@ Print and Check commands, put the following line in your .emacs: "Opaque" "Print" "Proof" - "Recursive\\s-+Extraction" - "Recursive\\s-+Extraction\\s-+Module" + "Recursive\\s-+Extraction\\(?:\\s-+Module\\)?" "Remove\\s-+LoadPath" "Pwd" "Qed" @@ -278,8 +279,14 @@ Print and Check commands, put the following line in your .emacs: "Extraction\\s-+Language" "Extraction\\s-+NoInline" "Grammar" - "\\`Hint" ;; Pierre fev-2003: Hack: must not match "Print Hint." - "Hints" +; "\\`Hint" ;; Pierre fev-2003: Hack: must not match "Print Hint." + "Hint\\s-+Resolve" + "Hint\\s-+Immediate" + "Hint\\s-+Rewrite" + "Hint\\s-+Unfold" + "Hint\\s-+Extern" + "Hint\\s-+Constructors" + "Hints" ;no more a keyword in v8 "Identity\\s-+Coercion" "Implicit\\s-+Arguments\\s-+Off" "Implicit\\s-+Arguments\\s-+On" @@ -403,6 +410,7 @@ Intro and Elim tactics, put the following line in your .emacs: "generalize" "hnf" "induction" + "coinduction" "injection" "instantiate" "intro[s]?" @@ -589,11 +597,16 @@ Idtac (Nop) tactic, put the following line in your .emacs: (defvar coq-reserved '("as" "ALL" - "Cases" + "True" + "False" + "Cases" + "match" "EX" "else" "end" "Fix" + "forall" + "fun" "if" "in" "into" @@ -669,7 +682,7 @@ Idtac (Nop) tactic, put the following line in your .emacs: "\\)\\s-+\\(" coq-ids "\\)\\s-*[:]")) (defconst coq-defn-with-hole-regexp (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) - "\\)\\s-+\\(" coq-id "\\)\\s-*[[:]")) + "\\)\\s-+\\(" coq-id "\\)\\s-*.")) (defvar coq-font-lock-keywords-1 (append coq-font-lock-terms @@ -709,6 +722,7 @@ Idtac (Nop) tactic, put the following line in your .emacs: (modify-syntax-entry ?_ "w") (modify-syntax-entry ?\' "_") (modify-syntax-entry ?\| ".") + (modify-syntax-entry ?\. "_") (condition-case nil ;; Try to use Emacs-21's nested comments. (modify-syntax-entry ?\* ". 23n") @@ -717,5 +731,6 @@ Idtac (Nop) tactic, put the following line in your .emacs: (modify-syntax-entry ?\( "()1") (modify-syntax-entry ?\) ")(4")) + (provide 'coq-syntax) ;;; coq-syntax.el ends here @@ -92,14 +92,14 @@ "COMMAND ABBREVIATION" ["Definition def<ctrl-backspace>" (insert-and-expand "def") t] ["Fixpoint fix<ctrl-backspace>" (insert-and-expand "fix") t] - ["Functional Scheme fs<ctrl-backspace>" (insert-and-expand "fs") t] - ["Functional Scheme w fsw<ctrl-backspace>" (insert-and-expand "fsw") t] + ["Lemma l<ctrl-backspace>" (insert-and-expand "l") t] + "" ["Inductive indv<ctrl-backspace>" (insert-and-expand "indv") t] ["Inductive1 indv1<ctrl-backspace>" (insert-and-expand "indv1") t] ["Inductive2 indv2<ctrl-backspace>" (insert-and-expand "indv2") t] ["Inductive3 indv3<ctrl-backspace>" (insert-and-expand "indv3") t] ["Inductive4 indv4<ctrl-backspace>" (insert-and-expand "indv4") t] - ["Lemma l<ctrl-backspace>" (insert-and-expand "l") t] + "" ["Module mo<ctrl-backspace>" (insert-and-expand "mo") t] ["Module (<:) mo2<ctrl-backspace>" (insert-and-expand "mo") t] ["Module (interactive) moi<ctrl-backspace>" (insert-and-expand "moi") t] @@ -110,13 +110,18 @@ ["Declare Module (<:) dm2<ctrl-backspace>" (insert-and-expand "dm") t] ["Declare Module (inter.) dmi<ctrl-backspace>" (insert-and-expand "dmi") t] ["Declare Module (inter. <:) dmi2<ctrl-backspace>" (insert-and-expand "dmi2") t] - + "" ["Scheme sc<ctrl-backspace>" (insert-and-expand "sc") t] + ["Functional Scheme fs<ctrl-backspace>" (insert-and-expand "fs") t] + ["Functional Scheme with fsw<ctrl-backspace>" (insert-and-expand "fsw") t] + "" ["hint Constructors hc<ctrl-backspace>" (insert-and-expand "hc") t] ["hint Immediate hi<ctrl-backspace>" (insert-and-expand "hi") t] ["hint Resolve hr<ctrl-backspace>" (insert-and-expand "hr") t] ["hint extern he<ctrl-backspace>" (insert-and-expand "he") t] ["hints hs<ctrl-backspace>" (insert-and-expand "hs") t] + "" + ["infix inf<ctrl-backspace>" (insert-and-expand "inf") t] ) ("Insert term" @@ -204,22 +209,41 @@ ["unfold u<ctrl-bacspace>" (insert-and-expand "u") t] ) + ["What are those #??" (holes-short-doc) t] + ["expand abbrev at point" expand-abbrev t] + ["list abbrevs" list-abbrevs t] + ["Insert Section..." coq-insert-section t] + ["Insert Module..." coq-insert-module t] ["Print..." coq-Print t] ["Check..." coq-Check t] ["Hints" coq-PrintHint t] ["Show ith goal..." coq-Show t] ["Search isos/pattern..." coq-SearchIsos t] - ["expand abbrev at point" expand-abbrev t] - ["What are those #??" (holes-short-doc) t] - ["list abbrevs" list-abbrevs t] ["3 buffers view" coq-three-b t] - ["Begin Section..." coq-begin-Section t] - ["End Section" coq-end-Section t] ["Compile" coq-Compile t] )) +(defun coq-insert-section (s) + (interactive "sSection name: ") + (insert "Section " s ".\n#\nEnd " s ".") +(replace-string-by-holes-backward-move-point 1 empty-hole-string) +) + +(setq-default module-kinds-table + '(("Module" 1) ("Module Type" 2) ("Declare Module" 3))) + +(defun coq-insert-module () + (interactive) + (let* ((mods (completing-read "kind of module: " module-kinds-table)) + (s (read-string "sModule name: "))) + (insert mods " " s ": #.\n#\nEnd " s ".") + (replace-string-by-holes-backward-move-point 2 empty-hole-string) + ) + ) +; (completing-read "Section name: " ) + ;; ----- outline (defvar coq-outline-regexp @@ -621,10 +645,11 @@ This is specific to coq-mode." (proof-defshortcut coq-Intros "Intros " [(control ?i)]) (proof-defshortcut coq-Apply "Apply " [(control ?a)]) -(proof-defshortcut coq-begin-Section "Section " [(control ?s)]) +;(proof-defshortcut coq-begin-Section "Section " [(control ?s)]) +(define-key coq-keymap [(control ?s)] 'coq-insert-section) +(define-key coq-keymap [(control ?m)] 'coq-insert-module) (define-key coq-keymap [(control ?e)] 'coq-end-Section) -(define-key coq-keymap [(control ?m)] 'coq-Compile) (define-key coq-keymap [(control ?o)] 'coq-SearchIsos) (define-key coq-keymap [(control ?p)] 'coq-Print) (define-key coq-keymap [(control ?c)] 'coq-Check) |