<?php
/*
 * Proofs/iInsertProofCoqAM.php
 * 
 * Copyright 2009, 2018 Pedro Quaresma <pedro@mat.uc.pt>
 * 
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 * 
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,
 * MA 02110-1301, USA.
 */


// Qualque modificação neste ficheiro deve ser propagada ao ficheiro
// com um nome correspondente no directório GeoThms


// Inserção da prova -  Coq + Area Method (by Julien Narboux)

// Os nomes dos ficheiros tem apenso o identificador de utilizador
// para desta forma permitir a escrita de ficheiros por mais do que um
// utilizador ao mesmo tempo.

$vNameProofCode = 'proof'.$pUserId.'.v';// a extensão v é para o Coq
$vNameProofCodeXML = 'proofCode'.$pUserId.'.xml';
$vNameProofProof = 'proof'.$pUserId.'_proof.tex';
$vNameProofErr = 'proof'.$pUserId.'.err';
$vNameProofErrors = 'proof'.$pUserId.'.errors';
$vNameProofPIC = 'proof'.$pUserId.'.pic';
$vNameProofTeX = 'proof'.$pUserId.'.tex';
$vNameProofDVI = 'proof'.$pUserId.'.dvi';
$vNameProofPS = 'proof'.$pUserId.'.ps';
$vNameProofPDF = 'proof'.$pUserId.'.pdf';
$vNameProofProofXML = 'proof'.$pUserId.'_proof.xml';
$vNameProofXML = 'proof'.$pUserId.'.xml';
$vNameProofBZ2 = $vNameProofXML.'.bz2';

$vNameProofAux = 'proof'.$pUserId.'.aux';
$vNameProofCodeConv = 'proof'.$pUserId.'.codeconv';
$vNameErrorsConv = 'proof'.$pUserId.'.errorsconv';
$vNameTempo = 'proof'.$pUserId.'.time';

$timeLimit = "600";

// Escreve o ficheiro ".v" referente ao código Coq
ob_start();
print $pCode."\n";
$prooffile=fopen($vNameProofCode,"w");
fwrite($prooffile,ob_get_contents()); 
fclose($prooffile); 
ob_end_clean(); 


//echo "./runCoqAM.bash $timeLimit $vNameTempo $vNameProofCode $vNameProofErrors";

ob_start();
system("./runCoqAM.bash $timeLimit $vNameTempo $vNameProofCode $vNameProofErrors");
ob_end_clean();
// verifica se há erros
system("grep Error $vNameProofErrors > $vNameProofErr");
// e toma nota do tempo
ob_start();
$sTime=system("sTimeCoq < $vNameTempo");
ob_end_clean();


$filename = $vNameProofErr;

