lib/scripts/unsymbolize.pl
author nipkow
Wed Aug 26 19:54:19 2009 +0200 (2009-08-26)
changeset 32416 4ea7648b6ae2
parent 29145 b1c6f4563df7
permissions -rw-r--r--
merged
     1 #
     2 # Author: Markus Wenzel, TU Muenchen
     3 #
     4 # unsymbolize.pl - remove unreadable symbol names from sources
     5 #
     6 
     7 sub unsymbolize {
     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     # Pure
    17     s/\\?\\<And>/!!/g;
    18     s/\\?\\<Colon>/::/g;
    19     s/\\?\\<Longrightarrow>/==>/g;
    20     s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
    21     s/\\?\\<Rightarrow>/=>/g;
    22     s/\\?\\<equiv>/==/g;
    23     s/\\?\\<dots>/.../g;
    24     s/\\?\\<lbrakk> ?/[| /g;
    25     s/\\?\\ ?<rbrakk>/ |]/g;
    26     s/\\?\\<lparr> ?/(| /g;
    27     s/\\?\\ ?<rparr>/ |)/g;
    28     # HOL
    29     s/\\?\\<longleftrightarrow>/<->/g;
    30     s/\\?\\<longrightarrow>/-->/g;
    31     s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    32     s/\\?\\<rightarrow>/->/g;
    33     s/\\?\\<not>/~/g;
    34     s/\\?\\<notin>/~:/g;
    35     s/\\?\\<noteq>/~=/g;
    36     s/\\?\\<some> ?/SOME /g;
    37     # outer syntax
    38     s/\\?\\<rightleftharpoons>/==/g;
    39     s/\\?\\<rightharpoonup>/=>/g;
    40     s/\\?\\<leftharpoondown>/<=/g;
    41 
    42     $result = $_;
    43 
    44     if ($text ne $result) {
    45 	print STDERR "fixing $file\n";
    46         if (! -f "$file~~") {
    47 	    rename $file, "$file~~" || die $!;
    48         }
    49 	open (FILE, "> $file") || die $!;
    50 	print FILE $result;
    51 	close FILE || die $!;
    52     }
    53 }
    54 
    55 
    56 ## main
    57 
    58 foreach $file (@ARGV) {
    59   eval { &unsymbolize($file); };
    60   if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
    61 }