author  oheimb 
Mon, 30 Apr 2001 13:17:17 +0200  
changeset 11273  673783831234 
parent 11272  165405d911f1 
child 11274  566a70a50956 
permissions  rwrr 
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 

11014  20 
sub subst_RS { 
11131  21 
s/ RS ([\w\'\.]+)/ [THEN $1]/g; 
22 
s/ RS \((.+?)\)/ [THEN $1]/g; 

11271  23 
s/\(([\w\'\.]+ \[THEN [\w\'\.]+\])\)/$1/g; 
11131  24 
s/\] \[THEN /, /g; 
25 
s/THEN sym\b/symmetric/g; 

11014  26 
} 
27 

11131  28 
sub subst_RS_standard { 
11027  29 
my $s = shift; 
30 
$_ = $s; 

11131  31 
s/\s+/ /sg; # remove multiple whitespace 
32 
s/\s/ /sg; # substitute all remaining tabs and newlines by space 

11027  33 
subst_RS(); 
11131  34 
s/\]\s*$/, standard]/g; 
11027  35 
$_; 
36 
} 

37 

11014  38 
sub decl { 
39 
my $s = shift; 

40 
my $a = shift; 

41 
$_ = $s; 

42 
subst_RS(); 

43 
s/, */ [$a] /g; 

44 
s/$/ [$a]/; 

45 
s/\] *\[/, /g; 

46 
"declare $_"; 

47 
} 

48 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

49 
sub process_tac { 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

50 
$prefer = ""; 
10972  51 
my $lead = shift; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

52 
my $t = shift; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

53 
my $simpmodmod = ($t =~ m/auto_tacforce_tacclarsimp_tac/) ? "simp " : ""; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

54 

fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

55 
$_ = $t; 
10972  56 
s/\s+/ /sg; # remove multiple whitespace 
57 
s/\s/ /sg; # substitute all remaining tabs and newlines by space 

58 
s/\( /\(/g; s/ \)/\)/g; # remove leading and trailing space inside parentheses 

59 
s/\[ /\[/g; s/ \]/\]/g; # remove leading and trailing space inside sq brackets 

60 
s/ ?\( ?\)/\(\)/g; # remove space before and inside empty tuples 

61 
s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

62 

11273
673783831234
improve support for EVERY', added support for EVERY
oheimb
parents:
11272
diff
changeset

63 
s/EVERY *\[(.*?)\]/$1/; 
673783831234
improve support for EVERY', added support for EVERY
oheimb
parents:
11272
diff
changeset

64 
if(s/EVERY\'\[(.*?)\] *(\d+)/$1 $2/) { 
11271  65 
$goal = $2; 
66 
s/,/ $goal,/g; 

67 
} 

10972  68 
s/Blast_tac 1/blast/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

69 
s/^Blast_tac (\d+)/{$prefer="prefer $1 "; "blast"}/e; 
10972  70 
s/Fast_tac 1/fast/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

71 
s/^Fast_tac (\d+)/{$prefer="prefer $1 "; "fast"}/e; 
10972  72 
s/Slow_tac 1/slow/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

73 
s/^Slow_tac (\d+)/{$prefer="prefer $1 "; "slow"}/e; 
10972  74 
s/Best_tac 1/best/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

75 
s/^Best_tac (\d+)/{$prefer="prefer $1 "; "best"}/e; 
10972  76 
s/Safe_tac/safe/g; 
77 
s/Clarify_tac 1/clarify/g; 

78 

79 
s/blast_tac \(claset\(\) (.*?)\) 1/blast $1/g; 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

80 
s/^blast_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "blast $1"}/e; 
10972  81 
s/fast_tac \(claset\(\) (.*?)\) 1/fast $1/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

82 
s/^fast_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "fast $1"}/e; 
10972  83 
s/slow_tac \(claset\(\) (.*?)\) 1/slow $1/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

84 
s/^slow_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "slow $1"}/e; 
10972  85 
s/best_tac \(claset\(\) (.*?)\) 1/best $1/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

86 
s/^best_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "best $1"}/e; 
10972  87 
s/safe_tac \(claset\(\) (.*?)\)/safe $1/g; 
88 
s/clarify_tac \(claset\(\) (.*?)\) 1/clarify $1/g; 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

