author  wenzelm 
Tue, 13 Feb 2001 16:31:18 +0100  
changeset 11109  ce1cefc6c14c 
parent 11081  ce9a6746cd1e 
child 11114  a0c3f2082c88 
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 { 
21 
s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g; 

22 
s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g; 

23 
s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4\]/g; 

24 
s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4\]/g; 

25 
s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3\]/g; 

26 
s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3\]/g; 

27 
s/\(([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2\]/g; 

28 
s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g; 

11068  29 
s/THEN sym\b/symmetric$1/g; 
11014  30 
} 
31 

11027  32 
sub subst_RS_fun { 
33 
my $s = shift; 

34 
$_ = $s; 

35 
subst_RS(); 

36 
$_; 

37 
} 

38 

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

41 
my $a = shift; 

42 
$_ = $s; 

43 
subst_RS(); 

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

45 
s/$/ [$a]/; 

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

47 
"declare $_"; 

48 
} 

49 

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

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

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

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

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

55 

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

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

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

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

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

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

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

63 

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

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

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

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

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

74 

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

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

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

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

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

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

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

85 

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

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

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

90 

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

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

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

95 

10972  96 
s/Asm_full_simp_tac 1/simp/g; 
97 
s/Full_simp_tac 1/simp (no_asm_use)/g; 

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

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

100 
s/ALLGOALS Asm_full_simp_tac/simp_all/g; 

11029  101 
s/ALLGOALS Full_simp_tac/simp_all (no_asm_use)/g; 
102 
s/ALLGOALS Asm_simp_tac/simp_all (no_asm_simp)/g; 

10972  103 
s/ALLGOALS Simp_tac/simp_all (no_asm)/g; 
104 

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

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

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

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

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

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

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

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

113 

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

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

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

11013  118 

10972  119 
s/hypsubst_tac 1/hypsubst/g; 
120 
s/arith_tac 1/arith/g; 

121 
s/strip_tac 1/intro strip/g; 

122 
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

123 

11009  124 
s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g; 
11068  125 
s/rotate_tac ~ *(\d+) (\d+)/rotate_tac [$2] $1/g; 
11013  126 
s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g; 
127 
s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g; 

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

11029  129 
s/induct_thm_tac ([\w\'\. \[,\]]+?) (\".*?\") (\d+)/induct_tac [$3] $2 rule: $1/g; 
11013  130 
s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g; 
131 
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

132 

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

134 
s/ORELSE//g; 
11014  135 
subst_RS(); 
10972  136 

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

139 

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

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

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

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

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

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

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

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

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

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

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

160 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

180 

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

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

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

188 

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

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

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

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

192 
} 
10939
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 backpatch_lemmanames { 
10972  195 
if($currfile ne "") { 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

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

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

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

199 
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

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

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

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

203 
} 
11068  204 
system("mv $currfile $currfile~0~") if($currfile ne $default); 
10972  205 
system("rm $tmpfile"); 
10939
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 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

208 

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

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

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

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

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

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

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

215 

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

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

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

222 
$lemmacount=0; 
10972  223 
$finalfile = "$currfile.thy"; 
224 
$tmpfile = "$finalfile.~0~"; 

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

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

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

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

228 

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

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

230 
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

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

232 
goto nl; 
10939
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 
s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

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

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

237 
$head=$1; $line=$2; $tail=$3; 
10972  238 
$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

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

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

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

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

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

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

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

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

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

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

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

250 
$_=$line; 
11013  251 
s/^Goalw *(\[[\w\'\.\s,]*\][\w\'\. \[,\]]+) *(.+)/ 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

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

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

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

255 
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

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

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

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

261 
s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/process_tac($1,$2).$3/se; 
11013  262 
s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/; 
263 
# remove outermost parentheses if around atoms 

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

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

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

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

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

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

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

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

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

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

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

274 
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

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

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

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

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

279 
select(STDOUT); 