<?php


  /*


  Este ficheiro já não deve estar activo --- verificar


  Pelo menos já não está actualizado correctamente --- verificar

  */

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


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

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

$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 $pCode."\n";
$prooffile=fopen($vNameProofCode,"w");
fwrite($prooffile,ob_get_contents()); 
fclose($prooffile); 
ob_end_clean(); 


ob_start();
system("./runCoqAM 600 $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 ou não
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
  @ mysql_query("ROLLBACK"); 
  echo "<meta http-equiv='refresh' content='3; url=insertUpdateProof.php' />\n";
  exit;
}
else {  // Caso não haja erros vai colocar o Proof status em "proved"
  
  // 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 comprimido (vazio)
  $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 = $pDemId";
  
  $resultadoproof = mysql_query($sqlproof,$ligacao);
  
  if (!$resultadoproof) {
    echo "Error - proof not inserted (L109)";
    // TRANSAÇÕES - ROLLBACK
    @ mysql_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 !!!
  $vStatus="Proved";
  
  $sqlProofStatus = "UPDATE demonstrations
                        SET status = '$vStatus',
                            statusN = $vResult
                      WHERE demId = $pDemId";
  
  $resultadoProofStatus = mysql_query($sqlProofStatus,$ligacao);
  
  if (!$resultadoProofStatus) {
    echo "Error - proof not inserted - status (L134)";
    // Transações - ROLLBACK
    @ mysql_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 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 = mysql_query($sqlComputer,$ligacao);
  $linhaComputer = mysql_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',0,0,0,'$sTime','$computerSpecs')";


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

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

 
?>