89 

fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

90 
s/Auto_tac/auto/g; 
10972  91 
s/Force_tac 1/force/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

92 
s/^Force_tac (\d+)/{$prefer="prefer $1 "; "force"}/e; 
10972  93 
s/Clarsimp_tac 1/clarsimp/g; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

94 

10972  95 
s/auto_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\)/auto $1 $2/g; 
96 
s/force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) 1/force $1 $2/g; 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

97 
s/^force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e; 
10972  98 
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

99 

10972  100 
s/Asm_full_simp_tac 1/simp/g; 
101 
s/Full_simp_tac 1/simp (no_asm_use)/g; 

102 
s/Asm_simp_tac 1/simp (no_asm_simp)/g; 

103 
s/Simp_tac 1/simp (no_asm)/g; 

104 
s/ALLGOALS Asm_full_simp_tac/simp_all/g; 

11029  105 
s/ALLGOALS Full_simp_tac/simp_all (no_asm_use)/g; 
106 
s/ALLGOALS Asm_simp_tac/simp_all (no_asm_simp)/g; 

10972  107 
s/ALLGOALS Simp_tac/simp_all (no_asm)/g; 
108 

109 
s/asm_full_simp_tac \(simpset\(\) (.*?)\) 1/simp $1/g; 

110 
s/full_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_use) $1/g; 

111 
s/asm_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_simp) $1/g; 

112 
s/simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm) $1/g; 

