#!/usr/bin/php
<?php 
require_once("TarskiTheorems.php");
//_______________________________________________________________

function break80($x)
// return an array of lines each of which is at most 80 characters, breaking a clause
//  at literal boundaries.  Append a period to the last line.
{  $t = explode("|",$x);
   $ans = array();
   $line = "";
   foreach($t as $literal)
      { if (strlen($literal) + strlen($line) < 77)
	        { if($line == "")
		         $line = $literal;
		      else
		         $line = $line . "|" . $literal;
		    }
	   else
	       { $ans[] = $line;   // will hang if any literal is longer than 77 characters
		     $line = "| $literal";  // put this literal on the next line
		   }
	  }
	$ans[] = $line . ".";
	return $ans;
}
//_______________________________________________________________

function InputFileAsArray($t, $diagrams, $sos, $settings, $cases)
// $t should be a member of $TarskiTheorems
// Generate the lines of an input file for proving $t
// and return an array of strings containing those lines.
// Make sure no line exceeds 80 characters.
// include the diagram if $diagrams is not false.
// include the members of $t->Cases if it is an array
 
{   global $NamedAxioms;
	global $NamedDefinitions;
	global $TarskiTermDefinitions;
	global $TarskiTheorems;
	global $NamedTheorems;
    $dflag = 0;   // set if Satz7.7 is used, so we can add it also as demodulator
	$lines = array();  // build the file contents by adding to this array
	$lines[] = "% This file was mechanically generated";
	$lines[] = "% from the master list in TarskiTheorems.php.";
	$lines[] = "% Tarski-Szmielew's axiom system is used."; 
	$lines[] = "% T is Tarski's B,  non-strict betweenness.";
	$lines[] = "% E is equidistance.";
	$lines[] = "% Names for the axioms follow the book SST";
	$lines[] = "% by Schwabhäuser, Szmielew, and Tarski.";
	$lines[] = "% This file attempts to prove " . $t->name . ".";
	$lines[] = "";
	foreach($settings as $line)
	    $lines[] = $line;
	$lines[] = "";
	$lines[] =  $sos ? "list(sos)." : "list(usable).";
	// next list the relevant axioms */
	$chapterName = get_chapter($t->name);
	$axioms = axioms_needed($chapterName, $t->name);
	foreach($axioms as $axiom)
	   { $lines[] = "% Following is axiom " . $axiom;
		 if($axiom == "A1" || $axiom == "A2" || $axiom == "A3" || $axiom == "A6")
		     { $lines[] = $NamedAxioms[$axiom]->PositiveForm . ".";
			 }
		 else if($axiom == "A5"  || $axiom =="A9")  // break it
		    { $a = break80($NamedAxioms[$axiom]->PositiveForm);
			  foreach($a as $line)
			     { $lines[] = $line;
				 }
			}
		 else if($axiom == "A4" || $axiom == "A7")
		     {  $lines[] = $NamedAxioms[$axiom . "-i"]->PositiveForm . ".";
				$lines[] = $NamedAxioms[$axiom . "-ii"]->PositiveForm . ".";
			 }
		 else  // axioms 8 and 10 have three parts
	         {  $lines[] = $NamedAxioms[$axiom . "-i"]->PositiveForm . ".";
				$lines[] = $NamedAxioms[$axiom . "-ii"]->PositiveForm . ".";
				$lines[] = $NamedAxioms[$axiom . "-iii"]->PositiveForm . ".";
			 }
	   }
	$lines[] = "";
   // OK, finished with axioms, now for the theorems.
    foreach($TarskiTheorems as $alreadyproved)
	   { if($alreadyproved->name == $t->name)
		     break;  // done writing theorems
		 $lines[] = "% Following is " . $alreadyproved->name;
		 $ell = $alreadyproved->PositiveForm;
		 foreach($ell as $q)
		    { $a = break80($q);
	 	 	  foreach($a as $x)
		    	{ $lines[] = $x;
				}
			}
		if($alreadyproved->name == "Satz7.7")
			{ $dflag = 1;
			}
	   }
	// OK, finished with the theorems, now for the definitions
	if($chapterName != "2" && $chapterName != 3) 
	    { $lines[] = "% Following defines the function insert";
		  $lines[] = $TarskiTermDefinitions['insert'] . ".";
		  $definitions = definitions_needed($chapterName);  // an array of names of definitions
	 	  foreach($definitions as $dname)
			{ $d = $NamedDefinitions[$dname];
			  $lines[] = "% Following is " . $dname;
			  foreach($d->LeftToRight as $clause)
				{ if(strlen($clause) < 78)
					 $lines[] = $clause . ".";
				  else
				     {  $b = break80($clause);
					    foreach($b as $z)
							{ $lines[] = $z;
							}
					}
				}
			  foreach($d->RightToLeft as $clause)
			    { if(strlen($clause) < 78)
				     $lines[] = $clause . ".";
				  else
					 {  $b = break80($clause);
						foreach($b as $z)
							{ $lines[] = $z;
							}	   
					}
				}
			}
		}
	$lines[] = "end_of_list.";  // that is, of list(usable)
	$lines[] = "";
	if($dflag == 1)
	   { // then use Satz7.7 as demodulator too
		 $lines[] = "list(demodulators).";
		 $lines[] = "% Following is Satz 7.7, the only theorem in SST that is an equality."; 
		 $lines[] = $NamedTheorems["Satz7.7"]->PositiveForm[0] . ".";
		 $lines[] = "end_of_list.";
		 $lines[] = "";
	   }
	//  OK,  onwards to this theorem
	$lines[] = "list(sos).";
	$lines[] = "% Following is the negated form of " . $t->name;
	$a = $t->NegatedForm;
	foreach($a as $line)
	   { if(strlen($line) < 79)
		     $lines[] = $line  . ".";
		 else
		    { $b = break80($line);
			  foreach($b as $z)
			      { $lines[] = $z;
				  }
			}
	
	   }
	if($diagrams && $t->Diagram != "")
	   { $lines[] = "% Following is the diagram:";
		 $diagram = $t->Diagram;
		 foreach($diagram as $line)
		    { $lines[] = $line . ".";;
			}
		}
	if($cases && $t->Cases != "")  // then $t->Cases should be an  array
	   { $lines[] = "% Following are tautologies:";
		 $tautologies= $t->Cases;
		 foreach($tautologies as $line)
		    { $lines[] = $line . ".";;
			}
		}
	$lines[] = "end_of_list.";   //  end of list(sos).
	if($diagrams && $t->Diagram != "")
		{ $lines[] = "";
		  $lines[] = "list(demodulators).";
		  $diagram = $t->Diagram;
		  foreach($diagram as $line)
			 { $temp = explode('=', $line);
				if(!is_array($temp) || count($temp) != 2)
				   { echo "error in diagram of "; echo $t->name; echo "\n";
				   }
			   $lines[] = trim($temp[1]) . " = " . trim($temp[0]) . ".";
			 }
		  // in at least one case (Lemma 12.11-case2) we need to make a demodulator from an item in list(sos).
		  // We also need this in Satz12.11-case1,  where there are several demodulators to make.
          foreach($t->NegatedForm as $line)
			{ if( !strstr($line, "|") && !strstr($line, "!=") && strstr($line, "="))
				  { $temp = explode('=', $line);
					$left = trim($temp[0]);
					$right = trim($temp[1]);
					if(strlen($left) <= 2 
					   && strstr($right,"(")    // so don't introduce a demodulator of one atom to another
					  )
						{ $lines[] = $right. " = " . $left . ".";
						}
				  }
			 }	
		  $lines[] = "end_of_list."; // end of list(demodulators)
		}
	return $lines;
}
//_______________________________________________________________

