<?php
/*
 * Interaction/evaluateCodeCoqJN.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.
 */

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

echo "<h1>Versão Coq + Area Method (by Julien Narboux)</h1>";

// Escreve o ficheiro "txt" referente ao código
// começa por apagar os ficheiros anteriores
// 
// 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.

// No caso do Coq a extensão tem de ser "v"

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


$vNameProofCodeConv = 'proof'.$pUserId.'.codeconv';
$vNameErrorsConv = 'proof'.$pUserId.'.errorsconv';
$vNameTempo = 'proof'.$pUserId.'.time'; // este é próprio do Coq


ob_start();
print $pCode."\n";
$texfile=fopen($vNameProofCode,"w");
fwrite($texfile,ob_get_contents()); 
fclose($texfile); 
ob_end_clean(); 


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

ob_start();
system("/usr/bin/time --output=$vNameTempo -f %E coqc $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 "<a href='insertCodeProver.php?argumento=$pCodeTmpId&teoId=$vTeoId&insercao=$insercao'>go back</a>\n";
  echo "</center>\n";
 }
 else { // Caso não haja erros vai colocar o Proof status em "proved"

  $result=1; 
  // no campo status tem-se
  //   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)

  // O Coq + Area Method (J. Narboux) não produz nenhuma prova
  
  // ficheiro "PDF" (prova) - vazio
  system("echo > $vNameProofPDF"); 
  
  // as medidas de eficiência resumem-se ao tempo, o qual já foi
  // obtido aquando da demonstração
  
  // 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";
  

  // Vai escrever a informação na base de dados como uma lista
  // delimitada por ';'. Seria preferível guardar directamente a
  // tabela HTML, mas há conta dos caracteres especiais isso dá
  // asneira


  $vProofResults = $result." ; ".$sTime." ; ".$computerSpecs." . ";
  
  $vProofResults = htmlspecialchars("$vProofResults", ENT_QUOTES);

  // o ficheiro referente à prova
  // O Coq + Area Method (J. Narboux) não produz nenhuma prova
  
  // ficheiro "PDF" (prova) - Neste caso não pode ser vazio dado que
  // no ficheiro principal esse facto é usado para destinguir entre a
  // primeira vez e todas as outras vezes, vou simplesmente colocar uma 
  // referência ao provador 
  system("echo Coq > $vNameProofPDF");   

  $fp      = fopen($vNameProofPDF, 'r');
  $content = fread($fp, filesize($vNameProofPDF));
  $content = addslashes($content);
  fclose($fp);
  
  // e agora a inserção da prova + medidas de eficiência
  
  $sqlfigure = "UPDATE codeTmp
                   SET proof        = '$content',
                       proofResults = '$vProofResults'
                 WHERE codeTmpId = '$argumento'";
  
  $resultadofigure = mysqli_query($ligacao,$sqlfigure);
  
  if (!$resultadofigure) {
    echo "Error";
    exit;
  }
  echo "<meta http-equiv='refresh' content='1; url=insertCodeProver.php?argumento=$pCodeTmpId&teoId=$vTeoId&insercao=$insercao' />";
 }

?>