<?php
/*
 * Proofs/iInsertProofGCLCproverEuk.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 - GCLCprover + Conversor EukcleidesToGCLC


// -> $pCode, o código do teorema
// ...


// Após a conversão do código de Eukleides para GCLC todo o restante
// processamento é idêntico ao GCLCprover

// 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.
// este é o código antes da conversão
$vNameProofCodeEuk = 'proof'.$pUserId.'.euk2gclc'; 

$vNameProofCode = 'proof'.$pUserId.'.code';
$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';

// Escreve o ficheiro ".euk2gclc" referente ao código para ser convertido
ob_start();
print $pCode."\n";
$prooffile=fopen($vNameProofCodeEuk,"w");
fwrite($prooffile,ob_get_contents()); 
fclose($prooffile); 
ob_end_clean(); 


// Conversão de Eukleides para GCLCprover

system("./euk2gclc < $vNameProofCodeEuk > $vNameProofCode");

// A partir daqui tudo é igual

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 "<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='5; url=insertUpdateProof.php' />\n";
  exit;
}
else { // Caso não haja erros vai processar a prova
  // Vai produzir o texto LaTeX referente à Prova
  // Pré-processa o ficheiro proof_proof.tex gerado pelo gclc 
  // pelo sed para substituir o estilo por omissão do gclc pelo estilo
  // landscape
  ob_start();
  system("sed -e 's/{gclc_proof}/\[landscape\]{gclcproof}/g' $vNameProofProof > $vNameProofTeX");  
  
  system("latex $vNameProofTeX"); 
  system("latex $vNameProofTeX"); 
  system("dvips $vNameProofDVI"); 
  system("ps2pdf $vNameProofPS"); 
  
  ob_end_clean(); 
  
  
  
  // Vai agora criar os ficheiros XML referente ao código e à prova
  echo "<p>Processing the XML file, please wait</p>\n";
  system("/usr/local/bin/gclc  $vNameProofCode $vNameProofCodeXML -xml > $vNameProofErrors");
  
  // modifica o estilo de saída (código) para "Natural Language"
  // É o conteúdo do ficheiro modificado que é inserido na BD
  system("sed -e 's/GeoConsHTML.xsl/GeoConsNL.xsl/g' $vNameProofCodeXML > $vNameProofAux");
  
  // e agora  inserção do ficheiro referente à prova
  system("cp $vNameProofProofXML $vNameProofXML");
  // vai conprimir o ficheiro com o bzip2, é necessário apagar o
  // ficheiro comprimido, caso exista.
  system("rm $vNameProofBZ2");
  system("bzip2 $vNameProofXML");
  
  // Agora a inserção do código em formato XML
  $fpCodeXML      = fopen($vNameProofAux, 'r');
  $contentCodeXML = fread($fpCodeXML, filesize($vNameProofAux));
  $contentCodeXML = addslashes($contentCodeXML);
  fclose($fpCodeXML);
  
  // e agora a inserção da prova em formato PDF
  $fpPDF      = fopen($vNameProofPDF, 'r');
  $contentPDF = fread($fpPDF, filesize($vNameProofPDF));
  $contentPDF = addslashes($contentPDF);
  fclose($fpPDF);
  
  // Agora a inserção da prova em formato XML comprimido
  $fpBZ2      = fopen($vNameProofBZ2, 'r');
  $contentBZ2 = fread($fpBZ2, filesize($vNameProofBZ2));
  $contentBZ2 = addslashes($contentBZ2);
  fclose($fpBZ2);
  
  $sqlproof = "UPDATE demonstrations
                  SET codeXML  = '$contentCodeXML',
                      proof    = '$contentPDF',
                      proofXML = '$contentBZ2'
                WHERE demId = $pDemId";
  
  $resultadoproof = mysqli_query($ligacao,$sqlproof);
  
  if (!$resultadoproof) {
    echo "Error - proof not inserted";
    // TRANSAÇÕES - ROLLBACK
    @ mysqli_query("ROLLBACK");    
    echo "<meta http-equiv=\"refresh\" content=\"2; url=../forms.php\" />";
    exit;
  }
  
  
  // Fim - inserção da prova
  
  // Preenchimento do campo "status"
  
  // vai obter o resultado da tentativa de prova
  ob_start();
  $vResult=system("provedDisproved < $vNameProofTeX");
  ob_end_clean();
  //   1 = proved (if the conjecture was proved valid)
  //   0 = disproved (if the conjecture was proved invalid)
  //   2 = Failed to prove the conjecture (if neither of above two)
  if ($vResult==1) 
    $vStatus="Proved";
  elseif ($vResult==2)
    $vStatus="Disproved";
  else
    $vStatus="Failed to prove the conjecture";
  
  $sqlProofStatus = "UPDATE demonstrations
                         SET status = '$vStatus'
                       WHERE demId = $pDemId";
  
  $resultadoProofStatus = mysqli_query($ligacao,$sqlProofStatus);
  
  if (!$resultadoProofStatus) {
    echo "Error - proof not inserted";
    // Transações - ROLLBACK
    @ mysqli_query("ROLLBACK"); 
    echo "<meta http-equiv=\"refresh\" content=\"2; url=../forms.php\" />";
    exit;
  }
  
  // E agora os resultados das medidas de eficiência
  
  if ($pProverId==2 || $pProverId==3) {
    // para o  provador GCLCprover 1.0
    // ou
    // para o provador GCLCprover 1.0 após o conversor euktogclcprover 1.0
    ob_start();
    $elimSteps=system("nEliminationSteps < $vNameProofTeX");
    $geoSteps=system("nGeometricSteps < $vNameProofTeX");
    $algSteps=system("nAlgebraicSteps < $vNameProofTeX");
    $totalSteps=system("nTotalSteps < $vNameProofTeX");
    $sTime=system("sTime < $vNameProofTeX");
    ob_end_clean();
  }
  
  // Vai obter os dados do Computador de serviço 
  // isto é na tabela "computador" estão os dados do meu computador
  // actual, aquele aonde os programas estão a ser executados.
  
  $sqlComputer = "SELECT CPUBrand,CPUType,speed,RAM
                     FROM computer";
  
  $resultadoComputer = mysqli_query($ligacao,$sqlComputer);
  $linhaComputer = mysqli_fetch_assoc($resultadoComputer);
  
  $pCPUBrand = trim($linhaComputer['CPUBrand']);
  $pCPUType  = trim($linhaComputer['CPUType']);
  $pSpeed    = trim($linhaComputer['speed']);
  $pRAM      = trim($linhaComputer['RAM']);
  
  $computerSpecs = $pCPUBrand." ".$pCPUType.", ".$pSpeed."GHz, ".$pRAM."GB";
  
  
  
  $sqlProofMeasures = "UPDATE measures
                          SET elimSteps     = '$elimSteps',
                              geoSteps      = '$geoSteps',
                              algSteps      = '$algSteps',
                              timeCPU       = '$sTime',
                              computerSpecs = '$computerSpecs'
                        WHERE measuresId = $pDemId";
   
  $resultadoProofMeasures = mysqli_query($ligacao,$sqlProofMeasures);
  
  if (!$resultadoProofMeasures) {
    echo "Error - proof not updated - Measures";
    // Transações - ROLLBACK
    @ mysqli_query("ROLLBACK"); 
    echo "<meta http-equiv='refresh' content='0; url=../forms.php' />";
    exit;
  }
} // fim da actualização da prova + status


// E agora os resultados das medidas de eficiência

ob_start();
$elimSteps=system("nEliminationSteps < $vNameProofProof");
$geoSteps=system("nGeometricSteps < $vNameProofProof");
$algSteps=system("nAlgebraicSteps < $vNameProofProof");
$totalSteps=system("nTotalSteps < $vNameProofProof");
$sTime=system("sTime < $vNameProofProof");
ob_end_clean();


// Vai obter os dados do Computador de serviço 
// isto é na tabela "computador" estão os dados do meu computador
// actual, aquele aonde os programas estão a ser executados.

$sqlComputer = "SELECT CPUBrand,CPUType,speed,RAM
                  FROM computer";

$resultadoComputer = mysqli_query($ligacao,$sqlComputer);
$linhaComputer = mysqli_fetch_assoc($resultadoComputer);

$pCPUBrand = trim($linhaComputer['CPUBrand']);
$pCPUType  = trim($linhaComputer['CPUType']);
$pSpeed    = trim($linhaComputer['speed']);
$pRAM      = trim($linhaComputer['RAM']);

$computerSpecs = $pCPUBrand." ".$pCPUType.", ".$pSpeed."GHz, ".$pRAM."GB";

$sqlProofMeasures = "INSERT INTO measures
                        (measuresId,elimSteps,geoSteps,algSteps,timeCPU,
                         computerSpecs)
                          VALUES
                        ('$pDemId','$elimSteps','$geoSteps','$algSteps',
                         '$sTime','$computerSpecs')";


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

if ( !$resultadoProofMeasures ) {
  // Transações - ROLLBACK
  @ mysqli_query("ROLLBACK");
  echo "Error - proof not inserted --- measures";
  echo "<meta http-equiv='refresh' content='0; url=../forms.php' />"; 
  exit;
}

// Está tudo bem - Termina a transação.
@mysqli_query("COMMIT");
   
// fim da inserção da prova + status + medidas de eficiência

?>