function TheoremsByChapter( $chapter)
// return an array of all theorems from the specified chapter
{ $ans = array();
  global $TarskiTheorems;
  foreach($TarskiTheorems as $t)
	{ $c = get_chapter($t->name);
	  if($c == $chapter)
		 $ans[] = $t;
	}
  return $ans;
}
 
//_______________________________________________________________
function array_to_file($filename, $directory, $array)
// open the file, write the strings in $array (which is an array of strings)
// one string per line, and close the file.  Put the file in the specified
// directory.  Create the directory and/or file if they don't exist.  Overwrite
// the file if it does exist.
{ if(!file_exists($directory))
	 mkdir($directory);
  $fp = fopen($directory . "/" . $filename, 'w');
  foreach($array as $x)
    { fwrite($fp, $x . "\n");
	}
  fclose($fp);
}
//_______________________________________________________________
function WriteInputFile($theorem, $directory, $diagrams, $settings, $sos = false, $cases = false)
// generate and write to the specified directory an input file for the specified theorem.
// $settings is an array of legal Otter commands including a period at the end of each line.
// use diagrams if $diagrams is not false. 
// if $sos is specified, put everything in list(sos) and have an empty list(usable).

{ $filename = $theorem->name . ".in";
  $lines = InputFileAsArray($theorem, $diagrams, $sos, $settings, $cases);
  array_to_file($filename, $directory, $lines);
}
//_______________________________________________________________
function InputFilesByChapter($chapter, $directory, $diagrams, $settings, $sos = false, $cases = false)
/* Write the input files for the specified chapter to the specified directory,
   using diagrams if $diagrams is not false, 
   and return an array of the filenames.
   if $sos is specified, put everything in list(sos) and have an empty list(usable).
*/
{ $theorems = TheoremsByChapter($chapter);
  $ans = array();
  foreach($theorems as $t)
	 { WriteInputFile($t, $directory, $diagrams, $settings,  $sos, $cases);
	   $ans[] = $t->name;
	 }
  return $ans;
}
//_________________________________________________________________
function GetProofFromOutputFile($theorem_name, $directory = "./")
// return an array containing the proof from the output file specified (without .out)
// If that file doesn't exist or doesn't contain a proof, return false.
{ $path = $directory . "/" . $theorem_name . ".out";
  if(!file_exists($path))
      { echo "File $path does not exist";
	    return false;
	  }
  $fp = fopen($path, 'r');
  $contents = file($path);   // it might be a huge file but try it
  $ans = array();
  $flag = 0;
  foreach($contents as $line)
	  { if (strstr($line, "Length of proof"))  // first line of proof 
		    { $flag = 1;
			}
		if($flag == 1)
		    { $line = trim($line); // remove newline at end
			  // there are a couple of blank lines near the beginning 
			  if($line == "")
			     $line = " ";  // at least one character
			  $ans[] = $line;	  
			}
		if($flag == 1 && strstr($line, "\$F."))  // last line of proof
		    break;
	  }
	fclose($fp);
	if($flag == 0)
	   { echo "No proof in file $path\n";
		 return false;
	   } 
	return $ans;
}

