logic.perl:


#!/usr/bin/perl -T -w
# © Copyright 2001 John Halleck
# All rights reserved.

require 5.003; # or later.
               # Oddly enough, I don't remember what 5.003 features
               # were needed beyond just 5.000;
=head1 NAME

  John Halleck's Logic Calculator

=head1 AUTHOR

  John Halleck
  P.O. Box 58488 
  Salt Lake City, Utah, 84158-0488

  John.Halleck@utah.edu

=head1 SYNOPSIS

  Deal with producing Axiom based proofs on the web.

=head1 DESCRIPTION

  This program assists in producing proofs from an axiom system,
  by doing the grunt work of substitutions, Modus Ponens, etc..  There are
  several notations and axiom basees to chose from.

=head1 DOCUMENTATION

  http://www.cc.utah.edu/~nahaj/logic/calculate/

=head1 SOURCES

  http://www.cc.utah.edu/~nahaj/logic/calculate/

=head1 DESIGN NOTES

  This program was designed to get by on the meager ration of cputime that a
  web cgi program gets here.  This means that it can't do massive searches or
  checks.  It has to arrange for the computation to be spread out over several
  requests.  
  For example, this means that we ask notation and choice of system on separate
  pages, so that the processing involved can be done as two (relativly) small
  chunks instead of one big one.

=cut

use strict;  # Let us hold distributed code to higher standards.

# use integer; # We have no need of floating point here.
  # *** Good idea, *BUT* the ctime (amount of time used) call returns floating
  # point... And for testing I'm using ctime.
  # *** I need to uncomment this (and the ctime code, of course) for the
  # production version.

use Carp; # Lets get a chance to see where this happened.

# =============================================================================
# ====================== WEB LOGIC FRAME ======================================
# =================== ( And configuration ) ===================================

# Configuration.

use vars qw(
    $programlibraries $prefix
    $programtitle $programversion $programdate $programname $copyright
    $myaddress $myname
    $mytemp $systems
    $pagebase $pagebasehttp
    $systemsdir $notationsdir $symbolsurl
    $refererlog
    $goodpath
    $doingdebug
);

# ---  Derive:
$programname     = ($0 =~ m;(^|/)([^/]+)$;)[1] ;
$prefix =  $programname =~ m/^test/ ? 'test' : '';
$doingdebug = $prefix ne '';

# --- program information.

$myname         = 'John Halleck';
$myaddress      = 'John.Halleck@utah.edu';
$programtitle   = "$myname\'s Logic Calculator";
$programversion = '0.02_06';
$programdate    = 'April 16th, 2001';
$copyright      = "© Copyright 2001 by $myname, All Rights Reserved";


# --- Basic HTML configuration 

$pagebase     = 'http://www.cc.utah.edu/~nahaj/';
$pagebasehttp = "http://<a href=\"http://www.cc.utah.edu/\">www.cc.utah.edu"
              . "</a>/~<a href=\"$pagebase\">nahaj</a>/";
$refererlog   = '/home/nahaj/public_html/cgi-bin/ref.log';
              # (If any)

# --- cgi configuration.

$goodpath     = '/usr/bin:/usr/sbin:/usr/lib:/usr/ucb';

# --- installation information.
# --- Program specific (not frame specific) configureation information.
# --- It is here because it depends on things the frame already found.

# Status files.
$mytemp           = '/home/nahaj/logictemp/';

# Where to find logic systems.
$systemsdir       = "/home/nahaj/public_html/logic/${prefix}system/";
# Where to find logic notations.
$notationsdir     = "/home/nahaj/public_html/logic/${prefix}notation/";
# Where to find the code itself.
$programlibraries = "/home/nahaj/public_html/logic/${prefix}calculate/";
# Where to find special logic symbols.
$symbolsurl       = 'http://www.cc.utah.edu/~nahaj/logic/symbols/';

# =============================================================================
# Housekeeping:

select((select(STDOUT), $| = 1)[0]); # Syncronize standard out
select((select(STDERR), $| = 1)[0]); # and standard error.

# =============================================================================
# =============================================================================
# ---- Profiling.

  my ($user, $system, $cuser, $ctime) = times;

# =============================================================================
# Minor canned security.

  $ENV{'PATH'} = $goodpath;
  my $item;
  foreach $item (keys %ENV) {
     if    ($item =~ m/^LD_/)        {delete $ENV{$item}}
     elsif ($item =~ m/^SHLIB_PATH/) {delete $ENV{$item}}
  }
  delete @ENV{qw(IFS CDPATH ENV BASH_ENV PERLLIB PERL5LIB PAGER SHELL)};
  umask 0077;
  unshift @INC, $programlibraries if defined $programlibraries
                                          && $programlibraries ne ''
                                          && -e $programlibraries
                                          && -x _ && -d _;

# ==============================================================================
#                          Deal with HTML
# ==============================================================================

# ------------------ Put out HTML headers --------------------------------------

my $htmlidn = '-//W3C//DTD HTML 4.0//EN';
my $htmldtd = 'http://www.w3.org/TR/REC-html40/strict.dtd';

exit 1 if !print <<HEADER;
Content-type: text/html
Pragma: Nocache

<!DOCTYPE HTML PUBLIC "$htmlidn"
                      "$htmldtd">
<html lang="en"><head>
   <title>$programtitle</title>
   <link rev="MADE" href="mailto:$myaddress">
   <meta name="robots" content="NONE">
   <meta name="copyright"
         content="$copyright">
</head><body>
<h1>$programtitle</h1>
<p>$copyright</p>
HEADER

my $originaltime = $user+$system+$cuser+$ctime;
exit 1 if !print "<p>Resource accounting: Setup time: $originaltime</p>\n";

# -----------------  Deal with HTML input --------------------------------------

use vars qw( $text %input );

# Read in text
$text = ''; %input = ();
if (!defined $ENV{'REQUEST_METHOD'}) { # For debugging, try the command line
   if    (@ARGV) { $text  =       shift @ARGV }
   while (@ARGV) { $text .= '&' . shift @ARGV }
} elsif ($ENV{'REQUEST_METHOD'} eq "GET" && defined $ENV{'QUERY_STRING'}) {
   $text = $ENV{'QUERY_STRING'};
} elsif ($ENV{'REQUEST_METHOD'} eq "POST") {
   read (STDIN,$text,$ENV{'CONTENT_LENGTH'}) if defined $ENV{'CONTENT_LENGTH'};
}

# process it.
my ($field,$key,$val);
if (defined $text && $text ne '') {
  $text =~ s/\+/ /g; # http uses "+" to mean space... let us undo that.
  foreach $field (split (/&/, $text)) {
     next if $field eq '';
     ($key, $val) = split(/=/, $field, 2);
     $val = '' if !defined $val;
     # convert %XX from hex numbers to alphanumeric.
     $key =~ s/%(..)/pack("C",hex($1))/ge;
     $val =~ s/%(..)/pack("C",hex($1))/ge;
     if (!defined $input{$key}) {$input{$key} = $val}
     else                       {$input{$key} .= ', ' . $val}
  }
}

# ---- Make up a trailer subroutine for the user to call when they finish ------

sub htmltrailers {
my $haverefer = defined $ENV{'HTTP_REFERER'} && $ENV{'HTTP_REFERER'} ne ''
 && $ENV{'HTTP_REFERER'} !~ m;^http://www.cc.utah.edu/~nahaj/;
 && $ENV{'HTTP_REFERER'} !~ m;^http://www.cc.utah.edu/cgi-bin/cgiwrap/nahaj/;;

return 0 if !print "\n<hr title=\"Navigation\"><h1>Go to ...</h1><ul>\n";
return 0 if !&doprogramcommands();
return 0 if !print <<CANNEDEND;
<li><a href="${pagebase}logic/calculate/">Logic Calculator Page</a></li>
<li><a href="${pagebase}logic/">Logic Page</a></li>
<li><a href="${pagebase}">John Halleck's Home Page</a></li>
<li><a href="http://www.utah.edu/">University of Utah Home Page</a></li>
<li><a href="http://www.utah.com/">Utah's Home Page</a></li>
CANNEDEND

if ($haverefer) {
   return 0 if !print "<li><a href=\"$ENV{'HTTP_REFERER'}\">Back</a> "
                    . "($ENV{'HTTP_REFERER'})</li>\n";
   if (defined $refererlog && $refererlog ne '') {
      if ((!-e $refererlog && open (REF,'>' . $refererlog))
           ||                 open (REF,'>>'. $refererlog))
      {
            print REF $programname, ' <= ', $ENV{'HTTP_REFERER'}, "\n";
            close (REF);
      }
   }
}
return 0 if !print <<CANNEDEND2;
</ul>

<hr title="Page Maintenance"><pre>
This page is http://www.cc.utah.edu/cgi-bin/cgiwrap/nahaj/$programname
CANNEDEND2

my $hostname = `/usr/uucc/exec/hostname`;
chomp $hostname;
if (defined $hostname && $hostname ne '') {
   print "This page last served from underlying server $hostname\n";
}
return 0 if !print <<CANNEDEND3;
It is Version $programversion of $programtitle
$copyright

Send comments or complaints to $myname, at
   <a href="mailto:$myaddress">$myaddress</a>
The code for this page was last changed on $programdate
CANNEDEND3

# *** Warning *** These force us to use floating point.
   ($user, $system, $cuser, $ctime) = times;
   my $finaltime = $user+$system+$cuser+$ctime;
   my $differencetime = $finaltime - $originaltime;
   return 0 if !print "Resource Accounting: Setup: $originaltime, "
                    . "Processing: $differencetime, Total: $finaltime\n";
# *************** This code should probably be pulled from the release version.

   print "</pre></body></html>\n"; # Returns 0 if print fails.
}

# ==============================================================================
# Trivial error handling library

use vars qw ( $reportederrors ); $reportederrors = 0;

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

sub prephtmltext { # Make html text come out right (Quote what's needed)
   my $text = shift; # The order below is not arbitrary... think about it.
   $text =~ s/&/&amp;/g; $text =~ s/</&lt;/g; $text =~ s/>/&gt;/g;  
   return $text;
} 

sub preurltext {
  my $text = &prephtmltext(@_);
  $text =~ s/ /+/g;
  return $text;
}

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

sub htmldumptext { print '<p>' . &prephtmltext(@_) . "</p>\n" }

sub reporterror {
  if (!$reportederrors) {
    print "\n<hr title=\"ERROR REPORT\"><h1>ERRORS:</h1>\n";
    $reportederrors = 1;
  }
  &htmldumptext(@_);
  return 0;
}

sub myerror {
my $error = shift;
my $where = shift; $where = '' if !defined $where;
croak ("<pre>*** INTERNAL ERROR, please report this error " . $error . $where);
}
sub DEBUG   { &htmldumptext("DEBUG: " . shift) if $doingdebug } 


# ==============================================================================
# ==============================================================================
#           Actual problem related (Non web frame) code follows.
# ==============================================================================
# ==============================================================================
# File IO.

use vars qw ( $thisline $infile $outfile $infilename $outfilename);
undef $thisline; # Current input.
undef $infile; undef $outfile;
$infilename = $outfilename = '';

# ------------------------------------
# Echo finish processing a line.

# put out current line, and then get new line.
sub echoline   { return &fileoutput($thisline) && &nextline() }

# Put out text and then get new line.
sub finishline { return &fileoutput(@_)        && &nextline() }
# ------------------------------------
# Close input file

