<?php

/*
 * Interaction/evaluateCodeGCLCproverWM.php
 * 
 * Copyright 2010, 2016 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 - Wu's Method


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

require_once("../servidor.php");


// 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'; // este é a imagem para este teorema.
$vNameProofTeX = 'proof'.$pUserId.'.tex';
$vNameProofDVI = 'proof'.$pUserId.'.dvi';
$vNameProofPS = 'proof'.$pUserId.'.ps';
$vNameProofPDF = 'proof'.$pUserId.'.pdf';
$vNameFigureTeX = 'figure'.$pUserId.'.tex';
$vNameFigureDVI = 'figure'.$pUserId.'.dvi';
$vNameFigurePS = 'figure'.$pUserId.'.ps';
$vNameFigureEPSI = 'figure'.$pUserId.'.epsi';
$vNameFigureJPG = 'figure'.$pUserId.'.jpg';

$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(); 


ob_start();

system("/usr/local/bin/gclc $vNameProofCode $vNameProofPIC -w > $vNameProofErrors");
// erros sintacticos na imagem
system("grep Syntax $vNameProofErrors > $vNameProofErr");
// erros semânticos na imagem (faz o concatenar dos erros)
system("grep 'Run-time error' $vNameProofErrors >> $vNameProofErr");
// erros na construção da conjectura  (faz o concatenar dos erros)
system("grep ill-formed $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();
  
  // o ficheiro referente ~ prova
  
  $fp      = fopen($vNameProofPDF, 'r');
  $contentProof = fread($fp, filesize($vNameProofPDF));
  $contentProof = addslashes($contentProof);
  fclose($fp);


  // Obtêm agora as medidas de eficiência e constroí uma tabela
  // (HTML) com eles
  //
  // proof_proof.tex
  //

  // Método de Wu, só o nLargestPolynomial interessa
  ob_start();
  $nLargestPolynomial=system("./nLargestPolynomialWM < $vNameProofTeX");
  $sTime=system("./sTimeWM < $vNameProofTeX");
  $result=system("./provedDisprovedWM < $vNameProofTeX");
  ob_end_clean();

  $elimSteps=0;
  $geoSteps=0;
  $algSteps=0;

  
  // 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 
                   WHERE computerId = $servidorCPU";

//  echo $sqlComputer."<br/>";
  
  $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
  
  $pProofResults = $result." ; ".$elimSteps." ; ".$geoSteps." ; ".$algSteps." ; ".$nLargestPolynomial." ; ".$sTime." ; ".$computerSpecs;
  
  $pProofResults = htmlspecialchars("$pProofResults", ENT_QUOTES);


  // Vai produzir o texto LaTeX referente à Figura
  ob_start();
  print "\documentclass[12pt]{article}\n";
  // necessária em ambos os casos, no caso do GCLC só para lidar com as cores
  print "\usepackage{pstricks}\n"; 
  print "\usepackage{color}\n";
  if ($pDrwId==3 || $pDrwId==5 || $pDrwId==6) print "\usepackage{gclc}\n";
  print "\pagestyle{empty}\n";
  print "\begin{document}\n";
  print "\input{ $vNamePIC }\n";
  print "\end{document}\n";
  
  $texfile=fopen($vNameTeX,"w");
  fwrite($texfile,ob_get_contents()); 
  fclose($texfile); 
   
  system("latex $vNameFigureTeX"); 
  system("dvips $vNameFigureDVI -o $vNameFigurePS"); 
  system("ps2epsi $vNameFigurePS $vNameFigureEPSI");
  system("convert $vNameFigureEPSI $vNameFigureJPG");
  ob_end_clean(); 
  
  // e agora a inserção da imagem
  $fp      = fopen($vNameFigureJPG, 'r');
  $contentFigure = fread($fp, filesize($vNameFigureJPG));
  $contentFigure = addslashes($contentFigure);
  fclose($fp);


  // e agora a inserção da prova + medidas de eficiência + imagem
  
  $sqlProof = "UPDATE codeTmp
                  SET proof        = '$contentProof',
                      figure       = '$contentFigure',
                      proofResults = '$pProofResults'
                WHERE codeTmpId = '$argumento'";
  
  $resultadoProof = mysqli_query($ligacao,$sqlProof);
  
  if (!$resultadoProof) {
    echo "Error";
    exit;
  }

  echo "<meta http-equiv='refresh' content='1; url=insertCodeProver.php?argumento=$pCodeTmpId&teoId=$vTeoId&insercao=$insercao' />";
}

?>