//_________________________________________________________________
function WriteProofFile($theorem_name, $outdir, $proofdir)
// read the outputfile from $outdir, write the .prf file to $proofdir
{ $proof = GetProofFromOutputFile($theorem_name, $outdir);
  if(! is_array($proof))
     { echo "Proof not found\n";
	   return false;
	 }
  if(! file_exists( $proofdir))
     { echo "$proofdir allegedly does not exist.";
	   die();
     } 
  $proof_file = $proofdir . "/" . $theorem_name. ".prf";
  $fp = fopen($proof_file, "w");  
  if( !$fp) 
     { echo "Could not open $proof_file\n";
	   die(); // return false;
	 } 
  foreach($proof as $line)
      fwrite($fp, $line . "\n");
  fclose($fp);
  return true;
}
//_________________________________________________________________
function GetHintsFromProof($proof)
// $proof is an array containing a proof
// return  an array of hints corresponding to the steps of this proof
{ $ans = array();
  foreach($proof as $proofline)
	{ if(strstr($proofline, "[]"))
		continue;
	  $begin = strpos($proofline,"]");
	  if(!is_numeric($begin))
	     continue;
	  $proofline = substr($proofline, $begin+1);
	  $period = strrpos($proofline,".");
	  if(!is_numeric($period))
		 echo "Error: period expected in proof lines.\n";
	  $clause = trim(substr($proofline,0,$period) . ".");
	  if($clause != "\$F.")
	     $ans[] = $clause;	 
	}
  return $ans;
} 
//_________________________________________________________________
function InsertHintsIntoInputFile($theorem_name, $outdir, $indir)
// Get hints from the proof in the .out  file or .prf file found in directory $outdir,
// and insert them in list(hints) in the input file
// if anything goes wrong return false; else return true.
{ // are we going to use a .prf or a .out file?
  $outfile = $outdir . "/" . $theorem_name . ".out";
  $proof_file = $outdir . "/" . $theorem_name . ".prf";
  if(file_exists($proof_file))
      { $proof = file($proof_file);
	    echo "getting hints from $proof_file\n";
	  }
  else
      { echo "Proof file $proof_file does not exist.  Will try to get hints from the output file $outdir.$theorem_name .out instead.";
	    $proof = GetProofFromOutputFile($theorem_name , $outdir);
	  }
  if(! is_array($proof))
     { echo "Could not get proof from outputfile $outdir.$theorem_name.out.\n";
	   return false;
	 }
 $hints = GetHintsFromProof($proof);
  if(! is_array($hints))
	 { echo "Could not get hints from the proof of $theorem_name . $theorem_name .out.\n";
	   return false;
	 }  
  $infile = $indir . "/" . $theorem_name . ".in";
  $fp = fopen($infile, "a");  // write-only,  file pointer at end of file
  echo "Opening $infile\n"; 
  fwrite($fp, "\nlist(hints2).\n");
  if(!$fp)
     echo "failed to open $infile\n";
  foreach($hints as $clause)
     { //  echo $clause\n;
	   $err = fwrite($fp, $clause . "\n");
	   if($err == -1)
	      echo "File writing error\n";
	 }
  fwrite($fp, "end_of_list.\n");
  fclose($fp);
  return true;
}

