<?php

//Initialize the XML parser
$parser=xml_parser_create();

//Function to use at the start of an element
function start($parser,$element_name,$element_attrs) {

  global $i,$elementos;

  switch($element_name) {
//   case "RESULTS":
//     echo "-- Lista de Teoremas --<br />";
//     break; 
//   case "RESULT":
//     echo "Teorema<br/>";
//     break; 
//   case "USERNAME":
//     echo "Utilizador: ";
//     break; 
//  case "THEONAME":
//    echo "Nome do Teorema: ";
//     break; 
//  case "DESCRIPTION":
//    $elementos[$i] = "\begin{geothm}<br/>";
//    break; 
//   case "SHORTDESCRIPTION":
//     echo "Txt: ";
//     break; 
//   case "OBSERVATIONS":
//     echo "obs: ";
//     break; 
//   case "FIGCODE":
//     echo "Figura: <pre>";
//     break; 
  case "PROOFSCODE":
    $elementos[$i] = "";
    break; 
    //   case "BIBTEXENTRY":
//     echo "BibTeX: ";
//     break; 
  }
}

//Function to use at the end of an element
function stop($parser,$element_name) {

  global $i,$elementos;

  switch($element_name)    {
//   case "RESULT":
//     echo "<br/> - - - - - - - - <br/></br>";
//    break; 
//   case "USERNAME":
//     echo "<br/><br/> ";
//     break; 
//   case "THEONAME":
//     echo "<br/><br/>";
//     break; 
//  case "DESCRIPTION":
//    $elementos[$i].="<br/>\end{geothms}";
//    $i++;
//    break; 
//   case "SHORTDESCRIPTION":
//      echo "<br/><br/>";
//     break; 
//   case "OBSERVATIONS":
//      echo "<br/><br/>";
//      break; 
//   case "FIGCODE":
//      echo "</pre><br/><br/>";
//      break; 
  case "PROOFSCODE":
    $elementos[$i].="";
    $i++;
    break; 
//   case "BIBTEXENTRY":
//      echo "<br/><br/>";
//      break; 
  }
}

//Function to use when finding character data
function char($parser,$data)  {
  global $elementos,$i;
  //  echo $data;
  $elementos[$i].=$data;
}

//Specify element handler
xml_set_element_handler($parser,"start","stop");

//Specify data handler
xml_set_character_data_handler($parser,"char");

//Open XML file
$fp=fopen("geothms0301.xml","r");

//Read data
$i=0;
while ($data=fread($fp,4096))  {
  xml_parse($parser,$data,feof($fp)) or 
     die (sprintf("XML Error: %s at line %d", 
		  xml_error_string(xml_get_error_code($parser)),
		  xml_get_current_line_number($parser)));
 }

echo "Provas";
//print_r($elementos);

$aux=0;
while ($aux<=99) {
  //  print("<p>Nome Utilizador: ".$elementos[$aux]."</p>");
  //  $aux++;
  //  print("<p>Nome do Teorema: ".$elementos[$aux]."</p>");
  //  $aux++;


  echo "<br/>".$aux."<br/>";
  flush();
  //  exit;

  $vNameProofCode = 'proof'.$aux.'.code';
  $vNameProofCodeXML = 'proofCode'.$aux.'.xml';
  $vNameProofProof = 'proof'.$aux.'_proof.tex';
  $vNameProofErr = 'proof'.$aux.'.err';
  $vNameProofErrors = 'proof'.$aux.'.errors';
  $vNameProofPIC = 'proof'.$aux.'.pic';
  $vNameProofTeX = 'proof'.$aux.'.tex';
  $vNameProofDVI = 'proof'.$aux.'.dvi';
  $vNameProofPS = 'proof'.$aux.'.ps';
  $vNameProofPDF = 'proof'.$aux.'.pdf';
  $vNameProofProofXML = 'proof'.$aux.'_proof.xml';
  $vNameProofXML = 'proof'.$aux.'.xml';
  $vNameProofBZ2 = $vNameProofXML.'.bz2';
  
  $vNameProofAux = 'proof'.$aux.'.aux';
  $vNameProofCodeConv = 'proof'.$aux.'.codeconv';
  $vNameErrorsConv = 'proof'.$aux.'.errorsconv';
  
  // Escreve o ficheiro ".code" referente ao código
  ob_start();
  print $elementos[$aux]."\n";
  $prooffile=fopen($vNameProofCode,"w");
  fwrite($prooffile,ob_get_contents()); 
  fclose($prooffile); 
  ob_end_clean(); 
  
  ob_start();
  // aplica o  provador GCLCprover 1.0
  system("/usr/local/bin/gclc $vNameProofCode $vNameProofPIC  > $vNameProofErrors");
  // verifica se há erros
  system("grep Syntax $vNameProofErrors > $vNameProofErr");
  ob_end_clean(); 
  
  $filename = $vNameProofErr;
  
  // Vai verificar se houve erros ou não
  if  (file_exists($filename) and filesize($filename)>0) { // há erros 
    $file = fopen ($filename, "r");
    $contents = fread ($file, filesize ($filename));
    echo $contents;
    //system("rm proof.err");
    echo "<b>There are errors in the proof's $aux code.</b>\n";
    echo "<br/>\n";
    //exit;
  }
  else {   
    echo "<b>The Proof's code $aux is correct.</b>\n";
    echo "<br/>\n";
  }


  //  print("<p>".$elementos[$aux]."</p>");
  $aux++;
  //  print("<p>Descrição Breve: ".$elementos[$aux]."</p>");
  //  $aux++;
  //  print("<p>Observações: ".$elementos[$aux]."</p>");
  //  $aux++;
  //  print("<p>Código GCLC: <pre>".$elementos[$aux]."</pre></p>");
  //  $aux++;
  //  print("<p>Código GCLCprover: <pre>".$elementos[$aux]."</pre></p>");
  //  $aux++;
  //  print("<p>Referência BiBTeX: ".$elementos[$aux]."</p>");
  //  $aux++;
 }

  

//Free the XML parser
xml_parser_free($parser);

?>