author | oheimb |
Wed, 24 Jan 2001 17:53:01 +0100 | |
changeset 10972 | af160f8d3bd7 |
parent 10939 | fe14e54594a3 |
child 11000 | 498d0db8cd8a |
permissions | -rw-r--r-- |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
1 |
# |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
2 |
# $Id$ |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
3 |
# Author: David von Oheimb, TU Muenchen |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
4 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
5 |
# |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
6 |
# convert.pl - convert legacy tactic scripts to Isabelle/Isar tactic |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
7 |
# emulation using heuristics - leaves unrecognized patterns unchanged |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
8 |
# produces from each input file (on the command line) a new file with |
10972 | 9 |
# ".thy" appended and renames the original input file by appending "~0~" |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
10 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
11 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
12 |
sub thmlist { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
13 |
my $s = shift; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
14 |
$s =~ s/^\[(.*)\]$/$1/sg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
15 |
$s =~ s/, +/ /g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
16 |
$s =~ s/,/ /g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
17 |
$s; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
18 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
19 |
|
10972 | 20 |
sub mult_assumption { |
21 |
my $n = shift; |
|
22 |
my $r = ""; |
|
23 |
for($i=0; $i<$n; $i++) { $r = $r.", assumption"; } |
|
24 |
$r; |
|
25 |
} |
|
26 |
||
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
27 |
sub process_tac { |
10972 | 28 |
my $lead = shift; |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
29 |
my $t = shift; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
30 |
my $simpmodmod = ($t =~ m/auto_tac|force_tac|clarsimp_tac/) ? "simp " : ""; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
31 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
32 |
$_ = $t; |
10972 | 33 |
s/\s+/ /sg; # remove multiple whitespace |
34 |
s/\s/ /sg; # substitute all remaining tabs and newlines by space |
|
35 |
s/\( /\(/g; s/ \)/\)/g; # remove leading and trailing space inside parentheses |
|
36 |
s/\[ /\[/g; s/ \]/\]/g; # remove leading and trailing space inside sq brackets |
|
37 |
s/ ?\( ?\)/\(\)/g; # remove space before and inside empty tuples |
|
38 |
s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
39 |
|
10972 | 40 |
s/Blast_tac 1/blast/g; |
41 |
s/Fast_tac 1/fast/g; |
|
42 |
s/Slow_tac 1/slow/g; |
|
43 |
s/Best_tac 1/best/g; |
|
44 |
s/Safe_tac/safe/g; |
|
45 |
s/Clarify_tac 1/clarify/g; |
|
46 |
||
47 |
s/blast_tac \(claset\(\) (.*?)\) 1/blast $1/g; |
|
48 |
s/fast_tac \(claset\(\) (.*?)\) 1/fast $1/g; |
|
49 |
s/slow_tac \(claset\(\) (.*?)\) 1/slow $1/g; |
|
50 |
s/best_tac \(claset\(\) (.*?)\) 1/best $1/g; |
|
51 |
s/safe_tac \(claset\(\) (.*?)\)/safe $1/g; |
|
52 |
s/clarify_tac \(claset\(\) (.*?)\) 1/clarify $1/g; |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
53 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
54 |
s/Auto_tac/auto/g; |
10972 | 55 |
s/Force_tac 1/force/g; |
56 |
s/Clarsimp_tac 1/clarsimp/g; |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
57 |
|
10972 | 58 |
s/auto_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\)/auto $1 $2/g; |
59 |
s/force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) 1/force $1 $2/g; |
|
60 |
s/clarsimp_tac \(claset\(*\) (.*?), *simpset\(\) (.*?)\) 1/clarsimp $1 $2/g; |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
61 |
|
10972 | 62 |
s/Asm_full_simp_tac 1/simp/g; |
63 |
s/Full_simp_tac 1/simp (no_asm_use)/g; |
|
64 |
s/Asm_simp_tac 1/simp (no_asm_simp)/g; |
|
65 |
s/Simp_tac 1/simp (no_asm)/g; |
|
66 |
s/ALLGOALS Asm_full_simp_tac/simp_all/g; |
|
67 |
s/ALLGOALS Full_simp_tac 1/simp_all (no_asm_use)/g; |
|
68 |
s/ALLGOALS Asm_simp_tac 1/simp_all (no_asm_simp)/g; |
|
69 |
s/ALLGOALS Simp_tac/simp_all (no_asm)/g; |
|
70 |
||
71 |
s/asm_full_simp_tac \(simpset\(\) (.*?)\) 1/simp $1/g; |
|
72 |
s/full_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_use) $1/g; |
|
73 |
s/asm_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_simp) $1/g; |
|
74 |
s/simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm) $1/g; |
|
75 |
s/ALLGOALS \(asm_full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all $1/g; |
|
76 |
s/ALLGOALS \(full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_use) $1/g; |
|
77 |
s/ALLGOALS \(asm_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_simp) $1/g; |
|
78 |
s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g; |
|
79 |
||
80 |
s/atac 1/assumption/g; |
|
81 |
s/hypsubst_tac 1/hypsubst/g; |
|
82 |
s/arith_tac 1/arith/g; |
|
83 |
s/strip_tac 1/intro strip/g; |
|
84 |
s/split_all_tac 1/simp (no_asm_simp) only: split_tupled_all/g; |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
85 |
|
10972 | 86 |
s/rotate_tac ([~\d]+) 1/rotate_tac $1/g; |
87 |
s/rotate_tac ([~\d]+) (\d+)/rotate_tac [$2] $1/g; |
|
88 |
s/rename_tac *(\".*?\") *1/rename_tac $1/g; |
|
89 |
s/rename_tac *(\".*?\") *(\d+)/rename_tac [$2] $1/g; |
|
90 |
s/case_tac *(\".*?\") *1/case_tac $1/g; |
|
91 |
s/case_tac *(\".*?\") *(\d+)/case_tac [$2] $1/g; |
|
92 |
s/induct_tac *(\".*?\") *1/induct_tac $1/g; |
|
93 |
s/induct_tac *(\".*?\") *(\d+)/induct_tac [$2] $1/g; |
|
94 |
s/subgoal_tac *(\".*?\") *1/subgoal_tac $1/g; |
|
95 |
s/subgoal_tac *(\".*?\") *(\d+)/subgoal_tac [$2] $1/g; |
|
96 |
s/thin_tac *(\".*?\") *1/erule_tac P = $1 thin_rl/g; |
|
97 |
s/thin_tac *(\".*?\") *(\d+)/erule_tac [$2] P = $1/g; |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
98 |
|
10972 | 99 |
s/stac ([\w\.]+) 1/subst $1/g; |
100 |
s/rtac ([\w\.]+) 1/rule $1/g; |
|
101 |
s/rtac ([\w\.]+) (\d+)/rule_tac [$2] $1/g; |
|
102 |
s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/rule_tac $1 = $2 $3/g; |
|
103 |
s/ratac ([\w\.]+) (\d+) 1/"rule $1".mult_assumption($2)/eg; |
|
104 |
s/dtac ([\w\.]+) 1/drule $1/g; |
|
105 |
s/dtac ([\w\.]+) (\d+)/drule_tac [$2] $1/g; |
|
106 |
s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/drule_tac $1 = $2 $3/g; |
|
107 |
s/datac ([\w\.]+) (\d+) 1/"drule $1".mult_assumption($2)/eg; |
|
108 |
s/etac ([\w\.]+) 1/erule $1/g; |
|
109 |
s/etac ([\w\.]+) (\d+)/erule_tac [$2] $1/g; |
|
110 |
s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/erule_tac $1 = $2 $3/g; |
|
111 |
s/eatac ([\w\.]+) (\d+) 1/"erule $1".mult_assumption($2)/eg; |
|
112 |
s/forward_tac \[([\w\.]+)\] 1/frule $1/g; |
|
113 |
s/ftac ([\w\.]+) 1/frule $1/g; |
|
114 |
s/ftac ([\w\.]+) (\d+)/frule_tac [$2] $1/g; |
|
115 |
s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/frule_tac $1 = $2 $3/g; |
|
116 |
s/fatac ([\w\.]+) (\d+) 1/"frule $1".mult_assumption($2)/eg; |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
117 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
118 |
|
10972 | 119 |
s/THEN /, /g; |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
120 |
s/ORELSE/|/g; |
10972 | 121 |
s/fold_goals_tac *(\[[\w\. ,]*\]|[\w\.]+)/"fold ".thmlist($1)/eg; |
122 |
s/rewrite_goals_tac *(\[[\w\. ,]*\]|[\w\.]+)/"unfold ".thmlist($1)/eg; |
|
123 |
s/cut_facts_tac *(\[[\w\. ,]*\]|[\w\.]+) 1/"cut_tac ".thmlist($1)/eg; |
|
124 |
s/resolve_tac *(\[[\w\. ,]*\]|[\w\.]+) 1/"rule ".thmlist($1)/eg; |
|
125 |
s/EVERY *(\[[\w\. ,]*\]|[\w\.]+)/thmlist($1)/eg; |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
126 |
|
10972 | 127 |
s/addIs *(\[[\w\. ,]*\]|[\w\.]+)/"intro: ".thmlist($1)/eg; |
128 |
s/addSIs *(\[[\w\. ,]*\]|[\w\.]+)/"intro!: ".thmlist($1)/eg; |
|
129 |
s/addEs *(\[[\w\. ,]*\]|[\w\.]+)/"elim: ".thmlist($1)/eg; |
|
130 |
s/addSEs *(\[[\w\. ,]*\]|[\w\.]+)/"elim!: ".thmlist($1)/eg; |
|
131 |
s/addDs *(\[[\w\. ,]*\]|[\w\.]+)/"dest: ".thmlist($1)/eg; |
|
132 |
s/addSDs *(\[[\w\. ,]*\]|[\w\.]+)/"dest!: ".thmlist($1)/eg; |
|
133 |
s/delrules *(\[[\w\. ,]*\]|[\w\.]+)/"del: ".thmlist($1)/eg; |
|
134 |
s/addsimps *(\[[\w\. ,]*\]|[\w\.]+)/"$simpmodmod"."add: ".thmlist($1)/eg; |
|
135 |
s/delsimps *(\[[\w\. ,]*\]|[\w\.]+)/"$simpmodmod"."del: ".thmlist($1)/eg; |
|
136 |
s/addcongs *(\[[\w\. ,]*\]|[\w\.]+)/"cong add: ".thmlist($1)/eg; |
|
137 |
s/delcongs *(\[[\w\. ,]*\]|[\w\.]+)/"cong del: ".thmlist($1)/eg; |
|
138 |
s/addsplits *(\[[\w\. ,]*\]|[\w\.]+)/"split add: ".thmlist($1)/eg; |
|
139 |
s/delsplits *(\[[\w\. ,]*\]|[\w\.]+)/"split del: ".thmlist($1)/eg; |
|
140 |
||
141 |
s/([\w\.]+) RS ([\w\.]+)/$1 \[THEN $2\]/g; |
|
142 |
||
143 |
s/ +/ /g; # remove multiple whitespace |
|
144 |
s/\( /\(/; s/ \)/\)/g; # remove leading and trailing space inside parentheses |
|
145 |
s/^ *(.*?) *$/$1/s; # remove enclosing whitespace |
|
146 |
s/^\( *([\w\.]+) *\)$/$1/; # remove outermost parentheses if around atoms |
|
147 |
s/^([a-zA-Z])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
148 |
$_; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
149 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
150 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
151 |
sub thmname { "@@" . ++$thmcount . "@@"; } |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
152 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
153 |
sub backpatch_thmnames { |
10972 | 154 |
if($currfile ne "") { |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
155 |
select(STDOUT); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
156 |
close(ARGVOUT); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
157 |
open(TMPW, '>'.$finalfile); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
158 |
open TMPR,$tmpfile or die "Can't find tmp file $tmp: $!\n"; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
159 |
while(<TMPR>) { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
160 |
s/@@(\d+)@@/$thmnames[$1]/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
161 |
print TMPW $_; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
162 |
} |
10972 | 163 |
system("mv $currfile $currfile.~0~"); |
164 |
system("rm $tmpfile"); |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
165 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
166 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
167 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
168 |
sub done { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
169 |
my $name = shift; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
170 |
my $attr = shift; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
171 |
$thmnames[$thmcount] = $name.$attr; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
172 |
"done"; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
173 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
174 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
175 |
$next = "nonempty"; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
176 |
while (<>) { # main loop |
10972 | 177 |
if ($ARGV ne $currfile) { |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
178 |
$x=$_; backpatch_thmnames; $_=$x; |
10972 | 179 |
$currfile = $ARGV; |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
180 |
$thmcount=0; |
10972 | 181 |
$finalfile = "$currfile.thy"; |
182 |
$tmpfile = "$finalfile.~0~"; |
|
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
183 |
open(ARGVOUT, '>'.$tmpfile); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
184 |
select(ARGVOUT); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
185 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
186 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
187 |
nl: |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
188 |
if(!(s/;\s*?(\n?)$/$1/s)) {# no end_of_ML_command marker |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
189 |
$next = <>; $_ = $_ . $next; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
190 |
if($next) { goto nl; } |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
191 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
192 |
s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
193 |
nlc: |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
194 |
m/^(\s*)(.*?)(\s*)$/s; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
195 |
$head=$1; $line=$2; $tail=$3; |
10972 | 196 |
$tail =~ s/\s+\n/\n/sg; # remove trailing whitespace at end of lines |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
197 |
print $head; $_=$2.$tail; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
198 |
if ($line =~ m/^\(\*/) { # start comment |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
199 |
while (($i = index $_,"*)") == -1) { # no end comment |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
200 |
print $_; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
201 |
$_ = <>; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
202 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
203 |
print substr $_,0,$i+2; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
204 |
$_ = substr $_,$i+2; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
205 |
goto nlc; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
206 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
207 |
$_=$line; |
10972 | 208 |
s/^Goalw *(\[[\w\.\s,]*\]|[\w\.]+) *(.+)/ |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
209 |
"lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
210 |
s/^Goal *(.+)/"lemma ".thmname().": $1"/se; |
10972 | 211 |
s/ goal/"(*".thmname()."*) goal"/se; # ugly old-style goals |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
212 |
s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
213 |
s/^qed *\"(.*?)\"/done($1,"")/se; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
214 |
s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se; |
10972 | 215 |
s/^by(\s*\(?\s*)(.*?)$/"apply$1".process_tac($1,$2)/se; |
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
216 |
print "$_$tail"; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
217 |
if(!$next) { last; } # prevents reading finally from stdin (thru <>)! |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
218 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
219 |
backpatch_thmnames; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
220 |
select(STDOUT); |