<?php

// Este ficheiro é uma cópia exacta (deve ser) do ficheiro com nome
// correspondente no directório Geothms - iInsertPrfGeoThmCoqAM.php


  // Versão Coq + Area Method (by Julien Narboux)

$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';
$vNameTempo = 'proof'.$pUserId.'.time'; // este é próprio do Coq

$vNameProofAux = 'proof'.$pUserId.'_aux.txt';
$vNameProofCodeConv = 'proof'.$pUserId.'.codeconv';
$vNameErrorsConv = 'proof'.$pUserId.'.errorsconv';

$commandLineATP = "/usr/bin/time --output=$vNameTempo -f %e coqc $vNameProofCode > $vNameProofErrors";
$timeLimit = "600";



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

// Vai processar o código com o provador obtendo o tempo de imediato

// O runCoqAM é um "script bash" para poder processar o coq com "ulimit -t 600"

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, ou tempo limite excedido
  $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. ";
  echo "The proof was not inserted in the database</b>\n";
  echo "</center>\n";
  // TRANSAÇÕES - ROLLBACK
  @ mysql_query("ROLLBACK"); 
  echo "<meta http-equiv=\"refresh\" content=\"2; url=../forms.php\" />";
 }
 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
   system("echo > $vNameProofCodeXML ");
   
   // ficheiro "PDF" (prova) - vazio
   system("echo > $vNameProofPDF"); 

   // ficheiro "XML" (prova) - vazio
   system("echo > $vNameProofXML");
   
   // Agora a inserção do código em formato XML
   $fpCodeXML      = fopen($vNameProofCodeXML, 'r');
   $contentCodeXML = fread($fpCodeXML, filesize($vNameProofCodeXML));
   $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
   $fpXML      = fopen($vNameProofXML, 'r');
   $contentXML = fread($fpXML, filesize($vNameProofXML));
   $contentXML = addslashes($contentXML);
   fclose($fpXML);

   $sqlproof = "UPDATE demonstrations
                    SET commandLine = '$commandLineATP',
                        timeLimit = $timeLimit,
                        proof    = '$contentPDF',
                        proofXML = '$contentXML'
                  WHERE demId = $auxDemId";
   
   $resultadoproof = mysql_query($sqlproof,$ligacao);
   
   if (!$resultadoproof) {
     echo "Error - proof not inserted (CoqAM L101)";
     // TRANSAÇÕES - ROLLBACK
     @ mysql_query("ROLLBACK"); 
     echo "<meta http-equiv=\"refresh\" content=\"2; 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 = $auxDemId";
   
   $resultadoProofStatus = mysql_query($sqlProofStatus,$ligacao);
   
   if (!$resultadoProofStatus) {
     echo "Error - proof not inserted";
     // TRANSAÇÕES - ROLLBACK
     @ mysql_query("ROLLBACK"); 
     echo "<meta http-equiv=\"refresh\" content=\"2; url=../forms.php\" />";
     exit;
   }
   
   // E agora os resultados das medidas de eficiência

   // Neste caso só temos o tempo de execução - que já foi obtido aquando da prova
   
   // 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 = "UPDATE measures
                           SET elimSteps     = 0,
                               geoSteps      = 0,
                               algSteps      = 0,
                               timeCPU       = '$sTime',
                               numberTerms   = $nLargestPolynomial,
                               computerId    = $pComputerId
                         WHERE measuresId = $auxDemId";
   
   $resultadoProofMeasures = mysql_query($sqlProofMeasures,$ligacao);
   
   if (!$resultadoProofMeasures) {
     echo "Error - proof not updated - Measures (L174)";
     // TRANSAÇÕES - ROLLBACK
     @ mysql_query("ROLLBACK"); 
     echo "<meta http-equiv='refresh' content='0; url=updateGeoThm.php?argumento=$pTeoId' />";
     exit;
   }
 } // fim da actualização da prova + status + medidas de eficiência

// Está tudo bem - Termina a transação.
@mysql_query("COMMIT");

?>