// Vai verificar se houve erros
if  (file_exists($filename) and filesize($filename)>0) { 
  // há erros 
  $file = fopen ($filename, "r");
  $contents = fread ($file, filesize ($filename));
  echo $contents;
  
  echo "<center>\n";
  echo "<br>There are errors in the proof's code. The proof was not inserted in the database</b>\n";
  echo "</center>\n";
  // TRANSAÇÕES - ROLLBACK
  @ mysqli_query("ROLLBACK"); 
  //  echo "<meta http-equiv='refresh' content='3; url=insertUpdateProof.php' />\n";
  exit;
}
else {  // Não há erros (o tempo limite pode ter sido excedido). 
  
  // O Coq + Area Method (J. Narboux) não produz nenhuma prova
  
  // ficheiro XML (referente ao código) - vazio (só com uma linha em branco)
  system("echo > $vNameProofCodeXML");
  
  // ficheiro "PDF" (prova) - vazio (só com uma linha em branco)
  system("echo > $vNameProofPDF"); 
  
  // ficheiro "XML" (prova) - vazio (só com uma linha em branco)
  system("echo > $vNameProofXML");
  
  // Agora a inserção do código em formato XML (vazio)
  $fpCodeXML      = fopen($vNameProofCodeXML, 'r');
  $contentCodeXML = fread($fpCodeXML, filesize($vNameProofCodeXML));
  $contentCodeXML = addslashes($contentCodeXML);
  fclose($fpCodeXML);
  
  // e agora a inserção da prova em formato PDF (vazio)
  $fpPDF      = fopen($vNameProofPDF, 'r');
  $contentPDF = fread($fpPDF, filesize($vNameProofPDF));
  $contentPDF = addslashes($contentPDF);
  fclose($fpPDF);
  
  // Agora a inserção da prova em formato XML (vazio)
  $fpXML      = fopen($vNameProofXML, 'r');
  $contentXML = fread($fpXML, filesize($vNameProofXML));
  $contentXML = addslashes($contentXML);
  fclose($fpXML);
  
  $sqlproof = "UPDATE demonstrations
                  SET proof    = '$contentPDF',
                      proofXML = '$contentXML'
                WHERE demId = $pDemId";
  
  $resultadoproof = mysqli_query($ligacao,$sqlproof);
  
  if (!$resultadoproof) {
    echo "Error - proof not inserted (L107) <br />";
    // TRANSAÇÕES - ROLLBACK
    @ mysqli_query("ROLLBACK");    
    //    echo "<meta http-equiv=\"refresh\" content=\"3; url=../forms.php\" />";
    exit;
  }
  
  
  // Fim - inserção da prova
  
  // Preenchimento do campo "status"
  
  // Não tendo havido erros o resultado foi provado!

  // !!! Tentar distinguir entre erros sintácticos e erros dedutivos !!!
  // !!! É necessário colocar esta questão ao J. Narboux !!!

  if ($sTime < 600) {
    $vStatus="Proved";
    $vStatusN=1;
  }
  else {
    $vStatus="Time-out: Failed to prove the conjecture";
    $vStatusN=4;
  }

  $sqlProofStatus = "UPDATE demonstrations
                        SET status = '$vStatus',
                            statusN = $vStatusN
                      WHERE demId = $pDemId";
  
  $resultadoProofStatus = mysqli_query($ligacao,$sqlProofStatus);
  
  if (!$resultadoProofStatus) {
    echo "Error - proof not inserted - status (L132) <br />";
    // Transações - ROLLBACK
    @ mysqli_query("ROLLBACK"); 
    //    echo "<meta http-equiv=\"refresh\" content=\"3; url=../forms.php\" />";
    exit;
  }
  
  // E agora os resultados das medidas de eficiência
  

  // Neste caso só temos o tempo de execução que já foram obtidos e
  // estão na variável $sTime
  
  // Vai obter a identificação do Computador de serviço 
  // isto é o computador aonde os programas estão a ser executados.
  
  require_once("../servidor.php");
  
  $pComputerId = $servidorCPU; // valor fixado no ficheiro servidor.php
  $nLargestPolynomial = 0; // no método da área não tem significado 

  
  $sqlProofMeasures = "INSERT INTO measures
                        (measuresId,elimSteps,geoSteps,algSteps,timeCPU,
                         numberTerms,computerId)
                            VALUES
                        ('$pDemId',0,0,0,$sTime,$nLargestPolynomial,$pComputerId)";


  $resultadoProofMeasures = mysqli_query($ligacao,$sqlProofMeasures);

  //  echo $sqlProofMeasures;

  if ( !$resultadoProofMeasures ) {
    // Transações - ROLLBACK
    @ mysqli_query("ROLLBACK");
    echo "Error - proof not inserted --- measures (L175)<br />";
    //    echo "<meta http-equiv='refresh' content='3; url=../forms.php' />"; 
    exit;
  }
  
  // Está tudo bem - Termina a transacção.
  @mysqli_query("COMMIT");
  
  // fim da inserção da prova + status + medidas de eficiência
} 

 
?>