<?php
/*
 * Interaction/evaluateCodeGCLCproverEuk.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 GCLCprover + euk2gclc



// 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.


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

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 programa de desenho
// Consoante o programa de prova
// 3 - GCLC + euktogclcprover - 1.0.1.0 (os primeiro dois são para o
// gclc os dois últimos para o conversor)
//
// proof.errors ---> proof.err
//
ob_start();
// primeiro aplica o conversor euk2gclc 1.0
system("/usr/local/bin/euk2gclc < $vNameProofCode > $vNameProofCodeConv 2> $vNameErrorsConv");
system("cp $vNameProofCodeConv $vNameProofCode");
// depois aplica o provador GCLCprover 1.0
system("/usr/local/bin/gclc $vNameProofCode $vNameProofPIC > $vNameProofErrors");
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;
  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 processar a demonstração
  echo "<center>Running the Prover, wait please</center>";
  ob_start();
  // 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
  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();
  
  // Obtêm agora as medidas de eficiência e constroí uma tabela
  // (HTML) com eles
  //
  // proof_proof.tex
  //
  
  ob_start();
  $elimSteps=system("./nEliminationSteps < $vNameProofTeX");
  $geoSteps=system("./nGeometricSteps <  $vNameProofTeX");
  $algSteps=system("./nAlgebraicSteps <  $vNameProofTeX");
  $sTime=system("./sTime < $vNameProofTeX");
  $result=system("./provedDisproved < $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";
  

  // 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." ; ".$elimSteps." ; ".$geoSteps." ; ".$algSteps." ; ".$sTime." ; ".$computerSpecs." . ";
  
  $vProofResults = htmlspecialchars("$vProofResults", ENT_QUOTES);
  
  // o ficheiro referente à prova
  
  $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' />";
 }

