lib/scripts/unsymbolize
author wenzelm
Thu May 20 20:20:52 2010 +0200 (2010-05-20)
changeset 37012 106c56e916f8
parent 35022 c844b93dd147
child 41457 3bb2f035203f
permissions -rwxr-xr-x
enable shell script editor mode;
wenzelm@35022
     1
#!/usr/bin/env perl
wenzelm@10026
     2
#
wenzelm@10026
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@10026
     4
#
wenzelm@10026
     5
# unsymbolize.pl - remove unreadable symbol names from sources
wenzelm@10026
     6
#
wenzelm@10026
     7
wenzelm@35022
     8
use warnings;
wenzelm@35022
     9
use strict;
wenzelm@35022
    10
wenzelm@10026
    11
sub unsymbolize {
wenzelm@10026
    12
    my ($file) = @_;
wenzelm@10026
    13
wenzelm@10026
    14
    open (FILE, $file) || die $!;
wenzelm@35022
    15
    undef $/; my $text = <FILE>; $/ = "\n";         # slurp whole file
wenzelm@10026
    16
    close FILE || die $!;
wenzelm@10026
    17
wenzelm@10026
    18
    $_ = $text;
wenzelm@10026
    19
wenzelm@10026
    20
    # Pure
wenzelm@10026
    21
    s/\\?\\<And>/!!/g;
wenzelm@10026
    22
    s/\\?\\<Colon>/::/g;
wenzelm@10026
    23
    s/\\?\\<Longrightarrow>/==>/g;
wenzelm@10026
    24
    s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
wenzelm@10026
    25
    s/\\?\\<Rightarrow>/=>/g;
wenzelm@10026
    26
    s/\\?\\<equiv>/==/g;
wenzelm@10506
    27
    s/\\?\\<dots>/.../g;
wenzelm@10071
    28
    s/\\?\\<lbrakk> ?/[| /g;
wenzelm@10071
    29
    s/\\?\\ ?<rbrakk>/ |]/g;
wenzelm@10071
    30
    s/\\?\\<lparr> ?/(| /g;
wenzelm@10071
    31
    s/\\?\\ ?<rparr>/ |)/g;
wenzelm@10026
    32
    # HOL
paulson@13184
    33
    s/\\?\\<longleftrightarrow>/<->/g;
wenzelm@10026
    34
    s/\\?\\<longrightarrow>/-->/g;
wenzelm@10026
    35
    s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
wenzelm@10026
    36
    s/\\?\\<rightarrow>/->/g;
paulson@13184
    37
    s/\\?\\<not>/~/g;
wenzelm@27220
    38
    s/\\?\\<notin>/~:/g;
wenzelm@27220
    39
    s/\\?\\<noteq>/~=/g;
wenzelm@27220
    40
    s/\\?\\<some> ?/SOME /g;
wenzelm@10639
    41
    # outer syntax
wenzelm@10639
    42
    s/\\?\\<rightleftharpoons>/==/g;
wenzelm@10639
    43
    s/\\?\\<rightharpoonup>/=>/g;
wenzelm@10639
    44
    s/\\?\\<leftharpoondown>/<=/g;
wenzelm@10026
    45
wenzelm@35022
    46
    my $result = $_;
wenzelm@10026
    47
wenzelm@10026
    48
    if ($text ne $result) {
wenzelm@10026
    49
	print STDERR "fixing $file\n";
wenzelm@10026
    50
        if (! -f "$file~~") {
wenzelm@10026
    51
	    rename $file, "$file~~" || die $!;
wenzelm@10026
    52
        }
wenzelm@10026
    53
	open (FILE, "> $file") || die $!;
wenzelm@10026
    54
	print FILE $result;
wenzelm@10026
    55
	close FILE || die $!;
wenzelm@10026
    56
    }
wenzelm@10026
    57
}
wenzelm@10026
    58
wenzelm@10026
    59
wenzelm@10026
    60
## main
wenzelm@10026
    61
wenzelm@35022
    62
foreach my $file (@ARGV) {
wenzelm@10026
    63
  eval { &unsymbolize($file); };
wenzelm@10026
    64
  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
wenzelm@10026
    65
}