author  wenzelm 
Sat, 24 Nov 2001 16:54:32 +0100  
changeset 12282  f98beaaa7c4f 
parent 11329  ad8061b2da6c 
child 13076  70704dd48bd5 
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; 
11274  24 
s/\] \[THEN /, THEN /g; 
11131  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 

11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

61 
s/([^ ])\(/$1 \(/g; # possibly add space before opening parentheses 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

62 
s/\)([^ ])/\) $1/g; # possibly add space after closing parentheses 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

63 

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

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

68 
} 

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

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

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

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

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

79 

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

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

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

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

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

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

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

90 

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

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

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

95 

11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

96 
s/auto_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\)/auto $1 $2/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

97 
s/force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) 1/force $1 $2/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

98 
s/^force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

99 
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

100 

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

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

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

105 
s/ALLGOALS Asm_full_simp_tac/simp_all/g; 

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

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

11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

110 
s/asm_full_simp_tac \(simpset \(\) (.*?)\) 1/simp $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

111 
s/full_simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm_use) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

112 
s/asm_simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm_simp) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

113 
s/simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

114 
s/ALLGOALS \(asm_full_simp_tac \(simpset \(\) (.*?)\) \)/simp_all $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

115 
s/ALLGOALS \(full_simp_tac \(simpset \(\) (.*?)\) \)/simp_all (no_asm_use) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

116 
s/ALLGOALS \(asm_simp_tac \(simpset \(\) (.*?)\) \)/simp_all (no_asm_simp) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

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

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

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

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

11013  123 

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

126 
s/strip_tac 1/intro strip/g; 

127 
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

128 

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

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

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

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

138 

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

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

11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

166 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

186 

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

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

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

194 

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

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

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

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

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

199 

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

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

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

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

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

205 
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

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

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

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

209 
} 
11068  210 
system("mv $currfile $currfile~0~") if($currfile ne $default); 
10972  211 
system("rm $tmpfile"); 
10939
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 

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

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

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

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

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

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

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

221 

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

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

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

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

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

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

232 
select(ARGVOUT); 
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 

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

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

236 
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

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

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

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

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

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

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

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

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

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

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

248 
print; 
10939
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 
} 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

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

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

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

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

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

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

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

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

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

262 
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

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

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

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

268 
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

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

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

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

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

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

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

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

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

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

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

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

283 
s/^AddSDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest!")/seg; 
11114  284 
s/^AddXDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest?")/seg; 
11286  285 
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

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

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

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

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

290 
select(STDOUT); 