diff options
-rw-r--r-- | coq/coq-syntax.el | 82 | ||||
-rw-r--r-- | coq/coq.el | 20 | ||||
-rw-r--r-- | coq/ex-module.v | 14 | ||||
-rw-r--r-- | generic/proof-config.el | 5 | ||||
-rw-r--r-- | generic/proof-script.el | 19 | ||||
-rw-r--r-- | generic/proof-shell.el | 4 | ||||
-rw-r--r-- | isa/isa.el | 8 | ||||
-rw-r--r-- | isar/isar.el | 5 | ||||
-rw-r--r-- | lego/lego.el | 3 | ||||
-rw-r--r-- | plastic/plastic.el | 5 |
10 files changed, 120 insertions, 45 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 360ab3ac..349f5b86 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -90,6 +90,8 @@ version of coq by doing 'coqtop -v'." ) "CoInductive" "Definition" ;; careful: if not followed by :=, then it is a goal cmd "Fixpoint" + "GenFixpoint" ;; careful: may or not be a proof start + "Function" ;; careful: may or not be a proof start "CoInductive" "Inductive" "Inductive\\s-+Set" @@ -107,12 +109,14 @@ version of coq by doing 'coqtop -v'." ) (defvar coq-keywords-goal '("Add\\s-+Morphism" "Chapter" - "Declare\\s-+Module";;only if not followed by:=(see coq-proof-mode-p in coq.el) + "Declare\\s-+Module";;only if not followed by:=(see coq-goal-command-p below) "Module" "Module\\s-+Type" "Section" "Correctness" - "Definition";; only if not followed by := (see coq-proof-mode-p in coq.el) + "Definition";; only if not followed by := (see coq-goal-command-p below) + "GenFixpoint" ;;if {measure} or {wf} (see coq-goal-command-p below) + "Function" ;;if {measure} or {wf} (see coq-goal-command-p below) "Fact" "Goal" "Lemma" @@ -127,6 +131,10 @@ version of coq by doing 'coqtop -v'." ) ;; 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 @@ -157,32 +165,71 @@ of STRG matching REGEXP. Empty match are counted once." (setq str (substring str (match-end 0))))) nbmatch)) - - -(defun coq-goal-command-p (str) - "Decide whether argument is a goal or not" +; 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). It is the +; test when looking backward the start of the proof. It is NOT used +; elsewhere in the backtrack mechanism of 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-p-v80 (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))) + (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)) - ) + (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)) ) + ) ) +;We use this function in order to detect [Declare] modules [Type] +;openings. goal openings are detected by parsing the prompt. + +(defun coq-goal-command-str-v81-p (str) + "Decide whether STR is a module 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)) + )) + + +;; TODO: have something in the 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" --> no more need to coq-goal-command-str-v81-p +(defun coq-goal-command-p-v81 (span) + "see `coq-goal-command-p'" + (or (span-property span 'goalcmd) + ;; module starts are detected here + (coq-goal-command-str-v81-p (or (span-property span 'cmd) "")))) + + +(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-p-v80 span)) + (t (coq-goal-command-p-v80 span)) ;; this is temporary + )) (defvar coq-keywords-save-strict '("Defined" "Save" "Qed" "End" - "Admitted" + "Admitted" )) (defvar coq-keywords-save @@ -197,6 +244,7 @@ of STRG matching REGEXP. Empty match are counted once." ) ) + (defvar coq-keywords-kill-goal '("Abort")) @@ -323,7 +323,6 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no (s (string-match regex lastprompt)) (lprf (match-string 3 lastprompt)) ) - (message lprf) (cons (string-to-int (match-string 2 lastprompt)) (cons (string-to-int (match-string 4 lastprompt)) (cons (build-list-id-from-string lprf) nil))) @@ -367,6 +366,16 @@ pending proofs (in a list)." (set-span-property span 'statenum val) ) +(defun coq-get-span-goalcmd (span) + "Return the 'goalcmd flag of the SPAN." + (span-property span 'goalcmd) + ) + +(defun coq-set-span-goalcmd (span val) + "Set the 'goalcmd flag of the SPAN to VAL." + (set-span-property span 'goalcmd val) + ) + (defun coq-set-span-proofnum (span val) "Set the proof number of the SPAN to VAL." (set-span-property span 'proofnum val) @@ -398,12 +407,21 @@ This number is in the *last but one* prompt (variable `coq-last-but-one-statenum If locked span already has a state number, thne do nothing. Also updates `coq-last-but-one-statenum' to the last state number for next time." (if (and proof-shell-last-prompt proof-script-buffer) + ;; infos = promt infos of the very last prompt + ;; sp = last locked span, which we want to fill with prompt infos (let ((sp (proof-last-locked-span)) (infos (or (coq-last-prompt-info-safe) '(0 0 nil))) ) (unless (or (not sp) (coq-get-span-statenum sp)) (coq-set-span-statenum sp coq-last-but-one-statenum)) (setq coq-last-but-one-statenum (car infos)) + ;; set goalcmd property if this is a goal start + ;; (ie proofstack has changed and not a save cmd) + (unless + (or (not sp) (equal (span-property sp 'type) 'goalsave) + (<= (length (car (cdr (cdr infos)))) + (length coq-last-but-one-proofstack))) + (coq-set-span-goalcmd sp t)) ;; testing proofstack=nil is not good here because nil is the empty list OR ;; the no value, so we test proofnum as it is always set at the same time. ;; This is why this test is done before the next one (which sets proofnum) diff --git a/coq/ex-module.v b/coq/ex-module.v index 5b9d638a..413a4966 100644 --- a/coq/ex-module.v +++ b/coq/ex-module.v @@ -28,6 +28,10 @@ Module M. Parameter T:Set. Parameter x:T. End SIG. + Module Type SIG'. + Parameter T:Set. + Parameter x:T. + End SIG'. Lemma toto : O=O. Definition t:=nat. trivial. @@ -66,16 +70,13 @@ Module Type N'. Module Type M'. Declare Module K:N.SIG. End M'. - Declare Module N''. +(* Declare Module N''. *) Definition T:=nat. Definition x:=O. - End N''. +(* End N''. *) Declare Module N':M.SIG. (* no interactive def started *) - Declare Module N''':= N'. (* no interactive def started *) - Declare Module N''''. (* interactive def started *) - Parameter foo:nat. - End N''''. (* interactive def ended *) + Declare Module N''' :M.SIG. (* no interactive def started *) End N'. @@ -90,7 +91,6 @@ Save. Lemma bar:O=O. Module Type L. (* This should not be allowed by Coq, since the End L. below fails *) - Axiom foo: O=O. End L. (* fails --> if we go back to Module Type: unsync *) Module I. End I. diff --git a/generic/proof-config.el b/generic/proof-config.el index 9703279b..1d77cb60 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1160,8 +1160,11 @@ and that variable for details." ;; values as well as regexps. ;; FIXME: could just as easily give default value of ;; proof-std-goal-command-p here, why not? +;; Pierre: changed this to take the span as argument instead of the string, +;; This allows coq-mode to use a 'goalcmd attribute computed by looking at +;; coq messages when each command is sent. (defcustom proof-goal-command-p 'proof-generic-goal-command-p - "A function to test: is this really a goal command? + "A function to test: is this really a goal command span? This is added as a more refined addition to proof-goal-command-regexp, to solve the problem that Coq and some other provers can have goals which diff --git a/generic/proof-script.el b/generic/proof-script.el index 41499e31..41f691da 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1333,7 +1333,7 @@ With ARG, turn on scripting iff ARG is positive." (and (eq proof-completed-proof-behaviour 'closeany) (> proof-shell-proof-completed 0)) (and (eq proof-completed-proof-behaviour 'closegoal) - (funcall proof-goal-command-p cmd)))) + (funcall proof-goal-command-p span)))) (proof-done-advancing-autosave span)) ;; CASE 4: A "Require" type of command is seen (Coq). @@ -1442,7 +1442,7 @@ With ARG, turn on scripting iff ARG is positive." (proof-string-match proof-save-command-regexp cmd)) (incf lev)) ;; Decrement depth when a goal is hit - ((funcall proof-goal-command-p cmd) + ((funcall proof-goal-command-p gspan) (decf lev)) ;; Remainder cases: see if command matches something we ;; should count for a global undo @@ -1519,7 +1519,7 @@ With ARG, turn on scripting iff ARG is positive." (gspan (if swallow span (prev-span span 'type))) (newend (if swallow (span-end span) (span-start span))) (cmd (span-property span 'cmd)) - (newgoal (funcall proof-goal-command-p cmd)) + (newgoal (funcall proof-goal-command-p span)) nam hitsave dels ncmd) ;; Search backwards to see if we can find a previous goal ;; before a save or the start of the buffer. @@ -1533,7 +1533,8 @@ With ARG, turn on scripting iff ARG is positive." ;;(eq (span-property gspan 'type) 'proverproc) ;; NB: not necess currently (and (setq ncmd (span-property gspan 'cmd)) - (not (funcall proof-goal-command-p (setq cmd ncmd))) + (setq cmd ncmd) ; pc: is this ok? + (not (funcall proof-goal-command-p gspan)) (not (and proof-save-command-regexp (proof-string-match proof-save-command-regexp cmd) @@ -1575,7 +1576,7 @@ With ARG, turn on scripting iff ARG is positive." ;; is that they have no natural surrounding region, so makes ;; it difficult to define a region for revealing again. ;; [ best solution would be to support clicking on ellipsis] - (if (funcall proof-goal-command-p (span-property span 'cmd)) + (if (funcall proof-goal-command-p span) (incf proof-nesting-depth)) (if proof-shell-proof-completed @@ -2280,8 +2281,7 @@ Span deletion property set to flag DELETE-REGION." (or (eq (span-property span 'type) 'proof) (eq (span-property span 'type) 'comment) (eq (span-property span 'type) 'proverproc) - (not (funcall proof-goal-command-p - (span-property span 'cmd))))) + (not (funcall proof-goal-command-p span)))) (setq span (prev-span span 'type))) span))) @@ -2620,9 +2620,10 @@ assistant." ;; allow settings which are string or fn, so we don't need both regexp ;; and function hooks, and so that the other hooks can be functions too. -(defun proof-generic-goal-command-p (str) +(defun proof-generic-goal-command-p (span) "Is STR a goal? Decide by matching with `proof-goal-command-regexp'." - (proof-string-match-safe proof-goal-command-regexp str)) + (proof-string-match-safe proof-goal-command-regexp + (or (span-property span 'cmd) ""))) (defun proof-generic-state-preserving-p (cmd) "Is CMD state preserving? Match on `proof-non-undoables-regexp'." diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b42cb310..9db2a3b3 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -343,7 +343,9 @@ Does nothing if proof assistant is already running." ;; could add back code above for multiple shells <2> <3>, etc. ;; Seems hardly worth it. (apply 'make-comint (append (list proc (car prog-name-list) nil) - (cdr prog-name-list)))) + (cdr prog-name-list))) + ;(message (append (list proc (car prog-name-list) nil) (cdr prog-name-list))) + ) (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) @@ -508,8 +508,7 @@ you will be asked to retract the file or process the remainder of it." (ct 0) str i) (if (and span (prev-span span 'type) (not (eq (span-property (prev-span span 'type) 'type) 'comment)) - (isa-goal-command-p - (span-property (prev-span span 'type) 'cmd))) + (isa-goal-command-p (prev-span span 'type))) (concat "choplev 0" proof-terminal-string) (while span (setq str (span-property span 'cmd)) @@ -531,9 +530,10 @@ you will be asked to retract the file or process the remainder of it." (concat "ProofGeneral.repeat_undo " (int-to-string ct) proof-terminal-string)))) -(defun isa-goal-command-p (str) +(defun isa-goal-command-p (span) "Decide whether argument is a goal or not" - (proof-string-match isa-goal-command-regexp str)) ; this regexp defined in isa-syntax.el + (proof-string-match isa-goal-command-regexp ; this regexp defined in isa-syntax.el + (or (span-property span 'cmd) ""))) ;; Isabelle has no concept of a Linear context, so forgetting back ;; to the declaration of a particular something makes no real diff --git a/isar/isar.el b/isar/isar.el index 41871478..9bd0ef69 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -479,9 +479,10 @@ proof-shell-retract-files-regexp." -(defun isar-goal-command-p (str) +(defun isar-goal-command-p (span) "Decide whether argument is a goal or not" - (proof-string-match isar-goal-command-regexp str)) + (proof-string-match isar-goal-command-regexp + (or (span-property span 'cmd) ""))) (defun isar-global-save-command-p (span str) "Decide whether argument really is a global save command" diff --git a/lego/lego.el b/lego/lego.el index 1a6c10dd..e2f755ea 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -197,7 +197,8 @@ Given is the first SPAN which needs to be undone." (defun lego-goal-command-p (str) "Decide whether argument is a goal or not" - (proof-string-match lego-goal-command-regexp str)) + (proof-string-match lego-goal-command-regexp + (or (span-property span 'cmd) ""))) (defun lego-find-and-forget (span) (let (str ans) diff --git a/plastic/plastic.el b/plastic/plastic.el index 33b7179f..e6bf14d4 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -233,9 +233,10 @@ Given is the first SPAN which needs to be undone." (setq span (next-span span 'type))) (concat plastic-lit-string " &S Undo x" (int-to-string ct) proof-terminal-string))) -(defun plastic-goal-command-p (str) +(defun plastic-goal-command-p (span) "Decide whether argument is a goal or not" ;; NEED CHG. - (proof-string-match plastic-goal-command-regexp str)) + (proof-string-match plastic-goal-command-regexp + (or (span-property span 'cmd) ""))) (defun plastic-find-and-forget (span) ;; count the number of spans to undo. |