lib/scripts/unsymbolize.pl
author paulson
Tue, 28 May 2002 11:06:55 +0200
changeset 13184 197e5a88c9df
parent 10639 f902346264e9
child 14981 e73f8140af78
permissions -rw-r--r--
added <-> and ~
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
13184
197e5a88c9df added <-> and ~
paulson
parents: 10639
diff changeset
    31
    s/\\?\\<longleftrightarrow>/<->/g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    32
    s/\\?\\<longrightarrow>/-->/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    33
    s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    34
    s/\\?\\<rightarrow>/->/g;
13184
197e5a88c9df added <-> and ~
paulson
parents: 10639
diff changeset
    35
    s/\\?\\<not>/~/g;
10071
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    36
    s/\\?\\<epsilon> ?/SOME /g;
10639
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    37
    # outer syntax
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    38
    s/\\?\\<rightleftharpoons>/==/g;
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    39
    s/\\?\\<rightharpoonup>/=>/g;
f902346264e9 harpoons;
wenzelm
parents: 10506
diff changeset
    40
    s/\\?\\<leftharpoondown>/<=/g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    41
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    42
    $result = $_;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    43
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    44
    if ($text ne $result) {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    45
	print STDERR "fixing $file\n";
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    46
        if (! -f "$file~~") {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    47
	    rename $file, "$file~~" || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    48
        }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    49
	open (FILE, "> $file") || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    50
	print FILE $result;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    51
	close FILE || die $!;
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
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    56
## main
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    57
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    58
foreach $file (@ARGV) {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    59
  eval { &unsymbolize($file); };
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    60
  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    61
}