sub closein {
  undef $thisline; $infilename = '';
  return &myerror("Bad close on input file $infilename")
     if !defined $infile;
  return &myerror("Couldn't close input file ($!)")
     if !close ($infile);
  undef $infile;
  return 1
}

# ------------------------------------
# Next line.

sub nextline {
  my $raw = shift; $raw = 0 if !defined $raw;
  return &myerror("Attempt to get next from nowhere")
     if !defined $infile;
  while (defined ($thisline = <$infile>)) {
    chomp $thisline;
    return 1 if $raw;
    $thisline =~ s/^\s+//; $thisline =~ s/\s+$//;
    next if $thisline eq '' || $thisline  =~ m/^#/;    # Skip comments.
    return 1
  }
  return 1
}

# ------------------------------------
# Grabfile

sub grabfilebasic {
  return &myerror("No input file handle to read in grabfile")
    if !defined $infile;
  my $raw = shift; $raw = 0 if !defined $raw;
  my @result = (); my $item;
  while (defined ($item = <$infile>)) {
    next if $item =~ m/^\s*$/ || $item =~ m/^#/;
    $item =~ s/^\s+// if !$raw;
    $item =~ s/\s+$// if !$raw;
    push @result, $item; 
  }
  return @result;
}


# ------------------------------------
# Open input file

sub openinputfile {
  my $given  = shift;
  $infilename = '';
  return &myerror("Redundant attempt to open input file ($infilename, $given)")
     if defined $infile;
  return &myerror("No filename passed for openinputfile")
     if !defined $given || $given eq '';
  $infilename = $given;
  return &myerror("Attempt to open non-existant file $infilename")
     if !-e $infilename;
  return &myerror("Attempt to open unreadable file $infilename")
     if !-r _;
  return &myerror("Couldn't open $infilename for input ($!)")
     if !open (INPUTFILE, '<' . $infilename);
  $infile = \*INPUTFILE;
  return &myerror("File $infilename empty? ($!)?") 
     if !&nextline();
  return 1;
}

# ------------------------------------
# Close output file

sub closeout {
  return &myerror("Bad close on outfile $outfilename") if !defined $outfile;
  close ($outfile); undef $outfile; $outfilename = '';
  return 1
}

# ------------------------------------
# Open the output file.

sub openoutputfile {
  my $given  = shift;
  my $append = shift; $append = 0 if !defined $append;
  my $appendsym = $append ? '>>' : '>';

  return &myerror("Redundent attempt to openoutput. ($outfilename, $given)")
     if defined $outfile;
  return &myerror("No filename passed for openoutputfile")
     if !defined $given || $given eq '';
  $outfilename = $given;
  return &myerror("Couldn't open $outfilename for output ($!)")
     if !open (OUTPUTFILE, $appendsym . $outfilename);
  $outfile = \*OUTPUTFILE;
  return 1;
}

# -------------------------------------
# File output.

sub fileoutput {
   my $text      = shift;

   return &myerror("No text to output?")           if !defined $text;
   return &myerror("No file for output of: $text") if !defined $outfile;
   return &myerror("Couldn't do file print? ($!) $text")
     if !print $outfile $text, "\n";
   return 1
}

# -------------------------------------
# Array to file.

sub putfile {
   my $dataref = shift;
   return &myerror("No file handle for putfile.") if !defined $dataref;
   return &myerror("No file for array output")    if !defined $outfile;
   my $item;
   foreach $item (@$dataref) {
      return &myerror ("Unable to output array to file $!") 
        if !print $outfile $item, "\n";
   }
   return 1;
}

# ------------------------------------
# Copy input to output looking for marker

sub copytil { # Straight copy.
  my ($starttag, $endtag) = @_;

  return &myerror("End of file looking for field $starttag")
     if !defined $thisline;
  return &myerror("Looking for $starttag in non-starttag section?")
     if $thisline ne $starttag;
  return &myerror ("Unable to output $thisline in copy")
     if !&fileoutput($thisline);
  return &myerror ("Unable to get next line of $starttag")
     if !&nextline();

  while (defined $thisline) {
    if ($thisline eq $endtag) {
       return &fileoutput ($thisline) && &nextline(); # **** Exit.
    }
    return 0 if !&fileoutput($thisline) || !&nextline();
  }
  return &myerror("Ending tag $endtag not found");
}


sub compresstil { # Compress and compact datalines as you go. 
  my ($starttag, $endtag) = @_;

  return &myerror("End of file looking for field $starttag")
    if !defined $thisline;
  return &myerror("Looking for $starttag in non-starttag section?")
    if $thisline ne $starttag;
  return &myerror ("Unable to get new line in $starttag")
    if !&nextline();

  my $result = $starttag;
  while (defined $thisline) {
     $result .= ' ' . $thisline;
     if ($thisline eq $endtag) {
        $result =~ s/\s+/ /g; $result =~ s/ </</g; $result =~ s/> />/g;
        return &fileoutput($result) && &nextline(); # ******* EXIT *********
     }
     return 0 if !&nextline();
  }
  return &myerror("Ending tag $endtag not found");
}

# ==============================================================================
# ==============================================================================
# Support routines.

# Get a unique name (for a state file).
sub uniquestatename {
  my ($sec,$min,$hour,$mday,$mon,$year) = localtime($^T);
  my $result = '';
  $mon++; $year+=1900;
  $sec  = '0' . $sec   if $sec  < 10;
  $min  = '0' . $min   if $min  < 10;
  $hour = '0' . $hour  if $hour < 10;
  $mday = '0' . $mday  if $mday < 10;
  $mon  = '0' . $mon   if $mon  < 10;
  $result .= "$year-$mon-${mday}T$hour:$min:$sec";
  $result .= '.' . $$;
  if (defined $ENV{'REMOTE_ADDR'} && $ENV{'REMOTE_ADDR'} ne ''
     && $ENV{'REMOTE_ADDR'} =~ m/^([\w\.\d]+)$/)
     { $result = $1 . ':' . $result }
  if (defined $ENV{'REMOTE_HOST'} && $ENV{'REMOTE_HOST'} ne ''
     && $ENV{'REMOTE_HOST'} =~ m/^([\w\.]+)$/)
     { $result = $1 . '=' . $result; }
  return $result;
}

# =============================================================================
# =============================================================================

# general status of the logic calculator.
# These are often filled in by the routines that read the state file.

use vars qw ( $basesystem $basenotation $state $statefile $goal $cgoal
              $showchoices
            );

$basesystem   = $input{'SYSTEM'};   $basesystem  = '' if !defined $basesystem;
$basenotation = $input{'NOTATION'}; $basenotation= '' if !defined $basenotation;
$goal         = $input{'GOAL'};     $goal        = '' if !defined $goal;
$cgoal        = ''; # Cannonical goal.
$showchoices  = 1;

$state        = $input{'STATE'};    $state       = '' if !defined $state;
if ($state eq '') {
   $statefile = '';
} elsif ($state !~ m/^([^\/\\<>|\*]+)$/) {
   &myerror("Saved state name ($state) is bad?");
   $state = '';
   $statefile = '';
} else {
   $state = $1; # Untaint for perl.
   $statefile = $mytemp . $state;
   if (!-e $statefile) {
      &myerror("Saved state ($statefile) doesn't exist");
      $state = $statefile = '';
   }
}

# =============================================================================
#spew out the displays in a file.

sub outputhtml { return &fileoutput('<HDISPLAY>' . (shift) . '</HDISPLAY>') }
sub outputpre  { return &fileoutput('<PDISPLAY>' . (shift) . '</PDISPLAY>') }

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

sub displaydisplays {
  my $showoffers = shift; $showoffers = 0 if !defined $showoffers;
  my $pre = 0; # Assume not in a <pre> block when we start.

  # &DEBUG("Entering displaydisplays...");
  return &myerror ("Entering display, without state file?")
    if !defined $statefile || $statefile eq '';

  return 0 if !&openinputfile($statefile);

  return 0 if !print "<hr title=\"Display separator\">\n";

  if (!$showoffers) {
     return 0 if !print
                  "<p><a href=\"$programname\?STATE=$state\&SHOW\">",
                  "Redisplay Derivation with offers</a></p>\n";
  } else {
     return 0 if !print
                  "<p><a href=\"$programname\?STATE=$state\&SHOWCLEAN\">",
                  "Redisplay Derivation without offers</a></p>\n";
  }

  while (defined $thisline) {
    # &DEBUG("Display dealing with $thisline ...");
    if    ($thisline =~ m;^<HDISPLAY>(.*)</HDISPLAY>;) {
      if ($pre) { $pre = 0; return 0 if !print "</pre>" }
      return 0 if !print $1, "\n";
    } elsif ($thisline =~ m;^<PDISPLAY>(.*)</PDISPLAY>;) {
      if (!$pre) { $pre = 1; return 0 if !print "<pre>" }
      return 0 if !print $1, "\n";
    } elsif ($thisline=~m;^<GOAL>; && $thisline =~ m;<PRINT>([^<]+)</PRINT>;) {
        if ($pre) { $pre = 0; return 0 if !print "</pre>" }
        return 0 if !print "<p><b>Stated Goal: $1</b></p>\n";
      }
    elsif (!$showoffers) {}
    elsif ($thisline =~ m;^<OFFER NUMBER=\"(.+)\">(.+)</OFFER>;) {
        if ($pre) { $pre = 0; return 0 if !print "</pre>" }
        return 0 if !&displayoffer($1, $2);
      }
    return 0 if !&nextline();
  }
  # Clear it on the way out.
  if ($pre) { $pre = 0; return 0 if !print "</pre>\n" }
  return &closein();
}

# ==============================================================================
# ==============================================================================
# Current notation information.

use vars qw(%operator @operatorlist %synonym %constant %display %parsetokens);

# Operator => precidence.
%operator      = (); # underlying operators.
@operatorlist  = (); # our operators but sorted by length.

%parsetokens   = (); # Non-variable name tokens.
  $parsetokens{')'} = 'punctuation';
  $parsetokens{'('} = 'punctuation';
  $parsetokens{'{'} = 'punctuation';
  $parsetokens{'}'} = 'punctuation';
  $parsetokens{'['} = 'punctuation';
  $parsetokens{']'} = 'punctuation';
  $parsetokens{','} = 'punctuation';

%synonym   = (); # Alternate names for operations, etc.
%constant  = (); # Names known to be constants instead of variables.
%display   = (); # prefered display form of variables.

# ==============================================================================
# Load up notations.

sub loadconstants {
   my $list = shift; my $item;
   foreach $item (split(/\s+/, $list)) { $constant{$item} = 1 }
   return 1
}

sub loadoperators {
   my $list = shift; my $item;
   foreach $item (split(/\s+/, $list)) { $operator{$item} = 1 }
   return 1
}

sub loadasynonym {
   my ($op,@list) = split(/\s+/, shift); my $item;
   foreach $item (@list) {
      $synonym{$item} = $op;
      if (defined $parsetokens{$item} && $parsetokens{$item} ne $op) {
         &myerror("symbol $item ($op) already in use ($parsetokens{$item})");
         return 0;
      } else {
         $parsetokens{$item} = $op;
      }
   }
   return 1
}

sub loadadisplay {
  my $line = shift;
  if ($line !~ m/^(\S+)\s*(\S.*)$/) {
     &myerror("Bad DISPLAY line: `$line'");
  } elsif (!defined $operator{$1} && !defined $constant{$1}) {
     &myerror("notation: The operator $1 has display"
                  . " line but is not a listed operator\n");
  } else {
    $display{$1} = $2;
    return 1
  }
  return 0
}

