From 8b836f84d70fcea59ffa186f6809ebc6765b8a5f Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 3 Sep 1998 13:51:41 +0000 Subject: Renamed for new subdirectory structure --- coq-syntax.el | 275 ------ coq.el | 390 --------- coq/coq-syntax.el | 278 +++++++ coq/coq.el | 390 +++++++++ coq/coqtags | 56 ++ coqtags | 56 -- doc/script-management.texinfo | 440 ++++++++++ generic/pbp.el | 2 + generic/proof-indent.el | 124 +++ generic/proof-syntax.el | 104 +++ generic/proof.el | 1838 +++++++++++++++++++++++++++++++++++++++++ generic/span-extent.el | 82 ++ generic/span-overlay.el | 291 +++++++ isa-print-functions.ML | 172 ---- isa-syntax.el | 138 ---- isa.el | 341 -------- lego-syntax.el | 100 --- lego.el | 461 ----------- lego/lego-syntax.el | 100 +++ lego/lego.el | 461 +++++++++++ lego/legotags | 87 ++ legotags | 87 -- pbp.el | 2 - proof-indent.el | 124 --- proof-syntax.el | 104 --- proof.el | 1838 ----------------------------------------- script-management.texinfo | 440 ---------- span-extent.el | 79 -- span-overlay.el | 288 ------- 29 files changed, 4253 insertions(+), 4895 deletions(-) delete mode 100644 coq-syntax.el delete mode 100644 coq.el create mode 100644 coq/coq-syntax.el create mode 100644 coq/coq.el create mode 100644 coq/coqtags delete mode 100644 coqtags create mode 100644 doc/script-management.texinfo create mode 100644 generic/pbp.el create mode 100644 generic/proof-indent.el create mode 100644 generic/proof-syntax.el create mode 100644 generic/proof.el create mode 100644 generic/span-extent.el create mode 100644 generic/span-overlay.el delete mode 100644 isa-print-functions.ML delete mode 100644 isa-syntax.el delete mode 100644 isa.el delete mode 100644 lego-syntax.el delete mode 100644 lego.el create mode 100644 lego/lego-syntax.el create mode 100644 lego/lego.el create mode 100644 lego/legotags delete mode 100644 legotags delete mode 100644 pbp.el delete mode 100644 proof-indent.el delete mode 100644 proof-syntax.el delete mode 100644 proof.el delete mode 100644 script-management.texinfo delete mode 100644 span-extent.el delete mode 100644 span-overlay.el diff --git a/coq-syntax.el b/coq-syntax.el deleted file mode 100644 index b81a93e8..00000000 --- a/coq-syntax.el +++ /dev/null @@ -1,275 +0,0 @@ -;; coq-syntax.el Font lock expressions for Coq -;; Copyright (C) 1997, 1998 LFCS Edinburgh. -;; Author: Thomas Kleymann and Healfdene Goguen -;; Maintainer: LEGO Team - -;; $Log$ -;; Revision 2.0 1998/08/11 14:59:53 da -;; New branch -;; -;; Revision 1.2 1998/08/11 11:43:13 da -;; Renamed -fontlock to -syntax -;; -;; Revision 1.14 1998/06/11 12:20:14 hhg -;; Added "Scheme" as definition keyword. -;; -;; Revision 1.13 1998/06/10 11:38:04 hhg -;; Added "Mutual Inductive" as definition keyword. -;; Changed "\\s " into "\\s-" as whitespace pattern. -;; -;; Revision 1.12 1998/06/03 18:01:54 hhg -;; Changed Compute from command to tactic. -;; Added Fix, Destruct and Cofix as tactics. -;; Added Local as goal. -;; -;; Revision 1.11 1998/06/02 15:33:16 hhg -;; Minor modifications to comments -;; -;; Revision 1.10 1998/05/15 16:13:23 hhg -;; Added CoFixpoint and tactics. -;; Changed indentation. -;; -;; Revision 1.9 1998/05/05 14:19:39 hhg -;; Added CoInductive. -;; Made updates to reflect problem with "Definition", which couldn't be -;; used with proof scripts. -;; -;; Revision 1.8 1998/01/15 13:30:17 hhg -;; Added coq-shell-cd -;; Some new fontlocks -;; -;; Revision 1.7 1997/11/26 17:12:55 hhg -;; Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1 -;; -;; Revision 1.6 1997/11/06 16:46:20 hhg -;; Updates to Coq fontlock tables -;; -;; Revision 1.5 1997/10/30 15:58:29 hhg -;; Updates for coq, including: -;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string -;; * updates to keywords -;; * fix for goal regexp -;; -;; Revision 1.4 1997/10/24 14:51:07 hhg -;; Changed order of "Inversion_clear" and "Inversion" so that former is -;; fontified first. -;; Added "Print" to list of commands. -;; -;; Revision 1.3 1997/10/17 14:45:53 hhg -;; Added "Induction" as tactic -;; -;; Revision 1.2 1997/10/13 17:10:29 tms -;; *** empty log message *** -;; -;; Revision 1.1.2.2 1997/10/08 08:22:28 hhg -;; Updated undo, fixed bugs, more modularization -;; -;; Revision 1.1.2.1 1997/10/07 13:34:10 hhg -;; New structure to share as much as possible between LEGO and Coq. -;; -;; - -(require 'proof-syntax) - -;; ----- keywords for font-lock. - -(defvar coq-keywords-decl - '( -"Axiom" -"Hypothesis" -"Parameter" -"Variable" -)) - -(defvar coq-keywords-defn - '( -"CoFixpoint" -"CoInductive" -"Fixpoint" -"Inductive" -"Mutual\\s-+Inductive" -"Scheme" -)) - -(defvar coq-keywords-goal - '( -"Definition" -"Fact" -"Goal" -"Lemma" -"Local" -"Remark" -"Theorem" -)) - -(defvar coq-keywords-save - '( -"Defined" -"Save" -"Qed" -)) - -(defvar coq-keywords-kill-goal '( -"Abort" -)) - -(defvar coq-keywords-commands - '( -"AddPath" -"Cd" -"Check" -"Class" -"Coercion" -"DelPath" -"Eval" -"Extraction" -"Focus" -"Immediate" -"Hint" -"Infix" -"Opaque" -"Print" -"Proof" -"Pwd" -"Reset" -"Search" -"Show" -"Transparent" -)) - -(defvar coq-tactics - '( -"Absurd" -"Apply" -"Assumption" -"Auto" -"Case" -"Change" -"Clear" -"Cofix" -"Compute" -"Constructor" -"Contradiction" -"Cut" -"DHyp" -"DInd" -"Dependent" -"Destruct" -"Discriminate" -"Double" -"EApply" -"EAuto" -"Elim" -"End" -"Exact" -"Exists" -"Fix" -"Generalize" -"Grammar" -"Hnf" -"Induction" -"Injection" -"Intro" -"Intros" -"Intuition" -"Inversion_clear" -"Inversion" -"LApply" -"Left" -"Linear" -"Load" -"Pattern" -"Program_all" -"Program" -"Prolog" -"Realizer" -"Red" -"Reflexivity" -"Replace" -"Rewrite" -"Right" -"Section" -"Simplify_eq" -"Simpl" -"Specialize" -"Split" -"Symmetry" -"Syntax" -"Tauto" -"Transitivity" -"Trivial" -"Unfold" -)) - -(defvar coq-keywords - (append coq-keywords-goal coq-keywords-save coq-keywords-decl - coq-keywords-defn coq-keywords-commands coq-tactics) - "All keywords in a Coq script") - -(defvar coq-tacticals '( -"Do" -"Idtac" -"OrElse" -"Repeat" -"Try" -)) - -;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)" - "A regular expression indicating that the Coq process has identified - an error.") - -(defvar coq-id proof-id) - -(defvar coq-ids (proof-ids coq-id)) - -(defun coq-abstr-regexp (paren char) - (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" char)) - -(defvar coq-font-lock-terms - (list - - ;; lambda binders - (list (coq-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face) - - ;; Pi binders - (list (coq-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face) - - ;; Kinds - (cons (concat "\\\\|\\\\|\\ ".") - (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?\| ".") - (modify-syntax-entry ?\* ". 23") - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - -(defun coq-mode-config () - - (setq proof-terminal-char ?\.) - (setq proof-comment-start "(*") - (setq proof-comment-end "*)") - - (setq proof-assistant coq-assistant - proof-www-home-page coq-www-home-page) - - (setq proof-prf-string "Show" - proof-ctxt-string "Print All" - proof-help-string "Help") - - (setq proof-goal-command-p 'coq-goal-command-p - proof-count-undos-fn 'coq-count-undos - proof-find-and-forget-fn 'coq-find-and-forget - proof-goal-hyp-fn 'coq-goal-hyp - proof-state-preserving-p 'coq-state-preserving-p - proof-global-p 'coq-global-p - proof-parse-indent 'coq-parse-indent - proof-stack-to-indent 'coq-stack-to-indent) - - (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-kill-goal-command coq-kill-goal-command - proof-commands-regexp (ids-to-regexp coq-keywords)) - - (coq-init-syntax-table) - -;; font-lock - - (setq font-lock-keywords coq-font-lock-keywords-1) - - (proof-config-done) - - (define-key (current-local-map) [(control c) ?I] 'coq-Intros) - (define-key (current-local-map) [(control c) ?a] 'coq-Apply) - (define-key (current-local-map) [(control c) (control s)] 'coq-Search) - -;; 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 coq-shell-cd - 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-noise-regexp "" - proof-shell-assumption-regexp coq-id - proof-shell-goal-regexp coq-goal-regexp - proof-shell-first-special-char ?\360 - proof-shell-wakeup-char ?\371 ; done: prompt - ; The next three represent path annotation information - proof-shell-start-char ?\372 ; not done - proof-shell-end-char ?\373 ; not done - proof-shell-field-char ?\374 ; not done - proof-shell-goal-char ?\375 ; done - proof-shell-eager-annotation-start "\376" ; done - proof-shell-eager-annotation-end "\377" ; 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 nil - proof-analyse-using-stack t) - - ;; The following hook is removed once it's called. - (add-hook 'proof-shell-insert-hook 'coq-shell-init-hook nil t) - - (coq-init-syntax-table) - - (proof-shell-config-done)) - -(defun coq-pbp-mode-config () - (setq pbp-change-goal "Show %s.") - (setq pbp-error-regexp coq-error-regexp)) - -(provide 'coq) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el new file mode 100644 index 00000000..55d68f35 --- /dev/null +++ b/coq/coq-syntax.el @@ -0,0 +1,278 @@ +;; coq-syntax.el Font lock expressions for Coq +;; Copyright (C) 1997, 1998 LFCS Edinburgh. +;; Author: Thomas Kleymann and Healfdene Goguen +;; Maintainer: LEGO Team + +;; $Log$ +;; Revision 1.1 1998/09/03 13:51:13 da +;; Renamed for new subdirectory structure +;; +;; Revision 2.0 1998/08/11 14:59:53 da +;; New branch +;; +;; Revision 1.2 1998/08/11 11:43:13 da +;; Renamed -fontlock to -syntax +;; +;; Revision 1.14 1998/06/11 12:20:14 hhg +;; Added "Scheme" as definition keyword. +;; +;; Revision 1.13 1998/06/10 11:38:04 hhg +;; Added "Mutual Inductive" as definition keyword. +;; Changed "\\s " into "\\s-" as whitespace pattern. +;; +;; Revision 1.12 1998/06/03 18:01:54 hhg +;; Changed Compute from command to tactic. +;; Added Fix, Destruct and Cofix as tactics. +;; Added Local as goal. +;; +;; Revision 1.11 1998/06/02 15:33:16 hhg +;; Minor modifications to comments +;; +;; Revision 1.10 1998/05/15 16:13:23 hhg +;; Added CoFixpoint and tactics. +;; Changed indentation. +;; +;; Revision 1.9 1998/05/05 14:19:39 hhg +;; Added CoInductive. +;; Made updates to reflect problem with "Definition", which couldn't be +;; used with proof scripts. +;; +;; Revision 1.8 1998/01/15 13:30:17 hhg +;; Added coq-shell-cd +;; Some new fontlocks +;; +;; Revision 1.7 1997/11/26 17:12:55 hhg +;; Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1 +;; +;; Revision 1.6 1997/11/06 16:46:20 hhg +;; Updates to Coq fontlock tables +;; +;; Revision 1.5 1997/10/30 15:58:29 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; +;; Revision 1.4 1997/10/24 14:51:07 hhg +;; Changed order of "Inversion_clear" and "Inversion" so that former is +;; fontified first. +;; Added "Print" to list of commands. +;; +;; Revision 1.3 1997/10/17 14:45:53 hhg +;; Added "Induction" as tactic +;; +;; Revision 1.2 1997/10/13 17:10:29 tms +;; *** empty log message *** +;; +;; Revision 1.1.2.2 1997/10/08 08:22:28 hhg +;; Updated undo, fixed bugs, more modularization +;; +;; Revision 1.1.2.1 1997/10/07 13:34:10 hhg +;; New structure to share as much as possible between LEGO and Coq. +;; +;; + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defvar coq-keywords-decl + '( +"Axiom" +"Hypothesis" +"Parameter" +"Variable" +)) + +(defvar coq-keywords-defn + '( +"CoFixpoint" +"CoInductive" +"Fixpoint" +"Inductive" +"Mutual\\s-+Inductive" +"Scheme" +)) + +(defvar coq-keywords-goal + '( +"Definition" +"Fact" +"Goal" +"Lemma" +"Local" +"Remark" +"Theorem" +)) + +(defvar coq-keywords-save + '( +"Defined" +"Save" +"Qed" +)) + +(defvar coq-keywords-kill-goal '( +"Abort" +)) + +(defvar coq-keywords-commands + '( +"AddPath" +"Cd" +"Check" +"Class" +"Coercion" +"DelPath" +"Eval" +"Extraction" +"Focus" +"Immediate" +"Hint" +"Infix" +"Opaque" +"Print" +"Proof" +"Pwd" +"Reset" +"Search" +"Show" +"Transparent" +)) + +(defvar coq-tactics + '( +"Absurd" +"Apply" +"Assumption" +"Auto" +"Case" +"Change" +"Clear" +"Cofix" +"Compute" +"Constructor" +"Contradiction" +"Cut" +"DHyp" +"DInd" +"Dependent" +"Destruct" +"Discriminate" +"Double" +"EApply" +"EAuto" +"Elim" +"End" +"Exact" +"Exists" +"Fix" +"Generalize" +"Grammar" +"Hnf" +"Induction" +"Injection" +"Intro" +"Intros" +"Intuition" +"Inversion_clear" +"Inversion" +"LApply" +"Left" +"Linear" +"Load" +"Pattern" +"Program_all" +"Program" +"Prolog" +"Realizer" +"Red" +"Reflexivity" +"Replace" +"Rewrite" +"Right" +"Section" +"Simplify_eq" +"Simpl" +"Specialize" +"Split" +"Symmetry" +"Syntax" +"Tauto" +"Transitivity" +"Trivial" +"Unfold" +)) + +(defvar coq-keywords + (append coq-keywords-goal coq-keywords-save coq-keywords-decl + coq-keywords-defn coq-keywords-commands coq-tactics) + "All keywords in a Coq script") + +(defvar coq-tacticals '( +"Do" +"Idtac" +"OrElse" +"Repeat" +"Try" +)) + +;; ----- regular expressions +(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)" + "A regular expression indicating that the Coq process has identified + an error.") + +(defvar coq-id proof-id) + +(defvar coq-ids (proof-ids coq-id)) + +(defun coq-abstr-regexp (paren char) + (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" char)) + +(defvar coq-font-lock-terms + (list + + ;; lambda binders + (list (coq-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face) + + ;; Pi binders + (list (coq-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face) + + ;; Kinds + (cons (concat "\\\\|\\\\|\\ ".") + (modify-syntax-entry ?\& ".") + (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?\' "_") + (modify-syntax-entry ?\| ".") + (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4")) + +(defun coq-mode-config () + + (setq proof-terminal-char ?\.) + (setq proof-comment-start "(*") + (setq proof-comment-end "*)") + + (setq proof-assistant coq-assistant + proof-www-home-page coq-www-home-page) + + (setq proof-prf-string "Show" + proof-ctxt-string "Print All" + proof-help-string "Help") + + (setq proof-goal-command-p 'coq-goal-command-p + proof-count-undos-fn 'coq-count-undos + proof-find-and-forget-fn 'coq-find-and-forget + proof-goal-hyp-fn 'coq-goal-hyp + proof-state-preserving-p 'coq-state-preserving-p + proof-global-p 'coq-global-p + proof-parse-indent 'coq-parse-indent + proof-stack-to-indent 'coq-stack-to-indent) + + (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-kill-goal-command coq-kill-goal-command + proof-commands-regexp (ids-to-regexp coq-keywords)) + + (coq-init-syntax-table) + +;; font-lock + + (setq font-lock-keywords coq-font-lock-keywords-1) + + (proof-config-done) + + (define-key (current-local-map) [(control c) ?I] 'coq-Intros) + (define-key (current-local-map) [(control c) ?a] 'coq-Apply) + (define-key (current-local-map) [(control c) (control s)] 'coq-Search) + +;; 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 coq-shell-cd + 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-noise-regexp "" + proof-shell-assumption-regexp coq-id + proof-shell-goal-regexp coq-goal-regexp + proof-shell-first-special-char ?\360 + proof-shell-wakeup-char ?\371 ; done: prompt + ; The next three represent path annotation information + proof-shell-start-char ?\372 ; not done + proof-shell-end-char ?\373 ; not done + proof-shell-field-char ?\374 ; not done + proof-shell-goal-char ?\375 ; done + proof-shell-eager-annotation-start "\376" ; done + proof-shell-eager-annotation-end "\377" ; 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 nil + proof-analyse-using-stack t) + + ;; The following hook is removed once it's called. + (add-hook 'proof-shell-insert-hook 'coq-shell-init-hook nil t) + + (coq-init-syntax-table) + + (proof-shell-config-done)) + +(defun coq-pbp-mode-config () + (setq pbp-change-goal "Show %s.") + (setq pbp-error-regexp coq-error-regexp)) + +(provide 'coq) diff --git a/coq/coqtags b/coq/coqtags new file mode 100644 index 00000000..b6c72c78 --- /dev/null +++ b/coq/coqtags @@ -0,0 +1,56 @@ +#!/usr/local/bin/perl4 +$/=0777; + +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+=($&=~tr/\n/\n/); + while($d>0 && $a=~/\(\*|\*\)/) + { $a=$'; $cp+=2+length $`; $lp+=($`=~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+($&=~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\']+))\s*:/) + { $tagstring.=$1."\177".$7."\001".$lp.",".$cp."\n"; } + + elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+([\w\']+))\s*[:[]/) + { $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; diff --git a/coqtags b/coqtags deleted file mode 100644 index b6c72c78..00000000 --- a/coqtags +++ /dev/null @@ -1,56 +0,0 @@ -#!/usr/local/bin/perl4 -$/=0777; - -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+=($&=~tr/\n/\n/); - while($d>0 && $a=~/\(\*|\*\)/) - { $a=$'; $cp+=2+length $`; $lp+=($`=~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+($&=~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\']+))\s*:/) - { $tagstring.=$1."\177".$7."\001".$lp.",".$cp."\n"; } - - elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+([\w\']+))\s*[:[]/) - { $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; diff --git a/doc/script-management.texinfo b/doc/script-management.texinfo new file mode 100644 index 00000000..a7232b3c --- /dev/null +++ b/doc/script-management.texinfo @@ -0,0 +1,440 @@ +\input texinfo @c -*-texinfo-*- +@c %**start of header +@setfilename script-management.info +@settitle Script Management +@paragraphindent 0 +@c %**end of header + +@setchapternewpage odd + +@titlepage +@sp 10 +@comment The title is printed in a large font. +@center @titlefont{Script Management Mode} + +@c The following two commands start the copyright page. +@page +@vskip 0pt plus 1filll +Copyright @copyright{} 1997, 1998 LEGO Team, LFCS Edinburgh +@end titlepage + +@node Top, Credits, (dir), (dir) +@comment node-name, next, previous, up + +A @emph{proof script} is a sequence of commands to a proof assistant. +Proof mode is a mode designed to be customised for a particular proof +assistant, to manage communication with a proof process and thereby +support building and secure editing of proof scripts. Currently custom +modes exist for LEGO and Coq. + +@menu +* Credits:: The people Involved +* Introduction:: Introduction to Script Management +* Commands:: Proof mode Commands +* Multiple Files:: Proof developments spanning several files +* Proof by Pointing:: Proof using the Mouse +* An Active Terminator:: Active Terminator minor mode +* Walkthrough:: An example of using proof mode +* LEGO mode:: Extra Bindings for LEGO +* Coq mode:: Extra Bindings for Coq +* Internals:: The Seedy Underside of Proof mode +* Known Problems:: Caveat Emptor +@end menu + +@node Credits, Introduction, Top, Top +@comment node-name, next, previous, up +@unnumberedsec Credits + +Inspired by Yves Bertot's Centaur-based proof environment CtCoq, Healf +Goguen, Thomas Kleymann and Dilip Sequeira have implented a generic +proof mode for Emacs. The original proof-by-pointing algorithm has been +implemented by Yves Bertot. This manual was originally written by Dilip +Sequeira. + +@node Introduction, Commands, Credits, Top +@comment node-name, next, previous, up +@unnumberedsec Introduction + +Each script resides in an Emacs buffer, called a @emph{script buffer}, +which is divided into three regions: + +@itemize @bullet +@item The @emph{Locked} region appears in blue (underlined on monochrome +displays) and contains commands which have been sent to the proof process +and verified. The commands in the locked region cannot be edited. + +@item The @emph{Queue} region appears in pink (inverse video) and contains +commands waiting to be sent to the proof process. Like those in the +locked region, these commands can't be edited. + +@item The @emph{Editing} region contains the commands the user is working +on, and can be edited as normal Emacs text. +@end itemize + +These three regions appear in the buffer in the order above; that is, +the locked region is always at the start of the buffer, and the editing +region always at the end. The queue region only exists if there is input +waiting to be sent to the proof process. + +Proof mode has two operations which transfer commands between these +regions: assertion and retraction. These cause commands to be sent to +the proof process, and Emacs will summarise the results in the +@emph{Response Buffer}. + +@strong{Assertion} causes commands from the editing region to be +transferred to the queue region and sent one by one to the proof +process. If the command is accepted, it is transferred to the locked +region, but if an error occurs it is signalled to the user, and the +offending command is transferred back to the editing region together +with any remaining commands in the queue. @strong{Retraction} causes +commands to be transferred from the locked region to the editing region +(again via the queue region) and the appropriate 'undo' commands to be +sent to the proof process. + +As commands are transferred to the locked region, they are aggregated +into segments which constitute the smallest units which can be +undone. Typically a segment consists of a declaration or definition, or +all the text from a `goal' command to the corresponding `save' command, +or the individual commands in the proof of an unfinished goal. As the +mouse moves over the the region, the segment containing the pointer will +be highlighted. + +Commands in the editing region can be freely edited while +commands in the queue are transferred to the proof process. However, +assertion and retraction commands can only be issued when the queue is +empty. + +@node Commands, Multiple Files, Introduction, Top +@unnumberedsec Proof Mode Commands + +@table @kbd + +@item C-c C-b +assert the commands in the buffer. + +@item C-c return +assert the commands in the editing region up to and +including the one containing the point. + +@item C-c u +retract the segments in the locked region back to and +including the one containing the point. If point is outside the *Locked* +region, the last segment is undone. + +@item C-c C-u +retract the last segment in the locked region, and kill the text in it. +@footnote{Be careful with this, as it may delete more than you anticipate. +However, you can always recover the killed text using Emacs Undo.} + +@item C-c ' +move the point to the end of the locked region. If you are in a script +buffer other than the active scripting buffer, this will also transfer +you to the active one. + +@item C-c C-e +move the point to the next terminator + +@item C-c C-p +display the proof state in the response buffer + +@item C-c c +display the context in the response buffer + +@item C-c h +print proof-system specific help text in the response buffer + +@item C-c C-c +interrupt the process process. This may leave script management or the +proof process (or both) in an inconsistent state. + +@item C-c C-z +move the end of the locked region backwards to the end of the segment +containing the point. @footnote{Don't try this one at home, kids.} + +@item C-c C-t +Send the command at the point to the subprocess, not +recording it in the locked region. @footnote{This is supplied in order +to enable the user to test the types and values of expressions. There's +some checking that the command won't change the proof state, but it +isn't foolproof.} + +@item C-c C-v +Request a command from the minibuffer and send it to +the subprocess. Currently no checking whatsoever is done on the command. +@end table + +The command @code{proof-restart-script} can be used to completely +restart script management. + + +@node Multiple Files, An Active Terminator, Commands, Top +@unnumberedsec Multiple Files + +Proof mode has a rudimentary facility for operating with multiple files +in a proof development. This is currently only supported for LEGO. If +the user invokes script management in a different buffer from the one in +which it is running, one of two prompts will appear: + +@itemize @bullet +@item ``Steal script management?'' +if Emacs doesn't think the file is already part of the proof development +@item ``Reprocess this file?'' +if Emacs thinks the file is already included in the proof process. If +the user confirms, Emacs will cause the proof process to forget the +contents of the file, so that it is processed afresh. +@end itemize + +Currently this facility requires each script buffer to have a +corresponding file. + +When working with script management in multiple buffers, it is easy +to lose track of which buffer is the current script buffer. As a mnemonic +aid, the word @samp{Scripting} appears in the minor mode list of the +active scripting buffer. + +Caveats: +@itemize @minus +@item Note that if processing a buffer causes other files to be loaded +into the LEGO process, those files will be imported from disk rather +than from any Emacs buffer in which it is being edited, i.e.@: if your +file is going to be included indirectly, save it. + +@item However much you move around the file system in Emacs, the +LEGOPATH will be the LEGOPATH you started with. No concept of +"current directory" is currently supported. +@end itemize + +@node An Active Terminator, Proof by Pointing, Multiple Files, Top +@unnumberedsec An Active Terminator + +Proof mode has a minor mode which causes the terminator to become +active. When this mode is active, pressing the terminator key (@kbd{;} +for LEGO, @kbd{.} for Coq) outside a comment or quote will cause the +character to be entered into the buffer, and all the commands in the +editing region up to the point to be asserted. + +This mode can be toggled with the command +`proof-active-terminator-minor-mode' (@kbd{C-c ;} or @kbd{C-c .}) + +@node Proof by Pointing, Walkthrough, An Active Terminator, Top +@unnumberedsec Proof by Pointing + +@emph{This mode is currently very unreliable, and we do not guarantee +that it will work as discussed in this document.} + +Proof by pointing is a facility whereby proof commands can be generated +by using the mouse to select terms. When proving a goal, a summary of +the current proof state will appear in the response buffer. By moving +the mouse over the buffer, the structure of the goal and hypothesis +terms will be shown by highlighting. + +If a selection is made using the second (usually the middle) mouse +button, Emacs will generate the appropriate commands, insert them in the +script buffer, and send them to the proof process. These commands are +aggregated in the locked region as a single segment, so that a +mouse-generated command sequence can be retracted with a single +retraction command. + +Further Information about proof by pointing may be found in the paper +@cite{User Interfaces for Theorem Provers} by Yves Bertot and Laurent +Thery, to appear in @cite{Information and Computation}, from which +the following example is taken. + +@menu +* Proof by Pointing Example:: An example using proof by pointing +@end menu + +@node Proof by Pointing Example, ,Proof by Pointing,Proof by Pointing + +Suppose we wish to prove the lego term: + +@example +(((p a) \/ (q b)) /\ @{x:Prop@}(p x) -> (q x)) -> (Ex ([x:Prop] q(x))); +@end example + +Asserting this goal will result in the proof state + +@example +?0 : ((p a \/ q b) /\ @{x:Prop@}(p x)->q x)->Ex ([x:Prop]q x) +@end example + +appearing in the response buffer. Suppose our strategy is to use a +case analysis on the disjunction, starting with the @samp{p(a)} subterm. +Clicking on this term will cause script management to insert the following +command sequence in the script buffer, and execute it. + +@example +Intros H; Refine H; Intros H0 H1; +Refine or_elim H0 Then Intros H2; Try Refine H2; +@end example + + +The response buffer will then read + +@example + H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x + H0 : p a \/ q b + H1 : @{x:Prop@}(p x)->q x + H2 : p a + ?10 : Ex ([x:Prop]q x) +@end example + +Clicking on the subterm @samp{(p x)} in the hypothesis H1 will instruct +script management to prove an instance of @samp{(p x)} and deduce the +corresponding @samp{(q x)}. The commands + +@example +allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption; +@end example + +are inserted and executed, leaving the proof state as + +@example + H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x + H0 : p a \/ q b + H1 : @{x:Prop@}(p x)->q x + H2 : p a + H3 : (p a)->q a + ?20 : (q a)->Ex ([x:Prop]q x) +@end example + +Now clicking on the @samp{q x)} subterm in ?20 will prove the subgoal. We are +left with the other half of the original case analysis: + +@example + H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x + H0 : p a \/ q b + H1 : @{x:Prop@}(p x)->q x + H2 : q b + ?26 : Ex ([x:Prop]q x) +@end example + +Clicking on @samp{q x} proves the goal. + + + + +@node Walkthrough, LEGO mode, Proof by Pointing, Top +@unnumberedsec A Walkthrough + +Here's a LEGO example of how script management is used. + +First, we turn on active terminator minor mode by typing @kbd{C-c ;} +Then we enter + +`Module Walkthrough Import lib_logic;' + +The command should be lit in pink (or inverse video if you don't have a +colour display). As LEGO imports each module, a line will appear in the +response buffer showing the creation of context marks. Eventually the +command should turn blue, indicating that LEGO has successfully +processed it. Then type (on a separate line if you like) + +@samp{Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);} + +The goal should be echoed in the response buffer. + +@samp{Intros;} + +Whoops! @kbd{C-c C-u} to pretend that didn't happen. + +@samp{intros; andI;} + +A proof summary will appear in the response buffer. We could solve the +goal by pointing now, but we'll stay with the keyboard. + +@samp{Refine H; intros; Immed; Refine H; intros; Immed;} + +finishes the Goal. + +@samp{Save bland_commutes;} + +Moving the mouse pointer over the locked region now reveals that the +entire proof has been aggregated into a single segment. Suppose we +decide to call the goal something more sensible. Moving the cursor up +into the locked region, somewhere between `Goal' and `Save', we enter +@kbd{C-c u}. The segment is transferred back into the editing +region. Now we correct the goal name, move the cursor to the end of the +buffer, and type @kbd{C-c return}. Proof mode queues the commands for +processing and executes them. + +@node LEGO mode, Coq mode, Walkthrough, Top +@unnumberedsec LEGO mode + +LEGO mode is a mode derived from proof mode for editing LEGO scripts. +There are some abbreviations for common commands, which +add text to the buffer: + +@table @kbd +@item C-c i +intros +@item C-c I +Intros +@item C-c R +Refine +@end table + + +@node Coq mode, Known Problems, LEGO mode, Top +@unnumberedsec Coq mode + +Coq mode is a mode derived from proof mode for editing Coq scripts. +As well as custom popup menus, it has the following commands: + +@table @kbd + +@item C-c C-s +search for items in the library of a given type. This runs the +@kbd{Search} command of Coq. + +@end table + +In addition, there are some abbreviations for common commands, which +add text to the buffer: + +@table @kbd +@item C-c I +Intros +@item C-c a +Apply +@end table + +@node Known Problems, Internals, Coq mode, Top +@unnumberedsec Known Problems + +Since Emacs is pretty flexible, there are a whole bunch of things you +can do to confuse script management. When it gets confused, it may +become distressed, and may eventually sulk. In such instances +@code{proof-restart-script-management} may be of use. + +A few things to avoid: + +@itemize @minus +@item If you're using script management with multiple files, don't start +changing the file names. + +@item Script Management doesn't understand how to undo @code{Discharge} +commands in LEGO, and any attempts it makes to do so may leave it in an +inconsistent state. If you're undoing the effects of a @code{Discharge} +command, retract back to the declaration of whatever gets discharged. + +@item Proof by Pointing doesn't work very well, and is inefficiently +implemented. + +@item The locked and queue regions are not quite read-only: in particular +Emacs Undo can insert text into them. + +@item When a LEGO import command fails, the created "Mark" is not +forgotten, and the proof process thinks the file has been included. So +if you assert the command again, it will probably be accepted by LEGO, +because the relevant mark is in the namespace. +@end itemize + +Fixes for some of these may be provided in a future release. + +@node Internals, , Known Problems, Top +@unnumberedsec Internals + +I may one day document the script management internals here. Until then, +UtSL. +@bye diff --git a/generic/pbp.el b/generic/pbp.el new file mode 100644 index 00000000..23ffdd68 --- /dev/null +++ b/generic/pbp.el @@ -0,0 +1,2 @@ + +(provide 'pbp) diff --git a/generic/proof-indent.el b/generic/proof-indent.el new file mode 100644 index 00000000..bb42f462 --- /dev/null +++ b/generic/proof-indent.el @@ -0,0 +1,124 @@ +;; proof-indent.el Generic Indentation for Proof Assistants +;; Copyright (C) 1997, 1998 LFCS Edinburgh +;; Authors: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira +;; Maintainer: LEGO Team + +(require 'cl) +(require 'proof-syntax) + +(defvar proof-stack-to-indent nil + "Prover-specific code for indentation.") + +(defvar proof-parse-indent nil + "Proof-assistant specific function for parsing characters for + indentation which is invoked in `proof-parse-to-point.'. Must be a + function taking two arguments, a character (the current character) + and a stack reflecting indentation, and must return a stack. The + stack is a list of the form (c . p) where `c' is a character + representing the type of indentation and `p' records the column for + indentation. The generic `proof-parse-to-point.' function supports + parentheses and commands. It represents these with the characters + `?\(', `?\[' and `proof-terminal-char'. ") + +;; This is quite different from sml-mode, but borrows some bits of +;; code. It's quite a lot less general, but works with nested +;; comments. + +;; parse-to-point: If from is nil, parsing starts from either +;; proof-locked-end if we're in the proof-script-buffer or the +;; beginning of the buffer. Otherwise state must contain a valid +;; triple. + +(defun proof-parse-to-point (&optional from state) + (let ((comment-level 0) (stack (list (list nil 0))) + (end (point)) instring c) + (save-excursion + (if (null from) + (if (eq proof-script-buffer (current-buffer)) + (proof-goto-end-of-locked) + (goto-char 1)) + (goto-char from) + (setq instring (car state) + comment-level (nth 1 state) + stack (nth 2 state))) + (while (< (point) end) + (setq c (char-after (point))) + (cond + (instring + (if (eq c ?\") (setq instring nil))) + (t (cond + ((eq c ?\() + (cond + ((looking-at "(\\*") + (progn + (incf comment-level) + (forward-char))) + ((eq comment-level 0) + (setq stack (cons (list ?\( (point)) stack))))) + ((and (eq c ?\*) (looking-at "\\*)")) + (decf comment-level) + (forward-char)) + ((> comment-level 0)) + ((eq c ?\") (setq instring t)) + ((eq c ?\[) + (setq stack (cons (list ?\[ (point)) stack))) + ((or (eq c ?\)) (eq c ?\])) + (setq stack (cdr stack))) + ((looking-at proof-commands-regexp) + (setq stack (cons (list proof-terminal-char (point)) stack))) + ((and (eq c proof-terminal-char) + (eq (car (car stack)) proof-terminal-char)) (cdr stack)) + (proof-parse-indent + (setq stack (funcall proof-parse-indent c stack)))))) + (forward-char)) + (list instring comment-level stack)))) + +(defun proof-indent-line () + (interactive) + (if (and (eq proof-script-buffer (current-buffer)) + (< (point) (proof-locked-end))) + (if (< (current-column) (current-indentation)) + (skip-chars-forward "\t ")) + (save-excursion + (beginning-of-line) + (let* ((state (proof-parse-to-point)) + (beg (point)) + (indent (cond ((car state) 1) + ((> (nth 1 state) 0) 1) + (t (funcall proof-stack-to-indent (nth 2 state)))))) + (skip-chars-forward "\t ") + (if (not (eq (current-indentation) indent)) + (progn (delete-region beg (point)) + (indent-to indent))))) + (skip-chars-forward "\t "))) + +(defun proof-indent-region (start end) + (interactive "r") + (if (and (eq proof-script-buffer (current-buffer)) + (< (point) (proof-locked-end))) + (error "can't indent locked region!")) + (save-excursion + (goto-char start) + (beginning-of-line) + (let* ((beg (point)) + (state (proof-parse-to-point)) + indent) + ;; End of region changes with new indentation + (while (< (point) end) + (setq indent + (cond ((car state) 1) + ((> (nth 1 state) 0) 1) + (t (funcall proof-stack-to-indent (nth 2 state))))) + (skip-chars-forward "\t ") + (let ((diff (- (current-indentation) indent))) + (if (not (eq diff 0)) + (progn + (delete-region beg (point)) + (indent-to indent) + (setq end (- end diff))))) + (end-of-line) + (if (< (point) (point-max)) (forward-char)) + (setq state (proof-parse-to-point beg state) + beg (point)))))) + +(provide 'proof-indent) \ No newline at end of file diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el new file mode 100644 index 00000000..5caa8fe3 --- /dev/null +++ b/generic/proof-syntax.el @@ -0,0 +1,104 @@ +;; proof-syntax.el Generic font lock expressions +;; Copyright (C) 1997-1998 LFCS Edinburgh. +;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera +;; Maintainer: LEGO Team + +(require 'font-lock) + +;;; FIXME: change this to proof- +(defun ids-to-regexp (l) + "transforms a non-empty list of identifiers `l' into a regular + expression matching any of its elements" + (mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|")) + +;; Generic font-lock + +;; proof-commands-regexp is used for indentation +(defvar proof-commands-regexp "" + "Subset of keywords and tacticals which are terminated by the + `proof-terminal-char'") + + +(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" + "A regular expression for parsing identifiers.") + +;; For font-lock, we treat ,-separated identifiers as one identifier +;; and refontify commata using \{proof-unfontify-separator}. + +(defun proof-ids (proof-id) + "Function to generate a regular expression for separated lists of + identifiers." + (concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; font lock faces: declarations, errors, tacticals ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-have-color () + ()) + +(defvar font-lock-declaration-name-face +(progn + (cond + ((proof-have-color) + (copy-face 'bold 'font-lock-declaration-name-face) + + ;; Emacs 19.28 compiles this down to + ;; internal-set-face-1. This is not compatible with XEmacs + (set-face-foreground + 'font-lock-declaration-name-face "chocolate")) + (t (copy-face 'bold-italic 'font-lock-declaration-name-face))))) + +;; (if running-emacs19 +;; (setq font-lock-declaration-name-face +;; (face-name 'font-lock-declaration-name-face)) + +(defvar font-lock-tacticals-name-face +(if (proof-have-color) + (let ((face (make-face 'font-lock-tacticals-name-face))) + (dont-compile + (set-face-foreground face "MediumOrchid3")) + face) + (copy-face 'bold 'font-lock-tacticals-name-face))) + +(defvar font-lock-error-face +(if (proof-have-color) + (let ((face (make-face 'font-lock-error-face))) + (dont-compile + (set-face-foreground face "red")) + face) + (copy-face 'bold 'font-lock-error-face))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A big hack to unfontify commas in declarations and definitions. ;; +;; All that can be said for it is that the previous way of doing ;; +;; this was even more bogus. ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Refontify the whole line, 'cos that's what font-lock-after-change +;; does. + +(defun proof-zap-commas-region (start end length) + (save-excursion + (let + ((start (progn (goto-char start) (beginning-of-line) (point))) + (end (progn (goto-char end) (end-of-line) (point)))) + (goto-char start) + (while (search-forward "," end t) + (if (memq (get-char-property (- (point) 1) 'face) + '(font-lock-declaration-name-face + font-lock-function-name-face)) + (font-lock-remove-face (- (point) 1) (point)) + ))))) + +(defun proof-zap-commas-buffer () + (proof-zap-commas-region (point-min) (point-max) 0)) + +(defun proof-unfontify-separator () + (make-local-variable 'after-change-functions) + (setq after-change-functions + (append (delq 'proof-zap-commas-region after-change-functions) + '(proof-zap-commas-region)))) + + +(provide 'proof-syntax) diff --git a/generic/proof.el b/generic/proof.el new file mode 100644 index 00000000..c37f863b --- /dev/null +++ b/generic/proof.el @@ -0,0 +1,1838 @@ +;; proof.el Major mode for proof assistants +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, +;; Thomas Kleymann and Dilip Sequeira + +;; Maintainer: LEGO Team +;; Thanks to Robert Boyer, Rod Burstall, +;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens + + +(require 'cl) +(require 'compile) +(require 'comint) +(require 'etags) +(cond ((fboundp 'make-extent) (require 'span-extent)) + ((fboundp 'make-overlay) (require 'span-overlay)) + (t nil)) +(require 'proof-syntax) +(require 'proof-indent) +(require 'easymenu) +(require 'tl-list) + +(autoload 'w3-fetch "w3" nil t) + +(defmacro deflocal (var value docstring) + (list 'progn + (list 'defvar var 'nil docstring) + (list 'make-variable-buffer-local (list 'quote var)) + (list 'setq var value))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Generic config for proof assistant ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-assistant "" + "Name of the proof assistant") + +(defvar proof-www-home-page "" + "Web address for information on proof assistant") + +(defvar proof-shell-cd nil + "*Command of the inferior process to change the directory.") + +(defvar proof-shell-process-output-system-specific nil + "*Errors, start of proofs, abortions of proofs and completions of + proofs are recognised in the function `proof-shell-process-output'. + All other output from the proof engine is simply reported to the + user in the RESPONSE buffer. + + To catch further special cases, set this variable to a tuple of + functions '(condf . actf). Both are given (cmd string) as arguments. + `cmd' is a string containing the currently processed command. + `string' is the response from the proof system. To change the + behaviour of `proof-shell-process-output', (condf cmd string) must + return a non-nil value. Then (actf cmd string) is invoked. See the + documentation of `proof-shell-process-output' for the required + output format.") + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof mode variables ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconst proof-mode-version-string + "PROOF-MODE. ALPHA Version 2 (August 1998) LEGO Team ") + +(defconst proof-info-dir "/usr/local/share/info" + "Directory to search for Info documents on Script Management.") + +(defconst proof-universal-keys + (list (cons '[(control c) (control c)] 'proof-interrupt-process) + (cons '[(control c) (control v)] + 'proof-execute-minibuffer-cmd) + (cons '[(meta tab)] 'tag-complete-symbol)) + "List of keybindings which are valid in both in the script and the + response buffer. Elements of the list are tuples (k . f) + where `k' is a keybinding (vector) and `f' the designated function.") + +(defvar proof-prog-name-ask-p nil + "*If t, you will be asked which program to run when the inferior + process starts up.") + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Other buffer-local variables used by proof mode ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; These should be set before proof-config-done is called + +(defvar proof-terminal-char nil "terminator character") + +(defvar proof-comment-start nil "Comment start") +(defvar proof-comment-end nil "Comment end") + +(defvar proof-save-command-regexp nil "Matches a save command") +(defvar proof-save-with-hole-regexp nil "Matches a named save command") +(defvar proof-goal-with-hole-regexp nil "Matches a saved goal command") + +(defvar proof-goal-command-p nil "Is this a goal") +(defvar proof-count-undos-fn nil "Compute number of undos in a target segment") +(defvar proof-find-and-forget-fn nil "Compute command to forget up to point") + +(defvar proof-goal-hyp-fn nil + "A function which returns cons cell if point is at a goal/hypothesis. +First element of cell is a symbol, 'goal' or 'hyp'. The second +element is a string: the goal or hypothesis itself. This is used +when parsing the proofstate output") + +(defvar proof-kill-goal-command nil "How to kill a goal.") +(defvar proof-global-p nil + "Is this a global declaration") + +(defvar proof-state-preserving-p nil + "A predicate, non-nil if its argument preserves the proof state") + +(defvar pbp-change-goal nil + "*Command to change to the goal %s") + +;; these should be set in proof-pre-shell-start-hook + +(defvar proof-prog-name nil "program name for proof shell") +(defvar proof-mode-for-shell nil "mode for proof shell") +(defvar proof-mode-for-pbp nil "The actual mode for Proof-by-Pointing.") +(defvar proof-shell-insert-hook nil + "Function to config proof-system to interface") + +(defvar proof-pre-shell-start-hook) +(defvar proof-post-shell-exit-hook) + +(defvar proof-shell-prompt-pattern nil + "comint-prompt-pattern for proof shell") + +(defvar proof-shell-init-cmd nil + "The command for initially configuring the proof process") + +(defvar proof-shell-handle-delayed-output-hook + '(proof-pbp-focus-on-first-goal) + "*This hook is called after output from the PROOF process has been + displayed in the RESPONSE buffer.") + +(defvar proof-shell-handle-error-hook + '(proof-goto-end-of-locked-if-pos-not-visible-in-window) + "*This hook is called after an error has been reported in the + RESPONSE buffer.") + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Generic config for script management ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-shell-wakeup-char nil + "A character terminating the prompt in annotation mode") + +(defvar proof-shell-annotated-prompt-regexp "" + "Annotated prompt pattern") + +(defvar proof-shell-abort-goal-regexp nil + "*Regular expression indicating that the proof of the current goal + has been abandoned.") + +(defvar proof-shell-error-regexp nil + "A regular expression indicating that the PROOF process has + identified an error.") + +(defvar proof-shell-interrupt-regexp nil + "A regular expression indicating that the PROOF process has + responded to an interrupt.") + +(defvar proof-shell-proof-completed-regexp nil + "*Regular expression indicating that the proof has been completed.") + +(defvar proof-shell-result-start "" + "String indicating the start of an output from the prover following + a `pbp-goal-command' or a `pbp-hyp-command'.") + +(defvar proof-shell-result-end "" + "String indicating the end of an output from the prover following a + `pbp-goal-command' or a `pbp-hyp-command'.") + +(defvar proof-shell-start-goals-regexp "" + "String indicating the start of the proof state.") + +(defvar proof-shell-end-goals-regexp "" + "String indicating the end of the proof state.") + +(defvar pbp-error-regexp nil + "A regular expression indicating that the PROOF process has + identified an error.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Internal variables used by scripting and pbp ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-mode-name "Proof") + +(defvar proof-shell-echo-input t + "If nil, input to the proof shell will not be echoed") + +(defvar proof-terminal-string nil + "End-of-line string for proof process.") + +(defvar proof-re-end-of-cmd nil + "You are not authorised for this information.") + +(defvar proof-re-term-or-comment nil + "You are not authorised for this information.") + +(defvar proof-marker nil + "You are not authorised for this information.") + +(defvar proof-shell-buffer nil + "You are not authorised for this information.") + +(defvar proof-script-buffer nil + "You are not authorised for this information.") + +(defvar proof-pbp-buffer nil + "You are not authorised for this information.") + +(defvar proof-shell-busy nil + "You are not authorised for this information.") + +(deflocal proof-buffer-type nil + "You are not authorised for this information.") + +(defvar proof-action-list nil "action list") + +(defvar proof-included-files-list nil + "Files currently included in proof process") + +(deflocal proof-active-buffer-fake-minor-mode nil + "An indication in the modeline that this is the *active* buffer") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A couple of small utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-define-keys (map kbl) + "Adds keybindings `kbl' in `map'. The argument `kbl' is a list of + tuples (k . f) where `k' is a keybinding (vector) and `f' the + designated function." + (mapcar + (lambda (kbl) + (let ((k (car kbl)) (f (cdr kbl))) + (define-key map k f))) + kbl)) + +(defun proof-string-to-list (s separator) + "converts strings `s' separated by the character `separator' to a + list of words" + (let ((end-of-word-occurence (string-match (concat separator "+") s))) + (if (not end-of-word-occurence) + (if (string= s "") + nil + (list s)) + (cons (substring s 0 end-of-word-occurence) + (proof-string-to-list + (substring s + (string-match (concat "[^" separator "]") + s end-of-word-occurence)) separator))))) + +;; FIXME: this doesn't belong here (and shouldn't be called w3-* !!) +(defun w3-remove-file-name (address) + "remove the file name in a World Wide Web address" + (string-match "://[^/]+/" address) + (concat (substring address 0 (match-end 0)) + (file-name-directory (substring address (match-end 0))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Basic code for the locked region and the queue region ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-locked-hwm nil + "Upper limit of the locked region") + +(defvar proof-queue-loose-end nil + "Limit of the queue region that is not equal to proof-locked-hwm.") + +(defvar proof-locked-span nil + "Upper limit of the locked region") + +(defvar proof-queue-span nil + "Upper limit of the locked region") + +(make-variable-buffer-local 'proof-locked-span) +(make-variable-buffer-local 'proof-queue-span) + +(defun proof-init-segmentation () + (setq proof-queue-loose-end nil) + (if (not proof-queue-span) + (setq proof-queue-span (make-span 1 1))) + (set-span-property proof-queue-span 'start-closed t) + (set-span-property proof-queue-span 'end-open t) + (span-read-only proof-queue-span) + + (make-face 'proof-queue-face) + ;; Whether display has color or not + (cond ((and (fboundp 'device-class) + (eq (device-class (frame-device)) 'color)) + (set-face-background 'proof-queue-face "mistyrose")) + ((and (fboundp 'x-display-color-p) (x-display-color-p)) + (set-face-background 'proof-queue-face "mistyrose")) + (t (progn + (set-face-background 'proof-queue-face "Black") + (set-face-foreground 'proof-queue-face "White")))) + (set-span-property proof-queue-span 'face 'proof-queue-face) + + (detach-span proof-queue-span) + + (setq proof-locked-hwm nil) + (if (not proof-locked-span) + (setq proof-locked-span (make-span 1 1))) + (set-span-property proof-locked-span 'start-closed t) + (set-span-property proof-locked-span 'end-open t) + (span-read-only proof-locked-span) + + (make-face 'proof-locked-face) + ;; Whether display has color or not + (cond ((and (fboundp 'device-class) + (eq (device-class (frame-device)) 'color)) + (set-face-background 'proof-locked-face "lavender")) + ((and (fboundp 'x-display-color-p) (x-display-color-p)) + (set-face-background 'proof-locked-face "lavender")) + (t (set-face-property 'proof-locked-face 'underline t))) + (set-span-property proof-locked-span 'face 'proof-locked-face) + + (detach-span proof-locked-span)) + +(defsubst proof-lock-unlocked () + (span-read-only proof-locked-span)) + +(defsubst proof-unlock-locked () + (span-read-write proof-locked-span)) + +(defsubst proof-set-queue-endpoints (start end) + (set-span-endpoints proof-queue-span start end)) + +(defsubst proof-set-locked-endpoints (start end) + (set-span-endpoints proof-locked-span start end)) + +(defsubst proof-detach-queue () + (and proof-queue-span (detach-span proof-queue-span))) + +(defsubst proof-detach-locked () + (and proof-locked-span (detach-span proof-locked-span))) + +(defsubst proof-set-queue-start (start) + (set-span-endpoints proof-queue-span start (span-end proof-queue-span))) + +(defsubst proof-set-queue-end (end) + (set-span-endpoints proof-queue-span (span-start proof-queue-span) end)) + +(defun proof-detach-segments () + (proof-detach-queue) + (proof-detach-locked)) + +(defsubst proof-set-locked-end (end) + (if (>= (point-min) end) + (proof-detach-locked) + (set-span-endpoints proof-locked-span (point-min) end))) + +(defun proof-unprocessed-begin () + "proof-unprocessed-begin returns end of locked region in script + buffer and point-min otherwise." + (or + (and (eq proof-script-buffer (current-buffer)) + proof-locked-span (span-end proof-locked-span)) + (point-min))) + +(defun proof-locked-end () + "proof-locked-end returns the end of the locked region. It should + only be called if we're in the scripting buffer." + (if (eq proof-script-buffer (current-buffer)) + (proof-unprocessed-begin) + (error "bug: proof-locked-end called from wrong buffer"))) + +(defsubst proof-end-of-queue () + (and proof-queue-span (span-end proof-queue-span))) + +(defun proof-dont-show-annotations () + "This sets the display values of the annotations used to + communicate with the proof assistant so that they don't show up on + the screen." + (let ((disp (make-display-table)) + (i 128)) + (while (< i 256) + (aset disp i []) + (incf i)) + (cond ((fboundp 'add-spec-to-specifier) + (add-spec-to-specifier current-display-table disp + (current-buffer))) + ((boundp 'buffer-display-table) + (setq buffer-display-table disp))))) + +;;; in case Emacs is not aware of read-shell-command-map + +(defvar read-shell-command-map + (let ((map (make-sparse-keymap))) + (if (not (fboundp 'set-keymap-parents)) + (setq map (append minibuffer-local-map map)) + (set-keymap-parents map minibuffer-local-map) + (set-keymap-name map 'read-shell-command-map)) + (define-key map "\t" 'comint-dynamic-complete) + (define-key map "\M-\t" 'comint-dynamic-complete) + (define-key map "\M-?" 'comint-dynamic-list-completions) + map) + "Minibuffer keymap used by shell-command and related commands.") + + +;;; in case Emacs is not aware of the function read-shell-command +(or (fboundp 'read-shell-command) + ;; from minibuf.el distributed with XEmacs 19.11 + (defun read-shell-command (prompt &optional initial-input history) + "Just like read-string, but uses read-shell-command-map: +\\{read-shell-command-map}" + (let ((minibuffer-completion-table nil)) + (read-from-minibuffer prompt initial-input read-shell-command-map + nil (or history + 'shell-command-history))))) + +;; The package fume-func provides a function with the same name and +;; specification. However, fume-func's version is incorrect. +(and (fboundp 'fume-match-find-next-function-name) +(defun fume-match-find-next-function-name (buffer) + "General next function name in BUFFER finder using match. + The regexp is assumed to be a two item list the car of which is the regexp + to use, and the cdr of which is the match position of the function name" + (set-buffer buffer) + (let ((r (car fume-function-name-regexp)) + (p (cdr fume-function-name-regexp))) + (and (re-search-forward r nil t) + (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))) + +(defun proof-goto-end-of-locked-interactive () + "Jump to the end of the locked region." + (interactive) + (switch-to-buffer proof-script-buffer) + (goto-char (proof-locked-end))) + +(defun proof-goto-end-of-locked () + "Jump to the end of the locked region." + (goto-char (proof-locked-end))) + +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window () + "If the end of the locked region is not visible, jump to the end of + the locked region." + (interactive) + (let ((pos (save-excursion + (set-buffer proof-script-buffer) + (proof-locked-end)))) + (or (pos-visible-in-window-p pos (get-buffer-window + proof-script-buffer t)) + (proof-goto-end-of-locked-interactive)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Starting and stopping the proof-system shell ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-shell-live-buffer () + (and proof-shell-buffer + (comint-check-proc proof-shell-buffer) + proof-shell-buffer)) + +(defun proof-start-shell () + (if (proof-shell-live-buffer) + () + (run-hooks 'proof-pre-shell-start-hook) + (setq proof-included-files-list nil) + (if proof-prog-name-ask-p + (save-excursion + (setq proof-prog-name (read-shell-command "Run process: " + proof-prog-name)))) + (let ((proc + (concat "Inferior " + (substring proof-prog-name + (string-match "[^/]*$" proof-prog-name))))) + (while (get-buffer (concat "*" proc "*")) + (if (string= (substring proc -1) ">") + (aset proc (- (length proc) 2) + (+ 1 (aref proc (- (length proc) 2)))) + (setq proc (concat proc "<2>")))) + + (message (format "Starting %s process..." proc)) + + ;; Starting the inferior process (asynchronous) + (let ((prog-name-list (proof-string-to-list proof-prog-name " "))) + (apply 'make-comint (append (list proc (car prog-name-list) nil) + (cdr prog-name-list)))) + ;; To send any initialisation commands to the inferior process, + ;; consult proof-shell-config-done... + + (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) + (setq proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*"))) + + (save-excursion + (set-buffer proof-shell-buffer) + (funcall proof-mode-for-shell) + (set-buffer proof-pbp-buffer) + (funcall proof-mode-for-pbp)) + + (setq proof-script-buffer (current-buffer)) + (proof-init-segmentation) + (setq proof-active-buffer-fake-minor-mode t) + + (if (fboundp 'redraw-modeline) + (redraw-modeline) + (force-mode-line-update)) + + (or (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (list '(proof-active-buffer-fake-minor-mode + " Scripting"))))) + + (message + (format "Starting %s process... done." proc))))) + + +(defun proof-stop-shell () + "Exit the PROOF process + + Runs proof-shell-exit-hook if non nil" + + (interactive) + (save-excursion + (let ((buffer (proof-shell-live-buffer)) (proc)) + (if buffer + (progn + (save-excursion + (set-buffer buffer) + (setq proc (process-name (get-buffer-process))) + (comint-send-eof) + (save-excursion + (set-buffer proof-script-buffer) + (proof-detach-segments)) + (kill-buffer)) + (run-hooks 'proof-shell-exit-hook) + + ;;it is important that the hooks are + ;;run after the buffer has been killed. In the reverse + ;;order e.g., intall-shell-fonts causes problems and it + ;;is impossible to restart the PROOF shell + + (message (format "%s process terminated." proc))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof by pointing ;; +;; All very lego-specific at present ;; +;; To make sense of this code, you should read the ;; +;; relevant LFCS tech report by tms, yb, and djs ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defvar pbp-goal-command nil + "Command informing the prover that `pbp-button-action' has been + requested on a goal.") + +(defvar pbp-hyp-command nil + "Command informing the prover that `pbp-button-action' has been + requested on an assumption.") + +(defun pbp-button-action (event) + (interactive "e") + (mouse-set-point event) + (pbp-construct-command)) + +; Using the spans in a mouse behavior is quite simple: from the +; mouse position, find the relevant span, then get its annotation +; and produce a piece of text that will be inserted in the right +; buffer. + +(defun proof-expand-path (string) + (let ((a 0) (l (length string)) ls) + (while (< a l) + (setq ls (cons (int-to-string (aref string a)) + (cons " " ls))) + (incf a)) + (apply 'concat (nreverse ls)))) + +(defun proof-send-span (event) + (interactive "e") + (let* ((span (span-at (mouse-set-point event) 'type)) + (str (span-property span 'cmd))) + (cond ((and (eq proof-script-buffer (current-buffer)) (not (null span))) + (proof-goto-end-of-locked) + (cond ((eq (span-property span 'type) 'vanilla) + (insert str))))))) + +(defun pbp-construct-command () + (let* ((span (span-at (point) 'proof)) + (top-span (span-at (point) 'proof-top-element)) + top-info) + (if (null top-span) () + (setq top-info (span-property top-span 'proof-top-element)) + (pop-to-buffer proof-script-buffer) + (cond + (span + (proof-invisible-command + (format (if (eq 'hyp (car top-info)) pbp-hyp-command + pbp-goal-command) + (concat (cdr top-info) (proof-expand-path + (span-property span 'proof)))))) + ((eq (car top-info) 'hyp) + (proof-invisible-command (format pbp-hyp-command (cdr top-info)))) + (t + (proof-insert-pbp-command (format pbp-change-goal (cdr top-info)))))) + )) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Turning annotated output into pbp goal set ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-shell-first-special-char nil "where the specials start") +(defvar proof-shell-goal-char nil "goal mark") +(defvar proof-shell-start-char nil "annotation start") +(defvar proof-shell-end-char nil "annotation end") +(defvar proof-shell-field-char nil "annotated field end") +(defvar proof-shell-eager-annotation-start nil "eager ann. field start") +(defvar proof-shell-eager-annotation-end nil "eager ann. field end") + +(defvar proof-shell-assumption-regexp nil + "A regular expression matching the name of assumptions.") + +;; FIXME: da: where is this variable used? +;; dropped in favour of goal-char? +(defvar proof-shell-goal-regexp nil + "A regular expressin matching the identifier of a goal.") + +(defvar proof-shell-noise-regexp nil + "Unwanted information output from the proof process within + `proof-start-goals-regexp' and `proof-end-goals-regexp'.") + +(defun pbp-make-top-span (start end) + (let (span name) + (goto-char start) + ;; FIXME: why name? This is a character function + (setq name (funcall proof-goal-hyp-fn)) + (beginning-of-line) + (setq start (point)) + (goto-char end) + (beginning-of-line) + (backward-char) + (setq span (make-span start (point))) + (set-span-property span 'mouse-face 'highlight) + (set-span-property span 'proof-top-element name))) + + +;; Need this for processing error strings and so forth + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; The filter. First some functions that handle those few ;; +;; occasions when the glorious illusion that is script-management ;; +;; is temporarily suspended ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Output from the proof process is handled lazily, so that only +;; the output from the last of multiple commands is actually +;; processed (assuming they're all successful) + +(defvar proof-shell-delayed-output nil + "The last interesting output the proof process output, and what to do + with it.") + +(defvar proof-analyse-using-stack nil + "Are annotations sent by proof assistant local or global") + +;; FIXME: da: what's magical value 128 below? should be in defconst? +(defun proof-shell-analyse-structure (string) + (save-excursion + (let* ((ip 0) (op 0) ap (l (length string)) + (ann (make-string (length string) ?x)) + (stack ()) (topl ()) + (out (make-string l ?x)) c span) + (while (< ip l) + (if (< (setq c (aref string ip)) 128) + (progn (aset out op c) + (incf op))) + (incf ip)) + (display-buffer (set-buffer proof-pbp-buffer)) + (erase-buffer) + (insert (substring out 0 op)) + + (setq ip 0 + op 1) + (while (< ip l) + (setq c (aref string ip)) + (cond + ((= c proof-shell-goal-char) + (setq topl (cons op topl)) + (setq ap 0)) + ((= c proof-shell-start-char) + (if proof-analyse-using-stack + (setq ap (- ap (- (aref string (incf ip)) 128))) + (setq ap (- (aref string (incf ip)) 128))) + (incf ip) + (while (not (= (setq c (aref string ip)) proof-shell-end-char)) + (aset ann ap (- c 128)) + (incf ap) + (incf ip)) + (setq stack (cons op (cons (substring ann 0 ap) stack)))) + ((= c proof-shell-field-char) + (setq span (make-span (car stack) op)) + (set-span-property span 'mouse-face 'highlight) + (set-span-property span 'proof (car (cdr stack))) + ;; Pop annotation off stack + (and proof-analyse-using-stack + (progn + (setq ap 0) + (while (< ap (length (cadr stack))) + (aset ann ap (aref (cadr stack) ap)) + (incf ap)))) + ;; Finish popping annotations + (setq stack (cdr (cdr stack)))) + (t (incf op))) + (incf ip)) + (setq topl (reverse (cons (point-max) topl))) + ;; If we want Coq pbp: (setq coq-current-goal 1) + (while (setq ip (car topl) + topl (cdr topl)) + (pbp-make-top-span ip (car topl)))))) + +(defun proof-shell-strip-annotations (string) + (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x ))) + (while (< ip l) + (if (>= (aref string ip) proof-shell-first-special-char) + (if (char-equal (aref string ip) proof-shell-start-char) + (progn (incf ip) + (while (< (aref string ip) proof-shell-first-special-char) + (incf ip)))) + (aset out op (aref string ip)) + (incf op)) + (incf ip)) + (substring out 0 op))) + +(defun proof-shell-handle-delayed-output () + (let ((ins (car proof-shell-delayed-output)) + (str (cdr proof-shell-delayed-output))) + (display-buffer proof-pbp-buffer) + (save-excursion + (cond + ((eq ins 'insert) + (setq str (proof-shell-strip-annotations str)) + (set-buffer proof-pbp-buffer) + (erase-buffer) + (insert str)) + ((eq ins 'analyse) + (proof-shell-analyse-structure str)) + (t (set-buffer proof-pbp-buffer) + (insert "\n\nbug???"))))) + (run-hooks 'proof-shell-handle-delayed-output-hook) + (setq proof-shell-delayed-output (cons 'insert "done"))) + +(defun proof-shell-handle-error (cmd string) + (save-excursion + (display-buffer (set-buffer proof-pbp-buffer)) + (if (not (eq proof-shell-delayed-output (cons 'insert "done"))) + (progn + (set-buffer proof-pbp-buffer) + (erase-buffer) + (insert (proof-shell-strip-annotations + (cdr proof-shell-delayed-output))))) + (goto-char (point-max)) + (if (re-search-backward pbp-error-regexp nil t) + (delete-region (- (point) 2) (point-max))) + (newline 2) + (insert-string string) + (beep)) + (set-buffer proof-script-buffer) + (proof-detach-queue) + (delete-spans (proof-locked-end) (point-max) 'type) + (proof-release-lock) + (run-hooks 'proof-shell-handle-error-hook)) + +(defun proof-shell-handle-interrupt () + (save-excursion + (display-buffer (set-buffer proof-pbp-buffer)) + (goto-char (point-max)) + (newline 2) + (insert-string + "Interrupt: Script Management may be in an inconsistent state\n") + (beep)) + (set-buffer proof-script-buffer) + (if proof-shell-busy + (progn (proof-detach-queue) + (delete-spans (proof-locked-end) (point-max) 'type) + (proof-release-lock)))) + + +(defun proof-goals-pos (span maparg) + "Given a span, this function returns the start of it if corresponds + to a goal and nil otherwise." + (and (eq 'goal (car (span-property span 'proof-top-element))) + (span-start span))) + +(defun proof-pbp-focus-on-first-goal () + "If the `proof-pbp-buffer' contains goals, the first one is brought + into view." + (and (fboundp 'map-extents) + (let + ((pos (map-extents 'proof-goals-pos proof-pbp-buffer + nil nil nil nil 'proof-top-element))) + (and pos (set-window-point + (get-buffer-window proof-pbp-buffer t) pos))))) + + + +(defun proof-shell-process-output (cmd string) + "Deals with errors, start of proofs, abortions of proofs and + completions of proofs. All other output from the proof engine is + simply reported to the user in the RESPONSE buffer. To extend this + function, set `proof-shell-process-output-system-specific'. + + The basic output processing function - it can return one of 4 + things: 'error, 'interrupt, 'loopback, or nil. 'loopback means this + was output from pbp, and should be inserted into the script buffer + and sent back to the proof assistant." + (cond + ((string-match proof-shell-error-regexp string) + (cons 'error (proof-shell-strip-annotations + (substring string (match-beginning 0))))) + + ((string-match proof-shell-interrupt-regexp string) + 'interrupt) + + ((and proof-shell-abort-goal-regexp + (string-match proof-shell-abort-goal-regexp string)) + (setq proof-shell-delayed-output (cons 'insert "\n\nAborted")) + ()) + + ((string-match proof-shell-proof-completed-regexp string) + (setq proof-shell-delayed-output + (cons 'insert (concat "\n" (match-string 0 string))))) + + ((string-match proof-shell-start-goals-regexp string) + (let (start end) + (while (progn (setq start (match-end 0)) + (string-match proof-shell-start-goals-regexp + string start))) + (setq end (string-match proof-shell-end-goals-regexp string start)) + (setq proof-shell-delayed-output + (cons 'analyse (substring string start end))))) + + ((string-match proof-shell-result-start string) + (let (start end) + (setq start (+ 1 (match-end 0))) + (string-match proof-shell-result-end string) + (setq end (- (match-beginning 0) 1)) + (cons 'loopback (substring string start end)))) + + ;; hook to tailor proof-shell-process-output to a specific proof + ;; system + ((and proof-shell-process-output-system-specific + (funcall (car proof-shell-process-output-system-specific) + cmd string)) + (funcall (cdr proof-shell-process-output-system-specific) + cmd string)) + + (t (setq proof-shell-delayed-output (cons 'insert string))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Low-level commands for shell communication ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-shell-insert (string) + (set-buffer proof-shell-buffer) + (goto-char (point-max)) + + (run-hooks 'proof-shell-insert-hook) + (insert string) + + ;; xemacs and emacs19 have different semantics for what happens when + ;; shell input is sent next to a marker + ;; the following code accommodates both definitions + (if (marker-position proof-marker) + (let ((inserted (point))) + (comint-send-input) + (set-marker proof-marker inserted)) + (comint-send-input))) + +(defun proof-send (string) + (let ((l (length string)) (i 0)) + (while (< i l) + (if (= (aref string i) ?\n) (aset string i ?\ )) + (incf i))) + (save-excursion (proof-shell-insert string))) + +;; Note that this is not really intended for anything complicated - +;; just to stop the user accidentally sending a command while the +;; queue is running. +(defun proof-check-process-available (&optional relaxed) + "Checks + (1) Is a proof process running? + (2) Is the proof process idle? + (3) Does the current buffer own the proof process? + (4) Is the current buffer a proof script? + and signals an error if at least one of the conditions is not + fulfilled. If relaxed is set, only (1) and (2) are tested." + (if (proof-shell-live-buffer) + (cond + (proof-shell-busy (error "Proof Process Busy!")) + (relaxed ()) ;exit cond + ((not (eq proof-script-buffer (current-buffer))) + (error "Don't own proof process")))) + (if (not (or relaxed (eq proof-buffer-type 'script))) + (error "Must be running in a script buffer"))) + +(defun proof-grab-lock (&optional relaxed) + (proof-start-shell) + (proof-check-process-available relaxed) + (setq proof-shell-busy t)) + +(defun proof-release-lock () + (if (proof-shell-live-buffer) + (progn + (if (not proof-shell-busy) + (error "Bug: Proof process not busy")) + (if (not (eq proof-script-buffer (current-buffer))) + (error "Bug: Don't own process")) + (setq proof-shell-busy nil)))) + +; Pass start and end as nil if the cmd isn't in the buffer. + +(defun proof-start-queue (start end alist &optional relaxed) + (if start + (proof-set-queue-endpoints start end)) + (let (item) + (while (and alist (string= + (nth 1 (setq item (car alist))) + "COMMENT")) + (funcall (nth 2 item) (car item)) + (setq alist (cdr alist))) + (if alist + (progn + (proof-grab-lock relaxed) + (setq proof-shell-delayed-output (cons 'insert "Done.")) + (setq proof-action-list alist) + (proof-send (nth 1 item)))))) + +; returns t if it's run out of input + +(defun proof-shell-exec-loop () + (save-excursion + (set-buffer proof-script-buffer) + (if (null proof-action-list) (error "Non Sequitur")) + (let ((item (car proof-action-list))) + (funcall (nth 2 item) (car item)) + (setq proof-action-list (cdr proof-action-list)) + (while (and proof-action-list + (string= + (nth 1 (setq item (car proof-action-list))) + "COMMENT")) + (funcall (nth 2 item) (car item)) + (setq proof-action-list (cdr proof-action-list))) + (if (null proof-action-list) + (progn (proof-release-lock) + (proof-detach-queue) + t) + (proof-send (nth 1 item)) + nil)))) + +(defun proof-shell-insert-loopback-cmd (cmd) + "Insert command sequence triggered by the proof process +at the end of locked region (after inserting a newline and indenting)." + (save-excursion + (set-buffer proof-script-buffer) + (let (span) + (proof-goto-end-of-locked) + (newline-and-indent) + (insert cmd) + (setq span (make-span (proof-locked-end) (point))) + (set-span-property span 'type 'pbp) + (set-span-property span 'cmd cmd) + (proof-set-queue-endpoints (proof-locked-end) (point)) + (setq proof-action-list + (cons (car proof-action-list) + (cons (list span cmd 'proof-done-advancing) + (cdr proof-action-list))))))) + +;; ******** NB ********** +;; While we're using pty communication, this code is OK, since all +;; eager annotations are one line long, and we get input a line at a +;; time. If we go over to piped communication, it will break. + +(defun proof-shell-popup-eager-annotation () + "Eager annotations are annotations which the proof system produces +while it's doing something (e.g. loading libraries) to say how much +progress it's made. Obviously we need to display these as soon as they +arrive." + (let (mrk str file module) + (save-excursion + (goto-char (point-max)) + (search-backward proof-shell-eager-annotation-start) + (setq mrk (+ 1 (point))) + (search-forward proof-shell-eager-annotation-end) + (setq str (buffer-substring mrk (- (point) 1))) + (display-buffer (set-buffer proof-pbp-buffer)) + (goto-char (point-max)) + (insert str "\n")) + (if (string-match "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]" str) + (progn + (setq file (match-string 2 str) + module (match-string 1 str)) + (if (string= file "") + (setq file (buffer-file-name proof-script-buffer))) + (setq file (expand-file-name file)) + (if (string-match "\\(.*\\)\\.." file) + (setq file (match-string 1 file))) + (setq proof-included-files-list (cons (cons module file) + proof-included-files-list)))))) + +(defun proof-shell-filter (str) + "The filter for the shell-process. We sleep until we get a + wakeup-char in the input, then run proof-shell-process-output, and + set proof-marker to keep track of how far we've got." + (if (string-match proof-shell-eager-annotation-end str) + (proof-shell-popup-eager-annotation)) + (if (or + ;; Some proof systems can be hacked to have annotated prompts; + ;; for these we set proof-shell-wakeup-char to the annotation special. + (and proof-shell-wakeup-char + (string-match (char-to-string proof-shell-wakeup-char) str)) + ;; Others rely on a standard top-level (e.g. SML) whose prompt can't + ;; be hacked. For those we use the prompt regexp. + (string-match proof-shell-annotated-prompt-regexp str)) + (if (null (marker-position proof-marker)) + ;; Set marker to first prompt in output buffer, and sleep again. + (progn + (goto-char (point-min)) + (re-search-forward proof-shell-annotated-prompt-regexp) + ;; FIXME: da: why is this next line here? to delete the + ;; possibly several character prompt? why? + ;; TMS: Its purpose is to remove the wakeup + ;; character associated with the prompt. This + ;; should not be necessary anymore, because the wakeup + ;; character isn't displayed anyway; see + ;; `proof-dont-show-annotations'. Watch this space! + (backward-delete-char 1) + (set-marker proof-marker (point))) + ;; We've matched against a second prompt in str now. Search + ;; the output buffer for the second prompt after the one previously + ;; marked. + (let (string res cmd) + (goto-char (marker-position proof-marker)) + (re-search-forward proof-shell-annotated-prompt-regexp nil t) + (backward-char (- (match-end 0) (match-beginning 0))) + (setq string (buffer-substring (marker-position proof-marker) + (point))) + (goto-char (point-max)) ; da: assumed to be after a prompt? + (backward-delete-char 1) ; da: WHY? nasty assumption. + (setq cmd (nth 1 (car proof-action-list))) + (save-excursion + (setq res (proof-shell-process-output cmd string)) + (cond + ((and (consp res) (eq (car res) 'error)) + (proof-shell-handle-error cmd (cdr res))) + ((eq res 'interrupt) + (proof-shell-handle-interrupt)) + ((and (consp res) (eq (car res) 'loopback)) + (proof-shell-insert-loopback-cmd (cdr res)) + (proof-shell-exec-loop)) + (t (if (proof-shell-exec-loop) + (proof-shell-handle-delayed-output))))))))) + +(defun proof-last-goal-or-goalsave () + (save-excursion + (let ((span (span-at-before (proof-locked-end) 'type))) + (while (and span + (not (eq (span-property span 'type) 'goalsave)) + (or (eq (span-property span 'type) 'comment) + (not (funcall proof-goal-command-p + (span-property span 'cmd))))) + (setq span (prev-span span 'type))) + span))) + +;; This needs some work to make it generic, since most of the code +;; doesn't apply to Coq at all. +(defun proof-steal-process () + "This allows us to steal the process if we want to change the buffer + in which script management is running." + (proof-start-shell) + (if proof-shell-busy (error "Proof Process Busy!")) + (if (not (eq proof-buffer-type 'script)) + (error "Must be running in a script buffer")) + (cond + ((eq proof-script-buffer (current-buffer)) + nil) + (t + (let ((flist proof-included-files-list) + (file (expand-file-name (buffer-file-name))) span (cmd "")) + (if (string-match "\\(.*\\)\\.." file) (setq file (match-string 1 file))) + (while (and flist (not (string= file (cdr (car flist))))) + (setq flist (cdr flist))) + (if (null flist) + (if (not (y-or-n-p "Steal script management? " )) (error "Aborted")) + (if (not (y-or-n-p "Reprocess this file? " )) (error "Aborted"))) + (if (not (buffer-name proof-script-buffer)) + (message "Warning: Proof script buffer deleted: proof state may be inconsistent") + (save-excursion + (set-buffer proof-script-buffer) + (setq proof-active-buffer-fake-minor-mode nil) + (setq span (proof-last-goal-or-goalsave)) + ;; This won't work for Coq if we have recursive goals in progress + (if (and span (not (eq (span-property span 'type) 'goalsave))) + (setq cmd proof-kill-goal-command)) + (proof-detach-segments) + (delete-spans (point-min) (point-max) 'type))) + + (setq proof-script-buffer (current-buffer)) + (proof-init-segmentation) + (setq proof-active-buffer-fake-minor-mode t) + + (cond + (flist + (list nil (concat cmd "ForgetMark " (car (car flist)) ";") + `(lambda (span) (setq proof-included-files-list + (quote ,(cdr flist)))))) + ((not (string= cmd "")) + (list nil cmd 'proof-done-invisible)) + (t nil)))))) + +(defun proof-done-invisible (span) ()) + +(defun proof-invisible-command (cmd &optional relaxed) + "Send cmd to the proof process without responding to the user." + (proof-check-process-available relaxed) + (if (not (string-match proof-re-end-of-cmd cmd)) + (setq cmd (concat cmd proof-terminal-string))) + (proof-start-queue nil nil (list (list nil cmd + 'proof-done-invisible)) relaxed)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; User Commands ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; Script management uses two major segments: Locked, which marks text +; which has been sent to the proof assistant and cannot be altered +; without being retracted, and Queue, which contains stuff being +; queued for processing. proof-action-list contains a list of +; (span,command,action) triples. The loop looks like: Execute the +; command, and if it's successful, do action on span. If the +; command's not successful, we bounce the rest of the queue and do +; some error processing. +; +; when a span has been processed, we classify it as follows: +; 'goalsave - denoting a 'goalsave pair in the locked region +; a 'goalsave region has a 'name property which is the name of the goal +; 'comment - denoting a comment +; 'pbp - denoting a span created by pbp +; 'vanilla - denoting any other span. +; 'pbp & 'vanilla spans have a property 'cmd, which says what +; command they contain. + +; We don't allow commands while the queue has anything in it. So we +; do configuration by concatenating the config command on the front in +; proof-send + +;; proof-assert-until-point, and various gunk for its ;; +;; setup and callback ;; + +;; This code is for nested goals in Coq, and shouldn't affect things +;; in LEGO. It lifts "local" lemmas from inside goals out to top +;; level. + +(defun proof-lift-global (glob-span) + (let (start (next (span-at 1 'type)) str (goal-p nil)) + (while (and next (and (not (eq next glob-span)) (not goal-p))) + (if (and (eq (span-property next 'type) 'vanilla) + (funcall proof-goal-command-p (span-property next 'cmd))) + (setq goal-p t) + (setq next (next-span next 'type)))) + + (if (and next (not (eq next glob-span))) + (progn + (proof-unlock-locked) + (setq str (buffer-substring (span-start glob-span) + (span-end glob-span))) + (delete-region (span-start glob-span) (span-end glob-span)) + (goto-char (span-start next)) + (setq start (point)) + (insert str "\n") + (set-span-endpoints glob-span start (point)) + (set-span-start next (point)) + (proof-lock-unlocked))))) + +;; This is the actual callback for assert-until-point. + +(defun proof-done-advancing (span) + (let ((end (span-end span)) nam gspan next cmd) + (proof-set-locked-end end) + (proof-set-queue-start end) + (setq cmd (span-property span 'cmd)) + (cond + ((eq (span-property span 'type) 'comment) + (set-span-property span 'mouse-face 'highlight)) + ((string-match proof-save-command-regexp cmd) + ;; In coq, we have the invariant that if we've done a save and + ;; there's a top-level declaration then it must be the + ;; associated goal. (Notice that because it's a callback it + ;; must have been approved by the theorem prover.) + (if (string-match proof-save-with-hole-regexp cmd) + (setq nam (match-string 2 cmd))) + (setq gspan span) + (while (or (eq (span-property gspan 'type) 'comment) + (not (funcall proof-goal-command-p + (setq cmd (span-property gspan 'cmd))))) + (setq next (prev-span gspan 'type)) + (delete-span gspan) + (setq gspan next)) + + (if (null nam) + (if (string-match proof-goal-with-hole-regexp + (span-property gspan 'cmd)) + (setq nam (match-string 2 (span-property gspan 'cmd))) + ;; This only works for Coq, but LEGO raises an error if + ;; there's no name. + ;; FIXME: a nonsense for Isabelle. + (setq nam "Unnamed_thm"))) + + (set-span-end gspan end) + (set-span-property gspan 'mouse-face 'highlight) + (set-span-property gspan 'type 'goalsave) + (set-span-property gspan 'name nam) + + (proof-lift-global gspan)) + (t + (set-span-property span 'mouse-face 'highlight) + (if (funcall proof-global-p cmd) + (proof-lift-global span)))))) + +; depth marks number of nested comments. quote-parity is false if +; we're inside ""'s. Only one of (depth > 0) and (not quote-parity) +; should be true at once. -- hhg + +(defun proof-segment-up-to (pos) + "Create a list of (type,int,string) pairs from the end of the locked +region to pos, denoting the command and the position of its +terminator. type is one of comment, or cmd. 'unclosed-comment may be +consed onto the start if the segment finishes with an unclosed +comment." + (save-excursion + (let ((str (make-string (- (buffer-size) (proof-locked-end) -10) ?x)) + (i 0) (depth 0) (quote-parity t) done alist c) + (proof-goto-end-of-locked) + (while (not done) + (cond + ((and (= (point) pos) (> depth 0)) + (setq done t alist (cons 'unclosed-comment alist))) + ((= (point) (point-max)) + (if (not quote-parity) + (message "Warning: unclosed quote")) + (setq done t)) + ((and (looking-at "\\*)") quote-parity) + (if (= depth 0) + (progn (message "Warning: extraneous comment end") (setq done t)) + (setq depth (- depth 1)) (forward-char 2) + (if (eq i 0) + (setq alist (cons (list 'comment "" (point)) alist)) + (aset str i ?\ ) (incf i)))) + ((and (looking-at "(\\*") quote-parity) + (setq depth (+ depth 1)) (forward-char 2)) + ((> depth 0) (forward-char)) + (t + (setq c (char-after (point))) + (if (or (> i 0) (not (= (char-syntax c) ?\ ))) + (progn (aset str i c) (incf i))) + (if (looking-at "\"") + (setq quote-parity (not quote-parity))) + (forward-char) + (if (and (= c proof-terminal-char) quote-parity) + (progn + (setq alist + (cons (list 'cmd (substring str 0 i) (point)) alist)) + (if (>= (point) pos) (setq done t) (setq i 0))))))) + alist))) + +(defun proof-semis-to-vanillas (semis &optional callback-fn) + "Convert a sequence of semicolon positions (returned by the above +function) to a set of vanilla extents." + (let ((ct (proof-locked-end)) span alist semi) + (while (not (null semis)) + (setq semi (car semis) + span (make-span ct (nth 2 semi)) + ct (nth 2 semi)) + (if (eq (car (car semis)) 'cmd) + (progn + (set-span-property span 'type 'vanilla) + (set-span-property span 'cmd (nth 1 semi)) + (setq alist (cons (list span (nth 1 semi) + (or callback-fn 'proof-done-advancing)) + alist))) + (set-span-property span 'type 'comment) + (setq alist (cons (list span "COMMENT" 'proof-done-advancing) alist))) + (setq semis (cdr semis))) + (nreverse alist))) + +; Assert until point - We actually use this to implement the +; assert-until-point, active terminator keypress, and find-next-terminator. +; In different cases we want different things, but usually the information +; (i.e. are we inside a comment) isn't available until we've actually run +; proof-segment-up-to (point), hence all the different options when we've +; done so. + +(defun proof-assert-until-point + (&optional unclosed-comment-fun ignore-proof-process-p) + "Process the region from the end of the locked-region until point. + Default action if inside a comment is just to go until the start of + the comment. If you want something different, put it inside + unclosed-comment-fun. If ignore-proof-process-p is set, no commands + will be added to the queue." + (interactive) + (let ((pt (point)) + (crowbar (or ignore-proof-process-p (proof-steal-process))) + semis) + (save-excursion + (if (not (re-search-backward "\\S-" (proof-locked-end) t)) + (progn (goto-char pt) + (error "Nothing to do!"))) + (setq semis (proof-segment-up-to (point)))) + (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) + (funcall unclosed-comment-fun) + (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) + (if (and (not ignore-proof-process-p) (not crowbar) (null semis)) + (error "Nothing to do!")) + (goto-char (nth 2 (car semis))) + (and (not ignore-proof-process-p) + (let ((vanillas (proof-semis-to-vanillas (nreverse semis)))) + (if crowbar (setq vanillas (cons crowbar vanillas))) + (proof-start-queue (proof-locked-end) (point) vanillas)))))) + +;; insert-pbp-command - an advancing command, for use when ;; +;; PbpHyp or Pbp has executed in LEGO, and returned a ;; +;; command for us to run ;; + +(defun proof-insert-pbp-command (cmd) + (proof-check-process-available) + (let (span) + (proof-goto-end-of-locked) + (insert cmd) + (setq span (make-span (proof-locked-end) (point))) + (set-span-property span 'type 'pbp) + (set-span-property span 'cmd cmd) + (proof-start-queue (proof-locked-end) (point) + (list (list span cmd 'proof-done-advancing))))) + + +;; proof-retract-until-point and associated gunk ;; +;; most of the hard work (i.e computing the commands to do ;; +;; the retraction) is implemented in the customisation ;; +;; module (lego.el or coq.el) which is why this looks so ;; +;; straightforward ;; + + +(defun proof-done-retracting (span) + "Updates display after proof process has reset its state. See also +the documentation for `proof-retract-until-point'. It optionally +deletes the region corresponding to the proof sequence." + (let ((start (span-start span)) + (end (span-end span)) + (kill (span-property span 'delete-me))) + (proof-set-locked-end start) + (proof-set-queue-end start) + (delete-spans start end 'type) + (delete-span span) + (if kill (delete-region start end)))) + +(defun proof-setup-retract-action (start end proof-command delete-region) + (let ((span (make-span start end))) + (set-span-property span 'delete-me delete-region) + (list (list span proof-command 'proof-done-retracting)))) + +(defun proof-retract-target (target delete-region) + (let ((end (proof-locked-end)) + (start (span-start target)) + (span (proof-last-goal-or-goalsave)) + actions) + + (if (and span (not (eq (span-property span 'type) 'goalsave))) + (if (< (span-end span) (span-end target)) + (progn + (setq span target) + (while (and span (eq (span-property span 'type) 'comment)) + (setq span (next-span span 'type))) + (setq actions (proof-setup-retract-action + start end + (if (null span) "COMMENT" + (funcall proof-count-undos-fn span)) + delete-region) + end start)) + + (setq actions (proof-setup-retract-action (span-start span) end + proof-kill-goal-command + delete-region) + end (span-start span)))) + + (if (> end start) + (setq actions + (nconc actions (proof-setup-retract-action + start end + (funcall proof-find-and-forget-fn target) + delete-region)))) + + (proof-start-queue (min start end) (proof-locked-end) actions))) + +(defun proof-retract-until-point (&optional delete-region) + "Sets up the proof process for retracting until point. In + particular, it sets a flag for the filter process to call + `proof-done-retracting' after the proof process has actually + successfully reset its state. It optionally deletes the region in + the proof script corresponding to the proof command sequence. If + this function is invoked outside a locked region, the last + successfully processed command is undone." + (interactive) + (proof-check-process-available) + (let ((span (span-at (point) 'type))) + (if (null (proof-locked-end)) (error "No locked region")) + (and (null span) + (progn (proof-goto-end-of-locked) (backward-char) + (setq span (span-at (point) 'type)))) + (proof-retract-target span delete-region))) + +;; proof-try-command ;; +;; this isn't really in the spirit of script management, ;; +;; but sometimes the user wants to just try an expression ;; +;; without having to undo it in order to try something ;; +;; different. Of course you can easily lose sync by doing ;; +;; something here which changes the proof state ;; + +(defun proof-done-trying (span) + (delete-span span) + (proof-detach-queue)) + +(defun proof-try-command + (&optional unclosed-comment-fun) + + "Process the command at point, + but don't add it to the locked region. This will only happen if + the command satisfies proof-state-preserving-p. + + Default action if inside a comment is just to go until the start of + the comment. If you want something different, put it inside + unclosed-comment-fun." + (interactive) + (let ((pt (point)) semis crowbar test) + (setq crowbar (proof-steal-process)) + (save-excursion + (if (not (re-search-backward "\\S-" (proof-locked-end) t)) + (progn (goto-char pt) + (error "Nothing to do!"))) + (setq semis (proof-segment-up-to (point)))) + (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) + (funcall unclosed-comment-fun) + (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) + (if (and (not crowbar) (null semis)) (error "Nothing to do!")) + (setq test (car semis)) + (if (not (funcall proof-state-preserving-p (nth 1 test))) + (error "Command is not state preserving")) + (goto-char (nth 2 test)) + (let ((vanillas (proof-semis-to-vanillas (list test) + 'proof-done-trying))) + (if crowbar (setq vanillas (cons crowbar vanillas))) + (proof-start-queue (proof-locked-end) (point) vanillas))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; misc other user functions ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun proof-undo-last-successful-command () + "Undo last successful command, both in the buffer recording the + proof script and in the proof process. In particular, it deletes + the corresponding part of the proof script." + (interactive) + (goto-char (span-start (span-at-before (proof-locked-end) 'type))) + (proof-retract-until-point t)) + +(defun proof-interrupt-process () + (interactive) + (if (not (proof-shell-live-buffer)) + (error "Proof Process Not Started!")) + (if (not (eq proof-script-buffer (current-buffer))) + (error "Don't own process!")) + (if (not proof-shell-busy) + (error "Proof Process Not Active!")) + (save-excursion + (set-buffer proof-shell-buffer) + (comint-interrupt-subjob))) + + +(defun proof-find-next-terminator () + "Set point after next `proof-terminal-char'." + (interactive) + (let ((cmd (span-at (point) 'type))) + (if cmd (goto-char (span-end cmd)) + (and (re-search-forward "\\S-" nil t) + (proof-assert-until-point nil 'ignore-proof-process))))) + +(defun proof-process-buffer () + "Process the current buffer and set point at the end of the buffer." + (interactive) + (end-of-buffer) + (proof-assert-until-point)) + +;; For when things go horribly wrong + +(defun proof-restart-script () + (interactive) + (save-excursion + (if (buffer-live-p proof-script-buffer) + (progn + (set-buffer proof-script-buffer) + (setq proof-active-buffer-fake-minor-mode nil) + (delete-spans (point-min) (point-max) 'type) + (proof-detach-segments))) + (setq proof-shell-busy nil + proof-script-buffer nil) + (if (buffer-live-p proof-shell-buffer) + (kill-buffer proof-shell-buffer)) + (if (buffer-live-p proof-pbp-buffer) + (kill-buffer proof-pbp-buffer)))) + +;; A command for making things go horribly wrong - it moves the +;; end-of-locked-region marker backwards, so user had better move it +;; correctly to sync with the proof state, or things will go all +;; pear-shaped. + +(defun proof-frob-locked-end () + (interactive) + "Move the end of the locked region backwards. + Only for use by consenting adults." + (cond + ((not (eq proof-script-buffer (current-buffer))) + (error "Not in proof buffer")) + ((> (point) (proof-locked-end)) + (error "Can only move backwards")) + (t (proof-set-locked-end (point)) + (delete-spans (proof-locked-end) (point-max) 'type)))) + +(defvar proof-minibuffer-history nil + "The last command read from the minibuffer") + +(defun proof-execute-minibuffer-cmd () + (interactive) + (let (cmd) + (proof-check-process-available 'relaxed) + (setq cmd (read-string "Command: " nil 'proof-minibuffer-history)) + (proof-invisible-command cmd 'relaxed))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Popup and Pulldown Menu ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;; Menu commands for the underlying proof assistant +(defvar proof-ctxt-string "" + "Command to display context in proof assistant") + +(defvar proof-help-string "" + "Command to ask for help in proof assistant") + +(defvar proof-prf-string "" + "Command to display proof state in proof assistant") + +(defun proof-ctxt () + "List context." + (interactive) + (proof-invisible-command (concat proof-ctxt-string proof-terminal-string))) + +(defun proof-help () + "Print help message giving syntax." + (interactive) + (proof-invisible-command (concat proof-help-string proof-terminal-string))) + +(defun proof-prf () + "List proof state." + (interactive) + (proof-invisible-command (concat proof-prf-string proof-terminal-string))) + +;;; To be called from menu +(defun proof-info-mode () + "Info mode on proof mode." + (interactive) + (info "script-management")) + +(defun proof-exit () + "Exit Proof-assistant." + (interactive) + (proof-restart-script)) + +(defvar proof-help-menu + '("Help" + ["Proof assistant web page" + (w3-fetch proof-www-home-page) t] + ["Help on Emacs proof-mode" proof-info-mode t] + ) + "The Help Menu in Script Management.") + +(defvar proof-shared-menu + (append-element '( + ["Display context" proof-ctxt + :active (proof-shell-live-buffer)] + ["Display proof state" proof-prf + :active (proof-shell-live-buffer)] + ["Exit proof assistant" proof-exit + :active (proof-shell-live-buffer)] + "----" + ["Find definition/declaration" find-tag-other-window t] + ) + proof-help-menu)) + +(defvar proof-menu + (append '("Commands" + ["Toggle active terminator" proof-active-terminator-minor-mode + :active t + :style toggle + :selected proof-active-terminator-minor-mode] + "----") + (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) + "--:doubleLine" "----")) + proof-shared-menu + ) + "*The menu for the proof assistant.") + +(defvar proof-shell-menu proof-shared-menu + "The menu for the Proof-assistant shell") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Active terminator minor mode ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(deflocal proof-active-terminator-minor-mode nil + "active terminator minor mode flag") + +(defun proof-active-terminator-minor-mode (&optional arg) + "Toggle PROOF's Active Terminator minor mode. +With arg, turn on the Active Terminator minor mode if and only if arg +is positive. + +If Active terminator mode is enabled, a terminator will process the +current command." + + (interactive "P") + +;; has this minor mode been registered as such? + (or (assq 'proof-active-terminator-minor-mode minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (list '(proof-active-terminator-minor-mode + (concat " " proof-terminal-string)))))) + + (setq proof-active-terminator-minor-mode + (if (null arg) (not proof-active-terminator-minor-mode) + (> (prefix-numeric-value arg) 0))) + (if (fboundp 'redraw-modeline) + (redraw-modeline) + (force-mode-line-update))) + +(defun proof-process-active-terminator () + "Insert the terminator in an intelligent way and assert until the + new terminator. Fire up proof process if necessary." + (let ((mrk (point)) ins) + (if (looking-at "\\s-\\|\\'\\|\\w") + (if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t)) + (error "Nothing to do!"))) + (if (not (= (char-after (point)) proof-terminal-char)) + (progn (forward-char) (insert proof-terminal-string) (setq ins t))) + (proof-assert-until-point + (function (lambda () + (if ins (backward-delete-char 1)) + (goto-char mrk) (insert proof-terminal-string)))))) + +(defun proof-active-terminator () + (interactive) + (if proof-active-terminator-minor-mode + (proof-process-active-terminator) + (self-insert-command 1))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof mode configuration ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(define-derived-mode proof-mode fundamental-mode + proof-mode-name "Proof mode - not standalone" + ;; define-derived-mode proof-mode initialises proof-mode-map + (setq proof-buffer-type 'script)) + +;; This has to come after proof-mode is defined + +(define-derived-mode proof-shell-mode comint-mode + "proof-shell" "Proof shell mode - not standalone" + (setq proof-buffer-type 'shell) + (setq proof-shell-busy nil) + (setq proof-shell-delayed-output (cons 'insert "done")) + (setq comint-prompt-regexp proof-shell-prompt-pattern) + (add-hook 'comint-output-filter-functions 'proof-shell-filter nil t) + (setq comint-get-old-input (function (lambda () ""))) + (proof-dont-show-annotations) + (setq proof-marker (make-marker))) + +(easy-menu-define proof-shell-menu + proof-shell-mode-map + "Menu used in the proof assistant shell." + (cons proof-mode-name (cdr proof-shell-menu))) + +(easy-menu-define proof-mode-menu + proof-mode-map + "Menu used in proof mode." + (cons proof-mode-name (cdr proof-menu))) + +;; the following callback is an irritating hack - there should be some +;; elegant mechanism for computing constants after the child has +;; configured. + +(defun proof-config-done () + +;; calculate some strings and regexps for searching + + (setq proof-terminal-string (char-to-string proof-terminal-char)) + + (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) + (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) + + (make-local-variable 'comment-start) + (setq comment-start (concat proof-comment-start " ")) + (make-local-variable 'comment-end) + (setq comment-end (concat " " proof-comment-end)) + (make-local-variable 'comment-start-skip) + (setq comment-start-skip + (concat (regexp-quote proof-comment-start) "+\\s_?")) + + (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'")) + (setq proof-re-term-or-comment + (concat proof-terminal-string "\\|" (regexp-quote proof-comment-start) + "\\|" (regexp-quote proof-comment-end))) + +;; func-menu --- Jump to a goal within a buffer + (and (boundp 'fume-function-name-regexp-alist) + (defvar fume-function-name-regexp-proof + (cons proof-goal-with-hole-regexp 2)) + (push (cons major-mode 'fume-function-name-regexp-proof) + fume-function-name-regexp-alist)) + (and (boundp 'fume-find-function-name-method-alist) + (push (cons major-mode 'fume-match-find-next-function-name) + fume-find-function-name-method-alist)) + +;; Info + (or (memq proof-info-dir Info-default-directory-list) + (setq Info-default-directory-list + (cons proof-info-dir Info-default-directory-list))) + +;; keymaps and menus + (easy-menu-add proof-mode-menu proof-mode-map) + + (proof-define-keys proof-mode-map proof-universal-keys) + + (define-key proof-mode-map + (vconcat [(control c)] (vector proof-terminal-char)) + 'proof-active-terminator-minor-mode) + + (define-key proof-mode-map [(control c) (control e)] + 'proof-find-next-terminator) + + (define-key proof-mode-map (vector proof-terminal-char) + 'proof-active-terminator) + (define-key proof-mode-map [(control c) (return)] 'proof-assert-until-point) + (define-key proof-mode-map [(control c) (control t)] 'proof-try-command) + (define-key proof-mode-map [(control c) ?u] 'proof-retract-until-point) + (define-key proof-mode-map [(control c) (control u)] + 'proof-undo-last-successful-command) + + (define-key proof-mode-map [(control c) ?\'] + 'proof-goto-end-of-locked-interactive) + (define-key proof-mode-map [(control button1)] 'proof-send-span) + (define-key proof-mode-map [(control c) (control b)] 'proof-process-buffer) + (define-key proof-mode-map [(control c) (control z)] 'proof-frob-locked-end) + + (define-key proof-mode-map [tab] 'proof-indent-line) + (make-local-variable 'indent-line-function) + (setq indent-line-function 'proof-indent-line) + + (define-key (current-local-map) [(control c) (control p)] 'proof-prf) + (define-key (current-local-map) [(control c) ?c] 'proof-ctxt) + (define-key (current-local-map) [(control c) ?h] 'proof-help) + +;; For fontlock + (remove-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer t) + (add-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer nil t) + (remove-hook 'font-lock-mode-hook 'proof-unfontify-separator t) + (add-hook 'font-lock-mode-hook 'proof-unfontify-separator nil t) + +;; if we don't have the following, zap-commas fails to work. + + (and (boundp 'font-lock-always-fontify-immediately) + (setq font-lock-always-fontify-immediately t)) + + (run-hooks 'proof-mode-hook)) + +(defun proof-shell-config-done () + (accept-process-output (get-buffer-process (current-buffer))) + + ;; If the proof process in invoked on a different machine e.g., + ;; for proof-prog-name="rsh fastmachine proofprocess", one needs + ;; to adjust the directory: + (and proof-shell-cd + (proof-shell-insert (format proof-shell-cd + ;; under Emacs 19.34 default-directory contains "~" which causes + ;; problems with LEGO's internal Cd command + (expand-file-name default-directory)))) + + (if proof-shell-init-cmd + (proof-shell-insert proof-shell-init-cmd)) + +;; Note that proof-marker actually gets set in proof-shell-filter. +;; This is manifestly a hack, but finding somewhere more convenient +;; to do the setup is tricky. + + (while (null (marker-position proof-marker)) + (if (accept-process-output (get-buffer-process (current-buffer)) 15) + () + (error "Failed to initialise proof process")))) + +(define-derived-mode pbp-mode fundamental-mode + proof-mode-name "Proof by Pointing" + ;; defined-derived-mode pbp-mode initialises pbp-mode-map + (setq proof-buffer-type 'pbp) + (suppress-keymap pbp-mode-map 'all) +; (define-key pbp-mode-map [(button2)] 'pbp-button-action) + (proof-define-keys pbp-mode-map proof-universal-keys) + (erase-buffer)) + + +(provide 'proof) diff --git a/generic/span-extent.el b/generic/span-extent.el new file mode 100644 index 00000000..6e6183cd --- /dev/null +++ b/generic/span-extent.el @@ -0,0 +1,82 @@ +;;; This file implements spans in terms of extents, for xemacs. +;;; Copyright (C) 1998 LFCS Edinburgh +;;; Author: Healfdene Goguen + +;; Maintainer: LEGO Team + +;; $Log$ +;; Revision 1.1 1998/09/03 13:51:33 da +;; Renamed for new subdirectory structure +;; +;; Revision 2.0 1998/08/11 15:00:13 da +;; New branch +;; +;; Revision 1.4 1998/06/10 14:01:48 hhg +;; Wrote generic span functions for making spans read-only or read-write. +;; +;; Revision 1.3 1998/06/02 15:36:44 hhg +;; Corrected comment about this being for xemacs. +;; +;; Revision 1.2 1998/05/19 15:30:27 hhg +;; Added header and log message. +;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bridging the emacs19/xemacs gulf ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Now define "spans" in terms of extents. + +(defsubst make-span (start end) + (make-extent start end)) + +(defsubst detach-span (span) + (detach-extent span)) + +(defsubst set-span-endpoints (span start end) + (set-extent-endpoints span start end)) + +(defsubst set-span-start (span value) + (set-extent-endpoints span value (extent-end-position span))) + +(defsubst set-span-end (span value) + (set-extent-endpoints span (extent-start-position span) value)) + +(defsubst span-read-only (span) + (set-span-property span 'read-only t)) + +(defsubst span-read-write (span) + (set-span-property span 'read-only nil)) + +(defsubst span-property (span name) + (extent-property span name)) + +(defsubst set-span-property (span name value) + (set-extent-property span name value)) + +(defsubst delete-span (span) + (delete-extent span)) + +(defsubst delete-spans (start end prop) + (mapcar-extents 'delete-extent nil (current-buffer) start end nil prop)) + +(defsubst span-at (pt prop) + (extent-at pt nil prop)) + +(defsubst span-at-before (pt prop) + (extent-at pt nil prop nil 'before)) + +(defsubst span-start (span) + (extent-start-position span)) + +(defsubst span-end (span) + (extent-end-position span)) + +(defsubst prev-span (span prop) + (extent-at (extent-start-position span) nil prop nil 'before)) + +(defsubst next-span (span prop) + (extent-at (extent-end-position span) nil prop nil 'after)) + + +(provide 'span-extent) diff --git a/generic/span-overlay.el b/generic/span-overlay.el new file mode 100644 index 00000000..e67ad33c --- /dev/null +++ b/generic/span-overlay.el @@ -0,0 +1,291 @@ +;;; This file implements spans in terms of overlays, for emacs19. +;;; Copyright (C) 1998 LFCS Edinburgh +;;; Author: Healfdene Goguen + +;; Maintainer: LEGO Team + +;; $Log$ +;; Revision 1.1 1998/09/03 13:51:34 da +;; Renamed for new subdirectory structure +;; +;; Revision 2.0 1998/08/11 15:00:13 da +;; New branch +;; +;; Revision 1.9 1998/06/10 14:02:39 hhg +;; Wrote generic span functions for making spans read-only or read-write. +;; Fixed bug in add-span and remove-span concerning return value of +;; span-traverse. +;; +;; Revision 1.8 1998/06/10 12:41:47 hhg +;; Compare span-end first rather than span-start in span-lt, because +;; proof-lock-span is often changed and has starting point 1. +;; Factored out common code of add-span and remove-span into +;; span-traverse. +;; +;; Revision 1.7 1998/06/03 17:40:07 hhg +;; Changed last-span to before-list. +;; Added definitions of foldr and foldl if they aren't already loaded. +;; Changed definitions of add-span, remove-span and find-span-aux to be +;; non-recursive. +;; Removed detach-extent since this file isn't used by xemacs. +;; Added function append-unique to avoid repetitions in list generated by +;; spans-at-region. +;; Changed next-span so it uses member-if. +;; +;; Revision 1.6 1998/06/02 15:36:51 hhg +;; Corrected comment about this being for emacs19. +;; +;; Revision 1.5 1998/05/29 09:50:10 tms +;; o outsourced indentation to proof-indent +;; o support indentation of commands +;; o replaced test of Emacs version with availability test of specific +;; features +;; o C-c C-c, C-c C-v and M-tab is now available in all buffers +;; +;; Revision 1.4 1998/05/21 17:27:41 hhg +;; Removed uninitialized os variable in spans-at-region. +;; +;; Revision 1.3 1998/05/21 08:28:52 hhg +;; Initialize 'before pointer in add-span-aux when last-span is nil. +;; Removed span-at-type. +;; Fixed bug in span-at-before, where (span-start span) may be nil. +;; Added spans-at-(point|region)[-prop], which fixes bug of C-c u at end +;; of buffer. +;; +;; Revision 1.2 1998/05/19 15:31:37 hhg +;; Added header and log message. +;; Fixed set-span-endpoints so it preserves invariant. +;; Changed add-span and remove-span so that they update last-span +;; correctly themselves, and don't take last-span as an argument. +;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bridging the emacs19/xemacs gulf ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; before-list represents a linked list of spans for each buffer. +;; It has the invariants of: +;; * being ordered wrt the starting point of the spans in the list, +;; with detached spans at the end. +;; * not having overlapping overlays of the same type. + +(defvar before-list nil + "Start of backwards-linked list of spans") + +(make-variable-buffer-local 'before-list) + + +(or (fboundp 'foldr) +(defun foldr (func a seq) + "Return (func (func (func (... (func a Sn) ...) S2) S1) S0) +when func's argument is 2 and seq is a sequence whose +elements = S0 S1 S2 ... Sn. [tl-seq.el]" + (let ((i (length seq))) + (while (> i 0) + (setq i (1- i)) + (setq a (funcall func a (elt seq i))) + ) + a))) + +(or (fboundp 'foldl) +(defun foldl (func a seq) + "Return (... (func (func (func a S0) S1) S2) ...) +when func's argument is 2 and seq is a sequence whose +elements = S0 S1 S2 .... [tl-seq.el]" + (let ((len (length seq)) + (i 0)) + (while (< i len) + (setq a (funcall func a (elt seq i))) + (setq i (1+ i)) + ) + a))) + +(defsubst span-start (span) + (overlay-start span)) + +(defsubst span-end (span) + (overlay-end span)) + +(defun set-span-property (span name value) + (overlay-put span name value)) + +(defsubst span-property (span name) + (overlay-get span name)) + +(defun span-read-only-hook (overlay after start end &optional len) + (error "Region is read-only")) + +(defun span-read-only (span) + (set-span-property span 'modification-hooks '(span-read-only-hook)) + (set-span-property span 'insert-in-front-hooks '(span-read-only-hook))) + +(defun span-read-write (span) + (set-span-property span 'modification-hooks nil) + (set-span-property span 'insert-in-front-hooks nil)) + +(defun int-nil-lt (m n) + (cond + ((eq m n) nil) + ((not n) t) + ((not m) nil) + (t (< m n)))) + +;; We use end first because proof-locked-queue is often changed, and +;; its starting point is always 1 +(defun span-lt (s u) + (or (int-nil-lt (span-end s) (span-end u)) + (and (eq (span-end s) (span-end u)) + (int-nil-lt (span-start s) (span-start u))))) + +(defun span-traverse (span prop) + (cond + ((not before-list) + ;; before-list empty + 'empty) + ((funcall prop before-list span) + ;; property holds for before-list and span + 'hd) + (t + ;; traverse before-list for property + (let ((l before-list) (before (span-property before-list 'before))) + (while (and before (not (funcall prop before span))) + (setq l before) + (setq before (span-property before 'before))) + l)))) + +(defun add-span (span) + (let ((ans (span-traverse span 'span-lt))) + (cond + ((eq ans 'empty) + (set-span-property span 'before nil) + (setq before-list span)) + ((eq ans 'hd) + (set-span-property span 'before before-list) + (setq before-list span)) + (t + (set-span-property span 'before + (span-property ans 'before)) + (set-span-property ans 'before span))))) + +(defun make-span (start end) + (add-span (make-overlay start end))) + +(defun remove-span (span) + (let ((ans (span-traverse span 'eq))) + (cond + ((eq ans 'empty) + (error "Bug: empty span list")) + ((eq ans 'hd) + (setq before-list (span-property before-list 'before))) + (ans + (set-span-property ans 'before (span-property span 'before))) + (t (error "Bug: span does not occur in span list"))))) + +;; extent-at gives "smallest" extent at pos +;; we're assuming right now that spans don't overlap +(defun spans-at-point (pt) + (let ((overlays nil) (os nil)) + (setq os (overlays-at pt)) + (while os + (if (not (memq (car os) overlays)) + (setq overlays (cons (car os) overlays))) + (setq os (cdr os))) + overlays)) + +;; assumes that there are no repetitions in l or m +(defun append-unique (l m) + (foldl (lambda (n a) (if (memq a m) n (cons a n))) m l)) + +(defun spans-at-region (start end) + (let ((overlays nil) (pos start)) + (while (< pos end) + (setq overlays (append-unique (spans-at-point pos) overlays)) + (setq pos (next-overlay-change pos))) + overlays)) + +(defun spans-at-point-prop (pt prop) + (let ((f (cond + (prop (lambda (spans span) + (if (span-property span prop) (cons span spans) + spans))) + (t (lambda (spans span) (cons span spans)))))) + (foldl f nil (spans-at-point pt)))) + +(defun spans-at-region-prop (start end prop) + (let ((f (cond + (prop (lambda (spans span) + (if (span-property span prop) (cons span spans) + spans))) + (t (lambda (spans span) (cons span spans)))))) + (foldl f nil (spans-at-region start end)))) + +(defun span-at (pt prop) + (car (spans-at-point-prop pt prop))) + +(defsubst detach-span (span) + (remove-span span) + (delete-overlay span) + (add-span span)) + +(defsubst delete-span (span) + (remove-span span) + (delete-overlay span)) + +;; The next two change ordering of list of spans: +(defsubst set-span-endpoints (span start end) + (remove-span span) + (move-overlay span start end) + (add-span span)) + +(defsubst set-span-start (span value) + (set-span-endpoints span value (span-end span))) + +;; This doesn't affect invariant: +(defsubst set-span-end (span value) + (set-span-endpoints span (span-start span) value)) + +(defsubst delete-spans (start end prop) + (mapcar 'delete-span (spans-at-region-prop start end prop))) + +(defun map-spans-aux (f l) + (cond (l (cons (funcall f l) (map-spans-aux f (span-property l 'before)))) + (t ()))) + +(defsubst map-spans (f) + (map-spans-aux f before-list)) + +(defun find-span-aux (prop-p l) + (while (and l (not (funcall prop-p l))) + (setq l (span-property l 'before))) + l) + +(defun find-span (prop-p) + (find-span-aux prop-p before-list)) + +(defun span-at-before (pt prop) + (let ((prop-pt-p + (cond (prop (lambda (span) + (let ((start (span-start span))) + (and start (> pt start) + (span-property span prop))))) + (t (lambda (span) + (let ((start (span-start span))) + (and start (> pt start)))))))) + (find-span prop-pt-p))) + +(defun prev-span (span prop) + (let ((prev-prop-p + (cond (prop (lambda (span) (span-property span prop))) + (t (lambda (span) t))))) + (find-span-aux prev-prop-p (span-property span 'before)))) + +;; overlays are [start, end) +;; If there are two spans overlapping then this won't work. +(defun next-span (span prop) + (let ((l (member-if (lambda (span) (span-property span prop)) + (overlays-at + (next-overlay-change (overlay-start span)))))) + (if l (car l) nil))) + + +(provide 'span-overlay) diff --git a/isa-print-functions.ML b/isa-print-functions.ML deleted file mode 100644 index 3af539a5..00000000 --- a/isa-print-functions.ML +++ /dev/null @@ -1,172 +0,0 @@ -(* - isa-print-functions.ML - - Customized version of Isabelle printing for script management - mode. - - $Id$ - -*) - - - -val proof_state_special_prefix="\248"; -val proof_state_special_suffix="\249"; -val goal_start_special="\253"; - - - -(* val orig_prs_fn = !prs_fn; *) -(* val orig_warning_fn = !warning_fn; *) -(* val orig_error_fn = !error_fn; *) - -(* copied from Pure/library.ML: *) -local - fun out s = - (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); - - fun prefix_lines prfx txt = - txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode; -in - -(*hooks for output channels: normal, warning, error*) - -(* da: NO CHANGES NEEDED YET *) -val () = - (prs_fn := (fn s => out s); - warning_fn := (fn s => out (prefix_lines "### " s)); - error_fn := (fn s => out (prefix_lines "*** " s))) - -end; - - - -local - - (* utils *) - - fun ins_entry (x, y) [] = [(x, [y])] - | ins_entry (x, y) ((pair as (x', ys')) :: pairs) = - if x = x' then (x', y ins ys') :: pairs - else pair :: ins_entry (x, y) pairs; - - fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env - | add_consts (t $ u, env) = add_consts (u, add_consts (t, env)) - | add_consts (Abs (_, _, t), env) = add_consts (t, env) - | add_consts (_, env) = env; - - fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env - | add_vars (Var (xi, T), env) = ins_entry (T, xi) env - | add_vars (Abs (_, _, t), env) = add_vars (t, env) - | add_vars (t $ u, env) = add_vars (u, add_vars (t, env)) - | add_vars (_, env) = env; - - fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env) - | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env - | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env; - - fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs; - fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; - - - (* prepare atoms *) - - fun consts_of t = sort_cnsts (add_consts (t, [])); - fun vars_of t = sort_idxs (add_vars (t, [])); - fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, []))); - -in - - fun script_print_goals maxgoals state = - let - val {sign, ...} = rep_thm state; - - val prt_term = Sign.pretty_term sign; - val prt_typ = Sign.pretty_typ sign; - val prt_sort = Sign.pretty_sort sign; - - fun prt_atoms prt prtT (X, xs) = Pretty.block - [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", - Pretty.brk 1, prtT X]; - - fun prt_var (x, ~1) = prt_term (Syntax.free x) - | prt_var xi = prt_term (Syntax.var xi); - - fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) - | prt_varT xi = prt_typ (TVar (xi, [])); - - val prt_consts = prt_atoms (prt_term o Const) prt_typ; - val prt_vars = prt_atoms prt_var prt_typ; - val prt_varsT = prt_atoms prt_varT prt_sort; - - - fun print_list _ _ [] = () - | print_list name prt lst = (writeln ""; - Pretty.writeln (Pretty.big_list name (map prt lst))); - - fun print_subgoals (_, []) = () - | print_subgoals (n, A :: As) = (Pretty.writeln (Pretty.blk (0, - [Pretty.str (goal_start_special ^ - " " ^ string_of_int n ^ ". "), prt_term A])); - print_subgoals (n + 1, As)); - - val print_ffpairs = - print_list "Flex-flex pairs:" (prt_term o Logic.mk_flexpair); - - val print_consts = print_list "Constants:" prt_consts o consts_of; - val print_vars = print_list "Variables:" prt_vars o vars_of; - val print_varsT = print_list "Type variables:" prt_varsT o varsT_of; - - - val {prop, ...} = rep_thm state; - val (tpairs, As, B) = Logic.strip_horn prop; - val ngoals = length As; - - fun print_gs (types, sorts) = - (Pretty.writeln (prt_term B); - if ngoals = 0 then writeln "No subgoals!" - else if ngoals > maxgoals then - (print_subgoals (1, take (maxgoals, As)); - writeln ("A total of " ^ string_of_int ngoals ^ " subgoals...")) - else print_subgoals (1, As); - - print_ffpairs tpairs; - - if types andalso ! show_consts then print_consts prop else (); - if types then print_vars prop else (); - if sorts then print_varsT prop else ()); - in - setmp show_no_free_types true - (setmp show_types (! show_types orelse ! show_sorts) - (setmp show_sorts false print_gs)) - (! show_types orelse ! show_sorts, ! show_sorts) - end; - -end; - - - - -(* Pure/goals.ML declares print_current_goals_fn. *) - -val orig_print_current_goals_fn = !print_current_goals_fn; - -fun script_mode_print_current_goals_fn n max th = - (writeln ("Level " ^ string_of_int n); script_print_goals max th); - -local - fun out s = - (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); - fun cgf i j t = - (out proof_state_special_prefix; - script_mode_print_current_goals_fn i j t; - out proof_state_special_suffix) -in - val () = (print_current_goals_fn := cgf) -end - - - - - - \ No newline at end of file diff --git a/isa-syntax.el b/isa-syntax.el deleted file mode 100644 index f7667127..00000000 --- a/isa-syntax.el +++ /dev/null @@ -1,138 +0,0 @@ -;; isa-syntax.el Syntax expressions for Isabelle -;; - -(require 'proof-syntax) - - -;;; Proof mode customization: how should it work? -;;; Presently we have a bunch of variables in proof.el which are -;;; set from a bunch of similarly named variables in -syntax.el. -;;; -;;; Seems a bit daft: why not just have the customization in -;;; one place, and settings hardwired in -syntax.el. -;;; -;;; That way we can see which settings are part of instantiation of -;;; proof.el, and which are part of cusomization for . - -;; ------ customize groups - -;(defgroup isa-scripting nil -; "Customization of Isabelle script management" -; :group 'external -; :group 'languages) - -;(defgroup isa-syntax nil -; "Customization of Isabelle's syntax recognition" -; :group 'isa-scripting) - -;; ----- syntax for font-lock and other features - -;; FIXME: this command-keyword orientation isn't good -;; enough for Isabelle, since we can have arbitrary -;; ML code around. One solution is to define a -;; restricted language consisting of the interactive -;; commands. We'd still need regexps below, though. -;; Alternatively: customize this for Marcus Wenzel's -;; proof language. - -(defvar isa-keywords-decl - '("val") - "Isabelle keywords for declarations") -; :group 'isa-syntax -; :type '(repeat string)) - -(defvar isa-keywords-defn - '("bind_thm") - "Isabelle keywords for definitions") -; :group 'isa-syntax -; :type '(repeat string)) - -;; isa-keywords-goal is used to manage undo actions -(defvar isa-keywords-goal - '("goal" "goalw" "goalw_cterm") - "Isabelle commands to begin an interactive proof") -; :group 'isa-syntax -; :type '(repeat string)) - -(defvar isa-keywords-save - '("qed" "result" "uresult" "bind_thm" "store_thm") - "Isabelle commands to extract the proved theorem") -; :group 'isa-syntax -; :type '(repeat string)) - -;; FIXME: and a whole lot more... should be conservative -;; and use any identifier -(defvar isa-keywords-commands - '("by" "goal")) - -;; See isa-command-table in Isamode/isa-menus.el to get this list. -;; BUT: tactics are not commands, so appear inside some expression. -(defvar isa-tactics - '("resolve_tac" "assume_tac")) - -(defvar isa-keywords - (append isa-keywords-goal isa-keywords-save isa-keywords-decl - isa-keywords-defn isa-keywords-commands isa-tactics) - "All keywords in a Isabelle script") - -(defvar isa-tacticals '("REPEAT" "THEN" "ORELSE" "TRY")) - -;; ----- regular expressions - -;; this should come from isa-ml-compiler stuff. -(defvar isa-error-regexp - "^.*Error:" - "A regular expression indicating that the Isa process has identified - an error.") - -(defvar isa-id proof-id) - -(defvar isa-ids (proof-ids isa-id)) - -(defun isa-abstr-regexp (paren char) - (concat paren "\\s-*\\(" isa-ids "\\)\\s-*" char)) - -(defvar isa-font-lock-terms - (list - - ;; lambda binders - (list (isa-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face) - - ;; Pi binders - (list (isa-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face) - - ;; Kinds - (cons (concat "\\\\|\\\\|\\]>? *\\|^\\*\\* .*" ; for ML - proof-shell-cd "cd \"%s\";" - ;; this one not set: proof-shell-abort-goal-regexp - proof-shell-proof-completed-regexp "No subgoals!" - proof-shell-error-regexp isa-error-regexp - proof-shell-interrupt-regexp "Interrupt" ; FIXME: only good for NJ/SML - proof-shell-noise-regexp "" - proof-shell-assumption-regexp isa-id ; matches name of assumptions - proof-shell-goal-regexp "^[ \t]*[0-9]+\\. " ; matches subgoal heading - ;; We can't hack the SML prompt, so set wakeup-char to nil. - proof-shell-wakeup-char nil - proof-shell-start-goals-regexp "\370" - proof-shell-end-goals-regexp "\371" - ;; initial command configures Isabelle by hacking print functions. - ;; may need to set directory somewhere for this: - ;; /home/da/devel/lego/elisp/ or $PROOFGENERIC_HOME ? - proof-shell-init-cmd "use \"isa-print-functions.ML\";" - ;; === ANNOTATIONS === remaining ones broken - proof-shell-goal-char ?\375 - proof-shell-first-special-char ?\360 - proof-shell-eager-annotation-start "\376" - proof-shell-eager-annotation-end "\377" - proof-shell-annotated-prompt-regexp proof-shell-prompt-pattern ; impossible to annotate! - proof-shell-result-start "\372 Pbp result \373" - proof-shell-result-end "\372 End Pbp result \373" - proof-analyse-using-stack t - proof-shell-start-char ?\372 - proof-shell-end-char ?\373 - proof-shell-field-char ?\374) - "Table of settings for configuration of proof shell mode to Isabelle.") - - -;; ===== outline mode - -;;; FIXME: test and add more things here -(defvar isa-outline-regexp - (ids-to-regexp '("goal" "Goal" "prove_goal")) - "Outline regexp for Isabelle ML files") - -;;; End of a command needs parsing to find, so this is approximate. -(defvar isa-outline-heading-end-regexp ";[ \t\n]*") - -;; -(defvar isa-shell-outline-regexp isa-goal-regexp) -(defvar isa-shell-outline-heading-end-regexp isa-goal-regexp) - -;;; ---- end-outline - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; FIXME: I don't think they should be here at all. - -(define-derived-mode isa-shell-mode proof-shell-mode - "isa-shell" "Inferior shell mode for isabelle shell" - (isa-shell-mode-config)) - -(define-derived-mode isa-mode proof-mode - "isa" "Isabelle Mode" - (isa-mode-config)) - -(define-derived-mode isa-pbp-mode pbp-mode - "pbp" "Proof-by-pointing support for Isabelle" - (isa-pbp-mode-config)) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Code that's Isabelle specific ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -;; FIXME: think about the next variable. I've changed sense from -;; LEGO and Coq's treatment. -(defconst isa-not-undoable-commands-regexp - (ids-to-regexp '("undo" "back")) - "Regular expression matching commands which are *not* undoable.") - -;; This next function is the important one for undo operations. -(defun isa-count-undos (span) - "Count number of undos in a span, return the command needed to undo that far." - (let ((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))) - (concat "choplev 0" proof-terminal-string) - (while span - (setq str (span-property span 'cmd)) - (cond ((eq (span-property span 'type) 'vanilla) - (or (string-match isa-not-undoable-commands-regexp str) - (setq ct (+ 1 ct)))) - ((eq (span-property span 'type) 'pbp) - ;; this case probably redundant for Isabelle, unless - ;; we think of some nice ways of matching non-undoable - ;; commands. - (cond ((not (string-match isa-not-undoable-commands-regexp str)) - (setq i 0) - (while (< i (length str)) - (if (= (aref str i) proof-terminal-char) - (setq ct (+ 1 ct))) - (setq i (+ 1 i)))) - (t nil)))) - (setq span (next-span span 'type))) - (concat "choplev " (int-to-string ct) proof-terminal-string)))) - -(defun isa-goal-command-p (str) - "Decide whether argument is a goal or not" - (string-match isa-goal-command-regexp str)) ; this regexp defined in isa-syntax.el - -;; Isabelle has no concept of a Linear context, so forgetting back -;; to the declaration of a particular something makes no real -;; sense. Perhaps in the future there will be functions to remove -;; theorems from theories, but even then all we could do is -;; forget particular theorems one by one. - -;; FIXME: next function and variable DEAD, irrelevant. -(defconst isa-keywords-decl-defn-regexp - (ids-to-regexp (append isa-keywords-decl isa-keywords-defn)) - "Declaration and definition regexp.") - -(defun isa-find-and-forget (span) - (let (str ans) - (while (and span (not ans)) - (setq str (span-property span 'cmd)) - (cond - - ((eq (span-property span 'type) 'comment)) - - ((eq (span-property span 'type) 'goalsave) - (setq ans (concat isa-forget-id-command - (span-property span 'name) proof-terminal-string))) - - ((string-match (concat "\\`\\(" isa-keywords-decl-defn-regexp - "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str) - (setq ans (concat isa-forget-id-command - (match-string 2 str) proof-terminal-string))) - - ;; If it's not a goal but it contains "Definition" then it's a - ;; declaration - ((and (not (isa-goal-command-p str)) - (string-match - (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str)) - (setq ans (concat isa-forget-id-command - (match-string 2 str) proof-terminal-string)))) - - (setq span (next-span span 'type))) - - (or ans "COMMENT"))) - -(defvar isa-current-goal 1 - "Last goal that emacs looked at.") - -;; Parse proofstate output. Isabelle does not display -;; named hypotheses in the proofstate output: they -;; appear as a list in each subgoal. Ignore -;; that aspect for now and just return the -;; subgoal number. -(defun isa-goal-hyp () - (if (looking-at proof-shell-goal-regexp) - (cons 'goal (match-string 1)))) - -(defun isa-state-preserving-p (cmd) - "Non-nil if command preserves the proofstate." - (string-match isa-not-undoable-commands-regexp cmd)) - -;; FIXME: I don't really know what this means, but lego sets -;; it to always return nil. Probably should be able to -;; leave it unset. -(defun isa-global-p (cmd) - nil) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Indentation ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; -;; Sadly this is pretty pointless for Isabelle. -;; Proof scripts in Isabelle don't really have an easily-observed -;; block structure -- a case split can be done by any obscure tactic, -;; and then solved in a number of steps that bears no relation to the -;; number of cases! And the end is certainly not marked in anyway. -;; -(defun isa-stack-to-indent (stack) - (cond - ((null stack) 0) - ((null (car (car stack))) - (nth 1 (car stack))) - (t (save-excursion - (goto-char (nth 1 (car stack))) - (+ isa-indent (current-column)))))) - -(defun isa-parse-indent (c stack) - "Indentation function for Isabelle. Does nothing." - stack) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Isa shell startup and exit hooks ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun isa-pre-shell-start () - (setq proof-prog-name isa-prog-name) - (setq proof-mode-for-shell 'isa-shell-mode) - (setq proof-mode-for-pbp 'isa-pbp-mode)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Configuring proof and pbp mode and setting up various utilities ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun isa-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 ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?\| ".") - (modify-syntax-entry ?\* ". 23") - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - -(defun isa-mode-config () - (apply 'setq isa-mode-config-table) - (isa-init-syntax-table) - ;; font-lock - (setq font-lock-keywords isa-font-lock-keywords-1) - (proof-config-done) - (define-key (current-local-map) [(control c) ?I] 'isa-Intros) - (define-key (current-local-map) [(control c) ?a] 'isa-Apply) - (define-key (current-local-map) [(control c) (control s)] 'isa-Search) - ;; outline - ;; FIXME: do we need to call make-local-variable here? - (make-local-variable 'outline-regexp) - (setq outline-regexp isa-outline-regexp) - (make-local-variable 'outline-heading-end-regexp) - (setq outline-heading-end-regexp isa-outline-heading-end-regexp) - ;; tags - ; (and (boundp 'tag-table-alist) - ; (setq tag-table-alist - ; (append '(("\\.ML$" . isa-ML-file-tags-table) - ; ("\\.thy$" . isa-thy-file-tags-table)) - ; tag-table-alist))) - (setq blink-matching-paren-dont-ignore-comments t) - ;; hooks and callbacks - (add-hook 'proof-pre-shell-start-hook 'isa-pre-shell-start nil t)) - - -(defun isa-shell-mode-config () - ;; The following hook is removed once it's called. - ;; FIXME: maybe add this back later. - ;;(add-hook 'proof-shell-insert-hook 'isa-shell-init-hook nil t) - (isa-init-syntax-table) - (apply 'setq isa-shell-mode-config-table) - (proof-shell-config-done)) - -;; FIXME: broken, of course, as is all PBP everywhere. -(defun isa-pbp-mode-config () - (setq pbp-change-goal "Show %s.") - (setq pbp-error-regexp isa-error-regexp)) - -(provide 'isa) diff --git a/lego-syntax.el b/lego-syntax.el deleted file mode 100644 index 60ede04f..00000000 --- a/lego-syntax.el +++ /dev/null @@ -1,100 +0,0 @@ -;; lego-fontlock.el Font lock expressions for LEGO -;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. -;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira -;; Maintainer: LEGO Team - -(require 'proof-syntax) - -;; ----- keywords for font-lock. - -(defconst lego-keywords-goal '("$?Goal")) - -(defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen")) - -(defconst lego-commands - (append lego-keywords-goal lego-keywords-save - '("allE" "allI" "andE" "andI" "Assumption" "Claim" - "Cut" "Discharge" "DischargeKeep" - "echo" "exE" "exI" "Expand" "ExpAll" - "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" - "impE" "impI" "Induction" "Inductive" - "Invert" "Init" "intros" "Intros" "Module" "Next" - "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify" - "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze")) - "Subset of LEGO keywords and tacticals which are terminated by a \?;") - -(defconst lego-keywords - (append lego-commands - '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion" - "NoReductions" "Parameters" "Relation" "Theorems"))) - -(defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) - -;; ----- regular expressions for font-lock -(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)" - "A regular expression indicating that the LEGO process has - identified an error.") - -(defvar lego-id proof-id) - -(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*") - "*For font-lock, we treat \",\" separated identifiers as one identifier - and refontify commata using \\{lego-fixup-change}.") - -(defconst lego-arg-list-regexp "\\s *\\(\\[[^]]+\\]\\s *\\)*" - "Regular expression maching a list of arguments.") - -(defun lego-decl-defn-regexp (char) - (concat "\\[\\s *\\(" lego-ids "\\)" lego-arg-list-regexp char)) -; Examples -; ^ ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ -; [ sort = -; [ sort [n:nat] = -; [ sort [abbrev=...][n:nat] = - -(defconst lego-definiendum-alternative-regexp - (concat "\\(" lego-id "\\)" lego-arg-list-regexp "\\s * ==") - "Regular expression where the first match identifies the definiendum.") - -(defvar lego-font-lock-terms - (list - - ; lambda binders - (list (lego-decl-defn-regexp "[:|]") 1 - 'font-lock-declaration-name-face) - - ; let binders - (list lego-definiendum-alternative-regexp 1 'font-lock-function-name-face) - (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face) - - ; Pi and Sigma binders - (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1 - 'font-lock-declaration-name-face) - - ;; Kinds - (cons (concat "\\\\|\\ - -(require 'lego-syntax) -(require 'outline) -(require 'proof) - -;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; User Configuration ;;; -;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; I believe this is standard for Linux under RedHat -tms -(defvar lego-tags "/usr/lib/lego/lib_Type/" - "*the default TAGS table for the LEGO library") - -(defvar lego-indent 2 "*Indentation") - -(defvar lego-test-all-name "test_all" - "*The name of the LEGO module which inherits all other modules of the - library.") - -(defvar lego-help-menu-list - '(["The LEGO Reference Card" (w3-fetch lego-www-refcard) t] - ["The LEGO library (WWW)" (w3-fetch lego-library-www-page) t]) - "List of menu items, as defined in `easy-menu-define' for LEGO - specific help.") - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; Configuration of Generic Proof Package ;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Users should not need to change this. - -(defvar lego-shell-process-output - '((lambda (cmd string) (string-match "^Module" cmd)) . - (lambda (cmd string) - (setq proof-shell-delayed-output - (cons 'insert "Imports done!")))) - "Acknowledge end of processing import declarations.") - -(defvar lego-assistant "LEGO" - "Name of proof assistant") - -(defconst lego-process-config "Configure PrettyOn; Configure AnnotateOn;" - "Command to enable pretty printing of the LEGO process.") - -(defconst lego-pretty-set-width "Configure PrettyWidth %s; " - "Command to adjust the linewidth for pretty printing of the LEGO - process.") - -(defconst lego-interrupt-regexp "Interrupt.." - "Regexp corresponding to an interrupt") - -(defvar lego-path-name "LEGOPATH" - "The name of the environmental variable to search for modules. This - is used by \\{legogrep} to find the files corresponding to a - search.") - -(defvar lego-path-separator ":" - "A character indicating how the items in the \\{lego-path-name} are - separated.") - - -;; ----- web documentation - -(defvar lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/") - -(defvar lego-www-latest-release - (concat (w3-remove-file-name lego-www-home-page) - "html/release-1.3/") - "The WWW address for the latest LEGO release.") - -(defvar lego-www-refcard (concat lego-www-latest-release - "refcard.ps.gz")) - -(defvar lego-library-www-page - (concat lego-www-latest-release "library/library.html") - "The HTML documentation of the LEGO library.") - -;; ----- legostat and legogrep, courtesy of Mark Ruys - -(defvar legogrep-command (concat "legogrep -n \"\" " lego-test-all-name) - "Last legogrep command used in \\{legogrep}; default for next legogrep.") - -(defvar legostat-command "legostat -t") - -(defvar legogrep-regexp-alist - '(("^\\([^:( \t\n]+\\)[:( \t]+\\([0-9]+\\)[:) \t]" 1 2 nil ("%s.l"))) - "Regexp used to match legogrep hits. See `compilation-error-regexp-alist'.") - -;; ----- lego-shell configuration options - -(defvar lego-prog-name "lego" - "*Name of program to run as lego.") - -(defvar lego-shell-prompt-pattern "^\\(Lego>[ \201]*\\)+" - "*The prompt pattern for the inferior shell running lego.") - -(defvar lego-shell-cd "Cd \"%s\";" - "*Command of the inferior process to change the directory.") - -(defvar lego-shell-abort-goal-regexp "KillRef: ok, not in proof state" - "*Regular expression indicating that the proof of the current goal - has been abandoned.") - -(defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" - "*Regular expression indicating that the proof has been completed.") - -(defvar lego-save-command-regexp - (concat "^" (ids-to-regexp lego-keywords-save))) -(defvar lego-goal-command-regexp - (concat "^" (ids-to-regexp lego-keywords-goal))) - -(defvar lego-kill-goal-command "KillRef;") -(defvar lego-forget-id-command "Forget ") - -(defvar lego-undoable-commands-regexp - (ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal" - "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption" - "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI" - "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed" - "Invert")) "Undoable list") - -;; ----- outline - -(defvar lego-goal-regexp "\\?\\([0-9]+\\)") - -(defvar lego-outline-regexp - (concat "[[*]\\|" - (ids-to-regexp - '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive" - "Unfreeze")))) - -(defvar lego-outline-heading-end-regexp ";\\|\\*)") - -(defvar lego-shell-outline-regexp lego-goal-regexp) -(defvar lego-shell-outline-heading-end-regexp lego-goal-regexp) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(define-derived-mode lego-shell-mode proof-shell-mode - "lego-shell" "Inferior shell mode for lego shell" - (lego-shell-mode-config)) - -(define-derived-mode lego-mode proof-mode - "lego" "Lego Mode" - (lego-mode-config) - (easy-menu-change (list proof-mode-name) (car proof-help-menu) - (append (cdr proof-help-menu) lego-help-menu-list))) - -(define-derived-mode lego-pbp-mode pbp-mode - "pbp" "Proof-by-pointing support for LEGO" - (lego-pbp-mode-config)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Code that's lego specific ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Martin Steffen has pointed -;; out that calling lego-get-path has to deal with a user who hasn't -;; set the environmental variable LEGOPATH. It is probably best if -;; lego is installed as a shell script which sets a sensible default -;; for LEGOPATH if the user hasn't done so before. See the -;; documentation of the library for further details. - -(defun lego-get-path () - (let ((path-name (getenv lego-path-name))) - (cond ((not path-name) - (message "Warning: LEGOPATH has not been set!") - (setq path-name "."))) - (proof-string-to-list path-name lego-path-separator))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; This is how to work out what the undo commands are, given the ;; -;; first span which needs to be undone ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; needs to handle Normal as well -;; it should ignore Normal TReg Normal VReg and (Normal ...) -(defun lego-count-undos (span) - (let ((ct 0) str i) - (while span - (setq str (span-property span 'cmd)) - (cond ((eq (span-property span 'type) 'vanilla) - (if (or (string-match lego-undoable-commands-regexp str) - (and (string-match "Equiv" str) - (not (string-match "Equiv\\s +[TV]Reg" str)))) - (setq ct (+ 1 ct)))) - ((eq (span-property span 'type) 'pbp) - (setq i 0) - (while (< i (length str)) - (if (= (aref str i) proof-terminal-char) (setq ct (+ 1 ct))) - (setq i (+ 1 i))))) - (setq span (next-span span 'type))) - (concat "Undo " (int-to-string ct) proof-terminal-string))) - -(defun lego-goal-command-p (str) - "Decide whether argument is a goal or not" - (string-match lego-goal-command-regexp str)) - -(defun lego-find-and-forget (span) - (let (str ans) - (while (and span (not ans)) - (setq str (span-property span 'cmd)) - - (cond - - ((eq (span-property span 'type) 'comment)) - - ((eq (span-property span 'type) 'goalsave) - (setq ans (concat lego-forget-id-command - (span-property span 'name) proof-terminal-string))) - - ;; alternative definitions - ((string-match lego-definiendum-alternative-regexp str) - (setq ans (concat lego-forget-id-command (match-string 1 str) - proof-terminal-string))) - ;; declarations - ((string-match (concat "\\`\\$?" (lego-decl-defn-regexp "[:|=]")) str) - (let ((ids (match-string 1 str))) ; returns "a,b" - (string-match proof-id ids) ; matches "a" - (setq ans (concat lego-forget-id-command(match-string 1 ids) - proof-terminal-string)))) - - ((string-match "\\`\\(Inductive\\|\\Record\\)\\s-*\\[\\s-*\\w+\\s-*:[^;]+\\`Parameters\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str) - (setq ans (concat lego-forget-id-command - (match-string 2 str) proof-terminal-string))) - - ((string-match - "\\`\\(Inductive\\|Record\\)\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str) - (setq ans - (concat lego-forget-id-command (match-string 2 str) - proof-terminal-string))) - - ((string-match "\\`\\s-*Module\\s-+\\(\\S-+\\)\\W" str) - (setq ans (concat "ForgetMark " (match-string 1 str) - proof-terminal-string)))) - - (setq span (next-span span 'type))) - (or ans - "COMMENT"))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Other stuff which is required to customise script management ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun lego-goal-hyp () - (cond - ((looking-at proof-shell-goal-regexp) - (cons 'goal (match-string 1))) - ((looking-at proof-shell-assumption-regexp) - (cons 'hyp (match-string 1))) - (t nil))) - - -(defun lego-state-preserving-p (cmd) - (not (string-match lego-undoable-commands-regexp cmd))) - -(defun lego-global-p (cmd) - nil) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Commands specific to lego ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun lego-intros () - "intros." - (interactive) - (insert "intros ")) - -(defun lego-Intros () - "List proof state." - (interactive) - (insert "Intros ")) - -(defun lego-Refine () - "List proof state." - (interactive) - (insert "Refine ")) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Lego Indentation ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun lego-stack-to-indent (stack) - (cond - ((null stack) 0) - ((null (car (car stack))) - (nth 1 (car stack))) - (t (save-excursion - (goto-char (nth 1 (car stack))) - (+ lego-indent (current-column)))))) - -(defun lego-parse-indent (c stack) - (cond - ((eq c ?\{) (cons (list c (point)) stack)) - ((eq c ?\}) (cdr stack)) - (t stack))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Lego shell startup and exit hooks ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defvar lego-shell-current-line-width nil - "Current line width of the LEGO process's pretty printing module. - Its value will be updated whenever the corresponding screen gets - selected.") - -;; The line width needs to be adjusted if the LEGO process is -;; running and is out of sync with the screen width - -(defun lego-shell-adjust-line-width () - "Uses LEGO's pretty printing facilities to adjust the line width of - the output." - (save-excursion - (set-buffer proof-shell-buffer) - (and (proof-shell-live-buffer) - (let ((current-width - (window-width (get-buffer-window proof-shell-buffer)))) - (if (equal current-width lego-shell-current-line-width) () - ; else - (setq lego-shell-current-line-width current-width) - (insert (format lego-pretty-set-width (- current-width 1))) - ))))) - -(defun lego-pre-shell-start () - (setq proof-prog-name lego-prog-name) - (setq proof-mode-for-shell 'lego-shell-mode) - (setq proof-mode-for-pbp 'lego-pbp-mode)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Configuring proof and pbp mode and setting up various utilities ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun lego-init-syntax-table () - "Set appropriate values for syntax table in current buffer." - - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?\| ".") - (modify-syntax-entry ?\* ". 23") - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - -(defun lego-mode-config () - - (setq proof-terminal-char ?\;) - (setq proof-comment-start "(*") - (setq proof-comment-end "*)") - - (setq proof-assistant lego-assistant - proof-www-home-page lego-www-home-page) - - (setq proof-prf-string "Prf" - proof-ctxt-string "Ctxt" - proof-help-string "Help") - - (setq proof-goal-command-p 'lego-goal-command-p - proof-count-undos-fn 'lego-count-undos - proof-find-and-forget-fn 'lego-find-and-forget - proof-goal-hyp-fn 'lego-goal-hyp - proof-state-preserving-p 'lego-state-preserving-p - proof-global-p 'lego-global-p - proof-parse-indent 'lego-parse-indent - proof-stack-to-indent 'lego-stack-to-indent) - - (setq proof-save-command-regexp lego-save-command-regexp - proof-save-with-hole-regexp lego-save-with-hole-regexp - proof-goal-with-hole-regexp lego-goal-with-hole-regexp - proof-kill-goal-command lego-kill-goal-command - proof-commands-regexp (ids-to-regexp lego-commands)) - - (lego-init-syntax-table) - - (proof-config-done) - - (define-key (current-local-map) [(control c) ?i] 'lego-intros) - (define-key (current-local-map) [(control c) ?I] 'lego-Intros) - (define-key (current-local-map) [(control c) ?r] 'lego-Refine) - -;; outline - - (make-local-variable 'outline-regexp) - (setq outline-regexp lego-outline-regexp) - - (make-local-variable 'outline-heading-end-regexp) - (setq outline-heading-end-regexp lego-outline-heading-end-regexp) - -;; tags - (cond ((boundp 'tags-table-list) - (make-local-variable 'tags-table-list) - (setq tags-table-list (cons lego-tags tags-table-list)))) - - (and (boundp 'tag-table-alist) - (setq tag-table-alist - (append '(("\\.l$" . lego-tags) - ("lego" . lego-tags)) - tag-table-alist))) - - (setq font-lock-keywords lego-font-lock-keywords-1) - -;; where to find files - - (setq compilation-search-path (cons nil (lego-get-path))) - - (setq blink-matching-paren-dont-ignore-comments t) - -;; font-lock - -;; if we don't have the following in xemacs, zap-commas fails to work. - - (and (boundp 'font-lock-always-fontify-immediately) - (setq font-lock-always-fontify-immediately t)) - -;; hooks and callbacks - - (add-hook 'proof-pre-shell-start-hook 'lego-pre-shell-start nil t) - (add-hook 'proof-shell-insert-hook 'lego-shell-adjust-line-width)) - -;; insert standard header and footer in fresh buffers - -(defun lego-shell-mode-config () - (setq proof-shell-prompt-pattern lego-shell-prompt-pattern - proof-shell-cd lego-shell-cd - proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp - proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp - proof-shell-error-regexp lego-error-regexp - proof-shell-interrupt-regexp lego-interrupt-regexp - proof-shell-noise-regexp "Discharge\\.\\. " - proof-shell-assumption-regexp lego-id - proof-shell-goal-regexp lego-goal-regexp - proof-shell-first-special-char ?\360 - proof-shell-wakeup-char ?\371 - proof-shell-start-char ?\372 - proof-shell-end-char ?\373 - proof-shell-field-char ?\374 - proof-shell-goal-char ?\375 - proof-shell-eager-annotation-start "\376" - proof-shell-eager-annotation-end "\377" - proof-shell-annotated-prompt-regexp "Lego> \371" - proof-shell-result-start "\372 Pbp result \373" - proof-shell-result-end "\372 End Pbp result \373" - proof-shell-start-goals-regexp "\372 Start of Goals \373" - proof-shell-end-goals-regexp "\372 End of Goals \373" - proof-shell-init-cmd lego-process-config - proof-analyse-using-stack nil - proof-shell-process-output-system-specific lego-shell-process-output - lego-shell-current-line-width nil) - - (lego-init-syntax-table) - - (proof-shell-config-done)) - -(defun lego-pbp-mode-config () - (setq pbp-change-goal "Next %s;") - (setq pbp-error-regexp lego-error-regexp)) - -(provide 'lego) diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el new file mode 100644 index 00000000..60ede04f --- /dev/null +++ b/lego/lego-syntax.el @@ -0,0 +1,100 @@ +;; lego-fontlock.el Font lock expressions for LEGO +;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. +;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira +;; Maintainer: LEGO Team + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defconst lego-keywords-goal '("$?Goal")) + +(defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen")) + +(defconst lego-commands + (append lego-keywords-goal lego-keywords-save + '("allE" "allI" "andE" "andI" "Assumption" "Claim" + "Cut" "Discharge" "DischargeKeep" + "echo" "exE" "exI" "Expand" "ExpAll" + "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" + "impE" "impI" "Induction" "Inductive" + "Invert" "Init" "intros" "Intros" "Module" "Next" + "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify" + "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze")) + "Subset of LEGO keywords and tacticals which are terminated by a \?;") + +(defconst lego-keywords + (append lego-commands + '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion" + "NoReductions" "Parameters" "Relation" "Theorems"))) + +(defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) + +;; ----- regular expressions for font-lock +(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)" + "A regular expression indicating that the LEGO process has + identified an error.") + +(defvar lego-id proof-id) + +(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*") + "*For font-lock, we treat \",\" separated identifiers as one identifier + and refontify commata using \\{lego-fixup-change}.") + +(defconst lego-arg-list-regexp "\\s *\\(\\[[^]]+\\]\\s *\\)*" + "Regular expression maching a list of arguments.") + +(defun lego-decl-defn-regexp (char) + (concat "\\[\\s *\\(" lego-ids "\\)" lego-arg-list-regexp char)) +; Examples +; ^ ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ +; [ sort = +; [ sort [n:nat] = +; [ sort [abbrev=...][n:nat] = + +(defconst lego-definiendum-alternative-regexp + (concat "\\(" lego-id "\\)" lego-arg-list-regexp "\\s * ==") + "Regular expression where the first match identifies the definiendum.") + +(defvar lego-font-lock-terms + (list + + ; lambda binders + (list (lego-decl-defn-regexp "[:|]") 1 + 'font-lock-declaration-name-face) + + ; let binders + (list lego-definiendum-alternative-regexp 1 'font-lock-function-name-face) + (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face) + + ; Pi and Sigma binders + (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1 + 'font-lock-declaration-name-face) + + ;; Kinds + (cons (concat "\\\\|\\ + +(require 'lego-syntax) +(require 'outline) +(require 'proof) + +;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; User Configuration ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; I believe this is standard for Linux under RedHat -tms +(defvar lego-tags "/usr/lib/lego/lib_Type/" + "*the default TAGS table for the LEGO library") + +(defvar lego-indent 2 "*Indentation") + +(defvar lego-test-all-name "test_all" + "*The name of the LEGO module which inherits all other modules of the + library.") + +(defvar lego-help-menu-list + '(["The LEGO Reference Card" (w3-fetch lego-www-refcard) t] + ["The LEGO library (WWW)" (w3-fetch lego-library-www-page) t]) + "List of menu items, as defined in `easy-menu-define' for LEGO + specific help.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Configuration of Generic Proof Package ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Users should not need to change this. + +(defvar lego-shell-process-output + '((lambda (cmd string) (string-match "^Module" cmd)) . + (lambda (cmd string) + (setq proof-shell-delayed-output + (cons 'insert "Imports done!")))) + "Acknowledge end of processing import declarations.") + +(defvar lego-assistant "LEGO" + "Name of proof assistant") + +(defconst lego-process-config "Configure PrettyOn; Configure AnnotateOn;" + "Command to enable pretty printing of the LEGO process.") + +(defconst lego-pretty-set-width "Configure PrettyWidth %s; " + "Command to adjust the linewidth for pretty printing of the LEGO + process.") + +(defconst lego-interrupt-regexp "Interrupt.." + "Regexp corresponding to an interrupt") + +(defvar lego-path-name "LEGOPATH" + "The name of the environmental variable to search for modules. This + is used by \\{legogrep} to find the files corresponding to a + search.") + +(defvar lego-path-separator ":" + "A character indicating how the items in the \\{lego-path-name} are + separated.") + + +;; ----- web documentation + +(defvar lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/") + +(defvar lego-www-latest-release + (concat (w3-remove-file-name lego-www-home-page) + "html/release-1.3/") + "The WWW address for the latest LEGO release.") + +(defvar lego-www-refcard (concat lego-www-latest-release + "refcard.ps.gz")) + +(defvar lego-library-www-page + (concat lego-www-latest-release "library/library.html") + "The HTML documentation of the LEGO library.") + +;; ----- legostat and legogrep, courtesy of Mark Ruys + +(defvar legogrep-command (concat "legogrep -n \"\" " lego-test-all-name) + "Last legogrep command used in \\{legogrep}; default for next legogrep.") + +(defvar legostat-command "legostat -t") + +(defvar legogrep-regexp-alist + '(("^\\([^:( \t\n]+\\)[:( \t]+\\([0-9]+\\)[:) \t]" 1 2 nil ("%s.l"))) + "Regexp used to match legogrep hits. See `compilation-error-regexp-alist'.") + +;; ----- lego-shell configuration options + +(defvar lego-prog-name "lego" + "*Name of program to run as lego.") + +(defvar lego-shell-prompt-pattern "^\\(Lego>[ \201]*\\)+" + "*The prompt pattern for the inferior shell running lego.") + +(defvar lego-shell-cd "Cd \"%s\";" + "*Command of the inferior process to change the directory.") + +(defvar lego-shell-abort-goal-regexp "KillRef: ok, not in proof state" + "*Regular expression indicating that the proof of the current goal + has been abandoned.") + +(defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" + "*Regular expression indicating that the proof has been completed.") + +(defvar lego-save-command-regexp + (concat "^" (ids-to-regexp lego-keywords-save))) +(defvar lego-goal-command-regexp + (concat "^" (ids-to-regexp lego-keywords-goal))) + +(defvar lego-kill-goal-command "KillRef;") +(defvar lego-forget-id-command "Forget ") + +(defvar lego-undoable-commands-regexp + (ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal" + "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption" + "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI" + "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed" + "Invert")) "Undoable list") + +;; ----- outline + +(defvar lego-goal-regexp "\\?\\([0-9]+\\)") + +(defvar lego-outline-regexp + (concat "[[*]\\|" + (ids-to-regexp + '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive" + "Unfreeze")))) + +(defvar lego-outline-heading-end-regexp ";\\|\\*)") + +(defvar lego-shell-outline-regexp lego-goal-regexp) +(defvar lego-shell-outline-heading-end-regexp lego-goal-regexp) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-derived-mode lego-shell-mode proof-shell-mode + "lego-shell" "Inferior shell mode for lego shell" + (lego-shell-mode-config)) + +(define-derived-mode lego-mode proof-mode + "lego" "Lego Mode" + (lego-mode-config) + (easy-menu-change (list proof-mode-name) (car proof-help-menu) + (append (cdr proof-help-menu) lego-help-menu-list))) + +(define-derived-mode lego-pbp-mode pbp-mode + "pbp" "Proof-by-pointing support for LEGO" + (lego-pbp-mode-config)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Code that's lego specific ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Martin Steffen has pointed +;; out that calling lego-get-path has to deal with a user who hasn't +;; set the environmental variable LEGOPATH. It is probably best if +;; lego is installed as a shell script which sets a sensible default +;; for LEGOPATH if the user hasn't done so before. See the +;; documentation of the library for further details. + +(defun lego-get-path () + (let ((path-name (getenv lego-path-name))) + (cond ((not path-name) + (message "Warning: LEGOPATH has not been set!") + (setq path-name "."))) + (proof-string-to-list path-name lego-path-separator))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; This is how to work out what the undo commands are, given the ;; +;; first span which needs to be undone ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; needs to handle Normal as well +;; it should ignore Normal TReg Normal VReg and (Normal ...) +(defun lego-count-undos (span) + (let ((ct 0) str i) + (while span + (setq str (span-property span 'cmd)) + (cond ((eq (span-property span 'type) 'vanilla) + (if (or (string-match lego-undoable-commands-regexp str) + (and (string-match "Equiv" str) + (not (string-match "Equiv\\s +[TV]Reg" str)))) + (setq ct (+ 1 ct)))) + ((eq (span-property span 'type) 'pbp) + (setq i 0) + (while (< i (length str)) + (if (= (aref str i) proof-terminal-char) (setq ct (+ 1 ct))) + (setq i (+ 1 i))))) + (setq span (next-span span 'type))) + (concat "Undo " (int-to-string ct) proof-terminal-string))) + +(defun lego-goal-command-p (str) + "Decide whether argument is a goal or not" + (string-match lego-goal-command-regexp str)) + +(defun lego-find-and-forget (span) + (let (str ans) + (while (and span (not ans)) + (setq str (span-property span 'cmd)) + + (cond + + ((eq (span-property span 'type) 'comment)) + + ((eq (span-property span 'type) 'goalsave) + (setq ans (concat lego-forget-id-command + (span-property span 'name) proof-terminal-string))) + + ;; alternative definitions + ((string-match lego-definiendum-alternative-regexp str) + (setq ans (concat lego-forget-id-command (match-string 1 str) + proof-terminal-string))) + ;; declarations + ((string-match (concat "\\`\\$?" (lego-decl-defn-regexp "[:|=]")) str) + (let ((ids (match-string 1 str))) ; returns "a,b" + (string-match proof-id ids) ; matches "a" + (setq ans (concat lego-forget-id-command(match-string 1 ids) + proof-terminal-string)))) + + ((string-match "\\`\\(Inductive\\|\\Record\\)\\s-*\\[\\s-*\\w+\\s-*:[^;]+\\`Parameters\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str) + (setq ans (concat lego-forget-id-command + (match-string 2 str) proof-terminal-string))) + + ((string-match + "\\`\\(Inductive\\|Record\\)\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str) + (setq ans + (concat lego-forget-id-command (match-string 2 str) + proof-terminal-string))) + + ((string-match "\\`\\s-*Module\\s-+\\(\\S-+\\)\\W" str) + (setq ans (concat "ForgetMark " (match-string 1 str) + proof-terminal-string)))) + + (setq span (next-span span 'type))) + (or ans + "COMMENT"))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Other stuff which is required to customise script management ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-goal-hyp () + (cond + ((looking-at proof-shell-goal-regexp) + (cons 'goal (match-string 1))) + ((looking-at proof-shell-assumption-regexp) + (cons 'hyp (match-string 1))) + (t nil))) + + +(defun lego-state-preserving-p (cmd) + (not (string-match lego-undoable-commands-regexp cmd))) + +(defun lego-global-p (cmd) + nil) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to lego ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-intros () + "intros." + (interactive) + (insert "intros ")) + +(defun lego-Intros () + "List proof state." + (interactive) + (insert "Intros ")) + +(defun lego-Refine () + "List proof state." + (interactive) + (insert "Refine ")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lego Indentation ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-stack-to-indent (stack) + (cond + ((null stack) 0) + ((null (car (car stack))) + (nth 1 (car stack))) + (t (save-excursion + (goto-char (nth 1 (car stack))) + (+ lego-indent (current-column)))))) + +(defun lego-parse-indent (c stack) + (cond + ((eq c ?\{) (cons (list c (point)) stack)) + ((eq c ?\}) (cdr stack)) + (t stack))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lego shell startup and exit hooks ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar lego-shell-current-line-width nil + "Current line width of the LEGO process's pretty printing module. + Its value will be updated whenever the corresponding screen gets + selected.") + +;; The line width needs to be adjusted if the LEGO process is +;; running and is out of sync with the screen width + +(defun lego-shell-adjust-line-width () + "Uses LEGO's pretty printing facilities to adjust the line width of + the output." + (save-excursion + (set-buffer proof-shell-buffer) + (and (proof-shell-live-buffer) + (let ((current-width + (window-width (get-buffer-window proof-shell-buffer)))) + (if (equal current-width lego-shell-current-line-width) () + ; else + (setq lego-shell-current-line-width current-width) + (insert (format lego-pretty-set-width (- current-width 1))) + ))))) + +(defun lego-pre-shell-start () + (setq proof-prog-name lego-prog-name) + (setq proof-mode-for-shell 'lego-shell-mode) + (setq proof-mode-for-pbp 'lego-pbp-mode)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Configuring proof and pbp mode and setting up various utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-init-syntax-table () + "Set appropriate values for syntax table in current buffer." + + (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?\' "_") + (modify-syntax-entry ?\| ".") + (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4")) + +(defun lego-mode-config () + + (setq proof-terminal-char ?\;) + (setq proof-comment-start "(*") + (setq proof-comment-end "*)") + + (setq proof-assistant lego-assistant + proof-www-home-page lego-www-home-page) + + (setq proof-prf-string "Prf" + proof-ctxt-string "Ctxt" + proof-help-string "Help") + + (setq proof-goal-command-p 'lego-goal-command-p + proof-count-undos-fn 'lego-count-undos + proof-find-and-forget-fn 'lego-find-and-forget + proof-goal-hyp-fn 'lego-goal-hyp + proof-state-preserving-p 'lego-state-preserving-p + proof-global-p 'lego-global-p + proof-parse-indent 'lego-parse-indent + proof-stack-to-indent 'lego-stack-to-indent) + + (setq proof-save-command-regexp lego-save-command-regexp + proof-save-with-hole-regexp lego-save-with-hole-regexp + proof-goal-with-hole-regexp lego-goal-with-hole-regexp + proof-kill-goal-command lego-kill-goal-command + proof-commands-regexp (ids-to-regexp lego-commands)) + + (lego-init-syntax-table) + + (proof-config-done) + + (define-key (current-local-map) [(control c) ?i] 'lego-intros) + (define-key (current-local-map) [(control c) ?I] 'lego-Intros) + (define-key (current-local-map) [(control c) ?r] 'lego-Refine) + +;; outline + + (make-local-variable 'outline-regexp) + (setq outline-regexp lego-outline-regexp) + + (make-local-variable 'outline-heading-end-regexp) + (setq outline-heading-end-regexp lego-outline-heading-end-regexp) + +;; tags + (cond ((boundp 'tags-table-list) + (make-local-variable 'tags-table-list) + (setq tags-table-list (cons lego-tags tags-table-list)))) + + (and (boundp 'tag-table-alist) + (setq tag-table-alist + (append '(("\\.l$" . lego-tags) + ("lego" . lego-tags)) + tag-table-alist))) + + (setq font-lock-keywords lego-font-lock-keywords-1) + +;; where to find files + + (setq compilation-search-path (cons nil (lego-get-path))) + + (setq blink-matching-paren-dont-ignore-comments t) + +;; font-lock + +;; if we don't have the following in xemacs, zap-commas fails to work. + + (and (boundp 'font-lock-always-fontify-immediately) + (setq font-lock-always-fontify-immediately t)) + +;; hooks and callbacks + + (add-hook 'proof-pre-shell-start-hook 'lego-pre-shell-start nil t) + (add-hook 'proof-shell-insert-hook 'lego-shell-adjust-line-width)) + +;; insert standard header and footer in fresh buffers + +(defun lego-shell-mode-config () + (setq proof-shell-prompt-pattern lego-shell-prompt-pattern + proof-shell-cd lego-shell-cd + proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp + proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp + proof-shell-error-regexp lego-error-regexp + proof-shell-interrupt-regexp lego-interrupt-regexp + proof-shell-noise-regexp "Discharge\\.\\. " + proof-shell-assumption-regexp lego-id + proof-shell-goal-regexp lego-goal-regexp + proof-shell-first-special-char ?\360 + proof-shell-wakeup-char ?\371 + proof-shell-start-char ?\372 + proof-shell-end-char ?\373 + proof-shell-field-char ?\374 + proof-shell-goal-char ?\375 + proof-shell-eager-annotation-start "\376" + proof-shell-eager-annotation-end "\377" + proof-shell-annotated-prompt-regexp "Lego> \371" + proof-shell-result-start "\372 Pbp result \373" + proof-shell-result-end "\372 End Pbp result \373" + proof-shell-start-goals-regexp "\372 Start of Goals \373" + proof-shell-end-goals-regexp "\372 End of Goals \373" + proof-shell-init-cmd lego-process-config + proof-analyse-using-stack nil + proof-shell-process-output-system-specific lego-shell-process-output + lego-shell-current-line-width nil) + + (lego-init-syntax-table) + + (proof-shell-config-done)) + +(defun lego-pbp-mode-config () + (setq pbp-change-goal "Next %s;") + (setq pbp-error-regexp lego-error-regexp)) + +(provide 'lego) diff --git a/lego/legotags b/lego/legotags new file mode 100644 index 00000000..a3c13eab --- /dev/null +++ b/lego/legotags @@ -0,0 +1,87 @@ +#!/usr/local/bin/perl + +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]*\$?Goal\s*([\w\']+))\s*:/) + { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } + + elsif($stmt=~/^([ \t]*\$?\[\s*[\w\']+)/) + { do adddecs($stmt,$1) } + + elsif($stmt=~/^([ \t]*Inductive\s*\[\s*[\w\']+)/) + { do adddecs($stmt,$1) } + +# ---- we don't need to tag saves: all goals should be named! + +# elsif($stmt=~/([ \t]*\$?Save\s+([\w\']+))/) +# { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } +# +# elsif($stmt=~/^([ \t]*\$?SaveUnfrozen\s+([\w\']+))/) +# { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } + +# ---- Maybe do something smart with discharge as well? + + $cp=$newcp; $lp=$newlp; $a=$newa; + } + print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; +} +close tagfile; + + +sub adddecs { + $wk=$_[0]; + $tag=$_[1]; + while($wk=~/\[\s*([\w\']+)/) + { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; + while($wk=~/^\s*,\s*([\w\']+)/) + { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; } + $d=1; + while($d>0 && $wk=~/\[|\]/) + { $wk=$'; if($& eq "[") {$d++} else {$d--}; + } + } + 0; +} + diff --git a/legotags b/legotags deleted file mode 100644 index a3c13eab..00000000 --- a/legotags +++ /dev/null @@ -1,87 +0,0 @@ -#!/usr/local/bin/perl - -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]*\$?Goal\s*([\w\']+))\s*:/) - { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } - - elsif($stmt=~/^([ \t]*\$?\[\s*[\w\']+)/) - { do adddecs($stmt,$1) } - - elsif($stmt=~/^([ \t]*Inductive\s*\[\s*[\w\']+)/) - { do adddecs($stmt,$1) } - -# ---- we don't need to tag saves: all goals should be named! - -# elsif($stmt=~/([ \t]*\$?Save\s+([\w\']+))/) -# { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } -# -# elsif($stmt=~/^([ \t]*\$?SaveUnfrozen\s+([\w\']+))/) -# { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } - -# ---- Maybe do something smart with discharge as well? - - $cp=$newcp; $lp=$newlp; $a=$newa; - } - print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; -} -close tagfile; - - -sub adddecs { - $wk=$_[0]; - $tag=$_[1]; - while($wk=~/\[\s*([\w\']+)/) - { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; - while($wk=~/^\s*,\s*([\w\']+)/) - { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; } - $d=1; - while($d>0 && $wk=~/\[|\]/) - { $wk=$'; if($& eq "[") {$d++} else {$d--}; - } - } - 0; -} - diff --git a/pbp.el b/pbp.el deleted file mode 100644 index 23ffdd68..00000000 --- a/pbp.el +++ /dev/null @@ -1,2 +0,0 @@ - -(provide 'pbp) diff --git a/proof-indent.el b/proof-indent.el deleted file mode 100644 index bb42f462..00000000 --- a/proof-indent.el +++ /dev/null @@ -1,124 +0,0 @@ -;; proof-indent.el Generic Indentation for Proof Assistants -;; Copyright (C) 1997, 1998 LFCS Edinburgh -;; Authors: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira -;; Maintainer: LEGO Team - -(require 'cl) -(require 'proof-syntax) - -(defvar proof-stack-to-indent nil - "Prover-specific code for indentation.") - -(defvar proof-parse-indent nil - "Proof-assistant specific function for parsing characters for - indentation which is invoked in `proof-parse-to-point.'. Must be a - function taking two arguments, a character (the current character) - and a stack reflecting indentation, and must return a stack. The - stack is a list of the form (c . p) where `c' is a character - representing the type of indentation and `p' records the column for - indentation. The generic `proof-parse-to-point.' function supports - parentheses and commands. It represents these with the characters - `?\(', `?\[' and `proof-terminal-char'. ") - -;; This is quite different from sml-mode, but borrows some bits of -;; code. It's quite a lot less general, but works with nested -;; comments. - -;; parse-to-point: If from is nil, parsing starts from either -;; proof-locked-end if we're in the proof-script-buffer or the -;; beginning of the buffer. Otherwise state must contain a valid -;; triple. - -(defun proof-parse-to-point (&optional from state) - (let ((comment-level 0) (stack (list (list nil 0))) - (end (point)) instring c) - (save-excursion - (if (null from) - (if (eq proof-script-buffer (current-buffer)) - (proof-goto-end-of-locked) - (goto-char 1)) - (goto-char from) - (setq instring (car state) - comment-level (nth 1 state) - stack (nth 2 state))) - (while (< (point) end) - (setq c (char-after (point))) - (cond - (instring - (if (eq c ?\") (setq instring nil))) - (t (cond - ((eq c ?\() - (cond - ((looking-at "(\\*") - (progn - (incf comment-level) - (forward-char))) - ((eq comment-level 0) - (setq stack (cons (list ?\( (point)) stack))))) - ((and (eq c ?\*) (looking-at "\\*)")) - (decf comment-level) - (forward-char)) - ((> comment-level 0)) - ((eq c ?\") (setq instring t)) - ((eq c ?\[) - (setq stack (cons (list ?\[ (point)) stack))) - ((or (eq c ?\)) (eq c ?\])) - (setq stack (cdr stack))) - ((looking-at proof-commands-regexp) - (setq stack (cons (list proof-terminal-char (point)) stack))) - ((and (eq c proof-terminal-char) - (eq (car (car stack)) proof-terminal-char)) (cdr stack)) - (proof-parse-indent - (setq stack (funcall proof-parse-indent c stack)))))) - (forward-char)) - (list instring comment-level stack)))) - -(defun proof-indent-line () - (interactive) - (if (and (eq proof-script-buffer (current-buffer)) - (< (point) (proof-locked-end))) - (if (< (current-column) (current-indentation)) - (skip-chars-forward "\t ")) - (save-excursion - (beginning-of-line) - (let* ((state (proof-parse-to-point)) - (beg (point)) - (indent (cond ((car state) 1) - ((> (nth 1 state) 0) 1) - (t (funcall proof-stack-to-indent (nth 2 state)))))) - (skip-chars-forward "\t ") - (if (not (eq (current-indentation) indent)) - (progn (delete-region beg (point)) - (indent-to indent))))) - (skip-chars-forward "\t "))) - -(defun proof-indent-region (start end) - (interactive "r") - (if (and (eq proof-script-buffer (current-buffer)) - (< (point) (proof-locked-end))) - (error "can't indent locked region!")) - (save-excursion - (goto-char start) - (beginning-of-line) - (let* ((beg (point)) - (state (proof-parse-to-point)) - indent) - ;; End of region changes with new indentation - (while (< (point) end) - (setq indent - (cond ((car state) 1) - ((> (nth 1 state) 0) 1) - (t (funcall proof-stack-to-indent (nth 2 state))))) - (skip-chars-forward "\t ") - (let ((diff (- (current-indentation) indent))) - (if (not (eq diff 0)) - (progn - (delete-region beg (point)) - (indent-to indent) - (setq end (- end diff))))) - (end-of-line) - (if (< (point) (point-max)) (forward-char)) - (setq state (proof-parse-to-point beg state) - beg (point)))))) - -(provide 'proof-indent) \ No newline at end of file diff --git a/proof-syntax.el b/proof-syntax.el deleted file mode 100644 index 5caa8fe3..00000000 --- a/proof-syntax.el +++ /dev/null @@ -1,104 +0,0 @@ -;; proof-syntax.el Generic font lock expressions -;; Copyright (C) 1997-1998 LFCS Edinburgh. -;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera -;; Maintainer: LEGO Team - -(require 'font-lock) - -;;; FIXME: change this to proof- -(defun ids-to-regexp (l) - "transforms a non-empty list of identifiers `l' into a regular - expression matching any of its elements" - (mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|")) - -;; Generic font-lock - -;; proof-commands-regexp is used for indentation -(defvar proof-commands-regexp "" - "Subset of keywords and tacticals which are terminated by the - `proof-terminal-char'") - - -(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" - "A regular expression for parsing identifiers.") - -;; For font-lock, we treat ,-separated identifiers as one identifier -;; and refontify commata using \{proof-unfontify-separator}. - -(defun proof-ids (proof-id) - "Function to generate a regular expression for separated lists of - identifiers." - (concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*")) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; font lock faces: declarations, errors, tacticals ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun proof-have-color () - ()) - -(defvar font-lock-declaration-name-face -(progn - (cond - ((proof-have-color) - (copy-face 'bold 'font-lock-declaration-name-face) - - ;; Emacs 19.28 compiles this down to - ;; internal-set-face-1. This is not compatible with XEmacs - (set-face-foreground - 'font-lock-declaration-name-face "chocolate")) - (t (copy-face 'bold-italic 'font-lock-declaration-name-face))))) - -;; (if running-emacs19 -;; (setq font-lock-declaration-name-face -;; (face-name 'font-lock-declaration-name-face)) - -(defvar font-lock-tacticals-name-face -(if (proof-have-color) - (let ((face (make-face 'font-lock-tacticals-name-face))) - (dont-compile - (set-face-foreground face "MediumOrchid3")) - face) - (copy-face 'bold 'font-lock-tacticals-name-face))) - -(defvar font-lock-error-face -(if (proof-have-color) - (let ((face (make-face 'font-lock-error-face))) - (dont-compile - (set-face-foreground face "red")) - face) - (copy-face 'bold 'font-lock-error-face))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; A big hack to unfontify commas in declarations and definitions. ;; -;; All that can be said for it is that the previous way of doing ;; -;; this was even more bogus. ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Refontify the whole line, 'cos that's what font-lock-after-change -;; does. - -(defun proof-zap-commas-region (start end length) - (save-excursion - (let - ((start (progn (goto-char start) (beginning-of-line) (point))) - (end (progn (goto-char end) (end-of-line) (point)))) - (goto-char start) - (while (search-forward "," end t) - (if (memq (get-char-property (- (point) 1) 'face) - '(font-lock-declaration-name-face - font-lock-function-name-face)) - (font-lock-remove-face (- (point) 1) (point)) - ))))) - -(defun proof-zap-commas-buffer () - (proof-zap-commas-region (point-min) (point-max) 0)) - -(defun proof-unfontify-separator () - (make-local-variable 'after-change-functions) - (setq after-change-functions - (append (delq 'proof-zap-commas-region after-change-functions) - '(proof-zap-commas-region)))) - - -(provide 'proof-syntax) diff --git a/proof.el b/proof.el deleted file mode 100644 index c37f863b..00000000 --- a/proof.el +++ /dev/null @@ -1,1838 +0,0 @@ -;; proof.el Major mode for proof assistants -;; Copyright (C) 1994 - 1998 LFCS Edinburgh. -;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, -;; Thomas Kleymann and Dilip Sequeira - -;; Maintainer: LEGO Team -;; Thanks to Robert Boyer, Rod Burstall, -;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens - - -(require 'cl) -(require 'compile) -(require 'comint) -(require 'etags) -(cond ((fboundp 'make-extent) (require 'span-extent)) - ((fboundp 'make-overlay) (require 'span-overlay)) - (t nil)) -(require 'proof-syntax) -(require 'proof-indent) -(require 'easymenu) -(require 'tl-list) - -(autoload 'w3-fetch "w3" nil t) - -(defmacro deflocal (var value docstring) - (list 'progn - (list 'defvar var 'nil docstring) - (list 'make-variable-buffer-local (list 'quote var)) - (list 'setq var value))) - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Generic config for proof assistant ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defvar proof-assistant "" - "Name of the proof assistant") - -(defvar proof-www-home-page "" - "Web address for information on proof assistant") - -(defvar proof-shell-cd nil - "*Command of the inferior process to change the directory.") - -(defvar proof-shell-process-output-system-specific nil - "*Errors, start of proofs, abortions of proofs and completions of - proofs are recognised in the function `proof-shell-process-output'. - All other output from the proof engine is simply reported to the - user in the RESPONSE buffer. - - To catch further special cases, set this variable to a tuple of - functions '(condf . actf). Both are given (cmd string) as arguments. - `cmd' is a string containing the currently processed command. - `string' is the response from the proof system. To change the - behaviour of `proof-shell-process-output', (condf cmd string) must - return a non-nil value. Then (actf cmd string) is invoked. See the - documentation of `proof-shell-process-output' for the required - output format.") - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Proof mode variables ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defconst proof-mode-version-string - "PROOF-MODE. ALPHA Version 2 (August 1998) LEGO Team ") - -(defconst proof-info-dir "/usr/local/share/info" - "Directory to search for Info documents on Script Management.") - -(defconst proof-universal-keys - (list (cons '[(control c) (control c)] 'proof-interrupt-process) - (cons '[(control c) (control v)] - 'proof-execute-minibuffer-cmd) - (cons '[(meta tab)] 'tag-complete-symbol)) - "List of keybindings which are valid in both in the script and the - response buffer. Elements of the list are tuples (k . f) - where `k' is a keybinding (vector) and `f' the designated function.") - -(defvar proof-prog-name-ask-p nil - "*If t, you will be asked which program to run when the inferior - process starts up.") - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Other buffer-local variables used by proof mode ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; These should be set before proof-config-done is called - -(defvar proof-terminal-char nil "terminator character") - -(defvar proof-comment-start nil "Comment start") -(defvar proof-comment-end nil "Comment end") - -(defvar proof-save-command-regexp nil "Matches a save command") -(defvar proof-save-with-hole-regexp nil "Matches a named save command") -(defvar proof-goal-with-hole-regexp nil "Matches a saved goal command") - -(defvar proof-goal-command-p nil "Is this a goal") -(defvar proof-count-undos-fn nil "Compute number of undos in a target segment") -(defvar proof-find-and-forget-fn nil "Compute command to forget up to point") - -(defvar proof-goal-hyp-fn nil - "A function which returns cons cell if point is at a goal/hypothesis. -First element of cell is a symbol, 'goal' or 'hyp'. The second -element is a string: the goal or hypothesis itself. This is used -when parsing the proofstate output") - -(defvar proof-kill-goal-command nil "How to kill a goal.") -(defvar proof-global-p nil - "Is this a global declaration") - -(defvar proof-state-preserving-p nil - "A predicate, non-nil if its argument preserves the proof state") - -(defvar pbp-change-goal nil - "*Command to change to the goal %s") - -;; these should be set in proof-pre-shell-start-hook - -(defvar proof-prog-name nil "program name for proof shell") -(defvar proof-mode-for-shell nil "mode for proof shell") -(defvar proof-mode-for-pbp nil "The actual mode for Proof-by-Pointing.") -(defvar proof-shell-insert-hook nil - "Function to config proof-system to interface") - -(defvar proof-pre-shell-start-hook) -(defvar proof-post-shell-exit-hook) - -(defvar proof-shell-prompt-pattern nil - "comint-prompt-pattern for proof shell") - -(defvar proof-shell-init-cmd nil - "The command for initially configuring the proof process") - -(defvar proof-shell-handle-delayed-output-hook - '(proof-pbp-focus-on-first-goal) - "*This hook is called after output from the PROOF process has been - displayed in the RESPONSE buffer.") - -(defvar proof-shell-handle-error-hook - '(proof-goto-end-of-locked-if-pos-not-visible-in-window) - "*This hook is called after an error has been reported in the - RESPONSE buffer.") - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Generic config for script management ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defvar proof-shell-wakeup-char nil - "A character terminating the prompt in annotation mode") - -(defvar proof-shell-annotated-prompt-regexp "" - "Annotated prompt pattern") - -(defvar proof-shell-abort-goal-regexp nil - "*Regular expression indicating that the proof of the current goal - has been abandoned.") - -(defvar proof-shell-error-regexp nil - "A regular expression indicating that the PROOF process has - identified an error.") - -(defvar proof-shell-interrupt-regexp nil - "A regular expression indicating that the PROOF process has - responded to an interrupt.") - -(defvar proof-shell-proof-completed-regexp nil - "*Regular expression indicating that the proof has been completed.") - -(defvar proof-shell-result-start "" - "String indicating the start of an output from the prover following - a `pbp-goal-command' or a `pbp-hyp-command'.") - -(defvar proof-shell-result-end "" - "String indicating the end of an output from the prover following a - `pbp-goal-command' or a `pbp-hyp-command'.") - -(defvar proof-shell-start-goals-regexp "" - "String indicating the start of the proof state.") - -(defvar proof-shell-end-goals-regexp "" - "String indicating the end of the proof state.") - -(defvar pbp-error-regexp nil - "A regular expression indicating that the PROOF process has - identified an error.") - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Internal variables used by scripting and pbp ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defvar proof-mode-name "Proof") - -(defvar proof-shell-echo-input t - "If nil, input to the proof shell will not be echoed") - -(defvar proof-terminal-string nil - "End-of-line string for proof process.") - -(defvar proof-re-end-of-cmd nil - "You are not authorised for this information.") - -(defvar proof-re-term-or-comment nil - "You are not authorised for this information.") - -(defvar proof-marker nil - "You are not authorised for this information.") - -(defvar proof-shell-buffer nil - "You are not authorised for this information.") - -(defvar proof-script-buffer nil - "You are not authorised for this information.") - -(defvar proof-pbp-buffer nil - "You are not authorised for this information.") - -(defvar proof-shell-busy nil - "You are not authorised for this information.") - -(deflocal proof-buffer-type nil - "You are not authorised for this information.") - -(defvar proof-action-list nil "action list") - -(defvar proof-included-files-list nil - "Files currently included in proof process") - -(deflocal proof-active-buffer-fake-minor-mode nil - "An indication in the modeline that this is the *active* buffer") - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; A couple of small utilities ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun proof-define-keys (map kbl) - "Adds keybindings `kbl' in `map'. The argument `kbl' is a list of - tuples (k . f) where `k' is a keybinding (vector) and `f' the - designated function." - (mapcar - (lambda (kbl) - (let ((k (car kbl)) (f (cdr kbl))) - (define-key map k f))) - kbl)) - -(defun proof-string-to-list (s separator) - "converts strings `s' separated by the character `separator' to a - list of words" - (let ((end-of-word-occurence (string-match (concat separator "+") s))) - (if (not end-of-word-occurence) - (if (string= s "") - nil - (list s)) - (cons (substring s 0 end-of-word-occurence) - (proof-string-to-list - (substring s - (string-match (concat "[^" separator "]") - s end-of-word-occurence)) separator))))) - -;; FIXME: this doesn't belong here (and shouldn't be called w3-* !!) -(defun w3-remove-file-name (address) - "remove the file name in a World Wide Web address" - (string-match "://[^/]+/" address) - (concat (substring address 0 (match-end 0)) - (file-name-directory (substring address (match-end 0))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Basic code for the locked region and the queue region ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defvar proof-locked-hwm nil - "Upper limit of the locked region") - -(defvar proof-queue-loose-end nil - "Limit of the queue region that is not equal to proof-locked-hwm.") - -(defvar proof-locked-span nil - "Upper limit of the locked region") - -(defvar proof-queue-span nil - "Upper limit of the locked region") - -(make-variable-buffer-local 'proof-locked-span) -(make-variable-buffer-local 'proof-queue-span) - -(defun proof-init-segmentation () - (setq proof-queue-loose-end nil) - (if (not proof-queue-span) - (setq proof-queue-span (make-span 1 1))) - (set-span-property proof-queue-span 'start-closed t) - (set-span-property proof-queue-span 'end-open t) - (span-read-only proof-queue-span) - - (make-face 'proof-queue-face) - ;; Whether display has color or not - (cond ((and (fboundp 'device-class) - (eq (device-class (frame-device)) 'color)) - (set-face-background 'proof-queue-face "mistyrose")) - ((and (fboundp 'x-display-color-p) (x-display-color-p)) - (set-face-background 'proof-queue-face "mistyrose")) - (t (progn - (set-face-background 'proof-queue-face "Black") - (set-face-foreground 'proof-queue-face "White")))) - (set-span-property proof-queue-span 'face 'proof-queue-face) - - (detach-span proof-queue-span) - - (setq proof-locked-hwm nil) - (if (not proof-locked-span) - (setq proof-locked-span (make-span 1 1))) - (set-span-property proof-locked-span 'start-closed t) - (set-span-property proof-locked-span 'end-open t) - (span-read-only proof-locked-span) - - (make-face 'proof-locked-face) - ;; Whether display has color or not - (cond ((and (fboundp 'device-class) - (eq (device-class (frame-device)) 'color)) - (set-face-background 'proof-locked-face "lavender")) - ((and (fboundp 'x-display-color-p) (x-display-color-p)) - (set-face-background 'proof-locked-face "lavender")) - (t (set-face-property 'proof-locked-face 'underline t))) - (set-span-property proof-locked-span 'face 'proof-locked-face) - - (detach-span proof-locked-span)) - -(defsubst proof-lock-unlocked () - (span-read-only proof-locked-span)) - -(defsubst proof-unlock-locked () - (span-read-write proof-locked-span)) - -(defsubst proof-set-queue-endpoints (start end) - (set-span-endpoints proof-queue-span start end)) - -(defsubst proof-set-locked-endpoints (start end) - (set-span-endpoints proof-locked-span start end)) - -(defsubst proof-detach-queue () - (and proof-queue-span (detach-span proof-queue-span))) - -(defsubst proof-detach-locked () - (and proof-locked-span (detach-span proof-locked-span))) - -(defsubst proof-set-queue-start (start) - (set-span-endpoints proof-queue-span start (span-end proof-queue-span))) - -(defsubst proof-set-queue-end (end) - (set-span-endpoints proof-queue-span (span-start proof-queue-span) end)) - -(defun proof-detach-segments () - (proof-detach-queue) - (proof-detach-locked)) - -(defsubst proof-set-locked-end (end) - (if (>= (point-min) end) - (proof-detach-locked) - (set-span-endpoints proof-locked-span (point-min) end))) - -(defun proof-unprocessed-begin () - "proof-unprocessed-begin returns end of locked region in script - buffer and point-min otherwise." - (or - (and (eq proof-script-buffer (current-buffer)) - proof-locked-span (span-end proof-locked-span)) - (point-min))) - -(defun proof-locked-end () - "proof-locked-end returns the end of the locked region. It should - only be called if we're in the scripting buffer." - (if (eq proof-script-buffer (current-buffer)) - (proof-unprocessed-begin) - (error "bug: proof-locked-end called from wrong buffer"))) - -(defsubst proof-end-of-queue () - (and proof-queue-span (span-end proof-queue-span))) - -(defun proof-dont-show-annotations () - "This sets the display values of the annotations used to - communicate with the proof assistant so that they don't show up on - the screen." - (let ((disp (make-display-table)) - (i 128)) - (while (< i 256) - (aset disp i []) - (incf i)) - (cond ((fboundp 'add-spec-to-specifier) - (add-spec-to-specifier current-display-table disp - (current-buffer))) - ((boundp 'buffer-display-table) - (setq buffer-display-table disp))))) - -;;; in case Emacs is not aware of read-shell-command-map - -(defvar read-shell-command-map - (let ((map (make-sparse-keymap))) - (if (not (fboundp 'set-keymap-parents)) - (setq map (append minibuffer-local-map map)) - (set-keymap-parents map minibuffer-local-map) - (set-keymap-name map 'read-shell-command-map)) - (define-key map "\t" 'comint-dynamic-complete) - (define-key map "\M-\t" 'comint-dynamic-complete) - (define-key map "\M-?" 'comint-dynamic-list-completions) - map) - "Minibuffer keymap used by shell-command and related commands.") - - -;;; in case Emacs is not aware of the function read-shell-command -(or (fboundp 'read-shell-command) - ;; from minibuf.el distributed with XEmacs 19.11 - (defun read-shell-command (prompt &optional initial-input history) - "Just like read-string, but uses read-shell-command-map: -\\{read-shell-command-map}" - (let ((minibuffer-completion-table nil)) - (read-from-minibuffer prompt initial-input read-shell-command-map - nil (or history - 'shell-command-history))))) - -;; The package fume-func provides a function with the same name and -;; specification. However, fume-func's version is incorrect. -(and (fboundp 'fume-match-find-next-function-name) -(defun fume-match-find-next-function-name (buffer) - "General next function name in BUFFER finder using match. - The regexp is assumed to be a two item list the car of which is the regexp - to use, and the cdr of which is the match position of the function name" - (set-buffer buffer) - (let ((r (car fume-function-name-regexp)) - (p (cdr fume-function-name-regexp))) - (and (re-search-forward r nil t) - (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))) - -(defun proof-goto-end-of-locked-interactive () - "Jump to the end of the locked region." - (interactive) - (switch-to-buffer proof-script-buffer) - (goto-char (proof-locked-end))) - -(defun proof-goto-end-of-locked () - "Jump to the end of the locked region." - (goto-char (proof-locked-end))) - -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window () - "If the end of the locked region is not visible, jump to the end of - the locked region." - (interactive) - (let ((pos (save-excursion - (set-buffer proof-script-buffer) - (proof-locked-end)))) - (or (pos-visible-in-window-p pos (get-buffer-window - proof-script-buffer t)) - (proof-goto-end-of-locked-interactive)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Starting and stopping the proof-system shell ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun proof-shell-live-buffer () - (and proof-shell-buffer - (comint-check-proc proof-shell-buffer) - proof-shell-buffer)) - -(defun proof-start-shell () - (if (proof-shell-live-buffer) - () - (run-hooks 'proof-pre-shell-start-hook) - (setq proof-included-files-list nil) - (if proof-prog-name-ask-p - (save-excursion - (setq proof-prog-name (read-shell-command "Run process: " - proof-prog-name)))) - (let ((proc - (concat "Inferior " - (substring proof-prog-name - (string-match "[^/]*$" proof-prog-name))))) - (while (get-buffer (concat "*" proc "*")) - (if (string= (substring proc -1) ">") - (aset proc (- (length proc) 2) - (+ 1 (aref proc (- (length proc) 2)))) - (setq proc (concat proc "<2>")))) - - (message (format "Starting %s process..." proc)) - - ;; Starting the inferior process (asynchronous) - (let ((prog-name-list (proof-string-to-list proof-prog-name " "))) - (apply 'make-comint (append (list proc (car prog-name-list) nil) - (cdr prog-name-list)))) - ;; To send any initialisation commands to the inferior process, - ;; consult proof-shell-config-done... - - (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) - (setq proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*"))) - - (save-excursion - (set-buffer proof-shell-buffer) - (funcall proof-mode-for-shell) - (set-buffer proof-pbp-buffer) - (funcall proof-mode-for-pbp)) - - (setq proof-script-buffer (current-buffer)) - (proof-init-segmentation) - (setq proof-active-buffer-fake-minor-mode t) - - (if (fboundp 'redraw-modeline) - (redraw-modeline) - (force-mode-line-update)) - - (or (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist) - (setq minor-mode-alist - (append minor-mode-alist - (list '(proof-active-buffer-fake-minor-mode - " Scripting"))))) - - (message - (format "Starting %s process... done." proc))))) - - -(defun proof-stop-shell () - "Exit the PROOF process - - Runs proof-shell-exit-hook if non nil" - - (interactive) - (save-excursion - (let ((buffer (proof-shell-live-buffer)) (proc)) - (if buffer - (progn - (save-excursion - (set-buffer buffer) - (setq proc (process-name (get-buffer-process))) - (comint-send-eof) - (save-excursion - (set-buffer proof-script-buffer) - (proof-detach-segments)) - (kill-buffer)) - (run-hooks 'proof-shell-exit-hook) - - ;;it is important that the hooks are - ;;run after the buffer has been killed. In the reverse - ;;order e.g., intall-shell-fonts causes problems and it - ;;is impossible to restart the PROOF shell - - (message (format "%s process terminated." proc))))))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Proof by pointing ;; -;; All very lego-specific at present ;; -;; To make sense of this code, you should read the ;; -;; relevant LFCS tech report by tms, yb, and djs ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defvar pbp-goal-command nil - "Command informing the prover that `pbp-button-action' has been - requested on a goal.") - -(defvar pbp-hyp-command nil - "Command informing the prover that `pbp-button-action' has been - requested on an assumption.") - -(defun pbp-button-action (event) - (interactive "e") - (mouse-set-point event) - (pbp-construct-command)) - -; Using the spans in a mouse behavior is quite simple: from the -; mouse position, find the relevant span, then get its annotation -; and produce a piece of text that will be inserted in the right -; buffer. - -(defun proof-expand-path (string) - (let ((a 0) (l (length string)) ls) - (while (< a l) - (setq ls (cons (int-to-string (aref string a)) - (cons " " ls))) - (incf a)) - (apply 'concat (nreverse ls)))) - -(defun proof-send-span (event) - (interactive "e") - (let* ((span (span-at (mouse-set-point event) 'type)) - (str (span-property span 'cmd))) - (cond ((and (eq proof-script-buffer (current-buffer)) (not (null span))) - (proof-goto-end-of-locked) - (cond ((eq (span-property span 'type) 'vanilla) - (insert str))))))) - -(defun pbp-construct-command () - (let* ((span (span-at (point) 'proof)) - (top-span (span-at (point) 'proof-top-element)) - top-info) - (if (null top-span) () - (setq top-info (span-property top-span 'proof-top-element)) - (pop-to-buffer proof-script-buffer) - (cond - (span - (proof-invisible-command - (format (if (eq 'hyp (car top-info)) pbp-hyp-command - pbp-goal-command) - (concat (cdr top-info) (proof-expand-path - (span-property span 'proof)))))) - ((eq (car top-info) 'hyp) - (proof-invisible-command (format pbp-hyp-command (cdr top-info)))) - (t - (proof-insert-pbp-command (format pbp-change-goal (cdr top-info)))))) - )) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Turning annotated output into pbp goal set ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defvar proof-shell-first-special-char nil "where the specials start") -(defvar proof-shell-goal-char nil "goal mark") -(defvar proof-shell-start-char nil "annotation start") -(defvar proof-shell-end-char nil "annotation end") -(defvar proof-shell-field-char nil "annotated field end") -(defvar proof-shell-eager-annotation-start nil "eager ann. field start") -(defvar proof-shell-eager-annotation-end nil "eager ann. field end") - -(defvar proof-shell-assumption-regexp nil - "A regular expression matching the name of assumptions.") - -;; FIXME: da: where is this variable used? -;; dropped in favour of goal-char? -(defvar proof-shell-goal-regexp nil - "A regular expressin matching the identifier of a goal.") - -(defvar proof-shell-noise-regexp nil - "Unwanted information output from the proof process within - `proof-start-goals-regexp' and `proof-end-goals-regexp'.") - -(defun pbp-make-top-span (start end) - (let (span name) - (goto-char start) - ;; FIXME: why name? This is a character function - (setq name (funcall proof-goal-hyp-fn)) - (beginning-of-line) - (setq start (point)) - (goto-char end) - (beginning-of-line) - (backward-char) - (setq span (make-span start (point))) - (set-span-property span 'mouse-face 'highlight) - (set-span-property span 'proof-top-element name))) - - -;; Need this for processing error strings and so forth - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; The filter. First some functions that handle those few ;; -;; occasions when the glorious illusion that is script-management ;; -;; is temporarily suspended ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Output from the proof process is handled lazily, so that only -;; the output from the last of multiple commands is actually -;; processed (assuming they're all successful) - -(defvar proof-shell-delayed-output nil - "The last interesting output the proof process output, and what to do - with it.") - -(defvar proof-analyse-using-stack nil - "Are annotations sent by proof assistant local or global") - -;; FIXME: da: what's magical value 128 below? should be in defconst? -(defun proof-shell-analyse-structure (string) - (save-excursion - (let* ((ip 0) (op 0) ap (l (length string)) - (ann (make-string (length string) ?x)) - (stack ()) (topl ()) - (out (make-string l ?x)) c span) - (while (< ip l) - (if (< (setq c (aref string ip)) 128) - (progn (aset out op c) - (incf op))) - (incf ip)) - (display-buffer (set-buffer proof-pbp-buffer)) - (erase-buffer) - (insert (substring out 0 op)) - - (setq ip 0 - op 1) - (while (< ip l) - (setq c (aref string ip)) - (cond - ((= c proof-shell-goal-char) - (setq topl (cons op topl)) - (setq ap 0)) - ((= c proof-shell-start-char) - (if proof-analyse-using-stack - (setq ap (- ap (- (aref string (incf ip)) 128))) - (setq ap (- (aref string (incf ip)) 128))) - (incf ip) - (while (not (= (setq c (aref string ip)) proof-shell-end-char)) - (aset ann ap (- c 128)) - (incf ap) - (incf ip)) - (setq stack (cons op (cons (substring ann 0 ap) stack)))) - ((= c proof-shell-field-char) - (setq span (make-span (car stack) op)) - (set-span-property span 'mouse-face 'highlight) - (set-span-property span 'proof (car (cdr stack))) - ;; Pop annotation off stack - (and proof-analyse-using-stack - (progn - (setq ap 0) - (while (< ap (length (cadr stack))) - (aset ann ap (aref (cadr stack) ap)) - (incf ap)))) - ;; Finish popping annotations - (setq stack (cdr (cdr stack)))) - (t (incf op))) - (incf ip)) - (setq topl (reverse (cons (point-max) topl))) - ;; If we want Coq pbp: (setq coq-current-goal 1) - (while (setq ip (car topl) - topl (cdr topl)) - (pbp-make-top-span ip (car topl)))))) - -(defun proof-shell-strip-annotations (string) - (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x ))) - (while (< ip l) - (if (>= (aref string ip) proof-shell-first-special-char) - (if (char-equal (aref string ip) proof-shell-start-char) - (progn (incf ip) - (while (< (aref string ip) proof-shell-first-special-char) - (incf ip)))) - (aset out op (aref string ip)) - (incf op)) - (incf ip)) - (substring out 0 op))) - -(defun proof-shell-handle-delayed-output () - (let ((ins (car proof-shell-delayed-output)) - (str (cdr proof-shell-delayed-output))) - (display-buffer proof-pbp-buffer) - (save-excursion - (cond - ((eq ins 'insert) - (setq str (proof-shell-strip-annotations str)) - (set-buffer proof-pbp-buffer) - (erase-buffer) - (insert str)) - ((eq ins 'analyse) - (proof-shell-analyse-structure str)) - (t (set-buffer proof-pbp-buffer) - (insert "\n\nbug???"))))) - (run-hooks 'proof-shell-handle-delayed-output-hook) - (setq proof-shell-delayed-output (cons 'insert "done"))) - -(defun proof-shell-handle-error (cmd string) - (save-excursion - (display-buffer (set-buffer proof-pbp-buffer)) - (if (not (eq proof-shell-delayed-output (cons 'insert "done"))) - (progn - (set-buffer proof-pbp-buffer) - (erase-buffer) - (insert (proof-shell-strip-annotations - (cdr proof-shell-delayed-output))))) - (goto-char (point-max)) - (if (re-search-backward pbp-error-regexp nil t) - (delete-region (- (point) 2) (point-max))) - (newline 2) - (insert-string string) - (beep)) - (set-buffer proof-script-buffer) - (proof-detach-queue) - (delete-spans (proof-locked-end) (point-max) 'type) - (proof-release-lock) - (run-hooks 'proof-shell-handle-error-hook)) - -(defun proof-shell-handle-interrupt () - (save-excursion - (display-buffer (set-buffer proof-pbp-buffer)) - (goto-char (point-max)) - (newline 2) - (insert-string - "Interrupt: Script Management may be in an inconsistent state\n") - (beep)) - (set-buffer proof-script-buffer) - (if proof-shell-busy - (progn (proof-detach-queue) - (delete-spans (proof-locked-end) (point-max) 'type) - (proof-release-lock)))) - - -(defun proof-goals-pos (span maparg) - "Given a span, this function returns the start of it if corresponds - to a goal and nil otherwise." - (and (eq 'goal (car (span-property span 'proof-top-element))) - (span-start span))) - -(defun proof-pbp-focus-on-first-goal () - "If the `proof-pbp-buffer' contains goals, the first one is brought - into view." - (and (fboundp 'map-extents) - (let - ((pos (map-extents 'proof-goals-pos proof-pbp-buffer - nil nil nil nil 'proof-top-element))) - (and pos (set-window-point - (get-buffer-window proof-pbp-buffer t) pos))))) - - - -(defun proof-shell-process-output (cmd string) - "Deals with errors, start of proofs, abortions of proofs and - completions of proofs. All other output from the proof engine is - simply reported to the user in the RESPONSE buffer. To extend this - function, set `proof-shell-process-output-system-specific'. - - The basic output processing function - it can return one of 4 - things: 'error, 'interrupt, 'loopback, or nil. 'loopback means this - was output from pbp, and should be inserted into the script buffer - and sent back to the proof assistant." - (cond - ((string-match proof-shell-error-regexp string) - (cons 'error (proof-shell-strip-annotations - (substring string (match-beginning 0))))) - - ((string-match proof-shell-interrupt-regexp string) - 'interrupt) - - ((and proof-shell-abort-goal-regexp - (string-match proof-shell-abort-goal-regexp string)) - (setq proof-shell-delayed-output (cons 'insert "\n\nAborted")) - ()) - - ((string-match proof-shell-proof-completed-regexp string) - (setq proof-shell-delayed-output - (cons 'insert (concat "\n" (match-string 0 string))))) - - ((string-match proof-shell-start-goals-regexp string) - (let (start end) - (while (progn (setq start (match-end 0)) - (string-match proof-shell-start-goals-regexp - string start))) - (setq end (string-match proof-shell-end-goals-regexp string start)) - (setq proof-shell-delayed-output - (cons 'analyse (substring string start end))))) - - ((string-match proof-shell-result-start string) - (let (start end) - (setq start (+ 1 (match-end 0))) - (string-match proof-shell-result-end string) - (setq end (- (match-beginning 0) 1)) - (cons 'loopback (substring string start end)))) - - ;; hook to tailor proof-shell-process-output to a specific proof - ;; system - ((and proof-shell-process-output-system-specific - (funcall (car proof-shell-process-output-system-specific) - cmd string)) - (funcall (cdr proof-shell-process-output-system-specific) - cmd string)) - - (t (setq proof-shell-delayed-output (cons 'insert string))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Low-level commands for shell communication ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun proof-shell-insert (string) - (set-buffer proof-shell-buffer) - (goto-char (point-max)) - - (run-hooks 'proof-shell-insert-hook) - (insert string) - - ;; xemacs and emacs19 have different semantics for what happens when - ;; shell input is sent next to a marker - ;; the following code accommodates both definitions - (if (marker-position proof-marker) - (let ((inserted (point))) - (comint-send-input) - (set-marker proof-marker inserted)) - (comint-send-input))) - -(defun proof-send (string) - (let ((l (length string)) (i 0)) - (while (< i l) - (if (= (aref string i) ?\n) (aset string i ?\ )) - (incf i))) - (save-excursion (proof-shell-insert string))) - -;; Note that this is not really intended for anything complicated - -;; just to stop the user accidentally sending a command while the -;; queue is running. -(defun proof-check-process-available (&optional relaxed) - "Checks - (1) Is a proof process running? - (2) Is the proof process idle? - (3) Does the current buffer own the proof process? - (4) Is the current buffer a proof script? - and signals an error if at least one of the conditions is not - fulfilled. If relaxed is set, only (1) and (2) are tested." - (if (proof-shell-live-buffer) - (cond - (proof-shell-busy (error "Proof Process Busy!")) - (relaxed ()) ;exit cond - ((not (eq proof-script-buffer (current-buffer))) - (error "Don't own proof process")))) - (if (not (or relaxed (eq proof-buffer-type 'script))) - (error "Must be running in a script buffer"))) - -(defun proof-grab-lock (&optional relaxed) - (proof-start-shell) - (proof-check-process-available relaxed) - (setq proof-shell-busy t)) - -(defun proof-release-lock () - (if (proof-shell-live-buffer) - (progn - (if (not proof-shell-busy) - (error "Bug: Proof process not busy")) - (if (not (eq proof-script-buffer (current-buffer))) - (error "Bug: Don't own process")) - (setq proof-shell-busy nil)))) - -; Pass start and end as nil if the cmd isn't in the buffer. - -(defun proof-start-queue (start end alist &optional relaxed) - (if start - (proof-set-queue-endpoints start end)) - (let (item) - (while (and alist (string= - (nth 1 (setq item (car alist))) - "COMMENT")) - (funcall (nth 2 item) (car item)) - (setq alist (cdr alist))) - (if alist - (progn - (proof-grab-lock relaxed) - (setq proof-shell-delayed-output (cons 'insert "Done.")) - (setq proof-action-list alist) - (proof-send (nth 1 item)))))) - -; returns t if it's run out of input - -(defun proof-shell-exec-loop () - (save-excursion - (set-buffer proof-script-buffer) - (if (null proof-action-list) (error "Non Sequitur")) - (let ((item (car proof-action-list))) - (funcall (nth 2 item) (car item)) - (setq proof-action-list (cdr proof-action-list)) - (while (and proof-action-list - (string= - (nth 1 (setq item (car proof-action-list))) - "COMMENT")) - (funcall (nth 2 item) (car item)) - (setq proof-action-list (cdr proof-action-list))) - (if (null proof-action-list) - (progn (proof-release-lock) - (proof-detach-queue) - t) - (proof-send (nth 1 item)) - nil)))) - -(defun proof-shell-insert-loopback-cmd (cmd) - "Insert command sequence triggered by the proof process -at the end of locked region (after inserting a newline and indenting)." - (save-excursion - (set-buffer proof-script-buffer) - (let (span) - (proof-goto-end-of-locked) - (newline-and-indent) - (insert cmd) - (setq span (make-span (proof-locked-end) (point))) - (set-span-property span 'type 'pbp) - (set-span-property span 'cmd cmd) - (proof-set-queue-endpoints (proof-locked-end) (point)) - (setq proof-action-list - (cons (car proof-action-list) - (cons (list span cmd 'proof-done-advancing) - (cdr proof-action-list))))))) - -;; ******** NB ********** -;; While we're using pty communication, this code is OK, since all -;; eager annotations are one line long, and we get input a line at a -;; time. If we go over to piped communication, it will break. - -(defun proof-shell-popup-eager-annotation () - "Eager annotations are annotations which the proof system produces -while it's doing something (e.g. loading libraries) to say how much -progress it's made. Obviously we need to display these as soon as they -arrive." - (let (mrk str file module) - (save-excursion - (goto-char (point-max)) - (search-backward proof-shell-eager-annotation-start) - (setq mrk (+ 1 (point))) - (search-forward proof-shell-eager-annotation-end) - (setq str (buffer-substring mrk (- (point) 1))) - (display-buffer (set-buffer proof-pbp-buffer)) - (goto-char (point-max)) - (insert str "\n")) - (if (string-match "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]" str) - (progn - (setq file (match-string 2 str) - module (match-string 1 str)) - (if (string= file "") - (setq file (buffer-file-name proof-script-buffer))) - (setq file (expand-file-name file)) - (if (string-match "\\(.*\\)\\.." file) - (setq file (match-string 1 file))) - (setq proof-included-files-list (cons (cons module file) - proof-included-files-list)))))) - -(defun proof-shell-filter (str) - "The filter for the shell-process. We sleep until we get a - wakeup-char in the input, then run proof-shell-process-output, and - set proof-marker to keep track of how far we've got." - (if (string-match proof-shell-eager-annotation-end str) - (proof-shell-popup-eager-annotation)) - (if (or - ;; Some proof systems can be hacked to have annotated prompts; - ;; for these we set proof-shell-wakeup-char to the annotation special. - (and proof-shell-wakeup-char - (string-match (char-to-string proof-shell-wakeup-char) str)) - ;; Others rely on a standard top-level (e.g. SML) whose prompt can't - ;; be hacked. For those we use the prompt regexp. - (string-match proof-shell-annotated-prompt-regexp str)) - (if (null (marker-position proof-marker)) - ;; Set marker to first prompt in output buffer, and sleep again. - (progn - (goto-char (point-min)) - (re-search-forward proof-shell-annotated-prompt-regexp) - ;; FIXME: da: why is this next line here? to delete the - ;; possibly several character prompt? why? - ;; TMS: Its purpose is to remove the wakeup - ;; character associated with the prompt. This - ;; should not be necessary anymore, because the wakeup - ;; character isn't displayed anyway; see - ;; `proof-dont-show-annotations'. Watch this space! - (backward-delete-char 1) - (set-marker proof-marker (point))) - ;; We've matched against a second prompt in str now. Search - ;; the output buffer for the second prompt after the one previously - ;; marked. - (let (string res cmd) - (goto-char (marker-position proof-marker)) - (re-search-forward proof-shell-annotated-prompt-regexp nil t) - (backward-char (- (match-end 0) (match-beginning 0))) - (setq string (buffer-substring (marker-position proof-marker) - (point))) - (goto-char (point-max)) ; da: assumed to be after a prompt? - (backward-delete-char 1) ; da: WHY? nasty assumption. - (setq cmd (nth 1 (car proof-action-list))) - (save-excursion - (setq res (proof-shell-process-output cmd string)) - (cond - ((and (consp res) (eq (car res) 'error)) - (proof-shell-handle-error cmd (cdr res))) - ((eq res 'interrupt) - (proof-shell-handle-interrupt)) - ((and (consp res) (eq (car res) 'loopback)) - (proof-shell-insert-loopback-cmd (cdr res)) - (proof-shell-exec-loop)) - (t (if (proof-shell-exec-loop) - (proof-shell-handle-delayed-output))))))))) - -(defun proof-last-goal-or-goalsave () - (save-excursion - (let ((span (span-at-before (proof-locked-end) 'type))) - (while (and span - (not (eq (span-property span 'type) 'goalsave)) - (or (eq (span-property span 'type) 'comment) - (not (funcall proof-goal-command-p - (span-property span 'cmd))))) - (setq span (prev-span span 'type))) - span))) - -;; This needs some work to make it generic, since most of the code -;; doesn't apply to Coq at all. -(defun proof-steal-process () - "This allows us to steal the process if we want to change the buffer - in which script management is running." - (proof-start-shell) - (if proof-shell-busy (error "Proof Process Busy!")) - (if (not (eq proof-buffer-type 'script)) - (error "Must be running in a script buffer")) - (cond - ((eq proof-script-buffer (current-buffer)) - nil) - (t - (let ((flist proof-included-files-list) - (file (expand-file-name (buffer-file-name))) span (cmd "")) - (if (string-match "\\(.*\\)\\.." file) (setq file (match-string 1 file))) - (while (and flist (not (string= file (cdr (car flist))))) - (setq flist (cdr flist))) - (if (null flist) - (if (not (y-or-n-p "Steal script management? " )) (error "Aborted")) - (if (not (y-or-n-p "Reprocess this file? " )) (error "Aborted"))) - (if (not (buffer-name proof-script-buffer)) - (message "Warning: Proof script buffer deleted: proof state may be inconsistent") - (save-excursion - (set-buffer proof-script-buffer) - (setq proof-active-buffer-fake-minor-mode nil) - (setq span (proof-last-goal-or-goalsave)) - ;; This won't work for Coq if we have recursive goals in progress - (if (and span (not (eq (span-property span 'type) 'goalsave))) - (setq cmd proof-kill-goal-command)) - (proof-detach-segments) - (delete-spans (point-min) (point-max) 'type))) - - (setq proof-script-buffer (current-buffer)) - (proof-init-segmentation) - (setq proof-active-buffer-fake-minor-mode t) - - (cond - (flist - (list nil (concat cmd "ForgetMark " (car (car flist)) ";") - `(lambda (span) (setq proof-included-files-list - (quote ,(cdr flist)))))) - ((not (string= cmd "")) - (list nil cmd 'proof-done-invisible)) - (t nil)))))) - -(defun proof-done-invisible (span) ()) - -(defun proof-invisible-command (cmd &optional relaxed) - "Send cmd to the proof process without responding to the user." - (proof-check-process-available relaxed) - (if (not (string-match proof-re-end-of-cmd cmd)) - (setq cmd (concat cmd proof-terminal-string))) - (proof-start-queue nil nil (list (list nil cmd - 'proof-done-invisible)) relaxed)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; User Commands ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -; Script management uses two major segments: Locked, which marks text -; which has been sent to the proof assistant and cannot be altered -; without being retracted, and Queue, which contains stuff being -; queued for processing. proof-action-list contains a list of -; (span,command,action) triples. The loop looks like: Execute the -; command, and if it's successful, do action on span. If the -; command's not successful, we bounce the rest of the queue and do -; some error processing. -; -; when a span has been processed, we classify it as follows: -; 'goalsave - denoting a 'goalsave pair in the locked region -; a 'goalsave region has a 'name property which is the name of the goal -; 'comment - denoting a comment -; 'pbp - denoting a span created by pbp -; 'vanilla - denoting any other span. -; 'pbp & 'vanilla spans have a property 'cmd, which says what -; command they contain. - -; We don't allow commands while the queue has anything in it. So we -; do configuration by concatenating the config command on the front in -; proof-send - -;; proof-assert-until-point, and various gunk for its ;; -;; setup and callback ;; - -;; This code is for nested goals in Coq, and shouldn't affect things -;; in LEGO. It lifts "local" lemmas from inside goals out to top -;; level. - -(defun proof-lift-global (glob-span) - (let (start (next (span-at 1 'type)) str (goal-p nil)) - (while (and next (and (not (eq next glob-span)) (not goal-p))) - (if (and (eq (span-property next 'type) 'vanilla) - (funcall proof-goal-command-p (span-property next 'cmd))) - (setq goal-p t) - (setq next (next-span next 'type)))) - - (if (and next (not (eq next glob-span))) - (progn - (proof-unlock-locked) - (setq str (buffer-substring (span-start glob-span) - (span-end glob-span))) - (delete-region (span-start glob-span) (span-end glob-span)) - (goto-char (span-start next)) - (setq start (point)) - (insert str "\n") - (set-span-endpoints glob-span start (point)) - (set-span-start next (point)) - (proof-lock-unlocked))))) - -;; This is the actual callback for assert-until-point. - -(defun proof-done-advancing (span) - (let ((end (span-end span)) nam gspan next cmd) - (proof-set-locked-end end) - (proof-set-queue-start end) - (setq cmd (span-property span 'cmd)) - (cond - ((eq (span-property span 'type) 'comment) - (set-span-property span 'mouse-face 'highlight)) - ((string-match proof-save-command-regexp cmd) - ;; In coq, we have the invariant that if we've done a save and - ;; there's a top-level declaration then it must be the - ;; associated goal. (Notice that because it's a callback it - ;; must have been approved by the theorem prover.) - (if (string-match proof-save-with-hole-regexp cmd) - (setq nam (match-string 2 cmd))) - (setq gspan span) - (while (or (eq (span-property gspan 'type) 'comment) - (not (funcall proof-goal-command-p - (setq cmd (span-property gspan 'cmd))))) - (setq next (prev-span gspan 'type)) - (delete-span gspan) - (setq gspan next)) - - (if (null nam) - (if (string-match proof-goal-with-hole-regexp - (span-property gspan 'cmd)) - (setq nam (match-string 2 (span-property gspan 'cmd))) - ;; This only works for Coq, but LEGO raises an error if - ;; there's no name. - ;; FIXME: a nonsense for Isabelle. - (setq nam "Unnamed_thm"))) - - (set-span-end gspan end) - (set-span-property gspan 'mouse-face 'highlight) - (set-span-property gspan 'type 'goalsave) - (set-span-property gspan 'name nam) - - (proof-lift-global gspan)) - (t - (set-span-property span 'mouse-face 'highlight) - (if (funcall proof-global-p cmd) - (proof-lift-global span)))))) - -; depth marks number of nested comments. quote-parity is false if -; we're inside ""'s. Only one of (depth > 0) and (not quote-parity) -; should be true at once. -- hhg - -(defun proof-segment-up-to (pos) - "Create a list of (type,int,string) pairs from the end of the locked -region to pos, denoting the command and the position of its -terminator. type is one of comment, or cmd. 'unclosed-comment may be -consed onto the start if the segment finishes with an unclosed -comment." - (save-excursion - (let ((str (make-string (- (buffer-size) (proof-locked-end) -10) ?x)) - (i 0) (depth 0) (quote-parity t) done alist c) - (proof-goto-end-of-locked) - (while (not done) - (cond - ((and (= (point) pos) (> depth 0)) - (setq done t alist (cons 'unclosed-comment alist))) - ((= (point) (point-max)) - (if (not quote-parity) - (message "Warning: unclosed quote")) - (setq done t)) - ((and (looking-at "\\*)") quote-parity) - (if (= depth 0) - (progn (message "Warning: extraneous comment end") (setq done t)) - (setq depth (- depth 1)) (forward-char 2) - (if (eq i 0) - (setq alist (cons (list 'comment "" (point)) alist)) - (aset str i ?\ ) (incf i)))) - ((and (looking-at "(\\*") quote-parity) - (setq depth (+ depth 1)) (forward-char 2)) - ((> depth 0) (forward-char)) - (t - (setq c (char-after (point))) - (if (or (> i 0) (not (= (char-syntax c) ?\ ))) - (progn (aset str i c) (incf i))) - (if (looking-at "\"") - (setq quote-parity (not quote-parity))) - (forward-char) - (if (and (= c proof-terminal-char) quote-parity) - (progn - (setq alist - (cons (list 'cmd (substring str 0 i) (point)) alist)) - (if (>= (point) pos) (setq done t) (setq i 0))))))) - alist))) - -(defun proof-semis-to-vanillas (semis &optional callback-fn) - "Convert a sequence of semicolon positions (returned by the above -function) to a set of vanilla extents." - (let ((ct (proof-locked-end)) span alist semi) - (while (not (null semis)) - (setq semi (car semis) - span (make-span ct (nth 2 semi)) - ct (nth 2 semi)) - (if (eq (car (car semis)) 'cmd) - (progn - (set-span-property span 'type 'vanilla) - (set-span-property span 'cmd (nth 1 semi)) - (setq alist (cons (list span (nth 1 semi) - (or callback-fn 'proof-done-advancing)) - alist))) - (set-span-property span 'type 'comment) - (setq alist (cons (list span "COMMENT" 'proof-done-advancing) alist))) - (setq semis (cdr semis))) - (nreverse alist))) - -; Assert until point - We actually use this to implement the -; assert-until-point, active terminator keypress, and find-next-terminator. -; In different cases we want different things, but usually the information -; (i.e. are we inside a comment) isn't available until we've actually run -; proof-segment-up-to (point), hence all the different options when we've -; done so. - -(defun proof-assert-until-point - (&optional unclosed-comment-fun ignore-proof-process-p) - "Process the region from the end of the locked-region until point. - Default action if inside a comment is just to go until the start of - the comment. If you want something different, put it inside - unclosed-comment-fun. If ignore-proof-process-p is set, no commands - will be added to the queue." - (interactive) - (let ((pt (point)) - (crowbar (or ignore-proof-process-p (proof-steal-process))) - semis) - (save-excursion - (if (not (re-search-backward "\\S-" (proof-locked-end) t)) - (progn (goto-char pt) - (error "Nothing to do!"))) - (setq semis (proof-segment-up-to (point)))) - (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) - (funcall unclosed-comment-fun) - (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) - (if (and (not ignore-proof-process-p) (not crowbar) (null semis)) - (error "Nothing to do!")) - (goto-char (nth 2 (car semis))) - (and (not ignore-proof-process-p) - (let ((vanillas (proof-semis-to-vanillas (nreverse semis)))) - (if crowbar (setq vanillas (cons crowbar vanillas))) - (proof-start-queue (proof-locked-end) (point) vanillas)))))) - -;; insert-pbp-command - an advancing command, for use when ;; -;; PbpHyp or Pbp has executed in LEGO, and returned a ;; -;; command for us to run ;; - -(defun proof-insert-pbp-command (cmd) - (proof-check-process-available) - (let (span) - (proof-goto-end-of-locked) - (insert cmd) - (setq span (make-span (proof-locked-end) (point))) - (set-span-property span 'type 'pbp) - (set-span-property span 'cmd cmd) - (proof-start-queue (proof-locked-end) (point) - (list (list span cmd 'proof-done-advancing))))) - - -;; proof-retract-until-point and associated gunk ;; -;; most of the hard work (i.e computing the commands to do ;; -;; the retraction) is implemented in the customisation ;; -;; module (lego.el or coq.el) which is why this looks so ;; -;; straightforward ;; - - -(defun proof-done-retracting (span) - "Updates display after proof process has reset its state. See also -the documentation for `proof-retract-until-point'. It optionally -deletes the region corresponding to the proof sequence." - (let ((start (span-start span)) - (end (span-end span)) - (kill (span-property span 'delete-me))) - (proof-set-locked-end start) - (proof-set-queue-end start) - (delete-spans start end 'type) - (delete-span span) - (if kill (delete-region start end)))) - -(defun proof-setup-retract-action (start end proof-command delete-region) - (let ((span (make-span start end))) - (set-span-property span 'delete-me delete-region) - (list (list span proof-command 'proof-done-retracting)))) - -(defun proof-retract-target (target delete-region) - (let ((end (proof-locked-end)) - (start (span-start target)) - (span (proof-last-goal-or-goalsave)) - actions) - - (if (and span (not (eq (span-property span 'type) 'goalsave))) - (if (< (span-end span) (span-end target)) - (progn - (setq span target) - (while (and span (eq (span-property span 'type) 'comment)) - (setq span (next-span span 'type))) - (setq actions (proof-setup-retract-action - start end - (if (null span) "COMMENT" - (funcall proof-count-undos-fn span)) - delete-region) - end start)) - - (setq actions (proof-setup-retract-action (span-start span) end - proof-kill-goal-command - delete-region) - end (span-start span)))) - - (if (> end start) - (setq actions - (nconc actions (proof-setup-retract-action - start end - (funcall proof-find-and-forget-fn target) - delete-region)))) - - (proof-start-queue (min start end) (proof-locked-end) actions))) - -(defun proof-retract-until-point (&optional delete-region) - "Sets up the proof process for retracting until point. In - particular, it sets a flag for the filter process to call - `proof-done-retracting' after the proof process has actually - successfully reset its state. It optionally deletes the region in - the proof script corresponding to the proof command sequence. If - this function is invoked outside a locked region, the last - successfully processed command is undone." - (interactive) - (proof-check-process-available) - (let ((span (span-at (point) 'type))) - (if (null (proof-locked-end)) (error "No locked region")) - (and (null span) - (progn (proof-goto-end-of-locked) (backward-char) - (setq span (span-at (point) 'type)))) - (proof-retract-target span delete-region))) - -;; proof-try-command ;; -;; this isn't really in the spirit of script management, ;; -;; but sometimes the user wants to just try an expression ;; -;; without having to undo it in order to try something ;; -;; different. Of course you can easily lose sync by doing ;; -;; something here which changes the proof state ;; - -(defun proof-done-trying (span) - (delete-span span) - (proof-detach-queue)) - -(defun proof-try-command - (&optional unclosed-comment-fun) - - "Process the command at point, - but don't add it to the locked region. This will only happen if - the command satisfies proof-state-preserving-p. - - Default action if inside a comment is just to go until the start of - the comment. If you want something different, put it inside - unclosed-comment-fun." - (interactive) - (let ((pt (point)) semis crowbar test) - (setq crowbar (proof-steal-process)) - (save-excursion - (if (not (re-search-backward "\\S-" (proof-locked-end) t)) - (progn (goto-char pt) - (error "Nothing to do!"))) - (setq semis (proof-segment-up-to (point)))) - (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) - (funcall unclosed-comment-fun) - (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) - (if (and (not crowbar) (null semis)) (error "Nothing to do!")) - (setq test (car semis)) - (if (not (funcall proof-state-preserving-p (nth 1 test))) - (error "Command is not state preserving")) - (goto-char (nth 2 test)) - (let ((vanillas (proof-semis-to-vanillas (list test) - 'proof-done-trying))) - (if crowbar (setq vanillas (cons crowbar vanillas))) - (proof-start-queue (proof-locked-end) (point) vanillas))))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; misc other user functions ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(defun proof-undo-last-successful-command () - "Undo last successful command, both in the buffer recording the - proof script and in the proof process. In particular, it deletes - the corresponding part of the proof script." - (interactive) - (goto-char (span-start (span-at-before (proof-locked-end) 'type))) - (proof-retract-until-point t)) - -(defun proof-interrupt-process () - (interactive) - (if (not (proof-shell-live-buffer)) - (error "Proof Process Not Started!")) - (if (not (eq proof-script-buffer (current-buffer))) - (error "Don't own process!")) - (if (not proof-shell-busy) - (error "Proof Process Not Active!")) - (save-excursion - (set-buffer proof-shell-buffer) - (comint-interrupt-subjob))) - - -(defun proof-find-next-terminator () - "Set point after next `proof-terminal-char'." - (interactive) - (let ((cmd (span-at (point) 'type))) - (if cmd (goto-char (span-end cmd)) - (and (re-search-forward "\\S-" nil t) - (proof-assert-until-point nil 'ignore-proof-process))))) - -(defun proof-process-buffer () - "Process the current buffer and set point at the end of the buffer." - (interactive) - (end-of-buffer) - (proof-assert-until-point)) - -;; For when things go horribly wrong - -(defun proof-restart-script () - (interactive) - (save-excursion - (if (buffer-live-p proof-script-buffer) - (progn - (set-buffer proof-script-buffer) - (setq proof-active-buffer-fake-minor-mode nil) - (delete-spans (point-min) (point-max) 'type) - (proof-detach-segments))) - (setq proof-shell-busy nil - proof-script-buffer nil) - (if (buffer-live-p proof-shell-buffer) - (kill-buffer proof-shell-buffer)) - (if (buffer-live-p proof-pbp-buffer) - (kill-buffer proof-pbp-buffer)))) - -;; A command for making things go horribly wrong - it moves the -;; end-of-locked-region marker backwards, so user had better move it -;; correctly to sync with the proof state, or things will go all -;; pear-shaped. - -(defun proof-frob-locked-end () - (interactive) - "Move the end of the locked region backwards. - Only for use by consenting adults." - (cond - ((not (eq proof-script-buffer (current-buffer))) - (error "Not in proof buffer")) - ((> (point) (proof-locked-end)) - (error "Can only move backwards")) - (t (proof-set-locked-end (point)) - (delete-spans (proof-locked-end) (point-max) 'type)))) - -(defvar proof-minibuffer-history nil - "The last command read from the minibuffer") - -(defun proof-execute-minibuffer-cmd () - (interactive) - (let (cmd) - (proof-check-process-available 'relaxed) - (setq cmd (read-string "Command: " nil 'proof-minibuffer-history)) - (proof-invisible-command cmd 'relaxed))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; Popup and Pulldown Menu ;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;;; Menu commands for the underlying proof assistant -(defvar proof-ctxt-string "" - "Command to display context in proof assistant") - -(defvar proof-help-string "" - "Command to ask for help in proof assistant") - -(defvar proof-prf-string "" - "Command to display proof state in proof assistant") - -(defun proof-ctxt () - "List context." - (interactive) - (proof-invisible-command (concat proof-ctxt-string proof-terminal-string))) - -(defun proof-help () - "Print help message giving syntax." - (interactive) - (proof-invisible-command (concat proof-help-string proof-terminal-string))) - -(defun proof-prf () - "List proof state." - (interactive) - (proof-invisible-command (concat proof-prf-string proof-terminal-string))) - -;;; To be called from menu -(defun proof-info-mode () - "Info mode on proof mode." - (interactive) - (info "script-management")) - -(defun proof-exit () - "Exit Proof-assistant." - (interactive) - (proof-restart-script)) - -(defvar proof-help-menu - '("Help" - ["Proof assistant web page" - (w3-fetch proof-www-home-page) t] - ["Help on Emacs proof-mode" proof-info-mode t] - ) - "The Help Menu in Script Management.") - -(defvar proof-shared-menu - (append-element '( - ["Display context" proof-ctxt - :active (proof-shell-live-buffer)] - ["Display proof state" proof-prf - :active (proof-shell-live-buffer)] - ["Exit proof assistant" proof-exit - :active (proof-shell-live-buffer)] - "----" - ["Find definition/declaration" find-tag-other-window t] - ) - proof-help-menu)) - -(defvar proof-menu - (append '("Commands" - ["Toggle active terminator" proof-active-terminator-minor-mode - :active t - :style toggle - :selected proof-active-terminator-minor-mode] - "----") - (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) - "--:doubleLine" "----")) - proof-shared-menu - ) - "*The menu for the proof assistant.") - -(defvar proof-shell-menu proof-shared-menu - "The menu for the Proof-assistant shell") - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Active terminator minor mode ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(deflocal proof-active-terminator-minor-mode nil - "active terminator minor mode flag") - -(defun proof-active-terminator-minor-mode (&optional arg) - "Toggle PROOF's Active Terminator minor mode. -With arg, turn on the Active Terminator minor mode if and only if arg -is positive. - -If Active terminator mode is enabled, a terminator will process the -current command." - - (interactive "P") - -;; has this minor mode been registered as such? - (or (assq 'proof-active-terminator-minor-mode minor-mode-alist) - (setq minor-mode-alist - (append minor-mode-alist - (list '(proof-active-terminator-minor-mode - (concat " " proof-terminal-string)))))) - - (setq proof-active-terminator-minor-mode - (if (null arg) (not proof-active-terminator-minor-mode) - (> (prefix-numeric-value arg) 0))) - (if (fboundp 'redraw-modeline) - (redraw-modeline) - (force-mode-line-update))) - -(defun proof-process-active-terminator () - "Insert the terminator in an intelligent way and assert until the - new terminator. Fire up proof process if necessary." - (let ((mrk (point)) ins) - (if (looking-at "\\s-\\|\\'\\|\\w") - (if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t)) - (error "Nothing to do!"))) - (if (not (= (char-after (point)) proof-terminal-char)) - (progn (forward-char) (insert proof-terminal-string) (setq ins t))) - (proof-assert-until-point - (function (lambda () - (if ins (backward-delete-char 1)) - (goto-char mrk) (insert proof-terminal-string)))))) - -(defun proof-active-terminator () - (interactive) - (if proof-active-terminator-minor-mode - (proof-process-active-terminator) - (self-insert-command 1))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Proof mode configuration ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -(define-derived-mode proof-mode fundamental-mode - proof-mode-name "Proof mode - not standalone" - ;; define-derived-mode proof-mode initialises proof-mode-map - (setq proof-buffer-type 'script)) - -;; This has to come after proof-mode is defined - -(define-derived-mode proof-shell-mode comint-mode - "proof-shell" "Proof shell mode - not standalone" - (setq proof-buffer-type 'shell) - (setq proof-shell-busy nil) - (setq proof-shell-delayed-output (cons 'insert "done")) - (setq comint-prompt-regexp proof-shell-prompt-pattern) - (add-hook 'comint-output-filter-functions 'proof-shell-filter nil t) - (setq comint-get-old-input (function (lambda () ""))) - (proof-dont-show-annotations) - (setq proof-marker (make-marker))) - -(easy-menu-define proof-shell-menu - proof-shell-mode-map - "Menu used in the proof assistant shell." - (cons proof-mode-name (cdr proof-shell-menu))) - -(easy-menu-define proof-mode-menu - proof-mode-map - "Menu used in proof mode." - (cons proof-mode-name (cdr proof-menu))) - -;; the following callback is an irritating hack - there should be some -;; elegant mechanism for computing constants after the child has -;; configured. - -(defun proof-config-done () - -;; calculate some strings and regexps for searching - - (setq proof-terminal-string (char-to-string proof-terminal-char)) - - (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) - (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) - - (make-local-variable 'comment-start) - (setq comment-start (concat proof-comment-start " ")) - (make-local-variable 'comment-end) - (setq comment-end (concat " " proof-comment-end)) - (make-local-variable 'comment-start-skip) - (setq comment-start-skip - (concat (regexp-quote proof-comment-start) "+\\s_?")) - - (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'")) - (setq proof-re-term-or-comment - (concat proof-terminal-string "\\|" (regexp-quote proof-comment-start) - "\\|" (regexp-quote proof-comment-end))) - -;; func-menu --- Jump to a goal within a buffer - (and (boundp 'fume-function-name-regexp-alist) - (defvar fume-function-name-regexp-proof - (cons proof-goal-with-hole-regexp 2)) - (push (cons major-mode 'fume-function-name-regexp-proof) - fume-function-name-regexp-alist)) - (and (boundp 'fume-find-function-name-method-alist) - (push (cons major-mode 'fume-match-find-next-function-name) - fume-find-function-name-method-alist)) - -;; Info - (or (memq proof-info-dir Info-default-directory-list) - (setq Info-default-directory-list - (cons proof-info-dir Info-default-directory-list))) - -;; keymaps and menus - (easy-menu-add proof-mode-menu proof-mode-map) - - (proof-define-keys proof-mode-map proof-universal-keys) - - (define-key proof-mode-map - (vconcat [(control c)] (vector proof-terminal-char)) - 'proof-active-terminator-minor-mode) - - (define-key proof-mode-map [(control c) (control e)] - 'proof-find-next-terminator) - - (define-key proof-mode-map (vector proof-terminal-char) - 'proof-active-terminator) - (define-key proof-mode-map [(control c) (return)] 'proof-assert-until-point) - (define-key proof-mode-map [(control c) (control t)] 'proof-try-command) - (define-key proof-mode-map [(control c) ?u] 'proof-retract-until-point) - (define-key proof-mode-map [(control c) (control u)] - 'proof-undo-last-successful-command) - - (define-key proof-mode-map [(control c) ?\'] - 'proof-goto-end-of-locked-interactive) - (define-key proof-mode-map [(control button1)] 'proof-send-span) - (define-key proof-mode-map [(control c) (control b)] 'proof-process-buffer) - (define-key proof-mode-map [(control c) (control z)] 'proof-frob-locked-end) - - (define-key proof-mode-map [tab] 'proof-indent-line) - (make-local-variable 'indent-line-function) - (setq indent-line-function 'proof-indent-line) - - (define-key (current-local-map) [(control c) (control p)] 'proof-prf) - (define-key (current-local-map) [(control c) ?c] 'proof-ctxt) - (define-key (current-local-map) [(control c) ?h] 'proof-help) - -;; For fontlock - (remove-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer t) - (add-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer nil t) - (remove-hook 'font-lock-mode-hook 'proof-unfontify-separator t) - (add-hook 'font-lock-mode-hook 'proof-unfontify-separator nil t) - -;; if we don't have the following, zap-commas fails to work. - - (and (boundp 'font-lock-always-fontify-immediately) - (setq font-lock-always-fontify-immediately t)) - - (run-hooks 'proof-mode-hook)) - -(defun proof-shell-config-done () - (accept-process-output (get-buffer-process (current-buffer))) - - ;; If the proof process in invoked on a different machine e.g., - ;; for proof-prog-name="rsh fastmachine proofprocess", one needs - ;; to adjust the directory: - (and proof-shell-cd - (proof-shell-insert (format proof-shell-cd - ;; under Emacs 19.34 default-directory contains "~" which causes - ;; problems with LEGO's internal Cd command - (expand-file-name default-directory)))) - - (if proof-shell-init-cmd - (proof-shell-insert proof-shell-init-cmd)) - -;; Note that proof-marker actually gets set in proof-shell-filter. -;; This is manifestly a hack, but finding somewhere more convenient -;; to do the setup is tricky. - - (while (null (marker-position proof-marker)) - (if (accept-process-output (get-buffer-process (current-buffer)) 15) - () - (error "Failed to initialise proof process")))) - -(define-derived-mode pbp-mode fundamental-mode - proof-mode-name "Proof by Pointing" - ;; defined-derived-mode pbp-mode initialises pbp-mode-map - (setq proof-buffer-type 'pbp) - (suppress-keymap pbp-mode-map 'all) -; (define-key pbp-mode-map [(button2)] 'pbp-button-action) - (proof-define-keys pbp-mode-map proof-universal-keys) - (erase-buffer)) - - -(provide 'proof) diff --git a/script-management.texinfo b/script-management.texinfo deleted file mode 100644 index a7232b3c..00000000 --- a/script-management.texinfo +++ /dev/null @@ -1,440 +0,0 @@ -\input texinfo @c -*-texinfo-*- -@c %**start of header -@setfilename script-management.info -@settitle Script Management -@paragraphindent 0 -@c %**end of header - -@setchapternewpage odd - -@titlepage -@sp 10 -@comment The title is printed in a large font. -@center @titlefont{Script Management Mode} - -@c The following two commands start the copyright page. -@page -@vskip 0pt plus 1filll -Copyright @copyright{} 1997, 1998 LEGO Team, LFCS Edinburgh -@end titlepage - -@node Top, Credits, (dir), (dir) -@comment node-name, next, previous, up - -A @emph{proof script} is a sequence of commands to a proof assistant. -Proof mode is a mode designed to be customised for a particular proof -assistant, to manage communication with a proof process and thereby -support building and secure editing of proof scripts. Currently custom -modes exist for LEGO and Coq. - -@menu -* Credits:: The people Involved -* Introduction:: Introduction to Script Management -* Commands:: Proof mode Commands -* Multiple Files:: Proof developments spanning several files -* Proof by Pointing:: Proof using the Mouse -* An Active Terminator:: Active Terminator minor mode -* Walkthrough:: An example of using proof mode -* LEGO mode:: Extra Bindings for LEGO -* Coq mode:: Extra Bindings for Coq -* Internals:: The Seedy Underside of Proof mode -* Known Problems:: Caveat Emptor -@end menu - -@node Credits, Introduction, Top, Top -@comment node-name, next, previous, up -@unnumberedsec Credits - -Inspired by Yves Bertot's Centaur-based proof environment CtCoq, Healf -Goguen, Thomas Kleymann and Dilip Sequeira have implented a generic -proof mode for Emacs. The original proof-by-pointing algorithm has been -implemented by Yves Bertot. This manual was originally written by Dilip -Sequeira. - -@node Introduction, Commands, Credits, Top -@comment node-name, next, previous, up -@unnumberedsec Introduction - -Each script resides in an Emacs buffer, called a @emph{script buffer}, -which is divided into three regions: - -@itemize @bullet -@item The @emph{Locked} region appears in blue (underlined on monochrome -displays) and contains commands which have been sent to the proof process -and verified. The commands in the locked region cannot be edited. - -@item The @emph{Queue} region appears in pink (inverse video) and contains -commands waiting to be sent to the proof process. Like those in the -locked region, these commands can't be edited. - -@item The @emph{Editing} region contains the commands the user is working -on, and can be edited as normal Emacs text. -@end itemize - -These three regions appear in the buffer in the order above; that is, -the locked region is always at the start of the buffer, and the editing -region always at the end. The queue region only exists if there is input -waiting to be sent to the proof process. - -Proof mode has two operations which transfer commands between these -regions: assertion and retraction. These cause commands to be sent to -the proof process, and Emacs will summarise the results in the -@emph{Response Buffer}. - -@strong{Assertion} causes commands from the editing region to be -transferred to the queue region and sent one by one to the proof -process. If the command is accepted, it is transferred to the locked -region, but if an error occurs it is signalled to the user, and the -offending command is transferred back to the editing region together -with any remaining commands in the queue. @strong{Retraction} causes -commands to be transferred from the locked region to the editing region -(again via the queue region) and the appropriate 'undo' commands to be -sent to the proof process. - -As commands are transferred to the locked region, they are aggregated -into segments which constitute the smallest units which can be -undone. Typically a segment consists of a declaration or definition, or -all the text from a `goal' command to the corresponding `save' command, -or the individual commands in the proof of an unfinished goal. As the -mouse moves over the the region, the segment containing the pointer will -be highlighted. - -Commands in the editing region can be freely edited while -commands in the queue are transferred to the proof process. However, -assertion and retraction commands can only be issued when the queue is -empty. - -@node Commands, Multiple Files, Introduction, Top -@unnumberedsec Proof Mode Commands - -@table @kbd - -@item C-c C-b -assert the commands in the buffer. - -@item C-c return -assert the commands in the editing region up to and -including the one containing the point. - -@item C-c u -retract the segments in the locked region back to and -including the one containing the point. If point is outside the *Locked* -region, the last segment is undone. - -@item C-c C-u -retract the last segment in the locked region, and kill the text in it. -@footnote{Be careful with this, as it may delete more than you anticipate. -However, you can always recover the killed text using Emacs Undo.} - -@item C-c ' -move the point to the end of the locked region. If you are in a script -buffer other than the active scripting buffer, this will also transfer -you to the active one. - -@item C-c C-e -move the point to the next terminator - -@item C-c C-p -display the proof state in the response buffer - -@item C-c c -display the context in the response buffer - -@item C-c h -print proof-system specific help text in the response buffer - -@item C-c C-c -interrupt the process process. This may leave script management or the -proof process (or both) in an inconsistent state. - -@item C-c C-z -move the end of the locked region backwards to the end of the segment -containing the point. @footnote{Don't try this one at home, kids.} - -@item C-c C-t -Send the command at the point to the subprocess, not -recording it in the locked region. @footnote{This is supplied in order -to enable the user to test the types and values of expressions. There's -some checking that the command won't change the proof state, but it -isn't foolproof.} - -@item C-c C-v -Request a command from the minibuffer and send it to -the subprocess. Currently no checking whatsoever is done on the command. -@end table - -The command @code{proof-restart-script} can be used to completely -restart script management. - - -@node Multiple Files, An Active Terminator, Commands, Top -@unnumberedsec Multiple Files - -Proof mode has a rudimentary facility for operating with multiple files -in a proof development. This is currently only supported for LEGO. If -the user invokes script management in a different buffer from the one in -which it is running, one of two prompts will appear: - -@itemize @bullet -@item ``Steal script management?'' -if Emacs doesn't think the file is already part of the proof development -@item ``Reprocess this file?'' -if Emacs thinks the file is already included in the proof process. If -the user confirms, Emacs will cause the proof process to forget the -contents of the file, so that it is processed afresh. -@end itemize - -Currently this facility requires each script buffer to have a -corresponding file. - -When working with script management in multiple buffers, it is easy -to lose track of which buffer is the current script buffer. As a mnemonic -aid, the word @samp{Scripting} appears in the minor mode list of the -active scripting buffer. - -Caveats: -@itemize @minus -@item Note that if processing a buffer causes other files to be loaded -into the LEGO process, those files will be imported from disk rather -than from any Emacs buffer in which it is being edited, i.e.@: if your -file is going to be included indirectly, save it. - -@item However much you move around the file system in Emacs, the -LEGOPATH will be the LEGOPATH you started with. No concept of -"current directory" is currently supported. -@end itemize - -@node An Active Terminator, Proof by Pointing, Multiple Files, Top -@unnumberedsec An Active Terminator - -Proof mode has a minor mode which causes the terminator to become -active. When this mode is active, pressing the terminator key (@kbd{;} -for LEGO, @kbd{.} for Coq) outside a comment or quote will cause the -character to be entered into the buffer, and all the commands in the -editing region up to the point to be asserted. - -This mode can be toggled with the command -`proof-active-terminator-minor-mode' (@kbd{C-c ;} or @kbd{C-c .}) - -@node Proof by Pointing, Walkthrough, An Active Terminator, Top -@unnumberedsec Proof by Pointing - -@emph{This mode is currently very unreliable, and we do not guarantee -that it will work as discussed in this document.} - -Proof by pointing is a facility whereby proof commands can be generated -by using the mouse to select terms. When proving a goal, a summary of -the current proof state will appear in the response buffer. By moving -the mouse over the buffer, the structure of the goal and hypothesis -terms will be shown by highlighting. - -If a selection is made using the second (usually the middle) mouse -button, Emacs will generate the appropriate commands, insert them in the -script buffer, and send them to the proof process. These commands are -aggregated in the locked region as a single segment, so that a -mouse-generated command sequence can be retracted with a single -retraction command. - -Further Information about proof by pointing may be found in the paper -@cite{User Interfaces for Theorem Provers} by Yves Bertot and Laurent -Thery, to appear in @cite{Information and Computation}, from which -the following example is taken. - -@menu -* Proof by Pointing Example:: An example using proof by pointing -@end menu - -@node Proof by Pointing Example, ,Proof by Pointing,Proof by Pointing - -Suppose we wish to prove the lego term: - -@example -(((p a) \/ (q b)) /\ @{x:Prop@}(p x) -> (q x)) -> (Ex ([x:Prop] q(x))); -@end example - -Asserting this goal will result in the proof state - -@example -?0 : ((p a \/ q b) /\ @{x:Prop@}(p x)->q x)->Ex ([x:Prop]q x) -@end example - -appearing in the response buffer. Suppose our strategy is to use a -case analysis on the disjunction, starting with the @samp{p(a)} subterm. -Clicking on this term will cause script management to insert the following -command sequence in the script buffer, and execute it. - -@example -Intros H; Refine H; Intros H0 H1; -Refine or_elim H0 Then Intros H2; Try Refine H2; -@end example - - -The response buffer will then read - -@example - H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x - H0 : p a \/ q b - H1 : @{x:Prop@}(p x)->q x - H2 : p a - ?10 : Ex ([x:Prop]q x) -@end example - -Clicking on the subterm @samp{(p x)} in the hypothesis H1 will instruct -script management to prove an instance of @samp{(p x)} and deduce the -corresponding @samp{(q x)}. The commands - -@example -allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption; -@end example - -are inserted and executed, leaving the proof state as - -@example - H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x - H0 : p a \/ q b - H1 : @{x:Prop@}(p x)->q x - H2 : p a - H3 : (p a)->q a - ?20 : (q a)->Ex ([x:Prop]q x) -@end example - -Now clicking on the @samp{q x)} subterm in ?20 will prove the subgoal. We are -left with the other half of the original case analysis: - -@example - H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x - H0 : p a \/ q b - H1 : @{x:Prop@}(p x)->q x - H2 : q b - ?26 : Ex ([x:Prop]q x) -@end example - -Clicking on @samp{q x} proves the goal. - - - - -@node Walkthrough, LEGO mode, Proof by Pointing, Top -@unnumberedsec A Walkthrough - -Here's a LEGO example of how script management is used. - -First, we turn on active terminator minor mode by typing @kbd{C-c ;} -Then we enter - -`Module Walkthrough Import lib_logic;' - -The command should be lit in pink (or inverse video if you don't have a -colour display). As LEGO imports each module, a line will appear in the -response buffer showing the creation of context marks. Eventually the -command should turn blue, indicating that LEGO has successfully -processed it. Then type (on a separate line if you like) - -@samp{Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);} - -The goal should be echoed in the response buffer. - -@samp{Intros;} - -Whoops! @kbd{C-c C-u} to pretend that didn't happen. - -@samp{intros; andI;} - -A proof summary will appear in the response buffer. We could solve the -goal by pointing now, but we'll stay with the keyboard. - -@samp{Refine H; intros; Immed; Refine H; intros; Immed;} - -finishes the Goal. - -@samp{Save bland_commutes;} - -Moving the mouse pointer over the locked region now reveals that the -entire proof has been aggregated into a single segment. Suppose we -decide to call the goal something more sensible. Moving the cursor up -into the locked region, somewhere between `Goal' and `Save', we enter -@kbd{C-c u}. The segment is transferred back into the editing -region. Now we correct the goal name, move the cursor to the end of the -buffer, and type @kbd{C-c return}. Proof mode queues the commands for -processing and executes them. - -@node LEGO mode, Coq mode, Walkthrough, Top -@unnumberedsec LEGO mode - -LEGO mode is a mode derived from proof mode for editing LEGO scripts. -There are some abbreviations for common commands, which -add text to the buffer: - -@table @kbd -@item C-c i -intros -@item C-c I -Intros -@item C-c R -Refine -@end table - - -@node Coq mode, Known Problems, LEGO mode, Top -@unnumberedsec Coq mode - -Coq mode is a mode derived from proof mode for editing Coq scripts. -As well as custom popup menus, it has the following commands: - -@table @kbd - -@item C-c C-s -search for items in the library of a given type. This runs the -@kbd{Search} command of Coq. - -@end table - -In addition, there are some abbreviations for common commands, which -add text to the buffer: - -@table @kbd -@item C-c I -Intros -@item C-c a -Apply -@end table - -@node Known Problems, Internals, Coq mode, Top -@unnumberedsec Known Problems - -Since Emacs is pretty flexible, there are a whole bunch of things you -can do to confuse script management. When it gets confused, it may -become distressed, and may eventually sulk. In such instances -@code{proof-restart-script-management} may be of use. - -A few things to avoid: - -@itemize @minus -@item If you're using script management with multiple files, don't start -changing the file names. - -@item Script Management doesn't understand how to undo @code{Discharge} -commands in LEGO, and any attempts it makes to do so may leave it in an -inconsistent state. If you're undoing the effects of a @code{Discharge} -command, retract back to the declaration of whatever gets discharged. - -@item Proof by Pointing doesn't work very well, and is inefficiently -implemented. - -@item The locked and queue regions are not quite read-only: in particular -Emacs Undo can insert text into them. - -@item When a LEGO import command fails, the created "Mark" is not -forgotten, and the proof process thinks the file has been included. So -if you assert the command again, it will probably be accepted by LEGO, -because the relevant mark is in the namespace. -@end itemize - -Fixes for some of these may be provided in a future release. - -@node Internals, , Known Problems, Top -@unnumberedsec Internals - -I may one day document the script management internals here. Until then, -UtSL. -@bye diff --git a/span-extent.el b/span-extent.el deleted file mode 100644 index b49670b7..00000000 --- a/span-extent.el +++ /dev/null @@ -1,79 +0,0 @@ -;;; This file implements spans in terms of extents, for xemacs. -;;; Copyright (C) 1998 LFCS Edinburgh -;;; Author: Healfdene Goguen - -;; Maintainer: LEGO Team - -;; $Log$ -;; Revision 2.0 1998/08/11 15:00:13 da -;; New branch -;; -;; Revision 1.4 1998/06/10 14:01:48 hhg -;; Wrote generic span functions for making spans read-only or read-write. -;; -;; Revision 1.3 1998/06/02 15:36:44 hhg -;; Corrected comment about this being for xemacs. -;; -;; Revision 1.2 1998/05/19 15:30:27 hhg -;; Added header and log message. -;; - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Bridging the emacs19/xemacs gulf ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Now define "spans" in terms of extents. - -(defsubst make-span (start end) - (make-extent start end)) - -(defsubst detach-span (span) - (detach-extent span)) - -(defsubst set-span-endpoints (span start end) - (set-extent-endpoints span start end)) - -(defsubst set-span-start (span value) - (set-extent-endpoints span value (extent-end-position span))) - -(defsubst set-span-end (span value) - (set-extent-endpoints span (extent-start-position span) value)) - -(defsubst span-read-only (span) - (set-span-property span 'read-only t)) - -(defsubst span-read-write (span) - (set-span-property span 'read-only nil)) - -(defsubst span-property (span name) - (extent-property span name)) - -(defsubst set-span-property (span name value) - (set-extent-property span name value)) - -(defsubst delete-span (span) - (delete-extent span)) - -(defsubst delete-spans (start end prop) - (mapcar-extents 'delete-extent nil (current-buffer) start end nil prop)) - -(defsubst span-at (pt prop) - (extent-at pt nil prop)) - -(defsubst span-at-before (pt prop) - (extent-at pt nil prop nil 'before)) - -(defsubst span-start (span) - (extent-start-position span)) - -(defsubst span-end (span) - (extent-end-position span)) - -(defsubst prev-span (span prop) - (extent-at (extent-start-position span) nil prop nil 'before)) - -(defsubst next-span (span prop) - (extent-at (extent-end-position span) nil prop nil 'after)) - - -(provide 'span-extent) diff --git a/span-overlay.el b/span-overlay.el deleted file mode 100644 index f74350ed..00000000 --- a/span-overlay.el +++ /dev/null @@ -1,288 +0,0 @@ -;;; This file implements spans in terms of overlays, for emacs19. -;;; Copyright (C) 1998 LFCS Edinburgh -;;; Author: Healfdene Goguen - -;; Maintainer: LEGO Team - -;; $Log$ -;; Revision 2.0 1998/08/11 15:00:13 da -;; New branch -;; -;; Revision 1.9 1998/06/10 14:02:39 hhg -;; Wrote generic span functions for making spans read-only or read-write. -;; Fixed bug in add-span and remove-span concerning return value of -;; span-traverse. -;; -;; Revision 1.8 1998/06/10 12:41:47 hhg -;; Compare span-end first rather than span-start in span-lt, because -;; proof-lock-span is often changed and has starting point 1. -;; Factored out common code of add-span and remove-span into -;; span-traverse. -;; -;; Revision 1.7 1998/06/03 17:40:07 hhg -;; Changed last-span to before-list. -;; Added definitions of foldr and foldl if they aren't already loaded. -;; Changed definitions of add-span, remove-span and find-span-aux to be -;; non-recursive. -;; Removed detach-extent since this file isn't used by xemacs. -;; Added function append-unique to avoid repetitions in list generated by -;; spans-at-region. -;; Changed next-span so it uses member-if. -;; -;; Revision 1.6 1998/06/02 15:36:51 hhg -;; Corrected comment about this being for emacs19. -;; -;; Revision 1.5 1998/05/29 09:50:10 tms -;; o outsourced indentation to proof-indent -;; o support indentation of commands -;; o replaced test of Emacs version with availability test of specific -;; features -;; o C-c C-c, C-c C-v and M-tab is now available in all buffers -;; -;; Revision 1.4 1998/05/21 17:27:41 hhg -;; Removed uninitialized os variable in spans-at-region. -;; -;; Revision 1.3 1998/05/21 08:28:52 hhg -;; Initialize 'before pointer in add-span-aux when last-span is nil. -;; Removed span-at-type. -;; Fixed bug in span-at-before, where (span-start span) may be nil. -;; Added spans-at-(point|region)[-prop], which fixes bug of C-c u at end -;; of buffer. -;; -;; Revision 1.2 1998/05/19 15:31:37 hhg -;; Added header and log message. -;; Fixed set-span-endpoints so it preserves invariant. -;; Changed add-span and remove-span so that they update last-span -;; correctly themselves, and don't take last-span as an argument. -;; - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Bridging the emacs19/xemacs gulf ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; before-list represents a linked list of spans for each buffer. -;; It has the invariants of: -;; * being ordered wrt the starting point of the spans in the list, -;; with detached spans at the end. -;; * not having overlapping overlays of the same type. - -(defvar before-list nil - "Start of backwards-linked list of spans") - -(make-variable-buffer-local 'before-list) - - -(or (fboundp 'foldr) -(defun foldr (func a seq) - "Return (func (func (func (... (func a Sn) ...) S2) S1) S0) -when func's argument is 2 and seq is a sequence whose -elements = S0 S1 S2 ... Sn. [tl-seq.el]" - (let ((i (length seq))) - (while (> i 0) - (setq i (1- i)) - (setq a (funcall func a (elt seq i))) - ) - a))) - -(or (fboundp 'foldl) -(defun foldl (func a seq) - "Return (... (func (func (func a S0) S1) S2) ...) -when func's argument is 2 and seq is a sequence whose -elements = S0 S1 S2 .... [tl-seq.el]" - (let ((len (length seq)) - (i 0)) - (while (< i len) - (setq a (funcall func a (elt seq i))) - (setq i (1+ i)) - ) - a))) - -(defsubst span-start (span) - (overlay-start span)) - -(defsubst span-end (span) - (overlay-end span)) - -(defun set-span-property (span name value) - (overlay-put span name value)) - -(defsubst span-property (span name) - (overlay-get span name)) - -(defun span-read-only-hook (overlay after start end &optional len) - (error "Region is read-only")) - -(defun span-read-only (span) - (set-span-property span 'modification-hooks '(span-read-only-hook)) - (set-span-property span 'insert-in-front-hooks '(span-read-only-hook))) - -(defun span-read-write (span) - (set-span-property span 'modification-hooks nil) - (set-span-property span 'insert-in-front-hooks nil)) - -(defun int-nil-lt (m n) - (cond - ((eq m n) nil) - ((not n) t) - ((not m) nil) - (t (< m n)))) - -;; We use end first because proof-locked-queue is often changed, and -;; its starting point is always 1 -(defun span-lt (s u) - (or (int-nil-lt (span-end s) (span-end u)) - (and (eq (span-end s) (span-end u)) - (int-nil-lt (span-start s) (span-start u))))) - -(defun span-traverse (span prop) - (cond - ((not before-list) - ;; before-list empty - 'empty) - ((funcall prop before-list span) - ;; property holds for before-list and span - 'hd) - (t - ;; traverse before-list for property - (let ((l before-list) (before (span-property before-list 'before))) - (while (and before (not (funcall prop before span))) - (setq l before) - (setq before (span-property before 'before))) - l)))) - -(defun add-span (span) - (let ((ans (span-traverse span 'span-lt))) - (cond - ((eq ans 'empty) - (set-span-property span 'before nil) - (setq before-list span)) - ((eq ans 'hd) - (set-span-property span 'before before-list) - (setq before-list span)) - (t - (set-span-property span 'before - (span-property ans 'before)) - (set-span-property ans 'before span))))) - -(defun make-span (start end) - (add-span (make-overlay start end))) - -(defun remove-span (span) - (let ((ans (span-traverse span 'eq))) - (cond - ((eq ans 'empty) - (error "Bug: empty span list")) - ((eq ans 'hd) - (setq before-list (span-property before-list 'before))) - (ans - (set-span-property ans 'before (span-property span 'before))) - (t (error "Bug: span does not occur in span list"))))) - -;; extent-at gives "smallest" extent at pos -;; we're assuming right now that spans don't overlap -(defun spans-at-point (pt) - (let ((overlays nil) (os nil)) - (setq os (overlays-at pt)) - (while os - (if (not (memq (car os) overlays)) - (setq overlays (cons (car os) overlays))) - (setq os (cdr os))) - overlays)) - -;; assumes that there are no repetitions in l or m -(defun append-unique (l m) - (foldl (lambda (n a) (if (memq a m) n (cons a n))) m l)) - -(defun spans-at-region (start end) - (let ((overlays nil) (pos start)) - (while (< pos end) - (setq overlays (append-unique (spans-at-point pos) overlays)) - (setq pos (next-overlay-change pos))) - overlays)) - -(defun spans-at-point-prop (pt prop) - (let ((f (cond - (prop (lambda (spans span) - (if (span-property span prop) (cons span spans) - spans))) - (t (lambda (spans span) (cons span spans)))))) - (foldl f nil (spans-at-point pt)))) - -(defun spans-at-region-prop (start end prop) - (let ((f (cond - (prop (lambda (spans span) - (if (span-property span prop) (cons span spans) - spans))) - (t (lambda (spans span) (cons span spans)))))) - (foldl f nil (spans-at-region start end)))) - -(defun span-at (pt prop) - (car (spans-at-point-prop pt prop))) - -(defsubst detach-span (span) - (remove-span span) - (delete-overlay span) - (add-span span)) - -(defsubst delete-span (span) - (remove-span span) - (delete-overlay span)) - -;; The next two change ordering of list of spans: -(defsubst set-span-endpoints (span start end) - (remove-span span) - (move-overlay span start end) - (add-span span)) - -(defsubst set-span-start (span value) - (set-span-endpoints span value (span-end span))) - -;; This doesn't affect invariant: -(defsubst set-span-end (span value) - (set-span-endpoints span (span-start span) value)) - -(defsubst delete-spans (start end prop) - (mapcar 'delete-span (spans-at-region-prop start end prop))) - -(defun map-spans-aux (f l) - (cond (l (cons (funcall f l) (map-spans-aux f (span-property l 'before)))) - (t ()))) - -(defsubst map-spans (f) - (map-spans-aux f before-list)) - -(defun find-span-aux (prop-p l) - (while (and l (not (funcall prop-p l))) - (setq l (span-property l 'before))) - l) - -(defun find-span (prop-p) - (find-span-aux prop-p before-list)) - -(defun span-at-before (pt prop) - (let ((prop-pt-p - (cond (prop (lambda (span) - (let ((start (span-start span))) - (and start (> pt start) - (span-property span prop))))) - (t (lambda (span) - (let ((start (span-start span))) - (and start (> pt start)))))))) - (find-span prop-pt-p))) - -(defun prev-span (span prop) - (let ((prev-prop-p - (cond (prop (lambda (span) (span-property span prop))) - (t (lambda (span) t))))) - (find-span-aux prev-prop-p (span-property span 'before)))) - -;; overlays are [start, end) -;; If there are two spans overlapping then this won't work. -(defun next-span (span prop) - (let ((l (member-if (lambda (span) (span-property span prop)) - (overlays-at - (next-overlay-change (overlay-start span)))))) - (if l (car l) nil))) - - -(provide 'span-overlay) -- cgit v1.2.3