113 
s/ALLGOALS \(asm_full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all $1/g; 

114 
s/ALLGOALS \(full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_use) $1/g; 

115 
s/ALLGOALS \(asm_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_simp) $1/g; 

116 
s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g; 

117 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

118 
s/a(ssume_)?tac 1/assumption/g; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

119 
s/^a(ssume_)?tac (\d+)/{$prefer="prefer $2 "; "assumption"}/e; 
11068  120 
s/\bmp_tac 1/erule (1) notE impE/g; 
121 
s/\bmp_tac (\d+)/erule_tac [$1] notE impE, tactic \"assume_tac $1\"/g; 

11013  122 

10972  123 
s/hypsubst_tac 1/hypsubst/g; 
124 
s/arith_tac 1/arith/g; 

125 
s/strip_tac 1/intro strip/g; 

126 
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

127 

11263
e502756bcb11
added parentheses for 'b y' syntax, added primitive smp_tac support
oheimb
parents:
11198
diff
changeset

128 
s/smp_tac (\d+) (\d+)/tactic "smp_tac $1 $2"/g; 
11009  129 
s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g; 
11068  130 
s/rotate_tac ~ *(\d+) (\d+)/rotate_tac [$2] $1/g; 
11013  131 
s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g; 
132 
s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g; 

133 
s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g; 

11029  134 
s/induct_thm_tac ([\w\'\. \[,\]]+?) (\".*?\") (\d+)/induct_tac [$3] $2 rule: $1/g; 
11013  135 
s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g; 
136 
s/thin_tac (\".*?\") *(\d+)/erule_tac [$2] V = $1 in thin_rl/g; 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

137 

10972  138 
s/THEN /, /g; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

139 
s/ORELSE//g; 
11014  140 
subst_RS(); 
10972  141 

11068  142 
s/\(\"(.*?)\" *, *(\".*?\")\) *, */$1 = $2 and /g; # instantiations 
143 
s/\(\"(.*?)\" *, *(\".*?\")\)/$1 = $2/g; # last instantiation 

144 

11013  145 
s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g; 
146 
s/stac ([\w\'\. \[,\]]+?) 1/subst $1/g; 

147 
s/rtac ([\w\'\. \[,\]]+?) 1/rule $1/g; 

148 
s/rtac ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$2] $1/g; 

11068  149 
s/res_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$3] $1 in $2/g; 
11013  150 
s/dtac ([\w\'\. \[,\]]+?) 1/drule $1/g; 
151 
s/dtac ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$2] $1/g; 

11068  152 
s/dres_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$3] $1 in $2/g; 
11013  153 
s/datac ([\w\'\. \[,\]]+?) (\d+) 1/drule ($2) $1/g; 
154 
s/etac ([\w\'\. \[,\]]+?) 1/erule $1/g; 

155 
s/etac ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$2] $1/g; 

11068  156 
s/eres_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$3] $1 in $2/g; 
11013  157 
s/eatac ([\w\'\. \[,\]]+?) (\d+) 1/erule ($2) $1/g; 
158 
s/forward_tac \[([\w\'\. \[,\]]+)\] 1/frule $1/g; 

159 
s/forward_tac \[([\w\'\. \[,\]]+)\] (\d+)/frule_tac [$2] $1/g; 

160 
s/ftac ([\w\'\. \[,\]]+?) 1/frule $1/g; 

161 
s/ftac ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$2] $1/g; 

11068  162 
s/forw_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$3] $1 in $2/g; 
11013  163 
s/fatac ([\w\'\. \[,\]]+?) (\d+) 1/frule ($2) $1/g; 
164 

165 

166 
s/fold_goals_tac *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"fold ".thmlist($1)/eg; 

167 
s/rewrite_goals_tac *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"unfold ".thmlist($1)/eg; 

11068  168 
s/cut_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/cut_tac [$3] $1 in $2/g; 
169 
s/cut_facts_tac *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+) (\d+)/"cut_tac [$2] ".thmlist($1)/eg; 

11013  170 
s/resolve_tac *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+) 1/"rule ".thmlist($1)/eg; 
171 

172 
s/addIs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"intro: ".thmlist($1)/eg; 

173 
s/addSIs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"intro!: ".thmlist($1)/eg; 

174 
s/addEs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"elim: ".thmlist($1)/eg; 

175 
s/addSEs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"elim!: ".thmlist($1)/eg; 

176 
s/addDs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"dest: ".thmlist($1)/eg; 

177 
s/addSDs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"dest!: ".thmlist($1)/eg; 

178 
s/delrules *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"del: ".thmlist($1)/eg; 

179 
s/addsimps *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"$simpmodmod"."add: ".thmlist($1)/eg; 

180 
s/delsimps *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"$simpmodmod"."del: ".thmlist($1)/eg; 

181 
s/addcongs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"cong add: ".thmlist($1)/eg; 

182 
s/delcongs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"cong del: ".thmlist($1)/eg; 

183 
s/addsplits *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"split add: ".thmlist($1)/eg; 

184 
s/delsplits *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"split del: ".thmlist($1)/eg; 

185 

11068  186 
s/_tac \[1\]/_tac/g; 
11013  187 
s/ +/ /g; # remove multiple whitespace 
10972  188 
s/\( /\(/; s/ \)/\)/g; # remove leading and trailing space inside parentheses 
11013  189 
s/^ *(.*?) *$/$1/s; # remove enclosing whitespace 
10972  190 
s/^([azAZ])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

191 
$prefer."apply".$lead.$_; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

192 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

193 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

194 
sub lemmaname { 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

195 
$lemmanames[++$lemmacount] = "??unknown??"; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

196 
"@@" . $lemmacount . "@@"; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

197 
} 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

198 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

199 
sub backpatch_lemmanames { 
10972  200 
if($currfile ne "") { 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

201 
select(STDOUT); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

202 
close(ARGVOUT); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

203 
open(TMPW, '>'.$finalfile); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

204 
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

205 
while(<TMPR>) { 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

206 
s/@@(\d+)@@/$lemmanames[$1]/eg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

207 
print TMPW; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

208 
} 
11068  209 
system("mv $currfile $currfile~0~") if($currfile ne $default); 
10972  210 
system("rm $tmpfile"); 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

211 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

212 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

213 

fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

214 
sub done { 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

215 
my $name = shift; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

216 
my $attr = shift; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

217 
$lemmanames[$lemmacount] = $name.$attr; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

218 
"done"; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

219 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

220 

11013  221 
$currfile = ""; 
11068  222 
$default = "convert_default_stdout"; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

223 
while (<>) { # main loop 
10972  224 
if ($ARGV ne $currfile) { 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

225 
$x=$_; backpatch_lemmanames; $_=$x; 
11068  226 
$currfile = ($ARGV eq "" ? $default : $ARGV); 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

227 
$lemmacount=0; 
10972  228 
$finalfile = "$currfile.thy"; 
229 
$tmpfile = "$finalfile.~0~"; 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

230 
open(ARGVOUT, '>'.$tmpfile); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

231 
select(ARGVOUT); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

232 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

233 

fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

234 
nl: 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

235 
if(!s/;(\s*?(\n?$\(\*))/$1/s && !eof()) {# no end_of_ML_command marker 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

236 
$_ = $_ . <>; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

237 
goto nl; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

238 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

239 
s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

240 
nlc: 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

241 
m/^(\s*)(.*?)(\s*)$/s; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

242 
$head=$1; $line=$2; $tail=$3; 
10972  243 
$tail =~ s/\s+\n/\n/sg; # remove trailing whitespace at end of lines 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

244 
print $head; $_=$line.$tail; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

245 
if ($line =~ m/^\(\*/) { # start comment 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

246 
while (($i = index $_,"*)") == 1 && !eof()) { # no end comment 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

247 
print; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

248 
$_ = <>; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

249 
} 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

250 
if ($i == 1) { print; last; } 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

251 
print substr $_,0,$i+2; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

252 
$_ = substr $_,$i+2; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

253 
goto nlc; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

254 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

255 
$_=$line; 
11272  256 
if(!($head =~ m/^\n/)) { $head = "\n$head"; } 
11013  257 
s/^Goalw *(\[[\w\'\.\s,]*\][\w\'\. \[,\]]+) *(.+)/ 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

258 
"lemma ".lemmaname().": $2$head"."apply (unfold ".thmlist($1).")"/se; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

259 
s/^Goal *(.+)/"lemma ".lemmaname().": $1"/se; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

260 
s/\bgoal/"(*".lemmaname()."*)goal"/se; # ugly oldstyle goals 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

261 
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

262 
s/^qed *\"(.*?)\"/done($1,"")/se; 
11068  263 
s/^val *(\w+) *= *result *\( *\) *$/done($1,"")/se; 
264 
s/^bind_thm *\( *\"(.*?)\" *, *(result *\( *\) *?) *\) *$/done($1,"")/se; 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

265 
s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se; 
11131  266 
s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_standard($2)/se; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

267 
s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/process_tac($1,$2).$3/se; 
11263
e502756bcb11
added parentheses for 'b y' syntax, added primitive smp_tac support
oheimb
parents:
11198
diff
changeset

268 
s/^b\s+y(\s*)(.*?)(\s*)$/process_tac($1,"(".$2.")").$3/se; 
11013  269 
s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/; 
270 
# remove outermost parentheses if around atoms 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

271 
s/^Addsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

272 
s/^Delsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp del")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

273 
s/^Addsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

274 
s/^Delsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split del")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

275 
s/^AddIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

276 
s/^AddSIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro!")/seg; 
11114  277 
s/^AddXIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro?")/seg; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

278 
s/^AddEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

279 
s/^AddSEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim!")/seg; 
11114  280 
s/^AddXEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim?")/seg; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

281 
s/^AddDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

282 
s/^AddSDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest!")/seg; 
11114  283 
s/^AddXDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest?")/seg; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

284 
s/^AddIffs\s*\[?\s*([\w\'\. ,]*)\s*\]?</decl($1,"iff")/seg; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

285 
print "$_$tail"; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

286 
if(eof()) { last; } # prevents reading finally from stdin (thru <>)! 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

287 
} 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

288 
backpatch_lemmanames; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

289 
select(STDOUT); 