10026
|
1 |
#
|
|
2 |
# $Id$
|
|
3 |
# Author: Markus Wenzel, TU Muenchen
|
|
4 |
#
|
|
5 |
# unsymbolize.pl - remove unreadable symbol names from sources
|
|
6 |
#
|
|
7 |
|
|
8 |
sub unsymbolize {
|
|
9 |
my ($file) = @_;
|
|
10 |
|
|
11 |
open (FILE, $file) || die $!;
|
|
12 |
undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
|
|
13 |
close FILE || die $!;
|
|
14 |
|
|
15 |
$_ = $text;
|
|
16 |
|
|
17 |
# Pure
|
|
18 |
s/\\?\\<And>/!!/g;
|
|
19 |
s/\\?\\<Colon>/::/g;
|
|
20 |
s/\\?\\<Longrightarrow>/==>/g;
|
|
21 |
s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
|
|
22 |
s/\\?\\<Rightarrow>/=>/g;
|
|
23 |
s/\\?\\<equiv>/==/g;
|
10506
|
24 |
s/\\?\\<dots>/.../g;
|
10071
|
25 |
s/\\?\\<lbrakk> ?/[| /g;
|
|
26 |
s/\\?\\ ?<rbrakk>/ |]/g;
|
|
27 |
s/\\?\\<lparr> ?/(| /g;
|
|
28 |
s/\\?\\ ?<rparr>/ |)/g;
|
10026
|
29 |
# HOL
|
13184
|
30 |
s/\\?\\<longleftrightarrow>/<->/g;
|
10026
|
31 |
s/\\?\\<longrightarrow>/-->/g;
|
|
32 |
s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
|
|
33 |
s/\\?\\<rightarrow>/->/g;
|
13184
|
34 |
s/\\?\\<not>/~/g;
|
10071
|
35 |
s/\\?\\<epsilon> ?/SOME /g;
|
10639
|
36 |
# outer syntax
|
|
37 |
s/\\?\\<rightleftharpoons>/==/g;
|
|
38 |
s/\\?\\<rightharpoonup>/=>/g;
|
|
39 |
s/\\?\\<leftharpoondown>/<=/g;
|
10026
|
40 |
|
|
41 |
$result = $_;
|
|
42 |
|
|
43 |
if ($text ne $result) {
|
|
44 |
print STDERR "fixing $file\n";
|
|
45 |
if (! -f "$file~~") {
|
|
46 |
rename $file, "$file~~" || die $!;
|
|
47 |
}
|
|
48 |
open (FILE, "> $file") || die $!;
|
|
49 |
print FILE $result;
|
|
50 |
close FILE || die $!;
|
|
51 |
}
|
|
52 |
}
|
|
53 |
|
|
54 |
|
|
55 |
## main
|
|
56 |
|
|
57 |
foreach $file (@ARGV) {
|
|
58 |
eval { &unsymbolize($file); };
|
|
59 |
if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
|
|
60 |
}
|