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