#!/usr/bin/perl
#
# Idea: suck up latex file and look for the speical macro for
# proofnets.  Generate an input file for proofnetinator (the ML program) 
# generate the nets, and modify the latex file to point to them.
#

# define a bunch of globals
# these will be set by 
$infile = "DEADBEEF";       # input file: tex with proof net macros
$pn_specfile = "DEADBEEF";  # will write this file and feed it proofnetinator
$pn_prefix = "DEADBEEF";    # the files that proofnetinator/mpost generate will start with this
$tempfile = "DEADBEEF";     # write the modified version of infile here
$header = "";               # preamble for the geberated .mp file 
$footer = "";               # postamble for the geberated .mp file 
$quiet = "";             # supress some messages
$undo_mode = "";         # undo the usual operation of the program
$howmany = 0;               # how many proofnets are in this thing.

# set up the globals above based on the command line
process_args();
($pn_specfile, $pn_prefix, $tempfile) = setupfilenames($infile);


# Don't need to do much in undo mode
if ($undo_mode) {
  unprocess_infile();
  exit 0;
}


# OK were are really making proof nets
process_infile();

if($howmany == 0) {
  print "No proofnets found in file $infile... cleaning up..." unless $quiet;
  system "rm $tempfile $pn_specfile";
  print "exiting\n" unless $quiet;
  exit;
}

print "Found $howmany proofnets... invoking the proofnetinator\n" unless $quiet;
write_mp_file ($header,$footer);
print "Wrote $pn_prefix.mp..." unless $quiet;

print "Invoking METAPOST...\n" unless $quiet;
my $mpostretval = system "mpost $pn_prefix.mp"; 
if( $mpostretval != 0 ) { # if mpost failed
  print "METAPOST failed ... is \$TEX set to something sane\?\nGiving up!\n";
  exit $mpostretval;
}

print "cleaning up... " unless $quiet;
tidyfiles();
print "done\n" unless $quiet;

### MAIN PROG ENDS HERE ###--------------------------------------------


# The next too routines do the main work

#------------------#------------------#------------------#------------------
# writeout a modified version of the infile to tempfile
# and write the proofnet specification file
sub process_infile {

  open LATEXFILE, $infile or die "Can't open $infile";
  open TMPFILE, ">$tempfile" or die "Can't write to $tmpfile";
  open SPECFILE, ">$pn_specfile" or die "Can't write to $pn_specfile";

  while(<LATEXFILE>) {
    if(/^\\proofnet\{(.*)\}\{(.*)\}$/) {
      print "Found proofnet of $1\n" unless $quiet;
      print TMPFILE "\% PROOFNETIFY at work here\n";
      print TMPFILE "\%\\commentproofnet\{$1\}\{$2\}\n";
      $howmany++;
      print SPECFILE "$1 \t $2\n";
      print TMPFILE "\\includegraphics\{$pn_prefix$howmany.mps\}\n";
      print TMPFILE "\% PROOFNETIFY done -- remember to remove the \"comment\" above\n";
    }
    else {
      print TMPFILE $_;
    }
  }
  close LATEXFILE;
  close TMPFILE;
  close SPECFILE;
}




#------------------#------------------#------------------#------------------
# take a tex file which has already gone through proofnetify
# and reverse the process
sub unprocess_infile {

  print "Operating in undo mode: $infile will be reverted..." unless $quiet;

  open LATEXFILE, $infile or die "Can't open $infile\n";
  open TMPFILE, ">$tempfile" or die "Can't write to $tempfile\n";

  my $edit_here = 0;
 LINE: while(<LATEXFILE>) {
    if ( /^\% PROOFNETIFY at work here/ )  { $edit_here = 1; next LINE; }
    if ( /^\% PROOFNETIFY done/ )          { $edit_here = 0, next LINE; }
    if($edit_here) {
      s/^\%\\commentproofnet/\\proofnet/ && do {print TMPFILE $_; next LINE; };
      if ( /^\\includegraphics/ )          { next LINE; }
     }
    print TMPFILE $_;
  }
  close LATEXFILE;
  close TMPFILE;
  system "mv $tempfile $infile" and die "Can't update $infile\n";
  print "done!\n" unless $quiet;
  # remember systems returns 0 == false for sucess
}



#------------------#------------------#------------------#------------------
# move things about -- the only crucial part is the for loop
sub tidyfiles {
  system "mv $tempfile $infile";
  my $i;
  foreach $i (1 .. $howmany) {
    system "mv $pn_prefix.$i $pn_prefix$i.mps";
  }
  system "rm $pn_specfile";
}

#------------------#------------------#------------------#------------------

sub write_mp_file {
  my ($preamble, $postamble) = @_;

  # generate the header for the .mp file
  if ($preamble && -r $preamble) {
    system "cp $preamble $pn_prefix.mp" and die "can't write $pn_prefix.mp";
    # remember systems returns 0 == false for sucess
  }
  else {
    if ($preamble) {
      print "WARNING: couldn't read requested header file $preamble; using default.\n";
    }
    open MPFILE, ">$pn_prefix.mp" or die "can't write $pn_prefix.mp";
    print MPFILE <<'EOHEADER';
verbatimtex 
	    \documentclass{article}
	    \usepackage{linlog}
	    \begin{document}
etex

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

EOHEADER
    close MPFILE;
  }

  # invoke the proofnetinator
  my $success = system "proofnetinator < $pn_specfile >> $pn_prefix.mp";
  if ($success != 0 ) {
    print "Proofnetinator couldn't process proof net spec!\nCheck syntax of $pn_specfile\nCleaning up...";
    system "rm $pn_prefix";
    print "done.\n";
  }
  # now write the postamble
  if($postamble && -r $postamble) {
    system "cat $postamble >> $pn_prefix.mp";
  }
  else {
    if ($postamble) {
      print "WARNING: couldn't read requested footer file $postamble; using default.\n";
    }
    open MPFILE, ">>$pn_prefix.mp" or die "can't write $pn_prefix.mp";
    print MPFILE <<'EOFOOTER';

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

verbatimtex
	\end{document}
etex
end
EOFOOTER

  close MPFILE;
  }
  return true;
}


#------------------#------------------#------------------#------------------
# returns a list of filenames
# INPUT: the name of the input file
# OUTPUT:
# ( proofnet spec file,
#   stem for mp input files
#   tempfile name )
#
sub setupfilenames {
  my $stem = shift;
  $stem =~  s/\.\w*$//;
  my @suffixes = ("_pn.in", "_pn", "_proofnetify_tempfile");
  return map { $stem . $_} @suffixes;
}

#------------------#------------------#------------------#------------------

sub process_args {

  # iterate over options
 ARG: while (@ARGV > 1) {
    $_  = shift (@ARGV);
    /^\-q$/       and $quiet = true, next ARG;
    /^\-v$/       and $quiet = "", next ARG;
    /^\-u$/       and $undo_mode = true, next ARG;
    /^\-h$/       and $header = shift @ARGV, next ARG;
    /^\-f$/       and $footer = shift @ARGV, next ARG;
    print "ERROR: unrecognised option $_\n";
    usage_and_die();
  }

  # on loop exit we should have one arg left --  the input file
  if( @ARGV != 1) {
    usage_and_die();
  }
  $infile = shift @ARGV;
  return;
}


#------------------#------------------#------------------#------------------

sub usage_and_die  {
  print <<USAGE;
Usage: proofnetify \[options\] file.tex
      -f file  : footer for metapost file
      -h file  : header for metapost file
      -q       : quiet mode
      -u       : undo mode
      -v       : verbose mode
USAGE
  exit -1;
}