diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/BUGS | 22 | ||||
| -rw-r--r-- | coq/README | 38 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 488 | ||||
| -rw-r--r-- | coq/coq.el | 840 | ||||
| -rw-r--r-- | coq/coqtags | 73 | ||||
| -rw-r--r-- | coq/example.v | 14 | ||||
| -rw-r--r-- | coq/todo | 42 | ||||
| -rw-r--r-- | coq/x-symbol-coq.el | 98 |
8 files changed, 1615 insertions, 0 deletions
diff --git a/coq/BUGS b/coq/BUGS new file mode 100644 index 00000000..2cec29af --- /dev/null +++ b/coq/BUGS @@ -0,0 +1,22 @@ +-*- mode:outline -*- + +* Coq Proof General Bugs + +See also ../BUGS for generic bugs. + +** With new syntax in Coq 7, comments at end of files cannot be processed. + +Leads to annoying retract/process questions when switching buffers. +Workaround: don't use a comment as the last line of the buffer, for now. + +** coqtags doesn't find all declarations. + +It cannot handle lists e.g., with "Parameter x,y:nat" it only tags x +but not y. [The same problem exists for legotags] Workaround: don't +rely too much on the etags mechanism. + +** With Coq 7, multiple file handling and auto-compilation is buggy + +** Surely others that aren't mentioned here... + + Please report them to bugs@proofgeneral.org diff --git a/coq/README b/coq/README new file mode 100644 index 00000000..0ba57bf4 --- /dev/null +++ b/coq/README @@ -0,0 +1,38 @@ +Coq Proof General + +Originally written by Healfdene Goguen. +Later contributions by Patrick Loiseleur, Pierre Courtieu, + David Aspinall + +Status: supported +Maintainer: Pierre Courtieu +Coq version: 6.3, 6.3.1, 7.x +Coq homepage: http://pauillac.inria.fr/coq/assis-eng.html + +======================================== + +Coq Proof General has experimental multiple file handling for 6.3 +versions. It does not have support for proof by pointing. + +There is support for X Symbol, but not using a proper token language. + +There is a tags program, coqtags. + +======================================== + +Installation notes: + +Check the values of coq-tags and coq-prog-name in coq.el to see that +they correspond to the paths for coqtop and the library on your system. + +Install coqtags in a standard place or add <proof-home>/coq to your PATH. +NB: You may need to change the path to perl at the top of the file. + +Generate a TAGS file for the library by running + coqtags `find . -name \*.v -print` +in the root directory of the library, $COQTOP/theories. + + +======================================== + +$Id$ diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el new file mode 100644 index 00000000..e8f1fe64 --- /dev/null +++ b/coq/coq-syntax.el @@ -0,0 +1,488 @@ +;; coq-syntax.el Font lock expressions for Coq +;; Copyright (C) 1997, 1998 LFCS Edinburgh. +;; Authors: Thomas Kleymann and Healfdene Goguen +;; Maintainer: Pierre Courtieu <courtieu@lri.fr> + +;; $Id$ + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defvar coq-keywords-decl + '("Axiom[s]?" + "Hypotheses" + "Hypothesis" + "Parameter[s]?" + "Variable[s]?" + "Global\\s-+Variable" + ;;added tactic def here because it needs Reset to be undone correctly + "Tactic\\s-+Definition")) + +(defvar coq-keywords-defn + '("CoFixpoint" + "CoInductive" + "Fixpoint" + "Inductive" + "Inductive\\s-+Set" + "Inductive\\s-+Prop" + "Inductive\\s-+Type" + "Mutual\\s-+Inductive" + "Record" + "Scheme" + "Syntactic\\-+Definition" + "Structure")) + +(defvar coq-keywords-goal + '("Chapter" + "Section" + "Correctness" + "Definition" + "Fact" + "Goal" + "Lemma" + "Local" + "Remark" + "Theorem")) + +(defvar coq-keywords-save + '("Defined" + "Save" + "Qed" + "End")) + +(defvar coq-keywords-kill-goal + '("Abort")) + + + + +(defcustom coq-user-state-changing-commands nil + "List of user-defined Coq commands that need to be backtracked; +like Require, Definition, etc... + +For example if MyHint and MyRequire are user defined variants of the +Hint and Require commands, put the following line in your .emacs: + + (setq coq-user-state-changing-commands '(\"MyHint\" \"MyRequire\"))" + :type '(repeat regexp) + :group 'coq) + + +(defcustom coq-user-state-preserving-commands nil + "List of user defined Coq commands that do not need to be backtracked; +like Print, Check, Show etc... + +For example if MyPrint and MyCheck are user defined variants of the +Print and Check commands, put the following line in your .emacs: + + (setq coq-user-state-preserving-commands '(\"MyPrint\" \"MyCheck\"))" + :type '(repeat regexp) + :group 'coq) + +;; + +(defvar coq-keywords-state-preserving-commands + (append '("(*" ;;Pierre comments must not be undone + "Add\\s-+LoadPath" + "Add\\s-+ML\\s-+Path" + "Add\\s-+Rec\\s-+ML\\s-+Path" + "Add\\s-+Rec\\s-+LoadPath" + "Cd" + "Check" + "DelPath" + "Eval" + "Extraction" + "Extraction Module" + "Focus" ;; ??? + "Hint\\-+Rewrite" + "Inspect" + "Locate" + "Locate\\s-+File" + "Locate\\s-+Library" + "Opaque" + "Print" + "Proof" + "Recursive\\-+Extraction" + "Recursive\\-+Extraction\\-+Module" + "Remove\\-+LoadPath" + "Pwd" + "Qed" + "Reset" + "Save" + "Search" + "SearchIsos" + "SearchPattern" + "SearchRewrite" + "Set\\-+Hyps_limit" + "Set\\-+Undo" + "Set\\-+Set\\-+Printing\\-+Coercion[^s]" + "Show" + "Test\\s-+Printing\\s-+If" + "Test\\s-+Printing\\s-+Let" + "Test\\s-+Printing\\s-+Synth" + "Test\\s-+Printing\\s-+Wildcard" + "Unfocus" ; ??? + "Unset\\s-+Hyps_limit" + "Unset\\s-+Undo" + "Unset\\s-+Printing\\s-+Coercion[^s]" + "Transparent" + "Write\\s-+State") + coq-user-state-preserving-commands)) + +(defvar coq-keywords-state-changing-misc-commands + '("Add\\s-+Abstract\\s-+Ring" + "Add\\s-+Abstract\\s-+Semi\\s-+Ring" + "Add\\s-+Field" + "Add\\s-+Morphism" + "Add\\s-+Printing" + "Add\\s-+Ring" + "Add\\s-+Semi\\s-+Ring" + "Add\\s-+Setoid" + "Begin\\s-+Silent" + "Canonical\\s-+Structure" + "CoFixpoint" + "CoInductive" + "Coercion" + "Declare\\s-+ML\\s-+Module" + "End\\s-+Silent" + "Derive\\s-+Dependent\\s-+Inversion" + "Derive\\s-+Dependent\\s-+Inversion_clear" + "Derive\\s-+Inversion" + "Derive\\s-+Inversion_clear" + "Extract\\s-+Constant" + "Extract\\s-+Inductive" + "Extraction\\s-+Inline" + "Extraction\\s-+Language" + "Extraction\\s-+NoInline" + "Grammar" + "Hint" + "Hints" + "Identity\\s-+Coercion" + "Implicit\\s-+Arguments\\s-+Off" + "Implicit\\s-+Arguments\\s-+On" + "Implicits" + "Infix" + "Load" + "Read\\s-+Module" + "Remove\\s-+LoadPath" + "Remove\\s-+Printing\\s-+If\\s-+ident" + "Remove\\s-+Printing\\s-+Let\\s-+ident" + "Require" + "Require\\s-+Export" + "Reset\\s-+Extraction\\s-+Inline" + "Reset\\s-+Initial" + "Restart" + "Restore\\s-+State" + "Remove\\s-+Printing\\s-+If\\s-+ident" + "Remove\\s-+Printing\\s-+Let\\s-+ident" + "Restore\\s-+State" + "Set\\s-+Extraction\\s-+AutoInline" + "Set\\s-+Extraction\\s-+Optimize" + "Set\\s-+Implicit\\s-+Arguments" + "Set\\s-+Printing\\s-+Coercions" + "Set\\s-+Printing\\s-+Synth" + "Set\\s-+Printing\\s-+Wildcard" + "Unset\\s-+Extraction\\s-+AutoInline" + "Unset\\s-+Extraction\\s-+Optimize" + "Unset\\s-+Implicit\\s-+Arguments" + "Unset\\s-+Printing\\s-+Coercions" + "Unset\\s-+Printing\\s-+Synth" + "Unset\\s-+Printing\\s-+Wildcard" + "Syntax" + "Transparent")) + + + + +(defvar coq-keywords-state-changing-commands + (append + coq-keywords-state-changing-misc-commands + coq-keywords-decl + coq-keywords-defn + coq-keywords-goal + coq-user-state-changing-commands + ) + ) + +(defvar coq-keywords-commands + (append coq-keywords-state-changing-commands + coq-keywords-state-preserving-commands) + "All commands keyword.") + + +(defcustom coq-user-state-changing-tactics nil + "List of user defined Coq tactics that need to be backtracked; +like almost all tactics, but \"Idtac\" (\"Proof\" is a command actually). + +For example if MyIntro and MyElim are user defined variants of the +Intro and Elim tactics, put the following line in your .emacs: + + (setq coq-user-state-changing-tactics '(\"MyIntro\" \"MyElim\"))" + :type '(repeat regexp) + :group 'coq) + +(defvar coq-state-changing-tactics + (append '("Absurd" + "Apply" + "Assert" + "Assumption" + "Auto" + "AutoRewrite" + "Case" + "Cbv" + "Change" + "Clear" + "ClearBody" + "Cofix" + "Compare" + "Compute" + "Constructor" + "Contradiction" + "Cut" + "CutRewrite" + ;;"DHyp" + ;;"DInd" + "Decide Equality" + "Decompose" + "Dependent Inversion" + "Dependent Inversion_clear" + "Dependent Rewrite ->" + "Dependent Rewrite <-" + "Dependent\\s-+Inversion" + "Dependent\\s-+Inversion_clear" + "Destruct" + "DiscrR" + "Discriminate" + "Double\\-+Induction" + "EApply" + "EAuto" + "Elim" + "ElimType" + "Exact" + "Exists" + "Field" + "Fix" + "Fold" + "Fourier" + "Generalize" + "Hnf" + "Induction" + "Injection" + "Intro[s]?" + "Intuition" + "Inversion" + "Inversion_clear" + "LApply" + "Lazy" + "Left" + "LetTac" + "Linear" + "Load" + "Move" + "NewDestruct" + "NewInduction" + "Omega " + "Pattern" + "Pose" + "Program" + "Program_all" + "Prolog" + "Quote" + "Realizer" + "Red" + "Refine" + "Reflexivity" + "Rename" + "Replace" + "Resume" + "Rewrite" + "Right" + "Ring" + "Setoid_replace" + "Simpl" + "Simple Inversion" + "Simplify_eq" + "Specialize" + "Split" + "SplitAbsolu" + "SplitRmult" + "Suspend" + "Symmetry" + "Tauto" + "Transitivity" + "Trivial" + "Unfold") + coq-user-state-changing-tactics)) + +(defcustom coq-user-state-preserving-tactics nil + "List of user defined Coq tactics that do not need to be backtracked; +like \"Idtac\" (no other one to my knowledge ?). + +For example if MyIdtac and Do_nthing are user defined variants of the +Idtac (Nop) tactic, put the following line in your .emacs: + + (setq coq-user-state-preserving-tactics '(\"MyIdtac\" \"Do_nthing\"))" + :type '(repeat regexp) + :group 'coq) + +(defvar coq-state-preserving-tactics + (append '("Idtac") + coq-user-state-preserving-tactics)) + +(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-tacticals + '("Abstract" + "Do" + "Idtac" ; also in state-preserving-tactic + "Orelse" + "Repeat" + "Try") + "Keywords for tacticals in a Coq script.") + +(defvar coq-reserved + '("as" + "ALL" + "Cases" + "EX" + "else" + "end" + "Fix" + "if" + "in" + "into" + "let" + "of" + "then" + "using" + "with") + "Reserved keyworkds of Coq.") + +(defvar coq-symbols + '("|" + ":" + ";" + "," + "(" + ")" + "[" + "]" + "{" + "}" + ":=" + "=>" + "->" + ".") + "Punctuation Symbols used by Coq.") + +;; ----- regular expressions +(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\|Anomaly\\|Uncaught exception\\|Toplevel input\\)" + "A regexp indicating that the Coq process has identified an error.") + +(defvar coq-id proof-id) + +(defvar coq-ids (proof-ids coq-id)) + +(defun coq-first-abstr-regexp (paren) + (concat paren "\\s-*\\(" coq-ids "\\)\\s-*:")) + +(defun coq-next-abstr-regexp () + (concat ";[ \t]*\\(" coq-ids "\\)\\s-*:")) + +(defvar coq-font-lock-terms + (list + ;; lambda binders + (list (coq-first-abstr-regexp "\\[") 1 'font-lock-variable-name-face) + ;; Pi binders + (list (coq-first-abstr-regexp "(") 1 'font-lock-variable-name-face) + ;; second, third, etc. abstraction for Lambda of Pi binders + (list (coq-next-abstr-regexp) 1 'font-lock-variable-name-face) + ;; Kinds + (cons "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" 'font-lock-type-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 + (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-save))) +(defconst coq-save-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp coq-keywords-save) + "\\)\\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-*[:]?")) + ;; Papageno : ce serait plus propre d'omettre le `:' + ;; uniquement pour Correctness + ;; et pour Definition f [x,y:nat] := body +(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 "\\)\\s-*[[:]")) +(defvar coq-font-lock-keywords-1 + (append + coq-font-lock-terms + (list + (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-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 coq-reserved) '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-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 ?\' "_") + (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")) + +(provide 'coq-syntax) +;;; coq-syntax.el ends here diff --git a/coq/coq.el b/coq/coq.el new file mode 100644 index 00000000..89120a1e --- /dev/null +++ b/coq/coq.el @@ -0,0 +1,840 @@ +;; coq.el Major mode for Coq proof assistant +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Author: Healfdene Goguen +;; Maintainer: Pierre Courtieu <courtieu@lri.fr> + +;; $Id$ + +(require 'proof) +(require 'coq-syntax) + +;; Configuration + +(setq tags-always-exact t) ; Tags is unusable with Coq library otherwise: + +(defun coq-library-directory () + (let ((c (substring (shell-command-to-string "coqtop -where") 0 -1 ))) + (if (string-match c "not found") + "/usr/local/lib/coq" + c))) + + +(defcustom coq-tags (concat (coq-library-directory) "/theories/TAGS") + "the default TAGS table for the Coq library" + :type 'string + :group 'coq) + +(defconst coq-interrupt-regexp "User Interrupt." + "Regexp corresponding to an interrupt") + +(defcustom coq-default-undo-limit 100 + "Maximum number of Undo's possible when doing a proof." + :type 'number + :group 'coq) + +;; ----- web documentation + +(defcustom coq-www-home-page "http://coq.inria.fr/" + "Coq home page URL." + :type 'string + :group 'coq) + +;; ----- coq specific menu + +(defpgdefault menu-entries + '(["Print..." coq-Print t] + ["Check..." coq-Check t] + ["Hints" coq-PrintHint t] + ["Intros..." coq-Intros t] + ["Show ith goal..." coq-Show t] + ["Apply" coq-Apply t] + ["Search isos/pattern..." coq-SearchIsos t] + ["Begin Section..." coq-begin-Section t] + ["End Section" coq-end-Section t] + ["Compile" coq-Compile t])) + + +;; ----- coq-shell configuration options + +(defcustom coq-prog-name "coqtop -emacs" + "*Name of program to run as Coq." + :type 'string + :group 'coq) + +;; Command to initialize the Coq Proof Assistant +(defconst coq-shell-init-cmd + (format "Set Undo %s. " coq-default-undo-limit)) + + +;;Pierre: we will have both versions V6 and V7 during a while +;; the test with "coqtop -v" can be skipped if the variable +;; coq-version-is-V7 is already set (usefull for people +;; dealing with several version of coq) +(if (boundp 'coq-version-is-V7) () ; if this variable is bound, do nothing + (setq coq-version-is-V7 ; else test with "coqtop -v" + (if (string-match "version 7" (shell-command-to-string (concat coq-prog-name " -v"))) + (progn (message "coq is V7") t) + (progn (message "coq is not V7") nil)))) + +;; Command to reset the Coq Proof Assistant +;; Pierre: added Impl... because of a bug of Coq until V6.3 +;; (included). The bug is already fixed in the next version (V7). So +;; we will backtrack this someday. +(defconst coq-shell-restart-cmd + "Reset Initial.\n Implicit Arguments Off. ") + +(defvar coq-shell-prompt-pattern (concat "^" proof-id " < ") + "*The prompt pattern for the inferior shell running coq.") + +;; FIXME da: this was disabled (set to nil) -- why? +(defvar coq-shell-cd "Cd \"%s\". " + "*Command of the inferior process to change the directory.") + +(defvar coq-shell-abort-goal-regexp "Current goal aborted" + "*Regexp indicating that the current goal has been abandoned.") + +(defvar coq-shell-proof-completed-regexp "Subtree proved!" + "*Regular expression indicating that the proof has been completed.") + +(defvar coq-goal-regexp + "\\(============================\\)\\|\\(subgoal [0-9]+ is:\\)\n") + +;; ----- outline + +(defvar coq-outline-regexp + (concat "(\\*\\|" (proof-ids-to-regexp + '( +"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Hint" "Hints" "Hypothesis" "Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" "Remark" "Record" "Inductive" "Mutual" "Definition" "Fixpoint" "Save" "Qed" "Defined" "End" "Coercion")))) + +(defvar coq-outline-heading-end-regexp "\\*\)\n\\|\\.\n") + +(defvar coq-shell-outline-regexp coq-goal-regexp) +(defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) + +(defconst coq-kill-goal-command "Abort. ") +(defconst coq-forget-id-command "Reset %s. ") +(defconst coq-back-n-command "Back %s. ") ; Pierre: added + + + +(defconst coq-state-changing-tactics-regexp + (proof-ids-to-regexp coq-state-changing-tactics)) +(defconst coq-state-preserving-tactics-regexp + (proof-ids-to-regexp coq-state-preserving-tactics)) +(defconst coq-tactics-regexp + (proof-ids-to-regexp coq-tactics)) +(defconst coq-state-changing-commands-regexp + (proof-ids-to-regexp coq-keywords-state-changing-commands)) +(defconst coq-state-preserving-commands-regexp + (proof-ids-to-regexp coq-keywords-state-preserving-commands)) +(defvar coq-retractable-instruct-regexp + (proof-ids-to-regexp coq-retractable-instruct)) +(defvar coq-non-retractable-instruct-regexp + (proof-ids-to-regexp coq-non-retractable-instruct)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(eval-and-compile + (define-derived-mode coq-shell-mode proof-shell-mode + "coq-shell" nil + (coq-shell-mode-config))) + +(eval-and-compile + (define-derived-mode coq-response-mode proof-response-mode + "CoqResp" nil + (coq-response-config))) + +(eval-and-compile + (define-derived-mode coq-mode proof-mode + "coq" nil + (coq-mode-config))) + +(eval-and-compile + (define-derived-mode coq-goals-mode proof-goals-mode + "CoqGoals" nil + (coq-goals-mode-config))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Code that's coq specific ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun coq-set-undo-limit (undos) + (proof-shell-invisible-command (format "Set Undo %s. " undos))) + +;; +;; FIXME Papageno 05/1999: must take sections in account. +;; +;; da: have now combined count-undos and find-and-forget, they're the +;; same now we deal with nested proofs and send general sequence +;; "Abort. ... Abort. Back n. Undo n." +;; + +(defconst coq-keywords-decl-defn-regexp + (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn)) + "Declaration and definition regexp.") + +;; 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. + +(defun coq-goal-command-p (str) + "Decide whether argument is a goal or not" + (and (proof-string-match coq-goal-command-regexp str) + (not (proof-string-match "Definition.*:=" str)) + (not (proof-string-match "Recursive Definition" str)) + ;; da: 3.4 test: do not exclude Lemma: we want goal-command-p to + ;; succeed for nested goals too now. + ;; (should we also exclude Definition?) + (not (proof-string-match "Lemma.*:=" str)))) +;; )) + + +; Pierre: This is a try, for use in find-and-forget. It seems to work but +; is it correct with respect to the asynchronous communication between Coq +; and emacs? +; DA: should be okay, communication is not as asynchronous as you think +(defun coq-proof-mode-p () + "Allows to know if we are currentlly in proof mode. +Look at the last line of the *coq* buffer to see if the prompt +is the toplevel \"Coq <\". Returns nil if yes. +This assumes that no \"Resume\" command has been used." + (not (string-match "^Coq < " proof-shell-last-prompt))) + + +;; TODO : add the stuff to handle the "Correctness" command + +;; Pierre: May 29 2002 added a "Back n. " command in order to +;; synchronize more accurately. + +;; DA: rewrote to combine behaviour with count-undos, to work with +;; nested proofs. + +(defun coq-find-and-forget (span) + (let (str ans (naborts 0) (nbacks 0) (nundos 0)) + (while (and span (not ans)) + (setq str (span-property span 'cmd)) + (cond + ((eq (span-property span 'type) 'comment)) + + ;; FIXME: combine with coq-keywords-decl-defn-regexp case below? + ;; [ Maybe not: Section is being treated as a _goal_ command + ;; now, so this test has to appear before the goalsave ] + ((proof-string-match + (concat "Section\\s-+\\(" proof-id "\\)\\s-*") str) + (unless (eq (span-property span 'type) 'goalsave) + ;; If we're resetting to beginning of a section from + ;; inside, need to fix the nesting depth. + ;; FIXME: this is not good enough: the scanning loop + ;; exits immediately but Reset has implicit Aborts + ;; which are not being counted here. Really + ;; we need to set the "master reset" command which + ;; subsumes the others, but still count the depth. + (decf proof-nesting-depth)) + (setq ans (format coq-forget-id-command (match-string 2 str)))) + + ((eq (span-property span 'type) 'goalsave) + ;; Note da 6.10.99: in Lego and Isabelle, it's trivial to forget an + ;; unnamed theorem. Coq really does use the identifier + ;; "Unnamed_thm", though! So we don't need this test: + ;;(unless (eq (span-property span 'name) proof-unnamed-theorem-name) + + ;; da: try using just Back since "Reset" causes loss of proof + ;; state. + ;; (format coq-forget-id-command (span-property span 'name))) + (if (span-property span 'nestedundos) + (setq nbacks (+ 1 nbacks (span-property span 'nestedundos))))) + + ;; Unsaved goal commands: each time we hit one of these + ;; we need to issue Abort to drop the proof state. + ((coq-goal-command-p str) + (incf naborts)) + + ;; If we are already outside a proof, issue a Reset. + ;; [ improvement would be to see if the undoing + ;; will take us outside a proof, and use the first + ;; Reset found if so: but this is tricky to co-ordinate + ;; with the number of Backs, perhaps? ] + ((and + (not (coq-proof-mode-p));; (eq proof-nesting-depth 0) + (proof-string-match + (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" + proof-id + ;; Section .. End Section should be atomic! + "\\)\\s-*[\\[,:.]") str)) + (setq ans (format coq-forget-id-command (match-string 2 str)))) + + ;; FIXME: combine with coq-keywords-decl-defn-regexp case above? + ;; If it's not a goal but it contains "Definition" then it's a + ;; declaration [ da: is this not covered by above case??? ] + ((and (not (coq-proof-mode-p));; (eq proof-nesting-depth 0) + (proof-string-match + (concat "Definition\\s-+\\(" proof-id "\\)\\s-*") str)) + (setq ans (format coq-forget-id-command (match-string 2 str)))) + + ;; Outside a proof: cannot be a tactic, if unknown: do back + ;; (we may decide otherwise, it is false anyhow, use elisp + ;; vars instead for the perfect thing). + ((and (not (coq-proof-mode-p)) + (not (proof-string-match + (concat "\\`\\(" + coq-state-preserving-commands-regexp + "\\)") + str))) + (incf nbacks)) + + ;; inside a proof: if known command then back or nothing (depending + ;; on the command), + ;; if known "need not undo tactic" then nothing + ;; otherwise : undo (unknown tactics are considered needing undo, + ;; which is ok at 99%, use elisp vars for the + ;; 1% remaining). + ;; no undo if abort + ((coq-proof-mode-p) + (cond + ((proof-string-match + (concat "\\`\\(" coq-state-changing-commands-regexp "\\)") + str) + (incf nbacks)) + ((and (eq 0 naborts) + (not (proof-string-match + (concat "\\`\\(" coq-state-preserving-commands-regexp "\\)") + str)) + (not (proof-string-match + (concat "\\`\\(" coq-state-preserving-tactics-regexp "\\)") + str))) + (incf nundos)) + )) + ) + (setq span (next-span span 'type))) + + ;; Now adjust proof-nesting depth according to the + ;; number of proofs we've passed out of. + ;; FIXME: really this adjustment should be on the + ;; successful completion of the Abort commands, as + ;; a callback. + (setq proof-nesting-depth (- proof-nesting-depth naborts)) + + (setq ans + (concat + (if (stringp ans) ans) + (if (> naborts 0) + ;; ugly, but blame Coq + (let ((aborts "Abort. ")) + (while (> (decf naborts) 0) + (setq aborts (concat "Abort. " aborts))) + aborts)) + (if (> nbacks 0) + (concat "Back " (int-to-string nbacks) ". ")) + (if (> nundos 0) + (concat "Undo " (int-to-string nundos) ". ")))) + + (if (null ans) + proof-no-command;; FIXME: this is an error really (assert nil) + ans))) + + +(defvar coq-current-goal 1 + "Last goal that emacs looked at.") + +(defun coq-goal-hyp () + (cond + ((looking-at "============================\n") + (goto-char (match-end 0)) + (cons 'goal (int-to-string coq-current-goal))) + ((looking-at "subgoal \\([0-9]+\\) is:\n") + (goto-char (match-end 0)) + (cons 'goal (match-string 1)) + (setq coq-current-goal (string-to-int (match-string 1)))) + ((looking-at proof-shell-assumption-regexp) + (cons 'hyp (match-string 1))) + (t nil))) + +(defun coq-state-preserving-p (cmd) + (not (proof-string-match coq-retractable-instruct-regexp cmd))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to coq ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun coq-SearchIsos () + "Search a term whose type is isomorphic to given type +This is specific to coq-mode." + (interactive) + (let (cmd) + (proof-shell-ready-prover) + (setq cmd (read-string + (if coq-version-is-V7 "SearchPattern: " "SearchIsos: ") + nil 'proof-minibuffer-history)) + (proof-shell-invisible-command + (format (if coq-version-is-V7 "SearchPattern %s. " + "SearchIsos %s. ") cmd)))) + + +(defun coq-guess-or-ask-for-string (s) + (let ((guess + (if (region-exists-p) + (buffer-substring-no-properties (region-beginning) (region-end)) + (symbol-near-point)))) + (read-string + (if guess (concat s " (" guess "):")(concat s ":")) + nil 'proof-minibuffer-history guess)) + ) + +(defun coq-Print () + "Ask for an ident and print the corresponding term" + (interactive) + (let (cmd) + (proof-shell-ready-prover) + (setq cmd (coq-guess-or-ask-for-string "Print")) + (proof-shell-invisible-command + (format "Print %s. " cmd)))) + +(defun coq-Check () + "Ask for a term and print its type" + (interactive) + (let (cmd) + (proof-shell-ready-prover) + (setq cmd (coq-guess-or-ask-for-string "Check")) + (proof-shell-invisible-command + (format "Check %s. " cmd)))) + +(defun coq-Show () + "Ask for a number i and show the ith goal" + (interactive) + (let (cmd) + (proof-shell-ready-prover) + (setq cmd (read-string "Show Goal number: " nil 'proof-minibuffer-history)) + (proof-shell-invisible-command + (format "Show %s. " cmd)))) + +(defun coq-PrintHint () + "Print all hints applicable to the current goal" + (interactive) + (proof-shell-invisible-command "Print Hint. ")) + + +(defun coq-end-Section () + "Ends a Coq section." + (interactive) + (let ((count 1)) ; The number of section already "Ended" + 1 + (let ((section + (save-excursion + (progn + (while (and (> count 0) + (search-backward-regexp + "Chapter\\|Section\\|End" 0 t)) + (if (char-equal (char-after (point)) ?E) + (setq count (1+ count)) + (setq count (1- count)))) + (buffer-substring-no-properties + (progn (beginning-of-line) (forward-word 1) (point)) + (progn (end-of-line) (point))))))) + (insert (concat "End" section))))) + +(defun coq-Compile () + "compiles current buffer" + (interactive) + (let* ((n (buffer-name)) + (l (string-match ".v" n))) + (compile (concat "make " (substring n 0 l) ".vo")))) + +(proof-defshortcut coq-Intros "Intros " [(control ?i)]) +(proof-defshortcut coq-Apply "Apply " [(control ?a)]) +(proof-defshortcut coq-begin-Section "Section " [(control ?s)]) + +(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) +(define-key coq-keymap [(control ?h)] 'coq-PrintHint) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Indentation ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; FIXME mmw: code disabled; Is the new indentation scheme general +;; enough to handle Coq as well? + +;;; "Case" is represented by 'c' on the stack, and +;;; "CoInductive" is represented by 'C'. +;(defun coq-stack-to-indent (stack) +; (cond +; ((null stack) 0) +; ((null (car (car stack))) +; (nth 1 (car stack))) +; (t (let ((col (save-excursion +; (goto-char (nth 1 (car stack))) +; (current-column)))) +; (cond +; ((eq (car (car stack)) ?c) +; (save-excursion (move-to-column (current-indentation)) +; (cond +; ((eq (char-after (point)) ?|) (+ col 3)) +; ((proof-looking-at "end") col) +; (t (+ col 5))))) +; ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C)) +; (+ col (if (eq ?| (save-excursion +; (move-to-column (current-indentation)) +; (char-after (point)))) 2 4))) +; (t (1+ col))))))) +; +;(defun coq-parse-indent (c stack) +; (cond +; ((eq c ?C) +; (cond ((proof-looking-at "Case") +; (cons (list ?c (point)) stack)) +; ((proof-looking-at "CoInductive") +; (forward-char (length "CoInductive")) +; (cons (list c (- (point) (length "CoInductive"))) stack)) +; (t stack))) +; ((and (eq c ?e) (proof-looking-at "end") (eq (car (car stack)) ?c)) +; (cdr stack)) +; +; ((and (eq c ?I) (proof-looking-at "Inductive")) +; (forward-char (length "Inductive")) +; (cons (list c (- (point) (length "Inductive"))) stack)) +; +; ((and (eq c ?.) (or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C))) +; (cdr stack)) +; +; (t stack))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; 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))) + (if (file-exists-p (concat dir "Makefile")) + (let* + ((compiled-file (concat (substring + filename 0 + (string-match ".v$" filename)) ".vo")) + (command (shell-command-to-string + (concat "cd " dir ";" + "gmake -n -W " filename " " compiled-file + "| sed s/coqc/coqtop/")))) + (concat + (substring command 0 (string-match " [^ ]*$" command)) + " -emacs")) + coq-prog-name))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Coq shell startup and exit hooks ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun coq-pre-shell-start () + (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) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Configuring proof and pbp mode and setting up various utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun coq-mode-config () + + (setq proof-terminal-char ?\.) + (setq proof-script-command-end-regexp + (if coq-version-is-V7 "[.]\\([ \t\n\r]\\)\\|[.]\\'" "[.]")) + (setq proof-script-comment-start "(*") + (setq proof-script-comment-end "*)") + (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name + + (setq proof-assistant-home-page coq-www-home-page) + + (setq proof-mode-for-script 'coq-mode) + + (setq proof-guess-command-line 'coq-guess-command-line) + + ;; Commands sent to proof engine + (setq proof-showproof-command "Show. " + proof-context-command "Print All. " + proof-goal-command "Goal %s. " + proof-save-command "Save %s. " + proof-find-theorems-command "Search %s. ") +;; FIXME da: Does Coq have a help or about command? +;; proof-info-command "Help" + +;; 3.4: this is no longer used: setting to nil +;; enforces use of find-and-forget always. + (setq proof-kill-goal-command nil) + + (setq proof-goal-command-p 'coq-goal-command-p + proof-find-and-forget-fn 'coq-find-and-forget + pg-topterm-goalhyp-fn 'coq-goal-hyp + proof-state-preserving-p 'coq-state-preserving-p) + + (setq proof-save-command-regexp coq-save-command-regexp + proof-save-with-hole-regexp coq-save-with-hole-regexp + proof-goal-with-hole-regexp coq-goal-with-hole-regexp + proof-nested-undo-regexp coq-state-changing-commands-regexp) + + (setq + proof-indent-close-offset -1 + proof-indent-any-regexp + (proof-regexp-alt (proof-ids-to-regexp + (append (list "Cases" "end") coq-keywords)) "\\s(" "\\s)") + proof-indent-enclose-regexp "|" + proof-indent-open-regexp + (proof-regexp-alt (proof-ids-to-regexp '("Cases")) "\\s(") + proof-indent-close-regexp + (proof-regexp-alt (proof-ids-to-regexp '("end")) "\\s)")) + + ;; span menu + (setq + proof-script-span-context-menu-extensions 'coq-create-span-menu) + + ;; (setq proof-auto-multiple-files t) ; until Coq has real support + ;; da: Experimental support for multiple files based on discussions + ;; at TYPES 2000. + ;; (Pierre, please fix this as Coq users would like, and for Coq V7 !) + (setq coq-proof-shell-inform-file-processed-cmd + "Reset Initial. Compile Module %m. ") + ;; FIXME da: Coq is rather quiet when reading files with "Load <foo>." + ;; and sometimes even Require seems quiet? PG would like some guarantees + ;; that messages are issued. Also, the code to guess the complete file + ;; name is flaky, would be better if Coq displayed full path info for PG. + (setq coq-proof-shell-process-file + ;; FIXME da: Coq output Reinterning message should not + ;; be suppressed by "Begin Silent" for PG, and should be + ;; marked by eager annotation (special char). + ;; For Coq 7, we should get rid of 8 bit chars in PG, too. + (cons "Reinterning \\(.+\\)\\.\\.\\.done" + (lambda (str) + (let* + ((modname (match-string 1 str)) + ;; FIXME: next lines will return a directory but maybe + ;; not right one if proof-script-buffer happens to be nil! + (buf (or proof-script-buffer + proof-previous-script-buffer)) + (dir (if (buffer-live-p buf) + (with-current-buffer buf + default-directory) + ;; This next guess is pretty hopeless. + default-directory))) + (message "%s%s.v" dir modname) + (format "%s%s.v" dir modname))))) + + (setq coq-proof-shell-inform-file-retracted-cmd + ;; da: This is a HORRIBLE fragile hack! Instead of issuing a + ;; command to the prover we have to run a "coqdep" command to + ;; find out the dependencies. + (lambda (fname) + (let* + ;; Assume buffer is in correct directory, assume current directory + ;; is writeable, assume we have GNU make, etc, etc. + ;; I hope Coq V7 will provide this operation for us as + ;; a builtin (it should print out a series of messages which + ;; are matched by proof-shell-retract-files-regexp, one for + ;; each dependency). + ;; [In fact, I think this is what should happen when + ;; Require is undone] + ((depstr + (substring (shell-command-to-string + (concat + "coqdep *.v | grep " + (file-name-nondirectory + (file-name-sans-extension fname)) ".v" + " | awk '{print $1}' | sed 's/.vo:/.v/'")) 0 -1)) + (deps (split-string depstr)) + (current-included proof-included-files-list)) + ;; Now hack the proof-included-files-list to remove the + ;; dependencies of the retracted file and remove the + ;; locked regions + ;; FIXME: this is too low-level delving in PG. Should + ;; do with proof-shell-retract-files-regexp really. + (mapcar (lambda (dep) + (setq proof-included-files-list + (delete (file-truename dep) + proof-included-files-list))) + deps) + (proof-restart-buffers + (proof-files-to-buffers + (set-difference current-included + proof-included-files-list))) + ;; Return a comment thingy inserted into the shell + ;; buffer to help debugging. + (format "Print (* Proof General ran coqdep command for %s, result: %s. Removed files: %s *)" fname depstr deps)))) + + + ;;Coq V7 changes this + (setq proof-shell-start-silent-cmd + (if coq-version-is-V7 "Set Silent. " "Begin Silent. ") + proof-shell-stop-silent-cmd + (if coq-version-is-V7 "Unset Silent. " "End Silent. ")) +; (setq proof-shell-start-silent-cmd "Begin Silent. " +; proof-shell-stop-silent-cmd "End Silent. ") + + (coq-init-syntax-table) + +;; font-lock + + (setq font-lock-keywords coq-font-lock-keywords-1) + + (proof-config-done) + +;; outline + + (make-local-variable 'outline-regexp) + (setq outline-regexp coq-outline-regexp) + + (make-local-variable 'outline-heading-end-regexp) + (setq outline-heading-end-regexp coq-outline-heading-end-regexp) + +;; tags + (and (boundp 'tag-table-alist) + (setq tag-table-alist + (append '(("\\.v$" . coq-tags) + ("coq" . coq-tags)) + tag-table-alist))) + + (setq blink-matching-paren-dont-ignore-comments t) + +;; hooks and callbacks + + (add-hook 'proof-pre-shell-start-hook 'coq-pre-shell-start nil t)) + + + +(defun coq-shell-mode-config () + (setq + proof-shell-prompt-pattern coq-shell-prompt-pattern + proof-shell-cd-cmd coq-shell-cd + proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) + proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp + proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp + proof-shell-error-regexp coq-error-regexp + proof-shell-interrupt-regexp coq-interrupt-regexp + proof-shell-assumption-regexp coq-id + pg-subterm-first-special-char ?\360 + proof-shell-wakeup-char ?\371 ; done: prompt + ;; The next three represent path annotation information + pg-subterm-start-char ?\372 ; not done + pg-subterm-sep-char ?\373 ; not done + pg-subterm-end-char ?\374 ; not done + pg-topterm-char ?\375 ; done + proof-shell-eager-annotation-start "\376\\|\\[Reinterning" + proof-shell-eager-annotation-start-length 12 + proof-shell-eager-annotation-end "\377\\|done\\]" ; done + proof-shell-annotated-prompt-regexp + (concat proof-shell-prompt-pattern + (char-to-string proof-shell-wakeup-char)) ; done + proof-shell-result-start "\372 Pbp result \373" + proof-shell-result-end "\372 End Pbp result \373" + proof-shell-start-goals-regexp "[0-9]+ subgoals?" + proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp + proof-shell-init-cmd ; (concat + coq-shell-init-cmd + ; Coq has no global settings? + ; (proof-assistant-settings-cmd)) + proof-shell-restart-cmd coq-shell-restart-cmd + pg-subterm-anns-use-stack t) + + (coq-init-syntax-table) + (setq font-lock-keywords coq-font-lock-keywords-1) + + (proof-shell-config-done)) + +(defun coq-goals-mode-config () + (setq pg-goals-change-goal "Show %s. ") + (setq pg-goals-error-regexp coq-error-regexp) + (coq-init-syntax-table) + (setq font-lock-keywords coq-font-lock-keywords-1) + (proof-goals-config-done)) + +(defun coq-response-config () + (coq-init-syntax-table) + (setq font-lock-keywords coq-font-lock-keywords-1) + (proof-response-config-done)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Flags and other settings for Coq. +;; + +;; da: neither of these work very well. +;; I think "time" must just be for special search isos top level, +;; and "Focus" on works during a proof, so sending the setting +;; at the start of a session is wrong. + +;(defpacustom time-search-isos nil +; "Whether to display timing of SearchIsos in Coq." +; :type 'boolean +; :setting ("Time. " . "Untime. ")) + +(defpacustom print-only-first-subgoal nil + "Whether to just print the first subgoal in Coq." + :type 'boolean + :setting ("Focus. " . "Unfocus. ")) + +(defpacustom auto-compile-vos nil + "Whether to automatically compile vos and track dependencies." + :type 'boolean + :eval (if coq-auto-compile-vos + (setq proof-shell-inform-file-processed-cmd + coq-proof-shell-inform-file-processed-cmd + proof-shell-process-file + coq-proof-shell-process-file + proof-shell-inform-file-retracted-cmd + coq-proof-shell-inform-file-retracted-cmd) + (setq proof-shell-inform-file-processed-cmd nil + proof-shell-process-file nil + proof-shell-inform-file-retracted-cmd nil))) + +(provide 'coq) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Subterm markup -- it was added to Coq by Healf, but got removed. +;; Let's try faking something by regexp matching. + +;; FIXME: not operational yet +(defun coq-fake-constant-markup () + "Markup constants in Coq goal output by matching on regexps. +This is a horrible and approximate way of doing subterm markup. +\(Code used to be in Coq, but got lost between versions 5 and 7). +This is a hook setting for `pg-after-fontify-output-hook' to +enable identifiers to be highlighted and allow useful +mouse activation." + (goto-char (point-min)) + (while (re-search-forward "\(\w+[^\w]\)" nil t) + (replace-match "\372\200\373\\1\374" nil t))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Context-senstive in-span menu additions +;; + +;; da: message to Pierre: I just put these in as examples, +;; maybe you can suggest some better commands to use on +;; `thm'. (Check maybe not much use since appears before +;; in the buffer anyway) +(defun coq-create-span-menu (span idiom name) + (if (string-equal idiom "proof") + (let ((thm (span-property span 'name))) + (list ;(vector + ; "Check" + ; `(proof-shell-invisible-command + ; ,(format "Check %s." thm))) + (vector + "Print Proof" + `(proof-shell-invisible-command + ,(format "Print Proof %s." thm))))))) + +;;; Local Variables: *** +;;; tab-width:2 *** +;;; indent-tabs-mode:nil *** +;;; End: *** + + diff --git a/coq/coqtags b/coq/coqtags new file mode 100644 index 00000000..6d874e9d --- /dev/null +++ b/coq/coqtags @@ -0,0 +1,73 @@ +#!/usr/bin/perl +# +# Or perhaps: /usr/local/bin/perl +# +# # $Id$ +# +undef $/; + +if($#ARGV<$[) {die "No Files\n";} +open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; + +while(<>) +{ + print "Tagging $ARGV\n"; + $a=$_; + $cp=1; + $lp=1; + $tagstring=""; + + while(1) + { + +# ---- Get the next statement starting on a newline ---- + + if($a=~/^[ \t\n]*\(\*/) + { while($a=~/^\s*\(\*/) + { $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/); + while($d>0 && $a=~/\(\*|\*\)/) + { $a=$'; $cp+=2+length $`; $lp+=(($wombat=$`)=~tr/\n/\n/); + if($& eq "(*") {$d++} else {$d--}; + } + if($d!=0) {die "Unbalanced Comment?";} + } + } + + if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;} + while($a=~/^\n/) {$cp++;$lp++;$a=$'} + + if($a=~/^[^\.]*\./) + { $stmt=$&; + $newa=$'; + $newcp=$cp+length $&; + $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); } + else { last;} + +# ---- The above embarrasses itself if there are semicolons inside comments +# ---- inside commands. Could do better. + +# print "----- (",$lp,",",$cp,")\n", $stmt, "\n"; + + if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem))\s+([\w\']+))\s*:/) + { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; } + + elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/) + { do adddecs($stmt,$1) } + + elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/) + { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; } + + $cp=$newcp; $lp=$newlp; $a=$newa; + } + print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; +} +close tagfile; + +sub adddecs { + $wk=$_[0]; + $tag=$_[1]; + $sep=","; + while($tst=($wk=~/\s*([\w\']+)\s*([,:\[])/) && $sep eq ",") + { $sep=$2; $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; } + 0; +} diff --git a/coq/example.v b/coq/example.v new file mode 100644 index 00000000..5a3c5b59 --- /dev/null +++ b/coq/example.v @@ -0,0 +1,14 @@ +(* + Example proof script for Coq Proof General. + + $Id$ +*) + +Goal (A,B:Prop)(A /\ B) -> (B /\ A). + Intros A B H. + Induction H. + Apply conj. + Assumption. + Assumption. +Save and_comms. + diff --git a/coq/todo b/coq/todo new file mode 100644 index 00000000..607c6729 --- /dev/null +++ b/coq/todo @@ -0,0 +1,42 @@ +-*- mode:outline -*- + +* Things to do for Coq + +See also ../todo for generic things to do, priority codes. + + +** B Proof-by-Pointing [1 month] + da: Yves Bertot told me that his CtCoq proof-by-pointing code + is in the Coq kernel now, so would be useful for PG. + We need a Coq hacker to do this. + Perhaps for new version of Coq. + da: I have old version of code sent to my by Healf. + Pierre: Since the code is to be changed, I suggest that we + wait for V7. + da: V7 is here now... + +** C Improve X-Symbol support. Integrate with Coq syntax mechanism somehow? + pierre: Yes, the greatest would be to allow users to easily declare + new tokens/symbols and add new grammar rules (Coq allows this) + including the declared tokens. Indeed when I define the type set, + and its element emptyset, and predicate In, I want to be able to say + that emptyset and In are new tokens and asociate them with the right + symbols. I want to be able of that on the fly (maybe we can use the + 'File Variables' feature of Emacs). Another thing is that we may ask + Coq developers to be unicode compliant or something like that. + + +** D Add Patrick Loiseleur's commands to search for vernac or ml files. + (they are in a separate file that is part of Coq distrib. + should I really integrate that in PG ? Patrick) + (maybe not if they're orthogonal to PG, but might help users - da) + +** D Add coq-add-tactic with a tactic name, which adds that tactic to the + undoable tactics and to the font-lock. (2h) + Pierre: I fixed this I think, by making a non-undoable regexp + instead. This solves the problem of tactics that have been defined + in another file. + +** D Improve coqtags. It cannot handle lists e.g., with + Parameter x,y:nat + it only tags x but not y. [The same problem exists for legotags] diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el new file mode 100644 index 00000000..7d2c245e --- /dev/null +++ b/coq/x-symbol-coq.el @@ -0,0 +1,98 @@ +;; x-symbol-coq.el +;; +;; David Aspinall, adapted from file supplied by David von Obheimb +;; +;; $Id$ +;; + +(defvar x-symbol-coq-symbol-table + '((perpendicular () "False" "\\<bottom>") + (top () "True" "\\<top>") + (notsign () "~" "\\<not>") + (longarrowright () "->" "\\<longrightarrow>") + (logicaland () "/\\" "\\<and>") + (logicalor () "\\/" "\\<or>") + (equivalence () "<->" "\\<equiv>") + (existential1 () "EX" "\\<exists>") + ;; some naughty ones, but probably what you'd like + ;; (a mess in words like "searching" !!) + (Gamma () "Gamma" "\\<Gamma>") + (Delta () "Delta" "\\<Delta>") + (Theta () "Theta" "\\<Theta>") + (Lambda () "Lambda" "\\<Lambda>") + (Pi () "Pi" "\\<Pi>") + (Sigma () "Sigma" "\\<Sigma>") + (Phi () "Phi" "\\<Phi>") + (Psi () "Psi" "\\<Psi>") + (Omega () "Omega" "\\<Omega>") + (alpha () "alpha" "\\<alpha>") + (beta () "beta" "\\<beta>") + (gamma () "gamma" "\\<gamma>") + (delta () "delta" "\\<delta>") + (epsilon1 () "epsilon" "\\<epsilon>") + (zeta () "zeta" "\\<zeta>") + (eta () "eta" "\\<eta>") + (theta1 () "theta" "\\<theta>") + (kappa1 () "kappa" "\\<kappa>") + (lambda () "lambda" "\\<lambda>") +; (mu () "mu" "\\<mu>") +; (nu () "nu" "\\<nu>") +; (xi () "xi" "\\<xi>") +; (pi () "pi" "\\<pi>") + (rho () "rho" "\\<rho>") + (sigma () "sigma" "\\<sigma>") + (tau () "tau" "\\<tau>") + (phi1 () "phi" "\\<phi>") +; (chi () "chi" "\\<chi>") + (psi () "psi" "\\<psi>") + (omega () "omega" "\\<omega>"))) + +;; All the stuff X-Symbol complains about +(defvar x-symbol-coq-master-directory 'ignore) +(defvar x-symbol-coq-image-searchpath '("./")) +(defvar x-symbol-coq-image-cached-dirs '("images/" "pictures/")) +(defvar x-symbol-coq-image-file-truename-alist nil) +(defvar x-symbol-coq-image-keywords nil) +(defvar x-symbol-coq-font-lock-keywords nil) +(defvar x-symbol-coq-header-groups-alist nil) +(defvar x-symbol-coq-class-alist + '((VALID "Coq Symbol" (x-symbol-info-face)) + (INVALID "no Coq Symbol" (red x-symbol-info-face)))) +(defvar x-symbol-coq-class-face-alist nil) +(defvar x-symbol-coq-electric-ignore nil) +(defvar x-symbol-coq-required-fonts nil) +(defvar x-symbol-coq-case-insensitive nil) +(defvar x-symbol-coq-extra-menu-items nil) +(defvar x-symbol-coq-token-grammar nil) +(defvar x-symbol-coq-input-token-grammar nil) +(defvar x-symbol-coq-generated-data nil) + + +;Pierre: let's try this, phi1 will be encoded, but not phia or +;philosophy. problem: blaphi will be encoded, +; other problem: false1 sholud not be encoded + +;(defvar x-symbol-coq-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]")) +(defvar x-symbol-coq-token-shape nil) + +(defvar x-symbol-coq-table x-symbol-coq-symbol-table) +(defvar x-symbol-coq-user-table nil) +(defun x-symbol-coq-default-token-list (tokens) tokens) +(defvar x-symbol-coq-token-list 'x-symbol-coq-default-token-list) +(defvar x-symbol-coq-input-token-ignore nil) + +;; internal stuff +(defvar x-symbol-coq-exec-specs nil) +(defvar x-symbol-coq-menu-alist nil) +(defvar x-symbol-coq-grid-alist nil) +(defvar x-symbol-coq-decode-atree nil) +(defvar x-symbol-coq-decode-alist nil) +(defvar x-symbol-coq-encode-alist nil) +(defvar x-symbol-coq-nomule-decode-exec nil) +(defvar x-symbol-coq-nomule-encode-exec nil) + +(warn "Coq support for X-Symbol is highly incomplete! Please help improve it! +Send improvements to x-symbol-coq.el to proofgen@dcs.ed.ac.uk") + + +(provide 'x-symbol-coq) |