#!/usr/local/bin/perl -w
use strict "subs";

# version 1.1, 20040914

$otter = "otter";
$warning0 = "% automatically generated by raft from ";
$warning1 = "\n% DO NOT EDIT!\n\n";
$stderrsuffix = "err";

$status{127} = "program not found";
$status{101} = "input error";
$status{102} = "abnormal end";
$status{103} = "proved";
$status{104} = "sos empty";
$status{105} = "max given";
$status{106} = "max seconds";
$status{107} = "max generated";
$status{108} = "max kept";
$status{109} = "max memory";
$status{110} = "malloc null";
$status{111} = "interactive";
$status{112} = "segmentation fault";
$status{113} = "usr1";
$status{114} = "possible model";
$status{115} = "max levels";

sub add0
{
  $lemma = $head;
  if ($option)
  {
    $lemma =~ s/\s*$//;
  }
  else
  {
    $lemma =~ s/\.?\s*$//; # you can have a period, but it's not needed
  }
  $lemma =~ s/(\s*\@(\w+))*\s*//;
  $lemma =~ s/\@\@/\@/g;
  $lemma =~ s/^ +//mg if $option;
  die "no label: $head" if !($head =~ s/\s*\@(\w+)//);
  $name = $label = $1;
  die "label not unique: $label" if defined($count{$label});
  $count{$label} = 1;
  $label{$label} = 1;
  $formula{"$label\@0"} = $lemma;
}

sub add1
{
  $head = $head . "\@ALL " if !$option;
  while ($head =~ s/\s*\@(\w+)//)
  {
    $label = $1;
    die "label reused: $label"
      if (defined($label{$label}));
    $count = defined($count{$label}) ? $count{$label} : 0;
    $formula{"$label\@$count"} = $lemma;
    $count{$label} = $count + 1;
  }
}

sub expand
{
  die "unknown label: $label" if !defined($count{$label});
  for $i (0 .. ($count{$label} - 1))
  {
    $line = $_;
    $formula = $formula{"$label\@$i"};
    $line =~ s/\@$label/$formula/;
    $line =~ s/\@\@/\@/g;
    $body = $body . $line;
  }
}

$prefix = "";
$state = "";
$head = $body = $name = $lemma = "";
while (<>)
{
  s/\s*\%.*// if $state ne "PROOF";
  $key = "";
  $rest = $_;
  $key = $1 if $rest =~ s/^\s*(\w+)\s*\.?\s*//;
  if ($state eq "")
  {
    next if /^\s+$/;
    if ($key eq "AXIOM" || $key eq "LEMMA" || $key eq "OPTION")
    {
      $option = $key eq "OPTION";
      $state = $key;
      $head = $rest;
      next;
    }
    elsif ($key eq "DIRECTORY")
    {
      $prefix = $rest;
      chop($prefix);
      $prefix =~ s/\s*(.+)\s*/$1/;
      $prefix =~ s/\"(.*)\"/$1/;
      $prefix = $prefix."/" if $prefix ne "";
      next;
    }
    elsif ($key eq "PROVER")
    {
      $otter = $rest;
      chop($otter);
      $otter =~ s/\s*(.+)\s*/$1/;
      $otter =~ s/\"(.*)\"/$1/;
      next;
    }
    die "unknown item: $_";
  }
  elsif ($state eq "AXIOM" || $state eq "OPTION")
  {
    if ($key eq "MOIXA" || $key eq "NOITPO")
    {
      die "trailing garbage: $_" if $rest ne "";
      add0;
      add1;
      $state = "";
      $head = $body = $name = $lemma = "";
      next;
    }
    $head = $head . $_;
  }
  elsif ($state eq "LEMMA")
  {
    if ($key eq "PROOF")
    {
      add0;
      $state = $key;
      $current = $ARGV;
      $body = "$warning0$current$warning1$rest";
      next;
    }
    $head = $head . $_;
  }
  elsif ($state eq "PROOF")
  {
    if ($key eq "USEALL")
    {
      die "trailing garbage: $_" if $rest ne "";
      $body = $body . "\nformula_list(usable).\n";
      $_ = "\@ALL.\n";
      $label = "ALL";
      expand;
      $body = $body . "end_of_list.\n";
      next;
    }
    elsif ($key eq "FOORP" || $key eq "QED")
    {
      die "trailing garbage: $_" if $rest ne "";
      $body = $body . "\nformula_list(sos).\n-($lemma).\nend_of_list.\n"
        if $key eq "QED";
      $| = 1;
      print "$name: ";
      $replace = 1;
      if (open(IN,"<$prefix$name.in"))
      {
        $slash = $/;
	undef $/;
	$oldbody = <IN>;
	close(IN);
	$/ = $slash;
	$replace = $body ne $oldbody;
      }
      if ($replace)
      {
        if ($ARGV ne "-")
	{
	  $intime = (stat("$prefix$name.in"))[9];
	  if (-e _)
	  {
	    $rafttime = (stat($ARGV))[9];
	    die ("\n  $prefix$name.in is newer than $ARGV, did you edit it?".
	         "\n  I don't dare to replace it...".
		 "\n  touch $ARGV and rerun to continue\n")
	      if (-e _ && $intime > $rafttime)
          }
        }
        open(IN,">$prefix$name.in") or die "can't write $prefix$name.in";
        print IN $body;
	close(IN);
      }
      $run = 1;
      $intime = (stat("$prefix$name.in"))[9];
      $outtime = (stat("$prefix$name.out"))[9];
      if (-e _ && $intime <= $outtime)
      {
	$errtime = (stat("$prefix$name.$stderrsuffix"))[9];
	if (-e _ && $intime <= $errtime)
	{
	  $statustime = (stat("$prefix$name.log"))[9];
	  if (-e _ && $intime <= $statustime)
	  {
	    $run = 0;
	  }
        }
      }
      if (!$run && open(STATUS,"<$prefix$name.log"))
      {
	$status = <STATUS>;
	$status =~ s/^$name: //;
	chop($status);
	close(STATUS);
      }
      else
      {
        $run = 1;
      }
      if ($run)
      {
        $exitstatus =
	  (system ("$otter < $prefix$name.in > $prefix$name.out ".
	    "2> $prefix$name.$stderrsuffix"))
	  >> 8;
        $status = defined($status{$exitstatus}) ? $status{$exitstatus} :
	  "unknown status: $exitstatus";
	print $status;
        open(STATUS,">$prefix$name.log") or die "can't write $prefix$name.log";
	print STATUS "$name: $status\n";
	close(STATUS);
      }
      else
      {
        print "$status (cached)";
      }
      print "\n";
      add1;
      $state = "";
      $head = $body = $name = $lemma = "";
      next;
    }
    s/^[ \t]+//;
    if (/^[^%@]*\@(\w+)/)
    {
      $label = $1;
      expand;
    }
    else
    {
      s/\@\@/\@/g;
      $body = $body . $_;
    }
  }
  else
  {
    die "unknown state: $state";
  }
}