# ==============================================================================
# Init notations file.

sub initnotationsfile {
  my $notation   = shift;
  my $temp;

  return &myerror("Notation name not provided in initialization")
    if !defined $notation || $notation eq '';
  return &myerror("Bad characters in notation name. $notation")
    if $notation !~ m/^([\d\w\.]+)/;
  $notation = $1; # (Untainted for perl.)
  return &myerror("Notation file $notation couldn't be opened ($!)")
    if !&openinputfile($notationsdir . $notation . '.txt');
  return &myerror("Process notation called on non-notation? ($thisline)")
    if $thisline ne '<NOTATION>';
  return &myerror("Unable to write to notations status file")
    if !&echoline() || !&fileoutput("# ---- Notation: $notation");
 
  my $end = '';
  while (defined $thisline) {

     if ($thisline eq '</NOTATION>') {
        return &echoline() && &closein();

     } elsif ($thisline eq '<CONSTANTS>') {
        return 0 if !&compresstil('<CONSTANTS>', '</CONSTANTS>');

     } elsif ($thisline eq '<OPERATORS>') {
        return 0 if !&compresstil('<OPERATORS>', '</OPERATORS>');

     } elsif ($thisline eq '<DISPLAY>') {
        return 0 if !&copytil('<DISPLAY>', '</DISPLAY>');

     } elsif ($thisline eq '<SYNONYMS>') {
        return 0 if !&copytil('<SYNONYMS>', '</SYNONYMS>');

     } elsif ($thisline =~ m;<BASE>.*</BASE>;) {
        return 0 if !&echoline();

     } elsif ($thisline =~ m;<NAME>.*</NAME>;) {
        return 0 if !&echoline($thisline);

     } else {
        my $temp = $thisline; &nextline();
        return &myerror("Unknown line in init Notations file \"$temp\"");
     }
  }
  return &myerror("NOTATION not properly terminated?");
}

# ==============================================================================
# Deal with notations file.

sub processnotationsfile {
  %operator = (); %constant = (); 
  %display  = (); %synonym  = ();
  # &DEBUG("Processing notations file...");
  return &myerror("processnotationsfile called on $thisline")
    if $thisline ne '<NOTATION>';
  return 0 if !&nextline();
  my $item; my @list; my $op; my $last = 0;
  while (defined $thisline) {

     if ($thisline eq '</NOTATION>') {
       @operatorlist =  sort { length($a) < length($b) } keys %parsetokens;
       return &nextline();

     } elsif ($thisline =~ m;<CONSTANTS>(.+)</CONSTANTS>;) {
       return 0 if !&loadconstants($1) || !&nextline();

     } elsif ($thisline =~ m;<OPERATORS>(.+)</OPERATORS>;) {
       return 0 if !&loadoperators($1) || !&nextline();

     } elsif ($thisline eq '<SYNONYMS>') {
       return 0 if !&nextline(); # Flush start tag.
       while ($thisline ne '</SYNONYMS>') {
          return 0 if !&loadasynonym($thisline) || !&nextline();
       }
       return &myerror("SYNONYMS in notation not terminated")
         if !defined $thisline;
       return 0 if !&nextline(); # flush ending tag.

     } elsif ($thisline eq '<DISPLAY>') {
       return 0 if !&nextline(); # Flush start tag.
       while ($thisline ne '</DISPLAY>') {
         return 0 if !&loadadisplay($thisline) || !&nextline();
       }
       return &myerror("DISPLAY in notation not terminated.")
         if !defined $thisline;
       return 0 if !&nextline();

     } elsif ($thisline =~ m;<BASE>(.+)</BASE>$;) {
       $basenotation = $1;
       return 0 if !&nextline();

     } elsif ($thisline =~ m;<NAME>(.+)</NAME>;) {
       return 0 if !print "<h1>Notation: $1</h1>\n<p>$1</p>\n"
                && !&nextline();

     } else {
       return &myerror("Unknown line in Notations file: \"$thisline\"");
     }
  } 
  return &myerror("Notation file not properly terminated?");
}

# ==============================================================================
# ==============================================================================
# Deal with a print form of an expression.

# Output expressions.

# return standard form of an expression.
sub expressiontointernal {
  my $item = shift;
     myerror ("expressiontointernal had undefined item")
        if !defined $item;
  return $item  if !ref $item;
  return $$item if 'ARRAY' ne ref $item;
  my ($next, @arguments) = @$item;
  my $result = '(' . &expressiontointernal($next);
  foreach $item (@arguments) {
    $result .= ' ' . &expressiontointernal($item);
  }
  $result .= ')';
  return $result;
}

sub itokens { # Bust up internal form to tokens.
  my @tokens = ();
  my $given = shift; croak  "??? No given string is itokens" if !defined $given;
  while ($given ne '') {
    if ($given =~ m/^\s+(.*)$/)          { $given = $1                   }
    elsif ($given =~ m/^([\(\)])(.*)$/)  { $given = $2; push @tokens, $1 }
    elsif ($given =~ m/^([\w\d]+)(.*)$/) { $given = $2; push @tokens, $1 }
    else                                 { $given = '' }
  }
  return @tokens;
}

# Get expression, given standard form.
sub internaltoexpression {
  my $given = shift;
  my @stack = (); my @result = ();
  my $token;
  my @tokens = &itokens($given);
  foreach $token (@tokens) {
    if    ($token eq '(') { push @stack, '(' }
    elsif ($token ne ')') { push @stack, $token }
    else {
       @result = ();
       while ('(' ne ($token = pop @stack)) { unshift @result, $token }
       push @stack, [@result];
    }
  }
  if (@stack > 1) {
     myerror ("internaltoexpression has malformed internal $given (@tokens)")
  }
  my $item = pop @stack;
  return $item;
}


# Internal to external form.
sub internaltoexternal {
    return &expressiontoexternal(&internaltoexpression(@_));
}

# internal to HTML form.
sub internaltohtml {
   return &prephtmltext(&expressiontoexternal(&internaltoexpression(@_)));
}


# ==============================================================================

# Print an expression's structure as ASCII art.
# (Good for debugging also.)
sub printstructraw {
  my ($indentraw, $indent, $expression) = @_; my $op; my @list;
  if (!ref $expression || 'ARRAY' ne ref $expression) {
    $op = $expression; @list = ();
  } else {
    ($op, @list) = @$expression;
  }
  $op = '[UNDEF]' if !defined $op;
  my $opindent = ''; $opindent = "+--" if $indent ne '';
  print $indentraw, $opindent, " ", $op, "\n";
  my $last = pop @list; my $item;
  foreach $item (@list) {
     print $indent, "|\n"; &printstructraw($indent, $indent . '|   ', $item);
  }
  if (defined $last) {
     print $indent, "|\n"; &printstructraw($indent, $indent . '    ', $last);
  }
}
sub printstructure {
  print "<pre>\n"; &printstructraw('', '', @_); print "</pre>\n"
}

# ==============================================================================

sub convertequations {
   my $line = shift;
   while ($line =~ m;^(.*)<EQUATION>([^<]+)</EQUATION>(.*)$;) {
     $line = $1 . &internaltoexternal($2) . $3
   }
   return $line;
}

# ==============================================================================
# Deal with tokens.

# Parse state.

use vars qw( @inputtokens $lasterror); $lasterror = ''; @inputtokens = ();

# Takes in string, returns array of tokens.
sub tokenize {
  my $given = shift; $given = '' if !defined $given;
  my @result = (); my $processed = '';
  while ($given ne '') {

     if ($given =~ m/^(\s+)(.*)$/) { # White space.
       $processed .= $1; $given = $2; next;

     } elsif ($given =~ m/^([a-zA-Z][a-zA-Z_]*)(.*)$/) { # Identifier
       push @result, lc($1); $processed .= $1; $given = $2; next;

     } elsif ($given =~ m/^([\{\(\[\]\)\}\,])(.*)$/) { # Canned grouping
       push @result, $1; $processed .= $1; $given = $2; next;


     # Misc operators.
     } elsif ($given =~ m;^(/\\|\\/|==|=>|=|~|~>|->|\||-|\+|\*|>)(.*)$;) {
       push @result, $1; $processed .= $1; $given = $2; next;
     
     } else {
          return ("Unparsable input \"$processed\" . \"$given\"");
     }
  }

  # Take care of any synonyms.
  if (!%synonym) { return @result }
  my $index;
  # &DEBUG("In tokenize, doing synonyms.");
  foreach $index (0..(@result-1)) {
    if (defined $synonym{$result[$index]}) {
       $result[$index] = $synonym{$result[$index]}
    }
  }
  return @result;
}

sub seterror { if ($lasterror eq '') { $lasterror = shift }; return 0 }

sub match {
   my $given = shift;
   my $got; 
   if (!@inputtokens) {
      &seterror("Expected $given, but got nothing")
   } elsif ($given ne ($got = shift @inputtokens)) {
      &seterror("Expected $given, got $got") 
   } else {
      return 1
   } 
   return 0;
}

sub wehave {
   my $given = shift;
   return 0 if !@inputtokens || $given ne $inputtokens[0];
   shift @inputtokens;
   return 1
}

sub getvar {
   my $result = '';
   if    (!@inputtokens)                { &seterror("out of input?") }
   elsif ($inputtokens[0] =~ m/^[a-z]/) { $result = shift @inputtokens }
   else { &seterror("Non variable found in variable position") }
   return $result;
}

sub externaltoexpression {
  my $toparse = shift;
  $lasterror = ''; my $result = 'BADPARSE';
  # &DEBUG("Starting to parse $toparse");
  @inputtokens = &tokenize($toparse);
  &DEBUG("Tokenized as @inputtokens");
  $result = &parseexpression();
  if (@inputtokens) {
     &seterror("Unparsed input tokens? @inputtokens");
     &DEBUG("Unparsed input? @inputtokens");
  }
  $result = '' if $lasterror ne '';
  &DEBUG("Parse returning:");
  &printstructure($result) if $result ne '' && $doingdebug; 
  return $result;
}

sub parseexpression { return &parseseq() }

sub parseunit {
  my @result = (); my $temp = '';
  if (!@inputtokens)
     { &seterror("Parsing unit, Unexpected end of input."); return '???' }
  else {
     my $next = $inputtokens[0];
     if    ($next eq '(')
        { &match('('); $temp = &parseexpression(); &match(')'); return $temp }
     elsif ($next eq '[')
        { &match('['); $temp = &parseexpression(); &match(']'); return $temp }
     elsif ($next eq '{')
        { &match('{'); $temp = &parseexpression(); &match('}'); return $temp }
     elsif ($next eq 'FORALL' || $next eq 'EXISTS' || $next eq 'LAMBDA')
        { @result = ($next); &match($next); &match('('); 
          push @result, &getvar();
          &match(',');
          push @result, &parseexpression();
          &match(')');
          return \@result;
        }
     elsif ($constant {$next}) 
        { shift @inputtokens; return $next}
     elsif ($next =~ m/^[a-z][a-z0-9_]*/) # variable.
        { shift @inputtokens;
          # And possible function style predicates.
          if (!&wehave('(')) { return $next }
          else {
             @result = ($next, &parseexpression());
             while (&wehave(',')) { push @result, &parseexpression() }
             &match(')');
             return \@result;
          }
        }
     else {
        &seterror("Unrecognizable unit: $next"); shift @inputtokens;
     } 
  }
  return pop @result if @result == 1;
  return [@result];
}

