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