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