sub parseunary {
  if    (wehave('POS')) { return ('POS', &parseunary()) }
  elsif (wehave('NES')) { return ('NES', &parseunary()) }
  elsif (wehave('NOT')) { return ('NOT', &parseunary()) }
  else                  { return &parseunit() }
}

sub parseterm {
  my $result = &parseunary();
  if (&wehave('AND')) { $result = ['AND', $result, &parseunary() ] }
  return $result;
}

sub parsesum {
  my $result = &parseterm();
  if (&wehave('OR')) { $result = ['OR', $result, &parseterm() ] }
  return $result;
}

sub parseimp {
  my $result = &parsesum();
  if (&wehave('IMP')) { $result = ['IMP', $result, &parsesum() ]}
  return $result;
}

sub parseequiv {
  my $result = &parseimp();
  if (&wehave('EQV')) { $result = ['EQV', $result, &parseimp() ] }
  return $result;
}

sub parsestrimp {
  my $result = &parseequiv();
  if (&wehave('SMP')) { $result = ['SMP', $result, &parseequiv() ] }
  return $result;
}

sub parseseq {
  my $result = &parsestrimp();
  if (&wehave('SEQ')) { $result = ['SEQ', $result, &parsestrimp() ] }
  return $result;
}

# =====================================================================
# Recursive decent unparse...  

sub printlist {
   my $result = &printexpression(shift);
   foreach $item (@_) { $result .= ',' . &printexpression(shift) }
   return $result;
}

sub printunit {
   my $item = shift;
   return $item if !ref $item || 'ARRAY' ne ref $item;
   my ($op, @arguments) = @$item;
   return $display{$op} . '(' . &printlist(@arguments) . ')'
      if $op eq 'FORALL' || $op eq 'EXISTS' || $op eq 'LAMBDA';
   # If we got here, there are several possiblities...
   # Unfortunately, one of them is that we have an operator
   # we've never heard of, and don't have a display for.
   # (Such as a predicate...)
   if (!defined $display{$op}) {
      my $result = $op . '(' . &printexpression(shift @arguments);
      my $item; foreach $item(@arguments)
         { $result .= ',' . &printexpression($item) }
      return $result . ')';
   }
   return '(' . &printexpression($item) . ')'
}

sub printunary {
   my $given = shift; return $given if !ref $given || 'ARRAY' ne ref $given;
   my ($op, $argument) = @$given;
   return $display{$op} . &printunit($argument)
      if $op eq 'POS' || $op eq 'NES' || $op eq 'NOT';
   return &printunit($given)
}

sub printterm {
   my $given = shift; return $given if !ref $given || 'ARRAY' ne ref $given;
   my ($op, $argument1, $argument2) = @$given;
   return &printunary($argument1).$display{$op}.&printunary($argument2)
       if $op eq 'AND';
   return &printunary($given);
}

sub printsum {
   my $given = shift; return $given if !ref $given || 'ARRAY' ne ref $given;
   my ($op, $argument1, $argument2) = @$given;
   return &printterm($argument1).$display{$op}.&printterm($argument2) 
       if $op eq 'OR';
   return &printterm($given)
}

sub printimp {
   my $given = shift; return $given if !ref $given || 'ARRAY' ne ref $given;
   my ($op, $argument1, $argument2) = @$given;
   return &printsum($argument1).$display{$op}.&printsum($argument2) 
       if $op eq 'IMP';
   return &printsum($given);
}

sub printequiv {
   my $given = shift; return $given if !ref $given || 'ARRAY' ne ref $given;
   my ($op, $argument1, $argument2) = @$given;
   return &printimp($argument1).$display{$op}.&printimp($argument2) 
       if $op eq 'EQV';
   return &printimp($given);
}

sub printstrimp {
   my $given = shift; return $given if !ref $given || 'ARRAY' ne ref $given;
   my ($op, $argument1, $argument2) = @$given;
   return &printequiv($argument1).$display{$op}.&printequiv($argument2) 
       if $op eq 'SMP';
   return &printequiv($given);
}

sub printstreq {
   my $given = shift; return $given if !ref $given || 'ARRAY' ne ref $given;
   my ($op, $argument1, $argument2) = @$given;
   return &printstrimp($argument1).$display{$op}.&printstrimp($argument2) 
       if $op eq 'SEQ';
   return &printstrimp($given);
}

sub printexpression {
  my $item = shift;
  return '[?]' if !defined $item;
  return $item if !ref $item || 'ARRAY' ne ref $item;
  # &DEBUG("Printexpression called: " . &expressiontointernal(@_));
  return &printstreq($item);
}

sub expressiontoexternal {
  return &printexpression(@_);
}

# ==============================================================================
# Line displays

sub padline { # Pad text to a given size.
  my ($given, $to, $pre) = @_;
  $pre = 0 if !defined $pre; # Are we prepending padding?
  my $test = $given;
  $test =~ s/&lt;/</g; $test =~ s/&gt;/>/g; $test =~ s/&amp;/&/g;
  my $current = length($test);
  return $given if $current >= $to;
  my $short = $to - $current;
  return $given . ' 'x$short if !$pre;
  return ' 'x$short . $given;
}

# Prepare a standard display line.
sub dumplinedisplay {
  my ($equation,$printequation,$justification,$linenumber,$indentlevel) = @_;
  $indentlevel = 0 if !defined $indentlevel;
  my $indent = '';
  if ($indentlevel > 0) { $indent = '|  'x$indentlevel }
  $linenumber = &padline ($linenumber, 4, 1);
  my $prefix =$linenumber . ':' . $indent;
  my $postfix = ' ' . $justification;
  my $printform = "<EQUATION>$equation</EQUATION>";
  my $translation = &padline($printequation, 60);
  return &fileoutput("<XPDISPLAY>$prefix $printform $postfix</XPDISPLAY>")
      && &fileoutput("<PDISPLAY>$prefix $translation $postfix</PDISPLAY>");
}

# Put out a separation line for discharges.
sub dumpseparationline {
  my $level = (shift) - 1; $level = 0 if $level < 0;
  my $type  = shift; # 0 for start, 1 for end.
  my $indent =  2 + 2 + $level*3;
  my $prefix = ' 'x$indent;
  my $mark = $type ? "|--" : "+--";
  $mark .= "-----------------------";
  return '<PDISPLAY>' . $prefix . $mark . '</PDISPLAY>'
}


# ==============================================================================
# Handle global rule status.

use vars qw( %rule %ruleneed %rulegives @rules);
%rule = (); %ruleneed = (); %rulegives = (); @rules = ();

# ==============================================================================
# Handle rule stuff for display.

sub rawprocessrule {
  my ($short, $long, $need, $gives) = @_;
  # &DEBUG("rawprocessrule has: $short, $long, $need, $gives");
  if (exists $rule{$short}) { return 1 }
  $rule{$short}      = $long;
  $ruleneed{$short}  = $need;
  $rulegives{$short} = $gives;
  push @rules, $short;
  return 1;
}

sub processrule {
  # &DEBUG("Handle Rule called on $thisline");
  return &myerror("process RULE called on no rule? $thisline")
    if $thisline ne '<RULE>' || !&nextline();

  my $need = ''; my $gives = ''; my $short=''; my $long='';
  while (defined $thisline) {
     # &DEBUG("Handle Rule loop: $thisline");
     if ($thisline eq '</RULE>') {
        return 0 if !&rawprocessrule($short, $long, $need, $gives);
        # &DEBUG("Exiting RULE");
        return &nextline();
     } elsif ($thisline =~ m;<NEED>(.+)</NEED>;) {
       $need .= ',' if $need ne '';
       $need .= $1;
     } elsif ($thisline =~ m;<GIVES>(.+)</GIVES>;) {
       $gives .= ',' if $gives ne '';
       $gives .= $1;
     } elsif ($thisline =~ m;<SHORT>(.+)</SHORT>;) {
       $short = $1;
     } elsif ($thisline =~ m;<LONG>(.+)</LONG>;)   {
       $long = $1;
     } elsif ($thisline =~ m;^<HDISPLAY>;) {
     } elsif ($thisline =~ m;^<PDISPLAY>;) {
     } elsif ($thisline =~ m;^<XHDISPLAY>;) {
     } elsif ($thisline =~ m;^<XPDISPLAY>;) {
     } else {
       return &myerror("Unknown line while processing RULE, $thisline");
     }
     return 0 if !&nextline();
  }
  return &myerror("handle RULE not terminated.");
}

# ==============================================================================
# Initialize rule stuff.

sub initrule {
  return &myerror("Init RULE called on no rule? $thisline")
    if $thisline ne '<RULE>';

  my @needs; my @givens; my $short = ''; my $long = '';
  return 0 if !&echoline();
  while (defined $thisline) {
     if ($thisline eq '</RULE>') {
        my $item;
        if (@needs) {
           return 0 if !&outputpre("Rule requires:");
           foreach $item (@needs) {
             return 0 if !&fileoutput
                         ("<XPDISPLAY><EQUATION>$item</EQUATION></XPDISPLAY>")
                      || !&outputpre (&internaltoexternal($item));
           }
        }
        if (@givens) {
           return 0 if !&outputpre("Rule produces:");
           foreach $item (@givens) {
             return 0 if !&fileoutput
                          ("<XPDISPLAY><EQUATION>$item</EQUATION></XPDISPLAY>")
                      || !&outputpre (&internaltoexternal($item));
           }
        }
        return 0 if !&rawprocessrule($short, $long,
                                     join(',',@needs), join(',',@givens));
        return &echoline();
     } elsif ($thisline =~ m;^<NEED>(.+)</NEED>$;) {
        if ($1 ne '<PROGRAMATIC/>') { push @needs, $1 }
     } elsif ($thisline =~ m;^<GIVES>(.+)</GIVES>$;) {
        if ($1 ne '<PROGRAMATIC/>') { push @givens, $1 }
     } elsif ($thisline =~ m;^<SHORT>(.+)</SHORT>$;) {
        $short = $1;
        return 0 if !print "<h1>$1</h1>\n";
     } elsif ($thisline =~ m;^<LONG>(.+)</LONG>$;)   {
        $long = $1;
        return 0 if !&outputhtml ("<p>This system contains the rule: $1</p>")
                 || !print "<p>This system contains the rule: $1</p>\n";
     } else {
       return &myerror("Unknown line while processing RULE, $thisline");
     }
     return 0 if !&echoline();
  }
  return &myerror("Initialize RULE not terminated.");
}

# ==============================================================================
# Derivation housekeeping.

use vars qw( $lastline $lastoffer ); $lastline = 0; $lastoffer = 0;

use vars qw ( %have %need %chave %cneed);
%have = (); %need = (); %chave = (); %cneed = ();
# What do we have in the derivation?  What do we need?
# And the same for the canonical forms.
# ------------------------------------------------------------------------------

