lib/scripts/unsymbolize.pl
author wenzelm
Tue, 13 Feb 2001 16:31:18 +0100
changeset 11109 ce1cefc6c14c
parent 10639 f902346264e9
child 13184 197e5a88c9df
permissions -rw-r--r--
tuned;
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
# License: GPL (GNU GENERAL PUBLIC LICENSE)
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     5
#
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     6
# unsymbolize.pl - remove unreadable symbol names from sources
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     7
#
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     8
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     9
sub unsymbolize {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    10
    my ($file) = @_;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    11
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    12
    open (FILE, $file) || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    13
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    14
    close FILE || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    15
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    16
    $_ = $text;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    17
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    18
    # Pure
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    19
    s/\\?\\<And>/!!/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    20
    s/\\?\\<Colon>/::/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    21
    s/\\?\\<Longrightarrow>/==>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    22
    s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    23
    s/\\?\\<Rightarrow>/=>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    24
    s/\\?\\<equiv>/==/g;
10506
01333dbe1431 replace \<dots>;
wenzelm
parents: 10071
diff changeset
    25
    s/\\?\\<dots>/.../g;
10071
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    26
    s/\\?\\<lbrakk> ?/[| /g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    27
    s/\\?\\ ?<rbrakk>/ |]/g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    28
    s/\\?\\<lparr> ?/(| /g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    29
    s/\\?\\ ?<rparr>/ |)/g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    30
    # HOL
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;
10071
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    34
    s/\\?\\<epsilon> ?/SOME /g;
10639
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    35
    # outer syntax
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    36
    s/\\?\\<rightleftharpoons>/==/g;
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    37
    s/\\?\\<rightharpoonup>/=>/g;
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    38
    s/\\?\\<leftharpoondown>/<=/g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    39
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    40
    $result = $_;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    41
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    42
    if ($text ne $result) {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    43
	print STDERR "fixing $file\n";
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    44
        if (! -f "$file~~") {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    45
	    rename $file, "$file~~" || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    46
        }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    47
	open (FILE, "> $file") || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    48
	print FILE $result;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    49
	close FILE || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    50
    }
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
## main
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    55
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    56
foreach $file (@ARGV) {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    57
  eval { &unsymbolize($file); };
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    58
  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    59
}