lib/scripts/unsymbolize

cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)

#!/usr/bin/env perl
#
# Author: Markus Wenzel, TU Muenchen
#
# unsymbolize.pl - remove unreadable symbol names from sources
#

use warnings;
use strict;

sub unsymbolize {
    my ($file) = @_;

    open (FILE, $file) || die $!;
    undef $/; my $text = <FILE>; $/ = "\n";         # slurp whole file
    close FILE || die $!;

    $_ = $text;

    # Pure
    s/\\?\\<And>/!!/g;
    s/\\?\\<Colon>/::/g;
    s/\\?\\<Longrightarrow>/==>/g;
    s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
    s/\\?\\<Rightarrow>/=>/g;
    s/\\?\\<equiv>/==/g;
    s/\\?\\<dots>/.../g;
    s/\\?\\<lbrakk> ?/[| /g;
    s/\\?\\ ?<rbrakk>/ |]/g;
    s/\\?\\<lparr> ?/(| /g;
    s/\\?\\ ?<rparr>/ |)/g;
    # HOL
    s/\\?\\<longleftrightarrow>/<->/g;
    s/\\?\\<longrightarrow>/-->/g;
    s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    s/\\?\\<rightarrow>/->/g;
    s/\\?\\<not>/~/g;
    s/\\?\\<notin>/~:/g;
    s/\\?\\<noteq>/~=/g;
    s/\\?\\<some> ?/SOME /g;
    # outer syntax
    s/\\?\\<rightleftharpoons>/==/g;
    s/\\?\\<rightharpoonup>/=>/g;
    s/\\?\\<leftharpoondown>/<=/g;

    my $result = $_;

    if ($text ne $result) {
        print STDERR "fixing $file\n";
        if (! -f "$file~~") {
            rename $file, "$file~~" || die $!;
        }
        open (FILE, "> $file") || die $!;
        print FILE $result;
        close FILE || die $!;
    }
}


## main

foreach my $file (@ARGV) {
  eval { &unsymbolize($file); };
  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
}