author | wenzelm |
Wed, 26 Aug 1998 16:33:29 +0200 | |
changeset 5374 | 6ef3742b6153 |
parent 0 | a5a9c433f639 |
permissions | -rw-r--r-- |
clasohm@0 | 1 |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
clasohm@0 | 2 |
;; special function for Isabelle |
clasohm@0 | 3 |
;; |
clasohm@0 | 4 |
;; |
clasohm@0 | 5 |
; goalify.el |
clasohm@0 | 6 |
; |
clasohm@0 | 7 |
; Emacs command to change "goal" proofs to "prove_goal" proofs |
clasohm@0 | 8 |
; and reverse IN A REGION. |
clasohm@0 | 9 |
; [would be difficult in "sed" since replacements involve multiple lines] |
clasohm@0 | 10 |
; |
clasohm@0 | 11 |
;; origin is prove_goalify.el |
clasohm@0 | 12 |
;; enhanced by Franz Regensburger |
clasohm@0 | 13 |
;; corrected some errors in regular expressions |
clasohm@0 | 14 |
;; changed name prove_goalify --> goalify |
clasohm@0 | 15 |
;; added inverse functions ungoalify |
clasohm@0 | 16 |
; |
clasohm@0 | 17 |
; function goalify: |
clasohm@0 | 18 |
; |
clasohm@0 | 19 |
; val PAT = goalARGS;$ |
clasohm@0 | 20 |
; COMMANDS;$ |
clasohm@0 | 21 |
; val ID = result(); |
clasohm@0 | 22 |
; |
clasohm@0 | 23 |
; to |
clasohm@0 | 24 |
; |
clasohm@0 | 25 |
; val ID = prove_goalARGS |
clasohm@0 | 26 |
; (fn PAT=> |
clasohm@0 | 27 |
; [ |
clasohm@0 | 28 |
; COMMANDS |
clasohm@0 | 29 |
; ]); |
clasohm@0 | 30 |
;; |
clasohm@0 | 31 |
;; Note: PAT must be an identifier. _ as pattern is not supported. |
clasohm@0 | 32 |
;; |
clasohm@0 | 33 |
; function ungoalify: |
clasohm@0 | 34 |
; |
clasohm@0 | 35 |
; val ID = prove_goalARGS |
clasohm@0 | 36 |
; (fn PAT=> |
clasohm@0 | 37 |
; [ |
clasohm@0 | 38 |
; COMMANDS |
clasohm@0 | 39 |
; ]); |
clasohm@0 | 40 |
; |
clasohm@0 | 41 |
; |
clasohm@0 | 42 |
; to |
clasohm@0 | 43 |
; val PAT = goalARGS;$ |
clasohm@0 | 44 |
; COMMANDS;$ |
clasohm@0 | 45 |
; val ID = result(); |
clasohm@0 | 46 |
; |
clasohm@0 | 47 |
|
clasohm@0 | 48 |
|
clasohm@0 | 49 |
(defun ungoalify (alpha omega) |
clasohm@0 | 50 |
"Change well-formed prove_goal proofs to goal...result" |
clasohm@0 | 51 |
(interactive "r" |
clasohm@0 | 52 |
"*") |
clasohm@0 | 53 |
; 0: restrict editing to region |
clasohm@0 | 54 |
(narrow-to-region alpha omega) |
clasohm@0 | 55 |
|
clasohm@0 | 56 |
; 1: insert delimiter ID |
clasohm@0 | 57 |
(goto-char (point-min)) |
clasohm@0 | 58 |
(replace-regexp |
clasohm@0 | 59 |
"[ \t]*val[ \t]+\\([^ \t\n=]+\\)[ \t\n=]+prove_goal" "\\1") |
clasohm@0 | 60 |
|
clasohm@0 | 61 |
; 2: insertt delimiter ARGS PAT and before first command |
clasohm@0 | 62 |
(goto-char (point-min)) |
clasohm@0 | 63 |
(replace-regexp |
clasohm@0 | 64 |
"[ \n\t]*(fn[ \t]+\\([^=]+\\)=>[^(]*" "\\1\n") |
clasohm@0 | 65 |
|
clasohm@0 | 66 |
; 3: shift over all commands |
clasohm@0 | 67 |
; Note: only one line per command |
clasohm@0 | 68 |
(goto-char (point-max)) |
clasohm@0 | 69 |
(while (not (equal (point) (point-min))) |
clasohm@0 | 70 |
(goto-char (point-min)) |
clasohm@0 | 71 |
(replace-regexp |
clasohm@0 | 72 |
"[ \t]*\\(.*\\),[ \t]*\n" "by \\1;\n")) |
clasohm@0 | 73 |
|
clasohm@0 | 74 |
; 4: fix last |
clasohm@0 | 75 |
(goto-char (point-min)) |
clasohm@0 | 76 |
(replace-regexp |
clasohm@0 | 77 |
"[ \t]*\\(.*\\)[ \t\n]*\][ \t\n]*)[ \t\n]*;" "by \\1;") |
clasohm@0 | 78 |
|
clasohm@0 | 79 |
; 5: arange new val Pat = goal .. |
clasohm@0 | 80 |
(goto-char (point-min)) |
clasohm@0 | 81 |
(replace-regexp |
clasohm@0 | 82 |
"\\([^]*\\)\\([^]*\\)\\([^]*\\)\n\\([^]*\\)" |
clasohm@0 | 83 |
"val \\3= goal\\2;\n\\4\nval \\1 = result();") |
clasohm@0 | 84 |
|
clasohm@0 | 85 |
; widen again |
clasohm@0 | 86 |
(widen) |
clasohm@0 | 87 |
) |
clasohm@0 | 88 |
|
clasohm@0 | 89 |
|
clasohm@0 | 90 |
(defun goalify (alpha omega) |
clasohm@0 | 91 |
"Change well-formed goal...result proofs to use prove_goal" |
clasohm@0 | 92 |
(interactive "r" |
clasohm@0 | 93 |
"*") |
clasohm@0 | 94 |
|
clasohm@0 | 95 |
; 0: restrict editing to region |
clasohm@0 | 96 |
(narrow-to-region alpha omega) |
clasohm@0 | 97 |
|
clasohm@0 | 98 |
; 1: delimit the identifier in "val ID = result()" using ^Q |
clasohm@0 | 99 |
(goto-char (point-min)) |
clasohm@0 | 100 |
(replace-regexp "val[ \t\n]+\\([^ \t\n=]+\\)[ \t\n=]+result();[ \t]*$" |
clasohm@0 | 101 |
"\\1") |
clasohm@0 | 102 |
|
clasohm@0 | 103 |
; 2: replace terminal \"; by |
clasohm@0 | 104 |
(goto-char (point-min)) |
clasohm@0 | 105 |
(replace-regexp "\";[ \t]*$" "") |
clasohm@0 | 106 |
|
clasohm@0 | 107 |
; 3: replace lines "by ...;" with "...," |
clasohm@0 | 108 |
(goto-char (point-min)) |
clasohm@0 | 109 |
(replace-regexp "by[ \n\t]*\\([^;]*\\)[ \t\n]*;" "\t\\1,") |
clasohm@0 | 110 |
|
clasohm@0 | 111 |
; 4: removing the extra commas, those followed by ^Q |
clasohm@0 | 112 |
(goto-char (point-min)) |
clasohm@0 | 113 |
(replace-regexp ",[ \n\t]*" "") |
clasohm@0 | 114 |
|
clasohm@0 | 115 |
; 5: transforming goal... to prove_goal... |
clasohm@0 | 116 |
(goto-char (point-min)) |
clasohm@0 | 117 |
(replace-regexp |
clasohm@0 | 118 |
"val[ \t\n]+\\([^ \n\t=]+\\)[ \t\n=]+goal\\([^]*\\) |
clasohm@0 | 119 |
\\([^]*\\)\\([^]*\\)" |
clasohm@0 | 120 |
"val \\4 = prove_goal\\2\"\n (fn \\1 =>\n\t[\n\\3\n\t]);") |
clasohm@0 | 121 |
|
clasohm@0 | 122 |
; 6: widen again |
clasohm@0 | 123 |
(widen) |
clasohm@0 | 124 |
) |
clasohm@0 | 125 |