lib/scripts/unsymbolize.pl
author wenzelm
Wed, 14 May 2008 11:05:10 +0200
changeset 26882 9e824d8f4512
parent 14981 e73f8140af78
child 27220 31adee1f467a
permissions -rw-r--r--
renamed Position.path to Path.position; added line_file, ignore empty name;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     1
#
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     2
# $Id$
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     4
#
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     5
# unsymbolize.pl - remove unreadable symbol names from sources
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     6
#
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     7
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     8
sub unsymbolize {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     9
    my ($file) = @_;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    10
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    11
    open (FILE, $file) || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    12
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    13
    close FILE || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    14
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    15
    $_ = $text;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    16
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    17
    # Pure
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    18
    s/\\?\\<And>/!!/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    19
    s/\\?\\<Colon>/::/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    20
    s/\\?\\<Longrightarrow>/==>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    21
    s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    22
    s/\\?\\<Rightarrow>/=>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    23
    s/\\?\\<equiv>/==/g;
10506
01333dbe1431 replace \<dots>;
wenzelm
parents: 10071
diff changeset
    24
    s/\\?\\<dots>/.../g;
10071
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    25
    s/\\?\\<lbrakk> ?/[| /g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    26
    s/\\?\\ ?<rbrakk>/ |]/g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    27
    s/\\?\\<lparr> ?/(| /g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    28
    s/\\?\\ ?<rparr>/ |)/g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    29
    # HOL
13184
197e5a88c9df added <-> and ~
paulson
parents: 10639
diff changeset
    30
    s/\\?\\<longleftrightarrow>/<->/g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    31
    s/\\?\\<longrightarrow>/-->/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    32
    s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    33
    s/\\?\\<rightarrow>/->/g;
13184
197e5a88c9df added <-> and ~
paulson
parents: 10639
diff changeset
    34
    s/\\?\\<not>/~/g;
10071
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    35
    s/\\?\\<epsilon> ?/SOME /g;
10639
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    36
    # outer syntax
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    37
    s/\\?\\<rightleftharpoons>/==/g;
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    38
    s/\\?\\<rightharpoonup>/=>/g;
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    39
    s/\\?\\<leftharpoondown>/<=/g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    40
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    41
    $result = $_;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    42
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    43
    if ($text ne $result) {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    44
	print STDERR "fixing $file\n";
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    45
        if (! -f "$file~~") {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    46
	    rename $file, "$file~~" || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    47
        }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    48
	open (FILE, "> $file") || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    49
	print FILE $result;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    50
	close FILE || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    51
    }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    52
}
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    53
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    54
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    55
## main
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    56
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    57
foreach $file (@ARGV) {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    58
  eval { &unsymbolize($file); };
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    59
  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    60
}