|
1 # |
|
2 # $Id$ |
|
3 # |
|
4 # expandshort.pl - expand shorthand goal commands |
|
5 # |
|
6 |
|
7 sub expandshort { |
|
8 my ($file) = @_; |
|
9 |
|
10 open (FILE, $file) || die $!; |
|
11 undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file |
|
12 close FILE || die $!; |
|
13 |
|
14 $_ = $text; |
|
15 |
|
16 s/\bsafe_tac *\(claset *\( *\) *\)/Safe_tac/sg; |
|
17 s/ *\(Safe_tac\) *([0-9]+)/ Safe_tac \1/sg; |
|
18 s/ *\(Safe_tac\)/ Safe_tac/sg; |
|
19 s/\bby\(/by (/sg; |
|
20 s/\bba\b *(\d+);/by (assume_tac \1);/sg; |
|
21 s/\bbr\b *([^;]*) (\d+);/by (rtac \1 \2);/sg; |
|
22 s/\bbrs\b *([^;]*) (\d+);/by (resolve_tac \1 \2);/sg; |
|
23 s/\bbd\b *([^;]*) (\d+);/by (dtac \1 \2);/sg; |
|
24 s/\bbds\b *([^;]*) (\d+);/by (dresolve_tac \1 \2);/sg; |
|
25 s/\bbe\b *([^;]*) (\d+);/by (etac \1 \2);/sg; |
|
26 s/\bbes\b *([^;]*) (\d+);/by (eresolve_tac \1 \2);/sg; |
|
27 s/\bbw\b *([^;]*);/by (rewtac \1);/sg; |
|
28 s/\bbws\b *([^;]*);/by (rewrite_goals_tac \1);/sg; |
|
29 s/\bauto *\(\)/by (Auto_tac())/sg; |
|
30 s/dresolve_tac *\[(\w+)\] */dtac \1 /sg; |
|
31 s/eresolve_tac *\[(\w+)\] */etac \1 /sg; |
|
32 s/resolve_tac *\[(\w+)\] */rtac \1 /sg; |
|
33 s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac \1\2/sg; |
|
34 s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac \1 /sg; |
|
35 |
|
36 $result = $_; |
|
37 |
|
38 if ($text ne $result) { |
|
39 print STDERR "expanding $file\n"; |
|
40 if (! -f "$file~~") { |
|
41 rename $file, "$file~~" || die $!; |
|
42 } |
|
43 open (FILE, "> $file") || die $!; |
|
44 print FILE $result; |
|
45 close FILE || die $!; |
|
46 } |
|
47 } |
|
48 |
|
49 |
|
50 ## main |
|
51 |
|
52 foreach $file (@ARGV) { |
|
53 eval { &expandshort($file); }; |
|
54 if ($@) { print STDERR "*** expandshort $file: ", $@, "\n"; } |
|
55 } |