# Give out correct form of offer.
sub displayoffer {
   my $number = shift;
   my $offer = shift;
   my $line = '?';
   # &DEBUG("In displayoffer, with $offer");
   if      ($offer =~ m;^<SUBSTITUTE>(.*)</SUBSTITUTE>;) {
     # &DEBUG("Doing Substitute");
     my $given = $1; my $varlist; my $base;
     if ($given =~ m;^<BASE>([^<]+)</BASE>(.+)$;) {
        $varlist = $2; $base = $1;
     } else { $varlist = $given; $base='' }
     if ($varlist =~ m;^<NUMBER>([^<]+)</NUMBER>(.+)$;) {
        $line = $1; $varlist = $2;
     } else { $line = '?' }
     my @list = split(/\,/,$varlist);
     return 0 if !print "<form method=\"post\" action=\"$programname\">",
                    "<input type=\"hidden\" name=\"STATE\" value=\"$state\">",
                    "<input type=\"hidden\" name=\"BASE\" value=\"$base\">",
                    "<input type=\"hidden\" name=\"LINE\" value=\"$line\">",
                    "<input type=\"hidden\" name=\"VARS\" value=\"$varlist\">",
                    "<p>Substitution:<p>\n";
     my $count = 1;
     my $var;
     foreach $var (@list) {
       my $letter; my $restrictions;
       if ($var =~ m;^([\w\d]+)\:(.+);) { # With restrictions.
         $letter = $1; $restrictions = 'But may not contain: ' . $2;
       } else { # No restrictions.
         $letter = $var; $restrictions = '';
       }
       return 0 if !print
         "<br>$letter:<input type=\"TEXT\" name=\"$letter\" value=\"$letter\" ",
         "tabindex=\"$count\" size=\"70\" maxlength=\"300\">$restrictions\n";
       $count++;
     }
     return 0 if !print "<br><input type=\"submit\" name=\"GOTSUB\" " .
           "value=\"Submit substitution\" tabindex=\"$count\">";
     $count++;
     return print
            "<input type=\"reset\"  name=\"RESET\" tabindex=\"$count\">",
            "</FORM>\n";
   }
   # OK, not a substitution... must be a regular offer.
   my ($internal, $external, $lines, $justification) = $offer =~
     m;^<EQN>(.+)</EQN><SHOW>(.+)</SHOW><LINES>(.+)</LINES><JUST>(.+)</JUST>; ;
   if (defined $internal) {
      # &DEBUG("Non-substitute offer $internal");
      if (!exists $have{$internal}) {
         if ($internal eq $goal) {
            return 0 if !print "<br>Derive ",
               "<a href=\"$programname\?STATE=$state&OFFNUM=$number\">",
               $external, " (Your stated goal)</a>,  with justification: ",
               "$justification\n";
         } else {
         return 0 if !print "<br>Derive ",
            "<a href=\"$programname\?STATE=$state&OFFNUM=$number\">",
            $external,'</a> with justification: ',$justification,"\n";
         }
      } else {
        # &DEBUG("Offer resultant already exists.");
      }
   }
   return 1
}

# ==============================================================================
# load up derivation tables from the file.

sub rawloadstate {
  my $number = shift; my $line = shift;
  if ($line =~ m;^<EQN>([^<]+)</EQN><CANNON>([^<]+)</CANNON>(.*)$;) {
     $have{$1} = $number; $chave{$1} = $2;
     my $remaining = $3;
     while ($remaining =~ m;<NEED RULE\"([^\"<]+)\">([^<]+)</NEED>(.*)$;) {
       $need{$2} = "$1, $2";
       $remaining = $3;
     }
     return 1;
  } else { return &myerror("Bad DLINE? $line") }
}

sub loadstate {
  return &myerror ("Entering display, without state file?")
    if !defined $statefile;
  return 0 if !&openinputfile($statefile);
  # &DEBUG("Loading state...");
  while (defined $thisline) {
    if ($thisline =~ m;^<DLINE NUMBER=\"(\d+)\">(.+)</DLINE>$;) {
       # Line of derivation.
       return 0 if !&rawloadstate($1, $2) || !&nextline();
       next; 

    } elsif ($thisline eq '<RULE>') {
      return 0 if !&processrule(); next;

    } else { return 0 if !&nextline() }
  }
  return &closein();
}

# ==============================================================================
# housekeeping to add a line to a derivation.

