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