//_________________________________________________________________
function simple_negate($x)
// return the negation of $x, formed by adding or canceling an inital negation sign,
// or by exchanging != and =.   It assumes that $x$ is already trimmed.
{  if($x[0] == '-')
	   return substr($x,1);
   if(strstr($x, "!="))
       return str_replace("!=", "=", $x);
   if(strstr($x, "="))
       return str_replace("=", "!=", $x); 
   return "-" . $x;
}
//_________________________________________________________________
function InsertSubformulaHintsIntoInputFile($theorem,  $indir)
// $theorem should be a member of $TarskiTheorems.
// Get hints consisting of all literals and their negations occurring in $t->NegatedForm
// and insert them in list(hints) in the input file
// if anything goes wrong return false; else return true.
{ $hints = array();
  foreach($theorem->NegatedForm as $clause)
     { $literals = explode("|", $clause);
	   foreach($literals as $x)
	      { $x = trim($x);
		    $hints[] =  $x . ".";
		    $hints[] = simple_negate($x) . ".";
		  }
	 }
  if(is_array($theorem->Diagram))
	 { foreach($theorem->Diagram as $clause)
		  { $literals = explode("|", $clause);
			foreach($literals as $x)
				{ $x = trim($x);
				  $hints[] =  $x . ".";
				  $hints[] = simple_negate($x) . ".";
				}
		  }
	 }
  $infile = $indir . "/" . $theorem->name . ".in";
  $fp = fopen($infile, "a");  // write-only,  file pointer at end of file
  echo "Opening $infile\n"; 
  fwrite($fp, "\nlist(hints2).\n");
  if(!$fp)
     echo "failed to open $infile\n";
  foreach($hints as $clause)
     { //  echo $clause\n;
	   $err = fwrite($fp, $clause . "\n");
	   if($err == -1)
	      echo "File writing error\n";
	 }
  fwrite($fp, "end_of_list.\n");
  fclose($fp);
  return true;
}

  
  
	  
  

   
?>