diff options
-rw-r--r-- | coq/coq-syntax.el | 16 | ||||
-rw-r--r-- | coq/coq.el | 78 | ||||
-rw-r--r-- | coq/example.v | 32 |
3 files changed, 105 insertions, 21 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e8f1fe64..e5ace9d0 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -3,12 +3,20 @@ ;; Authors: Thomas Kleymann and Healfdene Goguen ;; Maintainer: Pierre Courtieu <courtieu@lri.fr> +;; To be added for coq 7.4: + +;;"And" -> ??? + ;; $Id$ (require 'proof-syntax) ;; ----- keywords for font-lock. + + + + (defvar coq-keywords-decl '("Axiom[s]?" "Hypotheses" @@ -17,7 +25,10 @@ "Variable[s]?" "Global\\s-+Variable" ;;added tactic def here because it needs Reset to be undone correctly - "Tactic\\s-+Definition")) + "Tactic\\s-+Definition" + "Meta\\s-+Definition" + "Recursive\\s-+Tactic\\s-+Definition" + "Recursive\\s-+Meta\\s-+Definition")) (defvar coq-keywords-defn '("CoFixpoint" @@ -35,6 +46,8 @@ (defvar coq-keywords-goal '("Chapter" + "Module\\s-+Type" + "Module" "Section" "Correctness" "Definition" @@ -162,6 +175,7 @@ Print and Check commands, put the following line in your .emacs: "Implicit\\s-+Arguments\\s-+Off" "Implicit\\s-+Arguments\\s-+On" "Implicits" + "Import" "Infix" "Load" "Read\\s-+Module" @@ -70,11 +70,24 @@ ;; 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)))) +;; We also have coq-version-is-V74, to deal with the new module system +(cond + ((boundp 'coq-version-is-V74) (setq coq-version-is-V7 t)) + ((boundp 'coq-version-is-V7) (setq coq-version-is-V74 nil)) + (t + (let* ((str (shell-command-to-string (concat coq-prog-name " -v"))) + (x (string-match "version \\([.0-9]*\\)" str)) + (num (match-string 1 str))) + (cond + ((string-match num "\\<6.") + (message "coq is V6") (setq coq-version-is-V7 nil) (setq coq-version-is-V74 nil)) + ((or (string-match num "\\<7.0") (string-match num "\\<7.1") + (string-match num "\\<7.2") (string-match num "\\<7.3")) + (message "coq is V7 =< 7.3") + (setq coq-version-is-V7 t) (setq coq-version-is-V74 nil)) + ;default: 7.3.1 and above ---> 7.4 + (t (message "coq is => V7.3.1") + (setq coq-version-is-V7 t) (setq coq-version-is-V74 t)))))) ;; Command to reset the Coq Proof Assistant ;; Pierre: added Impl... because of a bug of Coq until V6.3 @@ -99,12 +112,13 @@ (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")))) +"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Import" "Hint" "Hints" "Hypothesis" "Correctness" "Module" "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") @@ -131,6 +145,17 @@ (proof-ids-to-regexp coq-retractable-instruct)) (defvar coq-non-retractable-instruct-regexp (proof-ids-to-regexp coq-non-retractable-instruct)) + +(defvar coq-keywords-section + (cond + (coq-version-is-V74 '("Section" "Module\\-+Type" "Module")) + (t '("Section")))) + +(defvar coq-section-regexp +; (proof-ids-to-regexp coq-keywords-section) + "\\(\\<Section\\>\\|\\<Module\\>\\-+\\<Type\\>\\|\\<Module\\>\\)" +) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -199,20 +224,21 @@ ; 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." +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\" or \"Suspend\" 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)) @@ -222,9 +248,10 @@ This assumes that no \"Resume\" command has been used." ;; 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 ] + ;; now, so this test has to appear before the goalsave ] ((proof-string-match - (concat "Section\\s-+\\(" proof-id "\\)\\s-*") str) + (concat coq-section-regexp + "\\s-+\\(" proof-id "\\)\\(\\s-*\\(" proof-id "\\)\\)?") 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. @@ -234,8 +261,24 @@ This assumes that no \"Resume\" command has been used." ;; 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)))) - + (message "debut") + (message (concat "0=" (match-string 0 str))) + (message (concat "1=" (match-string 1 str))) + (message (concat "2=" (match-string 2 str))) + (message (concat "3=" (match-string 3 str))) + (message (concat "4=" (match-string 4 str))) + (message (concat "5=" (match-string 5 str))) + (message (concat "6=" (match-string 6 str))) + (message (concat "7=" (match-string 7 str))) + (message (concat "8=" (match-string 8 str))) + (message "fin") + + + (if (equal (match-string 2 str) "Type") ;Module Type id: take the third word + (progn + (setq ans (format coq-forget-id-command (match-string 5 str)))) + (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 @@ -251,6 +294,11 @@ This assumes that no \"Resume\" command has been used." ;; 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) + ;;Todo Hack: if Definition:foo. inside a "Module Type": it is + ;;not a proof start!! + ;(if (and (proof-string-match "Definition\\-+:[^=]?" str) + ; (inside-module-type)) + ; (incf nfalseaborts)) (incf naborts)) ;; If we are already outside a proof, issue a Reset. diff --git a/coq/example.v b/coq/example.v index 5a3c5b59..5d55a2ae 100644 --- a/coq/example.v +++ b/coq/example.v @@ -1,14 +1,36 @@ (* Example proof script for Coq Proof General. + + This is a legal script for coq 7.x, with + imbricated proofs definitions. + + Replace Section by Module (>= coq-7.4). $Id$ *) +Section sect. + Goal (A,B:Prop)(A /\ B) -> (B /\ A). - Intros A B H. - Induction H. - Apply conj. - Assumption. - Assumption. + Intros A B H. +Recursive Tactic Definition bar := Idtac. + Elim H. + Intros. + Lemma foo: (A:Set)Set. + Intro A. + Exact A. + Save. + Split. + Assumption. + Assumption. Save and_comms. +End sect. + +Module mod. +Definition type1:=Set. +End mod. + +Module Type newmod. +Definition type1:=Set. +End newmod. |