#!/usr/bin/perl
 
# script to convert proof output from RRPC into 
# latex code for a table, modify according to 
# your tastes...

# dan roy, http://web.mit.edu/droy/www

# 1: Get command line values:
if ($#ARGV !=0) {
    die "Usage:  $0 inputfile\n";
}
($infile) = @ARGV;
if (! -r $infile) {
    die "Can't read proof input file $infile\n";
}
if (! -f $infile) {
    die "Input $infile is not a plain file\n";
}

open(INPUT, $infile) ||
    die "Can't open $infile $!";		# Open the file

while (<INPUT>) {
    $t = $_;
    $t =~ s/_/\\_/g; # change _ into \_
    $t =~ s/([AS]\d*):/$1&/g; # first column is A## or S## -

    if ($t =~ m/(Res|Fact|Para)/) {
        # last column is Res/Fact/Para        
        $t =~ s/(Res|Fact|Para)(.*)/&$1$2/g; 
    } else {
        $t =~ s/\n/&\n/g;
    }

    $t =~ s/\n/\\\\\n/g; # add \\ to the end of lines 
    $t =~ s/([{}])/\\$1/g; # escape {'s and }'s 
    $t =~ s/~/\$\\neg\$/g; # change ~ into $\neg$
    $t =~ s/ v / \$\\vee\$ /g; # change or (v) into $\vee$

    print $t;
}

##print "\\\\\n";

close(INPUT);			# Close the file