sub addnewline {
  my ($given, $justification) = @_;
  my $parsed    = &internaltoexpression($given);     # parsed form.
  &DEBUG("*** addnewline called with $given");
  &printstructure($parsed) if $doingdebug;
  my $rawcanon  = &fullcanonicalform($parsed);      # in standard form.
  my $canon     = &expressiontointernal($rawcanon); # as a string.
  $lastline++;

  if ($have{$given}) {
     &reporterror("Line already exists as line $have{$given}");
     return 1; # In that sense it is already added.
  }

  return 0 if !&fileoutput('<LINE>');

  my $printform = &expressiontoexternal($parsed);
  # &DEBUG("   Print form: $printform");
  &dumplinedisplay($given, $printform, $justification, $lastline);
    # Tell user about it.

  my $line = "<DLINE NUMBER=\"$lastline\"><EQN>$given</EQN>"
           . "<CANNON>$canon</CANNON></DLINE>";
  return 0 if !&fileoutput($line);

  if (defined $goal && $goal eq $given) {
     return 0 if !print "<p><b>*** This line is the stated goal ***</b></p>\n"
  } elsif (defined $cgoal && $cgoal eq $canon && exists $rule{'US'}) {
     return 0 if !print "<p>*** This line is a variable renaming away ",
                 " from your stated goal.\n";
  }

  # &DEBUG("Rule list in newline is @rules");
  # my $debug; foreach $debug (keys %have) {
     # &DEBUG("  We have: $debug");
  # }
  my $item;
  foreach $item (@rules) {
     # &DEBUG("For each rule processing $item");

     if (defined $need{$item . ', '. $given}) {
        # Match up needs.
        # [Under construction]
        return 0 if !&fileoutput();
     }
     if ($item eq 'US') {
        # This should really be if we have substitution, and this is not an
        # assumption.
        my @variables = &freevars($given);
        # &DEBUG("addnewline had free variable list of @variables");
        my $offer = join(',',@variables); $lastoffer++;
        return 0 if !&fileoutput
        ("<OFFER NUMBER=\"$lastoffer\"><SUBSTITUTE><BASE>$given</BASE>"
         . "<NUMBER>$lastline</NUMBER>$offer</SUBSTITUTE></OFFER>");
     } elsif ($item eq 'N') {
         # &DEBUG("Necessatation applies.");
         $lastoffer++;
         my $result = "(NES $given)";
         return 0 if !$have{$result} && !&fileoutput(
                  "<OFFER NUMBER=\"$lastoffer\">".
                     "<EQN>$result</EQN>" .
                     '<SHOW>' . &internaltoexternal($result) . '</SHOW>' .
                     '<LINES>'. $lastline . '</LINES>'.
                     '<JUST>'. $lastline.', N</JUST>'.
                  '</OFFER>');
     } elsif ($item eq 'MP') {
       # Directly?  Check form.
       # &DEBUG("Entering MP part of addnewline");
       if ($given =~ m;^\(IMP ;) { # it is an implication...
          &DEBUG("Is implication of form:");&printstructure($parsed);
          my $antecedent = &expressiontointernal($parsed->[1]);
          &DEBUG("Form of antecedent:"); &printstructure($parsed->[1]);
          &DEBUG("Antecedent is $antecedent");
          if (defined $have{$antecedent}) { # can we do it?
             # &DEBUG("We have $given and $antecedent");
             #OK, dump an offer
             my $consequent = &expressiontointernal($parsed->[2]);
             croak "*** INTERNAL ERROR, no consequent expression $parsed->[2]"
                if !defined $consequent;
             &DEBUG ("Consequent is $consequent");
             if (!exists $have{$consequent}) {
                $lastoffer++;
                return 0 if !$have{$consequent} && !&fileoutput(
                  "<OFFER NUMBER=\"$lastoffer\">".
                     "<EQN>$consequent</EQN>" .
                     '<SHOW>' . &internaltoexternal($consequent) . '</SHOW>' .
                     '<LINES>'.$have{$antecedent}.' '. $lastline . '</LINES>'.
                     '<JUST>'. $have{$antecedent}.','.$lastline.',MP</JUST>'.
                  '</OFFER>');
            } else {
              # &DEBUG("Rejecting because we have consequent $consequent");
            }
          }
       }
       # Note that this is not an "elsif".  We really have to check
       # regardless of how the previous check turned out.
       # **** Are we the antecedent of someone else's MP?
       # &DEBUG("[We are $given]");
       my $test;
       foreach $test(keys %have) {
         # &DEBUG("Testing to see if we are antecedent of $test");
         if ($test =~ m;\(IMP $given (.+)\)$;) {
            &DEBUG("We are anticedent of $test ($have{$test})");
            my $consequent = $1;
            if (!exists $have{$consequent}) {
               $lastoffer++;
               return 0 if !$have{consequent} && !&fileoutput(
                 "<OFFER NUMBER=\"$lastoffer\">".
                    "<EQN>$consequent</EQN>" .
                    '<SHOW>' . &internaltoexternal($consequent) . '</SHOW>' .
                    '<LINES>'.$lastline.' '. $have{$test} . '</LINES>'.
                    '<JUST>' .$lastline.','. $have{$test} .',MP</JUST>'.
                 '</OFFER>');
            } else {
              # &DEBUG("Rejecting because we have consequent $consequent");
            }
         }
       } 
     } else {
     }
  }
  if (!$have{$given})  {$have{$given}  = $lastline }
  if (!$chave{$given}) {$chave{$given} = $lastline }
  return &fileoutput("</LINE>");
}
   
# ==============================================================================

# Initialize Schema.

sub initschema {
  # &DEBUG("Entering initschema...");
  return &myerror("SCHEMA called on non-schema, $thisline")
    if $thisline ne '<SCHEMA>';
  return &myerror("SCHEMA empty in initschema?")
    if !&nextline();
  my $internal; my $canon; my $justification;
  while (defined $thisline) {

     if ($thisline eq '</SCHEMA>') {
        return &myerror("No internal form given for schema?")
          if !defined $internal;
        return &myerror("No Justification given for schema?")
          if !defined $justification;
        return &addnewline($internal, $justification) && &nextline();

     } elsif ($thisline =~ m;^<EQN>(.+)</EQN>$;) {
       $internal = $1;
       return 0 if !&nextline();

     } elsif ($thisline =~ m;^<JUSTIFICATION>(.+)</JUSTIFICATION>$;) {
       $justification = $1;
       return 0 if !&nextline();

     } else {
       my $error = $thisline; &nextline();
       return &myerror("Unknown line in init SCHEMA: $error");
     }
  }
  return &myerror("SCHEMA not terminated.");
}

# ==============================================================================
# Process line schema.

sub processline {
  # &DEBUG("Entering processline...");
  return &myerror("LINE called on non-line, $thisline")
     if $thisline ne '<LINE>' || !&nextline();

  while (defined $thisline) {

     if ($thisline eq '</LINE>') {
        return &nextline(); # ***** EXIT ********
     } elsif ($thisline =~ m;^<EQN>;) {
     } elsif ($thisline =~ m;^<DLINE NUMBER=\"(\d+)\">;) {
       $lastline = $1 if $1 > $lastline;
     } elsif ($thisline =~ m;^<OFFER NUMBER=\"(\d+)\">;) {
       $lastoffer = $1 if $1 > $lastoffer;
     } elsif ($thisline =~ m;^<SOFFER NUMBER=\"(\d+)\">;) {
       $lastoffer = $1 if $1 > $lastoffer;
     } elsif ($thisline =~ m;^<XPDISPLAY>;) {
     } elsif ($thisline =~ m;^<XHDISPLAY>;) {
     } elsif ($thisline =~ m;^<HDISPLAY>;) {
     } elsif ($thisline =~ m;^<PDISPLAY>;) {
     } else {
       &myerror("Unknown line in processline: $thisline");
       return 0;
     }
     return 0 if !&nextline();
  }
  return &myerror("Missing </LINE> entry");
}

# ==============================================================================
# Process initial axioms.

sub initaxioms {
   return &myerror("initaxioms called on junk, $thisline")
     if $thisline ne '<INITIAL>';
   return &myerror("Unable to get lines in <INITIAL>")
     if !&nextline();

   while (defined $thisline) {
  
      if ($thisline eq '</INITIAL>') {
         return &nextline(); # **** EXIT *****

      } elsif ($thisline eq '<SCHEMA>') {
         return 0 if !&initschema();

      } else {
        my $temp = $thisline; &nextline();
        return &myerror("Unknown line in initial axioms, $thisline");
      }
   }
   return &myerror("INITIAL not terminated");
}

# ==============================================================================
# ==============================================================================
# Init systems file.

sub initsystemsfile {
  my $infilename  = '';
  my $system      = shift;
  &DEBUG("Entering systems file initialization...");
  return &myerror("No system defined")
    if !defined $system;
  return &myerror("System name bad ($system)")
    if $system !~ m/^([\d\w\.\+]+)$/;
  $system = $1;
  return &myerror("Unable to complete processing for system file.  $system")
    if ! &openinputfile($systemsdir . $system . '.txt');
  return &myerror("System's file doesn't start with system? $thisline")
    if $thisline ne '<SYSTEM>';
  return &myerror("Unable to get lines of system definition file")
    if ! &nextline();
  return &myerror("Unable to write systems info to file?")
    if ! &fileoutput('<SYSTEM>') || !&fileoutput("# ----  System: $system");

  &DEBUG("Doing sysfile copy...");
  return 0 if !print "<hr title=\"System\"><h1>System</h1>\n";
  while (defined $thisline) {
    # &DEBUG("init systems file processing $thisline");

    if ($thisline eq '</SYSTEM>') {
        return 0 if !&echoline();
        return 0 if !&fileoutput("<DERIVATION>");
        return &outputhtml("<hr title=\"Derivation\"><h1>Derivation</h1>");
    } 
    elsif ($thisline eq '<RULE>')    { return 0 if !&initrule()      }

    elsif ($thisline =~ m;^<BASE>(.*)</BASE>;) {
       $basesystem = $1;
       return 0 if !&finishline($thisline)
    }

    elsif ($thisline =~ m;^<NAME>(.*)</NAME>$;)  {
       return 0 if !print "<h1>System: $1</h1>\n<p>$1</p>\n"
                && !&finishline($thisline)
    }

    else {
      my $temp = $thisline; &nextline();
      return &myerror("Unknown item in systems file: $thisline\n");
    }
  }
  return &myerror('SYSTEM file didn\'t have end tag?');
}

# ==============================================================================
# Deal with systems file.

sub processsystemfile {
  my $choices   = shift; # Initial pass, or just echoing back out?
  my $item; my @list; my $op;
  # &DEBUG("Entering processsystemsfile...");
  return &myerror("Processsystem called on nonsystem, $thisline")
    if $thisline ne '<SYSTEM>';
  return 0 if !&nextline();
  while (defined $thisline) {

     if ($thisline eq '</SYSTEM>') {
       # &DEBUG("... Exiting processsystemsfile");
       return &nextline(); # ******** EXIT ***********
     }
     elsif ($thisline eq '<LINE>') { return 0 if !&processline($choices); next }
     elsif ($thisline eq '<RULE>') { return 0 if !&processrule();         next }
     elsif ($thisline =~ m;<BASE>([^<]+)</BASE>$;) {
       $basesystem = $1;
       return 0 if !&nextline();
     }
     if ($thisline !~ m;^<(\w+)>;) { return 0 if !&nextline();            next }

     if ($1 eq 'NAME' || $1 eq 'XHDISPLAY' || $1 eq 'HDISPLAY'
      || $1 eq 'XPDISPLAY' || $1 eq 'PDISPLAY') {
         return 0 if !&nextline();

     } else {
       return &myerror("Undefined line in Process System file: $thisline");
     }
  }
  return &myerror("SYSTEM file processing not terminated correctly?");
}


# ==============================================================================
# Substitution of free variables.

use vars qw( %substitute );
%substitute = ();

sub partsubstitute {
   my $local  = ''; my $olddef;
   my $equation = shift;
   if (!ref $equation || 'ARRAY' ne ref $equation) {
      return $equation               if !exists $substitute{$equation};
      return $substitute{$equation};
   }
   my @result = ();
   my @expression = @$equation; 
   my $op = shift @expression;
   push @result, $op;
   if ($op eq 'FORALL' || $op eq 'EXISTS' || $op eq 'LAMBDA') {
      $local = shift @expression;
      push @result, $local;
      if ($local ne '') { # don't substitute bound variables.
         if (!exists $substitute{$local}) {
            $local = ''
         } else {
            $olddef = $substitute{$local};
            delete $substitute{$local};
         }
      }
   }

   my $item;
   foreach $item (@expression) { push @result, &partsubstitute($item) }

   # But restore substitution when we leave the scope.
   $substitute{$local} = $olddef if $local ne '';
   return [@result];
}

sub fullsubstitute {
   my ($list, $equation) = @_;
   my @vars = keys %$list;
   # &DEBUG("Variables in full substitute: @vars");
   %substitute = %$list;; my $item;
   # foreach $item (@vars) { &DEBUG("Ready to sub $item as ".
   #         &expressiontoexternal($substitute{$item}))
   # }
   return &partsubstitute($equation);
}

# ==============================================================================
# ==============================================================================
# Support routines.
# ==============================================================================
# ==============================================================================

# Is this theorem on file?

sub checkfile {
  my $goal  = shift;
  my $which = shift;
  $goal = '=> ' . $goal;

  if (!defined $which || $which eq '') { return 0 }
  my $file = $systemsdir . $which;
  return 0 if !-e $file;
  return &myerror("Theorem check file $file could not be obtained.")
    if !&openinputfile($file);

  &DEBUG("In checkfile, looking at file $which, equation $goal");
  # *** This desparately needs rethink.
  # *** It should also probably be a database lookup.
  while (defined $thisline) {
     if ($thisline eq $goal) {
        # Clear other matching theorems.
        while (defined $thisline && $thisline =~ m/^=>/) {
          if (!&nextline()) { &closein(); return 0 }
        }
        $thisline = '' if !defined $thisline;
        my $nocontinue =  $thisline =~ m/NOCONTINUE/i;
        if (!&nextline()) { &closein(); return 0 }
        # Prefix?
        print "\n<hr title=\"GOAL ANALYSIS\"><H2>GOAL ANALYSIS</H2>\n";
        # Dump text;
        while (defined $thisline && $thisline !~ m/^=>/) {
          if ($thisline =~ m/REPLACE\:\s*(.+)$/) { $goal = $1 }
          while ($thisline =~ m;^(.*)<EQUATION>(.*)</EQUATION>(.*)$;i) {
             my ($pre, $eq, $post) = ($1, $2, $3);
             $thisline = $pre . &internaltoexternal($eq) . $post;
          }
          print $thisline, "\n";
          if (!&nextline()) { &closein(); return 0 }
        }
        if ($nocontinue) {
           return &closein(); 
        }
     } elsif (!&nextline()) { &closein(); return 0 }
  }
  &closein();
  return 0;
}

# ==============================================================================
# ==============================================================================
# Process goal line.

sub processgoal {
  my $given = $thisline;  return 0 if !&nextline();
  return &myerror("No text for processgoal?") if !defined $given;  
  return &myerror("processgoal processing non-goal line: $thisline")
    if ($given !~ m;^<GOAL>;) || ($given !~ m;</GOAL>$;) ;
  $goal  = $1 if $given =~ m;<EQN>([^<]+)</EQN>; ;
  $cgoal = $1 if $given =~ m;<CANNON>([^<]+)</CANNON>; ;
  return $goal ne '' || $cgoal ne '';
}

# ==============================================================================
# Reprocess

sub processstatusfile {
  my $givechoices = shift; $givechoices = 0 if !defined $givechoices;
  my $givenstate  = shift;
  if (!defined $givenstate) {
     $givenstate = $state;
  } else {
     $state = $givenstate;
     $statefile = $mytemp . $state;
  }
  # &DEBUG("Processing status file...");
  return &myerror("no name for saved state?")
    if !defined $statefile;
  return &myerror("saved state name was empty?")
    if $statefile eq '';
  return &myerror("Could not process status file.")
    if !&openinputfile($statefile);
  return &myerror("No initial line in file.")
    if !defined $thisline;
  #&DEBUG("First line is processing status file is $thisline");

  my $item; my @list; my $op;
  while (defined $thisline) {

     #&DEBUG("processstatusfile processing line: $thisline");
     if    ($thisline eq '<NOTATION>')  { return 0 if !&processnotationsfile() }
     elsif ($thisline eq '<SYSTEM>')    { return 0 if !&processsystemfile() }
     elsif ($thisline eq '<OFFER>')     { return 0 if !&nextline()          }
     elsif ($thisline eq '<SOFFER>')    { return 0 if !&nextline()          }
     elsif ($thisline eq '<LINE>')      { return 0 if !&processline()       }
     elsif ($thisline eq '<DERIVATION>')
                                        { return 0 if !&nextline()          }
     elsif ($thisline eq '</DERIVATION>')
                                        { return 0 if !&nextline()          }
     elsif ($thisline eq '<STATE>')     { return 0 if !&nextline()          }
     elsif ($thisline =~ m;^<GOAL>;)    { return 0 if !&processgoal()       }
     elsif ($thisline =~ m;^<PDISPLAY>;)
                                        { return 0 if !&nextline()          }
     elsif ($thisline =~ m;^<XPDISPLAY>;)
                                        { return 0 if !&nextline()          }
     elsif ($thisline =~ m;^<HDISPLAY>;)
                                        { return 0 if !&nextline()          }
     elsif ($thisline =~ m;^<XHDISPLAY>;)
                                        { return 0 if !&nextline()          }

     else {
       return &myerror("Undefined line in status: $thisline");
     }
  } 
  # &DEBUG("Processstatusfile returning...");
  return &closein();
}

# =====================================================================
# =====================================================================
# Free variables.

use vars qw ( %freevars ); %freevars = (); # Global only to subroutine below.

# Given an expression, set %freevars to the free variables in it.
# and any substitution restrictions.
sub freevarsraw { # Defined on structure 
  my ($item, @environment) = @_;
  if (!ref $item) {
     return if grep ($item eq $_, @environment); # Bound variable;
     my $varlist;
     if (defined $freevars{$item}) { $varlist = $freevars{$item} }
     else                          { $varlist = [] }
     my $test;
     foreach $test (@environment) { # If it is free, does it have restrictions?
        &DEBUG("Checking $test for restrictions");
        push @$varlist, $test if !grep ($test eq $_, @$varlist);
        &DEBUG("Gives: @$varlist");
     }
     $freevars{$item} = $varlist;
     return;
  }
  my @expression = @$item;
  my $op = shift @expression;
  push @environment, shift @expression
    if $op eq 'FORALL' || $op eq 'EXISTS' || $op eq 'LAMBDA';
  foreach $item (@expression) { &freevarsraw($item, @environment) }
  pop @environment
    if $op eq 'FORALL' || $op eq 'EXISTS' || $op eq 'LAMBDA';
  return;
}

sub freevars {
 %freevars = ();
 &freevarsraw(&internaltoexpression(@_));
 my @result = ();
 my $item;
 foreach $item (sort(keys %freevars)) {
     my $resolve = $freevars{$item};
     if (@$resolve > 0) {
        push @result, "$item:@$resolve";
     } else {
        push @result, $item;
     }
 }
 return @result;
}

# Get ALL variables in the expression.
use vars qw( @allvars ); @allvars = (); # Global only to subroutine below.
sub allvarsraw { # List of all variables used (free or otherwise) in expression
   my $item = shift;
   if (!ref $item) {
      push @allvars, $item if !grep ($item eq $_, @allvars);
      return;
   }
   my ($op, @arguments) = @$item;
   my $argument;
   foreach $argument (@arguments) {
      &allvarsraw($argument);
   }
}
sub allvars {
@allvars = ();
&allvarsraw(@_);
return @allvars;
}

# ==============================================================================
# Compare forms.

use vars qw( %mapping );
%mapping = ();

sub compareforms {
   my ($form, $test, $firstorder) = @_; $firstorder = 1 if !defined $firstorder;
   if (!ref $form) {
      if (!ref $test) { $test = &expressiontointernal($test) }
      if (!defined $mapping{$form}) { $mapping{$form} = $test; return 1 }
      else { return $mapping{$form} eq $test } 
   } elsif (!ref $test) { # Form is a structure and test is not?
     return 0;
   }
   my @theform = @$form; my @thetest = @$test;
   if ($firstorder) { # first order logic can't form match predicates,operators.
      $form = shift @theform; $test = shift @thetest;
      return 0 if $form ne $test; # but they must be exactly equal.
   }
   my $result = 1; # Be optimistic.
   while ($result) { # Compare corresponding items.
      $form = shift @theform; $test = shift @thetest;
      return !defined $form if !defined $test;
      return 0 if (!defined $form) &&  defined $test;
      $result = &compareforms ($form, $test);
   }
   return $result;
}

sub fullcompareforms {
   %mapping = ();
   return &compareforms(@_);
}

# ==============================================================================
# Make true canonical form.
# we need a true canonical form for looking things up in the index.
#
# FOO + FORALL(Z,A+Z) + HACK
# =>
# p + FORALL(x,q+x) + r
# # # Subtlety: The doesn't have to match substitution restrictions because
# # # those variables they would confict with are also being renamed.

use vars qw(%FORMVARS @preferedfree @preferedbound $countfree $countbound);

# Next bound variable name.
sub nextbound {
  if (@preferedbound>0) { return shift @preferedbound }
  else { $countbound++; return 'boundvar'.$countbound }
}
# Next free variable name.
sub nextfree {
  if (@preferedfree>0) { return shift @preferedfree }
  else { $countfree ++; return 'freevar' . $countfree } 
}

# Actually form the connonical form.
sub rawcanonicalform {
  my $item      = shift;
  $item = $$item if ref $item && 'ARRAY' ne ref $item;
  if (!ref $item) {
     if (defined $constant{$item})    { return $item }
     elsif (defined $FORMVARS{$item}) { return $FORMVARS{$item} }
     else {
       my $newvar = &nextfree();
       $FORMVARS{$item} = $newvar;
                                        return $newvar;
     }
  }
  my ($op, @list) = @$item;
  return [$op] if @list == 0;
  my @result = ($op); 

  my $olditem; my $oldvalue;
  if ($op eq 'FORALL' || $op eq 'EXISTS' || $op eq 'LAMBDA') {
    $olditem = shift @list;
    $oldvalue = $FORMVARS{$olditem};
    my $newvalue = &nextbound();
    $FORMVARS{$olditem} = $newvalue;
    push @result, $newvalue;
  }

  foreach $item (@list) { push @result, &rawcanonicalform($item) }

  if (defined $olditem) { $FORMVARS{$olditem} = $oldvalue }
  return [@result];
}

# Initialize for new expression, and do it.
sub fullcanonicalform {
$countfree  = 0; $countbound = 0;
@preferedfree  = qw( p q r s t u v w pa qa ra sa ta ua va wa );
@preferedbound = qw( x y z xa ya za xb yb yc xd yd zd );
%FORMVARS = ();
return &rawcanonicalform(@_);
}

sub storablecanonicalform {
   return &expressiontointernal(&fullcanonicalform(&internaltoexpression(@_)));
}

# ==============================================================================
# give selection from a file.

sub fileselection {
  my $filename = shift; # File to open.
  my $whatever = shift; # Name of what's in it.
  my $tellprog = shift; # Name as far as the program in concerned.
  my $todo     = shift; # What is the next state to process?
  my @choices = ();

  return &myerror("Bad filename to Summary file selection?")
    if !defined $filename || $filename eq '';
  return &myerror("Unable to get $whatever summary file $filename ($!)")
    if !&openinputfile($filename);

  while (defined $thisline) {
     push @choices, $thisline;
     return 0 if !&nextline();
  }
  return 0 if ! &closein();

  my $count = 0;
  return 0 if ! print "<form method=\"POST\" action=\"$programname\">\n";
  return 0 if $state ne '' && !print
           "<input type=\"HIDDEN\" name=\"STATE\" value=\"$state\">\n";
  return 0 if !print "<p>Select a $whatever:</p>\n";

  my $first = 1;
  return &myerror("no $whatever defined?") if @choices == 0;
  foreach $item (@choices) {
    $count ++;
    my ($newfilename, $filetext) = $item =~ m/^(\S+)\s+(.*)$/;
    return 0 if !print "<br><input type=\"RADIO\" name=\"$tellprog\" ",
                       "value=\"$newfilename\" tabindex=\"$count\"";
    return 0 if $first && !print " CHECKED"; $first = 0;
    return 0 if !print ">$filetext\n";
  }

  $count ++;
  return 0 if !print "<p><input type=\"SUBMIT\" name=\"$todo\" "
                   , "value=\"Continue\" tabindex=\"$count\"></p>";
  $count++;
  return print "<input type=\"RESET\" name=\"RESET\" tabindex=\"$count\">\n",
               "</FORM>\n";
}

# ==============================================================================
# Initial welcome message.

sub dowelcome {
return print <<WELCOME;

<hr title="Disclaimer"><h1>-- Debugging Disclaimer --</h1>
<p>This is a program currently being debugged... Therefore logging
   of any or all the input may be being done at any time.  And any
   or all of the data may be used to improve the program, provide
   stock proofs, etc.</p>
<p>If you object to this, don't use this program.</p>
<p>No waranties are made or implied in this program.  It may
   not live up to any of it's documentation. (But if you find
   this true, tell me...</p>
<p>This program may change at any time... Don't count on features
   to look the same from day to day.</p>
<p>Don't count on features that worked yesterday continuing to
   work today.</p>
<p>The debugging output code puts out graphic trees...  If you are
   trying to use a screen reader this will mess you up big time.
   Hopefully they will be removed when this stops being a prerelease
   copy.</p>
<p><b>TRYING TO UNDO A STEP BY PRESSING THE "BACK" BUTTON ON YOUR 
   BROWSER WILL MAKE THE PROGRAM VERY SICK.</b></p>

<hr title="Welcome"><h1>Welcome</h1>
<p>There are any number of calculators that do the grunge work
   of dealing with numbers.  There are not very many calculators
   that do any of the grunge work of dealing with logical proofs.</p>
<p>Much of the work of doing a proof is not in deciding what to
   do, but is in the mechanics of doing things like uniform
   substitution...  jobs that the computer is well suited for.</p>
<p>This program is my effort in the direction of making Axiom
   based proofs easier to produce, and axiom based systems
   easier to investigate.</p>
<p>I am seriously looking for feedback on this effort, and am
   interested in hearing comments (good or bad) that you
   may have about it.</p>
<p>Every program has compromises.  This has way too many.</p>
<p>No Kangaroos or anteaters were killed in the making of this program.</p>
<p>No spiders or visigoths were allowed to help program this.</p>

WELCOME
}

# ==============================================================================
# ==============================================================================
# Routines to dispatch to.
# ==============================================================================
# GETNOTATION

sub getnotation {

   return 0 if !print <<GETNOTATION;

<hr title="Select Notation"><h1>Select Notation</h1>
<p>There are many different logic notational systems in use, so
   you will have to choose one.</p>
<p>This list is skimpy, but I hope to have it grow later.</p>
<p>If you don't know what what to pick, the default choice is 
   probably best.</p>
<p>**** ONLY THE FIRST CHOICE HAS BEEN EXTENSIVELY DEBUGGED *****</p>
GETNOTATION

   return &fileselection($notationsdir . 'summary',
                         'notations', 'NOTATION', 'GOTNOTATION');
}

# ==============================================================================
# GOTNOTATION

sub gotnotation {
  # copy notation.
  # Then on to:
  if ($state ne '') {
     # Later change this to update based on new notation.
     $state = '';
     return &myerror("Internal state already set in get notation? $state");
  }
  my $newstate = &uniquestatename();
  my $newstatefile = $mytemp . $newstate;

  return &myerror("Unable to open output file. ($!)[$newstatefile]")
    if !&openoutputfile($newstatefile);
  return &myerror("Unable to write to status file ($!)")
    if !&fileoutput("<STATE>") || !&fileoutput("# -- File: $newstatefile\n");
  return &myerror("Didn't finish initial notations processing.")
    if !&initnotationsfile($basenotation);
  return &myerror("Couldn't close output file.($!)")
    if !&closeout();
  return &myerror("Unable to set status file $newstatefile mode ($!)")
    if 0==chmod(0600, $newstatefile);

  $state = $newstate;
  $statefile = $newstatefile;
  return &getsystem();
}

# ==============================================================================
# GETSYSTEM

sub getsystem {
   return &myerror("No state availiable in GETSYSTEM")
     if $state eq '';

   return 0 if !print <<GETSYSTEM;

<hr title="Select System"><h1>Select System</h1>
<p>Since there is no one "proper" set of axioms to
   base logic on, you'll have to chose.</p>
<p>If you don't know what to pick, the default choice is probably best.</p>
GETSYSTEM

   return &fileselection($systemsdir.'summary','systems','SYSTEM','GOTSYSTEM');
}

# ==============================================================================
# GOTSYSTEM

sub gotsystem {
  # &DEBUG("GOTSYSTEM...");
  return &myerror("GOTSYSTEM called without valid state variable?")
    if $state eq '';
  return &myerror("Unable to recall notation from state file")
    if ! &processstatusfile(0); ### Should this be notations only????
  return &myerror("Unable to regain system state: $state")
    if ! &openoutputfile($statefile, 1);
  return &myerror("Didn't finish initial system processing.")
    if ! &initsystemsfile($basesystem);
  return &myerror("Didn't finish initial axioms processing?")
    if ! &initaxioms();
  return &myerror("Unable to close state file ($!)")
    if ! &closeout();
  return &myerror("Unable to close input file ($!)")
    if ! &closein();

  return &getgoal(); 
}

# ==============================================================================
# GETGOAL

sub getgoal {
  return &myerror("GETGOAL called without state variable?")
    if $state eq '';

  $showchoices = 0; # Don't let them get ahead of us.
  return print <<NEWGOAL;

<hr title="Set derivation goal">
<h1>What are you trying to prove?</h1>
<p>The program *may* be able to give better assistance if it
   knows what theorem you are working towards.</p>
<p>If you have some specific goal (as opposed to just randomly
   trying things) please put in in below.  If you have *NO* specific
   goal please LEAVE IT BLANK.  (Putting in a word such as "none" will
   cause it to think you are trying to prove "none" as a theorem.)</p>
<form method="post" action="$programname">
   <input type="hidden" name="STATE" value="$state">
   <br>Goal of this derivation: (if any) \
   <input type="TEXT" name="GOAL" size="60" maxlength="300"
       value="$goal" tabindex="1">
   <br><input type="submit" name="GOTGOAL" value="Continue" tabindex="2">
</FORM>
NEWGOAL
}

# ==============================================================================
# GOTGOAL

sub gotgoal {
  # &DEBUG("GOT GOAL entered");
  return 0 if !&processstatusfile(0); # Get notation stuff.
  # &DEBUG("GOT GOAL processed status file");

  return 0 if !defined $goal || $goal eq '';
  my $pgoal = &prephtmltext($goal); # Printable goal.

  &DEBUG("original goal: $goal");
  my $expression = &externaltoexpression($goal);
  &DEBUG("Parsed form:"); &printstructure($expression) if $doingdebug;

  if ($lasterror ne '') {
     &reporterror("Couldn't parse goal $lasterror");
     $goal = '';
     return &getgoal();
  } else {
    print "</H2>Goal: $pgoal</H2>\n";
    &printstructure($expression);
    print "<p><b>Goal: $pgoal</b></p>\n";
    my $canon = &fullcanonicalform($expression);
    &DEBUG("Internal form of canononicalization: " . 
          &expressiontointernal($canon) . "\n");
    &printstructure($canon) if $doingdebug;
    my $igoal   = &expressiontointernal($expression);
    my $icanon  = &expressiontointernal($canon);
  
    # Do file lookups...
  
    &DEBUG("Hunting for theorem match in $basesystem for $icanon");
    my $sysname =  $basesystem;
    if   (&checkfile($icanon, 'all.badnews')
       || &checkfile($icanon, 'all.known')
       || &checkfile($icanon, $sysname . '.badnews')
       || &checkfile($icanon, $sysname . '.known') 
       ) {
       &getgoal();
       $showchoices = 0;
       return 1;
    } elsif (&openoutputfile($statefile, 1) 
          && &fileoutput("<GOAL><PRINT>$pgoal</PRINT><EQN>$igoal</EQN>" .
                         "<CANNON>$icanon</CANNON></GOAL>")
          && &closeout()) {
       $showchoices = 1;
    }
  }
  return 0
}

# ==============================================================================
# SHOW

sub doshow { return &displaydisplays(1) }

# ==============================================================================
# SHOWCLEAN

sub doshowclean { return &displaydisplays(0) }

# ==============================================================================
# GOTSUB
# Process a uniform substitution.

sub dogotsub {
  my $base = $input{'BASE'};
  my $line = $input{'LINE'}; $line = '?' if !defined $line;
  my $varlist = $input{'VARS'};
  return &myerror("Substitution had no variables list?")
    if !defined $varlist;
  return &myerror("Substitution base not defined?")
    if !defined $base;
  return &myerror("Unable to reprocess status file?")
    if !&processstatusfile(0);
  return &myerror("Unable to load derivation substate?")
    if !&loadstate();
  my @vars = split(/\,/, $varlist);
  my %realvars = ();
  my $item;
  foreach $item (@vars) {
     if ($item =~ m;^([\w\d]+)\:(.*)$;) { $realvars{$1}    = $2 }
     else                               { $realvars{$item} = '' }
  }
  my %variables = (); my $problems = 0;
  my $variable; my $newvalue;
  foreach $variable (sort keys %realvars) { # which are variables?
     $newvalue = $input{$variable};
     next if !defined $newvalue;
     &DEBUG("SUB: Processing $variable => $newvalue");
     next if $newvalue eq '';        # some users are confused.
     next if $variable eq $newvalue; # Null substitution.
     next if $variable =~ m;^\s+$;;
     my $parse = &externaltoexpression($newvalue);
     #&DEBUG("Parse of $newvalue is");
     #&printstructure($parse) if defined $parse;
     if ($lasterror ne '') {
        &reporterror ("Couldn't parse $newvalue [$lasterror]");
        $problems = 1;
        next;
     }
     my @restrictions = ();
     if ($realvars{$variable} eq '') { @restrictions = () }
     else { @restrictions = split(/,/, $realvars{$variable}) }
     if (@restrictions) {
        &DEBUG("Checking restrictions on $variable. (@restrictions)");
        my @thevars = &allvars($parse); # What do we have?
        &DEBUG("-- We have variables: @thevars");
        my $test;
        foreach $test (@restrictions) {
           &DEBUG("---- checking $test");
           if (grep ($test eq $_, @thevars)) {
              &reporterror("$variable may not have $test substituted for it, because it includes one of \"@thevars\" which are bond");
              $problems = 1;
           }
        }
        next if $problems;
     }
     $variables {$variable} = $parse;
  }
  if (%variables) {
     # Prepare the new line.
     # &DEBUG("Substitution ready on $base");
     my $item; my $justification = "$line,US";
     foreach $item (sort (keys(%variables))) {
        # &DEBUG("   $item => $input{$item}");
        $justification .= ", $input{$item}/$item";
     }
     # &DEBUG("Justification became: $justification");
   
     my $result = &fullsubstitute(\%variables, &internaltoexpression($base));
     # &DEBUG("After substitution\n"); &printstructure ($result);
     return &reporterror
          ("This substitution just reproduces line $have{$result}")
       if defined $have{$result};
     return &myerror("Can't reopen state file to append substitution?")
       if !&openoutputfile($statefile, 1);
     return &myerror("Can't add $newvalue to list?")
       if !&addnewline(&expressiontointernal($result), $justification);
     return &myerror ("Can't close file after substitution?")
       if !&closeout();
     # return &doshow;
  } else {
    &reporterror("No non-trivial substitutions given?");
  }
  return 0;
}

# ==============================================================================
# GOTNEWLINE

sub dogotnewline {
  my $which = $input{'OFFNUM'};
  return &myerror("NO derivation offer number?") if !defined $which;
  my $offer = '';
  return &myerror("Unable to reprocess status file?")
    if !&processstatusfile(0);
  return &myerror("Unable to determine derivation sub state?")
    if !&loadstate();
  return &myerror("Unable to open status file $!")
    if !&openinputfile($statefile);
  # &DEBUG("Looking for offer $which");
  while (defined $thisline) {
    # &DEBUG("checking for offer, $thisline");
    if ($thisline !~ m;<OFFER NUMBER=\"(\d+)\">; || $1 ne $which) {
       return 0 if !&nextline(1);
       next;
    }
    # &DEBUG("Got the offer");
    $offer = $thisline; 
    last;
  }
  return &myerror("Unable to close status file $!")
    if !&closein();
  return &myerror("Offer not found???") if $offer eq '';
  my($eqn, $just)= $offer =~ m;<EQN>([^,]+)</EQN>.*<JUST>([^<]+)</JUST>;;
  return &myerror("Malformed offer: $thisline") if !defined $just; 
  return &myerror("Couldn't update output file $!")
    if !&openoutputfile($statefile, 1);
  return 0 if !&addnewline($eqn, $just)
           || !&closeout();
  return 1;
}

# ==============================================================================
# Place holder for unwritten code.

sub placeholder {
   my $for = shift;
   &displaydisplays(1) if print "\n<hr title=\"Unimplemented\">",
                         "<h1>Unimplemented placeholder code for $for</h1>\n";
   return 0;
}

# GOTASSSUMPTION
sub dogotassumption { return &placeholder('dogotassumption') }

# GOTDISCHARGE
sub dogotdischarge { return &placeholder('dogotdischarge') }

# GOTUNDO
sub dogotundo      { return &placeholder('dogotundo') }

# SUBGOALS
sub getsubgoal     { return &placeholder('getsubgoal') }
sub gotsubgoal     { return &placeholder('gotsubgoal') }

# ==============================================================================
# State table and dispatch loop.
# ==============================================================================

# Actual code main loop.

sub initialdispatch {
# &DEBUG("Got to initial dispatch");
  if    (defined $input {'WELCOME'}     ) { return &dowelcome()       }
  elsif (defined $input {'GETNOTATION'} ) { return &getnotation()     }
  elsif (defined $input {'GOTNOTATION'} ) { return &gotnotation()     }
  elsif (defined $input {'NOTATION'}    ) { return &gotnotation()     }
  elsif (defined $input {'GETSYSTEM'}   ) { return &getsystem()       }
  elsif (defined $input {'GOTSYSTEM'}   ) { return &gotsystem()       }
  elsif (defined $input {'SYSTEM'}      ) { return &gotsystem()       }
  elsif (defined $input {'GETGOAL'}     ) { return &getgoal()         }
  elsif (defined $input {'GOTGOAL'}     ) { return &gotgoal()         }
  elsif (defined $input {'GOAL'}        ) { return &gotgoal()         }
  elsif (defined $input {'GETSUBGOAL'}  ) { return &getsubgoal()      }
  elsif (defined $input {'GOTSUBGOAL'}  ) { return &gotsubgoal()      }
  elsif (defined $input {'SUBGOAL'}     ) { return &gotsubgoal()      }
  elsif (defined $input {'SHOW'}        ) { return &doshow()          }
  elsif (defined $input {'SHOWCLEAN'}   ) { return &doshowclean()     }
  elsif (defined $input {'GOTNEWLINE'}  ) { return &dogotnewline()    }
  elsif (defined $input {'OFFNUM'}      ) { return &dogotnewline()    }
  elsif (defined $input {'GOTSUB'}      ) { return &dogotsub()        }
  elsif (defined $input {'BASE'}        ) { return &dogotsub()        }
  elsif (defined $input {'GOTASSUMP'}   ) { return &dogotassumption() }
  elsif (defined $input {'ASSUMPTION'}  ) { return &dogotassumption() }
  elsif (defined $input {'GOTDISCHARGE'}) { return &dogotdischarge()  }
  elsif (defined $input {'DISCHARGE'}   ) { return &dogotdischarge()  }
  elsif (defined $input {'UNDO'}        ) { return &dogotundo()       }
  else {
       return &myerror("No recognised state transition???")
          if defined $input {'STATE'};
       $input {'WELCOME'} = 'WELCOME';
       return 0 if !&dowelcome;
       return &getnotation;
  }
}

&initialdispatch(); # Take care of command related text.
&displaydisplays($showchoices) if  $state ne ''
                               && !defined $input{'GETSYSTEM'}
                               && !defined $input{'GETNOTATION'}
                               && !defined $input{'GOTNOTATION'}
                               && !defined $input{'SHOWCLEAN'}
                               && !defined $input{'SHOW'};


# =============================================================================
# Additions to the HTML trailer stuff.
# =============================================================================
# Extra navigation items for trailer..

sub doprogramcommands {
return print "<li><a href=\"$programname\">Start Over</a></li>\n"
      if $state ne '';
return 1;
}

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

exit !&htmltrailers(); # Final closing HTML trailers.
# We exit 0 if all ok, 1 if problems.

# =============================================================================
# ======================== END OF PROGRAM =====================================
# =============================================================================

Go to ...


This page is http://www.cc.utah.edu/~nahaj/logic/calculate/logic.perl.html
© Copyright 2003 by John Halleck, All Rights Reserved.
This snapshot was last modified on November 3rd, 2006