<?php  
session_start();
/*
 * Geothms/Forms/formGeoThm.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.
 */

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

$pTipoUtilizador = $_SESSION['tipoUtilizador'];
if ($pTipoUtilizador=="anonymous" || $pTipoUtilizador=="regular") { // separa por tipo de utilizador
  require($entradaFILE.'headerUsers.php');
  require($entradaFILE.'menuUsers.php');
}
else {
  require($entradaFILE.'headerAdmins.php');
  require($entradaFILE.'menuAdmins.php');
}
?>

<?php
require($entradaFILE.'dbLogin.php');
?>


<hr/>

<?php
$argumento = $_GET['argumento'];

//
// Geometric Theorem Info
//

// cria uma pesquisa para obter a informação do problema, qualquer
// (eventual) referência bibliográfica que haja terá de ser obtida
// à parte para salguardar o caso em que não há nenhuma referência
// bibliográfica.
$sql = "SELECT teoId,teoName,category,description,shortDescription,
               dateSubmission,userId
          FROM theorems
         WHERE theorems.teoId='$argumento'";

$resultado = mysqli_query($ligacao,$sql);

$ncampos =mysqli_num_fields($resultado);


$linha = mysqli_fetch_assoc($resultado);

$pTeoId            = $linha['teoId'];
$pTeoName          = $linha['teoName'];
//$pBibRef           = $linha['bibrefId'];
$pCategory         = $linha['category'];
$pDateSubmission   = $linha['dateSubmission'];
$pDescription      = $linha['description'];
$pShortDescription = $linha['shortDescription'];
$pUserId           = $linha['userId'];

$sqlUserId = "SELECT userId,name,email
                FROM users
               WHERE userId='$pUserId'";

$resultadoUserId = mysqli_query($ligacao,$sqlUserId);
$linhaUserId = mysqli_fetch_assoc($resultadoUserId);

$pUserName=trim($linhaUserId['name']);
$pUserEmail=trim($linhaUserId['email']);



// Pode haver mais do que uma referência bibliográfica para o mesmo
// problema

$sqlBibTeo = "SELECT theorems.teoId,bibrefId
                FROM theorems INNER JOIN bibtheorem
                     ON theorems.teoId=bibtheorem.teoId
               WHERE theorems.teoId='$pTeoId'";

$resultadoBibTeo = mysqli_query($ligacao,$sqlBibTeo);


$nlinhasBibTeo =  mysqli_num_rows($resultadoBibTeo);


// Vai produzir a versão LaTeX das referencias
$vNameReferenciasTeX = 'referencias'.$pUserId.'.tex';
$vNameReferenciasAUX = 'referencias'.$pUserId.'.aux';
$vNameReferenciasBiB = 'referencias'.$pUserId.'.bib';
$vNameReferenciasDVI = 'referencias'.$pUserId.'.dvi';
$vNameReferenciasEPS = 'referencias'.$pUserId.'.eps';
$vNameReferenciasPNG = 'referencias'.$pUserId.'.png';
ob_start();
print "\documentclass[12pt]{article}\n";
print "\pagestyle{empty}\n";
print "\addtolength{\\textwidth}{2cm}\n";
print "\begin{document}\n";
print "\large\n";
if ($nlinhasBibTeo==0) { // caso não haja referências |--> "No references" 
  print "No references\n";
}
else { // havendo mais do que uma referência bibliográfica tem de se
       // ter em conta que no LaTeX só pode haver um comando "nocite"
  $contabibrefs=1; 
  print "\\nocite{";
  while ($linhaBibTeo = mysqli_fetch_assoc($resultadoBibTeo)) {
    $pBibRefTeo = trim($linhaBibTeo['bibrefId']);
    print "$pBibRefTeo";
    if ($contabibrefs<$nlinhasBibTeo) 
      print ",";
    $contabibrefs++;
  }
  print "}\n";
  print "\bibliographystyle{alpha}\n";
  $bibcomand="\bibliography{".$vNameReferenciasBiB."}\n";
  print $bibcomand;
}
print "\end{document}\n";

  
$texfile=fopen($vNameReferenciasTeX,"w");
fwrite($texfile,ob_get_contents()); 
fclose($texfile); 
ob_end_clean(); 

if ($nlinhasBibTeo!=0) {  // se não há refs bibs não e necessário produzir o ficheiro BiBTeX
  // Vou agora produzir o ficheiro bib
  ob_start();
  // definições gerais
  print "@PREAMBLE{ {\\newcommand{\\noopsort}[1]{} \\newcommand{\singleletter}[1]{#1} } }\n";
  print "@STRING{ ADW = {Addison-Wesley} }\n";
  print "@STRING{ AMS = {American Mathematical Society} }\n\n";
  // e agora as entradas presentes na Base de Dados

  mysqli_data_seek($resultadoBibTeo,0); // re-posiciona o ponteiro para o ínicio.

  while ($linhaBibTeo = mysqli_fetch_assoc($resultadoBibTeo)) {
    $pBibRefTeo = trim($linhaBibTeo['bibrefId']);
    
    // e agora as entradas presentes na Base de Dados    
    // cria uma pesquisa
    $sqlBibrefs = "SELECT bibtexEntry
                     FROM bibrefs
                    WHERE bibrefId='$pBibRefTeo'";
    
    $resultadoBibrefs = mysqli_query($ligacao,$sqlBibrefs);
  
    $linhaBibrefs = mysqli_fetch_assoc($resultadoBibrefs);
    
    $pBiBTeXEntry = $linhaBibrefs['bibtexEntry'];
    
    print $pBiBTeXEntry."\n\n";
  }

  // Escreve o ficheiro BiBTeX
  
  $texfile=fopen($vNameReferenciasBiB,"w");
  fwrite($texfile,ob_get_contents()); 
  fclose($texfile); 
  ob_end_clean(); 
}
  
ob_start(); 
system("latex $vNameReferenciasTeX"); 

if ($nlinhasBibTeo!=0) { // se não há refs bibs não e necessário invocar o BiBTeX
  system("bibtex $vNameReferenciasAUX"); 
  system("latex $vNameReferenciasTeX"); 
  system("latex $vNameReferenciasTeX"); 
}
system("dvips -E $vNameReferenciasDVI -o $vNameReferenciasEPS"); 
system("convert $vNameReferenciasEPS $vNameReferenciasPNG"); 
ob_end_clean();

// Formata o enunciado através do LaTeX
ob_start();
print "\documentclass[12pt]{article}\n";
print "\usepackage[latin1]{inputenc}\n"; // para o caso de haver caracteres 8bits
print "\def\\ratio#1#2{\\frac{\overline{#1}}{\overline{#2}}}\n";
print "\\newtheorem{geothm}{Theorem}\n";
print "\pagestyle{empty}\n";
print "\addtolength{\\textwidth}{2cm}\n";
print "\begin{document}\n";
print "\large\n";
print $pDescription."\n";
print "\end{document}\n";

// Escreve o ficheiro LaTeX
$vNameEnunciadoTeX = 'enunciado'.$pUserId.'.tex';
$vNameEnunciadoDVI = 'enunciado'.$pUserId.'.dvi';
$vNameEnunciadoEPS = 'enunciado'.$pUserId.'.eps';
$vNameEnunciadoPNG = 'enunciado'.$pUserId.'.png';

$texfile=fopen($vNameEnunciadoTeX,"w");
fwrite($texfile,ob_get_contents());
fclose($texfile);
ob_end_clean();

ob_start();
system("latex $vNameEnunciadoTeX");
system("dvips -E $vNameEnunciadoDVI -o $vNameEnunciadoEPS");
system("convert $vNameEnunciadoEPS $vNameEnunciadoPNG");
ob_end_clean();

echo "<!-- ficha -->";
echo "<table width='100%' bgcolor='white' cellpadding='4' cellspacing='4'>";
echo "<tr>";
echo "<td width='100%' colspan='8' align='center'><span class='titulo'>$pTeoName Info</span></td>";
echo "</tr>";
echo "<tr>";
echo "<td align='left' width='25%' colspan='2'><span class='ficha'>Name of the Theorem</span></td>";
echo "<td width='50%' colspan='4'>$pTeoName</td>";
echo "<td align='left' width='12.5%' colspan='1'><span class='ficha'>Theorem's Id</span></td>";
echo "<td width='12.5%' colspan='1'>$pTeoId</td>";
echo "</tr>";
echo "<tr>";
echo "<td width='25%' colspan='2'><span class='ficha'>Contributor's Name</span></td>";
echo "<td width='75%' colspan='6'>$pUserName</td>";
//echo "<td width='12.5%' colspan='1'><span class='ficha'>Email</span></td>";
//echo "<td width='25%' colspan='2'>$pUserEmail</td>";
echo "</tr>";
echo "<tr>";
echo "<td width='25%' colspan='2'><span class='ficha'>Category</span> </td>";
echo "<td width='25%' colspan='2'>$pCategory</td>"; 
echo "<td width='25%' colspan='2'><span class='ficha'>Date of Submission</span></td>";
echo "<td width='25%' colspan='2'>$pDateSubmission</td>"; 
echo "</tr>";
echo "<tr>";
echo "<td width='25%' colspan='2'><span class='ficha'>Description</span></td>";
echo "<td width='75%' colspan='6'>$pShortDescription</td>";
echo "</tr>  ";
echo "<tr>";
echo "<td width='25%' colspan='2'><span class='ficha'>Formal Statement</span></td>";
echo "<td width='75%' colspan='6'><img src='view_imagePNG.php?argumento=$vNameEnunciadoPNG' alt='LaTeX'></td>";
echo "</tr>  ";
echo "<tr>";
if ($pBibRef=='noref') { // caso não haja referências bibliográficas
  echo "<td width='25%' colspan='2'><span class='ficha'>Bibliographic References</span></td>";
  echo "<td width='75%' colspan='6'>No references</td>";
}
else {
  echo "<td width='25%' colspan='2'><span class='ficha'>Bibliographic References</span></td>";
  echo "<td width='75%' colspan='6'><img src='view_imagePNG.php?argumento=$vNameReferenciasPNG' alt='No BibRef'></td>";
}
echo "</tr>";

//
// Theorem Figure Info --- A(s) figura(s) existente(s) para este teorema
//

//
// Para já não há divisão (em ficheiros) entre DGSs
//

// cria uma pesquisa para obter a informação da figura, qualquer
// (eventual) referência bibliográfica que haja terá de ser obtida
// aparte para salguardar o caso em que não há nenhuma referência
// bibliográfica.
$sqlFig = "SELECT figureId,teoId,drawerId,code,codeXML,dateSubmission,userId,figureSVG
             FROM figures
            WHERE teoId='$pTeoId'";

$resultadoFig = mysqli_query($ligacao,$sqlFig);
//$ncamposFig   = mysqli_num_fields($resultadoFig);

$nlinhasFig =  mysqli_num_rows($resultadoFig);

if ($nlinhasFig==0) {
  echo "<tr>";
  echo "<td width='100%' colspan='8' align='center'><span class='titulo'>$pTeoName - No Figures</span></td>";
  echo "</tr>";
 }
 else {
  echo "<tr>";
  echo "<td width='100%' colspan='8' align='center'><span class='titulo'>$pTeoName - Figure Info</span></td>";
  echo "</tr>";
 }


// mostra os detalhes para cada uma das imagens
$nImagem=0; // inicializa contador a zero
while ($linhaFig = mysqli_fetch_assoc($resultadoFig)) {

  $nImagem=$nImagem+1; // incrementa o contador de imagens

  if ($nImagem>1) // linha de separação entre imagens
    echo "<tr><td colspan='8'><hr></td></tr>";

  $pFigureId       = trim($linhaFig['figureId']); 
  $pDrwId          = trim($linhaFig['drawerId']); 
  $pCode           = trim($linhaFig['code']); 
  $pCodeXML        = trim($linhaFig['codeXML']); 
  $pFigure         = trim($linhaFig['figure']); 
  $pDateSubmission = trim($linhaFig['dateSubmission']); 
  $pUserIdDrw      = trim($linhaFig['userId']); 
  //  $pBibrefDrw      = trim($linhaFig['bibrefId']);
  $pFigureSVG      = trim($linhaFig['figureSVG']); 
  
  // Obtém o nome do Desenhador
  $sqlDrw = "SELECT name,version
               FROM drawers
              WHERE drawerId='$pDrwId'";
  $resultadoDrw = mysqli_query($ligacao,$sqlDrw);
  $linhaDrw = mysqli_fetch_assoc($resultadoDrw);
  
  // Obtém o identificador do Utilizador
  $sqlUsr = "SELECT name,email
               FROM users
              WHERE userId='$pUserIdDrw'";
  $resultadoUsr = mysqli_query($ligacao,$sqlUsr);
  $linhaUsr = mysqli_fetch_assoc($resultadoUsr);
  
  
  $pDrwName    = trim($linhaDrw['name']);
  $pDrwVersion = trim($linhaDrw['version']);
  
  $pUserName   = trim($linhaUsr['name']);
  $pUserEmail  = trim($linhaUsr['email']);
  


  // Escreve o ficheiro "xml" referente à descrição
  $vNameXML = 'figure'.$pUserId.'-'.$nImagem.'.xml';
  
  $texfileXML=fopen($vNameXML,"w");
  fwrite($texfileXML,$pCodeXML); 
  fclose($texfileXML); 
  
  // Escreve o ficheiro "svg" referente à imagem
  $vNameSVG = 'figure'.$pUserId.'-'.$nImagem.'.svg';
  
  $texfileSVG=fopen($vNameSVG,"w");
  fwrite($texfileSVG,$pFigureSVG); 
  fclose($texfileSVG); 
  

  echo "<tr>";
  echo "<td width='25%' colspan='2'><span class='ficha'>Drawer Name</span></td>";
  echo "<td width='25%' colspan='2'>$pDrwName</td>";
  echo "<td width='25%' colspan='2'><span class='ficha'>Drawer Version</span></td>";
  echo "<td width='25%' colspan='2'>$pDrwVersion</td>";
  echo "</tr>";
  echo "<tr>"; 
  echo "<td width='25%' colspan='2'><span class='ficha'>Date of Submission</span></td>";
  echo "<td width='25%' colspan='2'>$pDateSubmission</td>"; 
  echo "<td width='25%' colspan='2'><span class='ficha'>Contributor's Name</span></td>";
  echo "<td width='75%' colspan='2'>$pUserName</td>";
  echo "</tr>";
  echo "<tr>";
  echo "<td width='25%' colspan='2'><span class='ficha'>Bibliographic Reference(s)</span></td>"; 
  echo "<td width='25%' colspan='6'>\n";
  // Pode haver mais do que uma referência bibliográfica para a mesma
  // figura, como tal cria-se uma tabela para as colocar
  echo "<table>\n"; // vai conter uma só linha
  echo "<tr>\n"; 

  $sqlBibFig = "SELECT figures.figureId,teoId,bibrefId
                  FROM figures 
            INNER JOIN bibfigure USING(figureId)
                 WHERE teoId='$pTeoId'";

  $resultadoBibFig = mysqli_query($ligacao,$sqlBibFig);


  $nlinhasBibFig =  mysqli_num_rows($resultadoBibFig);

  if ($nlinhasBibFig==0) {
    echo "<td>&nbsp;</td>";
  }
  else {
    // mostra cada uma das referências bibliográficas
    $nBibFig=0; // inicializa contador a zero
    while ($linhaBibFig = mysqli_fetch_assoc($resultadoBibFig)) {
      
      $nBibFig+=1; // incrementa o contador de imagens
      
      $pBibRefFig      = trim($linhaBibFig['bibrefId']);

      echo "<td>$pBibRefFig"; 

      if ($nBibFig<$nlinhasBibFig) // coloca um ";" a separar as diferentes referências bibliográficas
	echo ";</td>";
      else
	echo "</td>";
    }
  }
  echo "</tr>\n";    
  echo "</table>\n";
  echo "</td>\n";
  echo "</tr>";
  echo "<tr>";
  echo "<td width='25%' colspan='2'><span class='ficha'>Figure</span></td>";
  echo "<td width='75%' colspan='6'><img src='view_imageDB.php?argumento=$pFigureId' alt='No Figure'></td>";
  echo "</tr>";
  echo "<tr>";
  echo "<td width='50%' colspan='4'><span class='ficha'>Description of the construction in natural language</span>\n";
  echo "<td width='50%' colspan='4'><a href='$vNameXML'>$vNameXML</a></td>\n";
  echo "</tr>";
  echo "<tr>";
  echo "<td width='50%' colspan='4'><span class='ficha'>Figure in SVG format</span>\n";
  echo "<td width='50%' colspan='4'><a href='$vNameSVG'>$vNameSVG</a></td>\n";
  echo "</tr>";
// fim do ciclo
 }


//
// Theorem - Proofs Info --- A(s) provas(s) existente(s) para este teorema
//

//
// Vai chamar um outro programa por cada um dos ATPs existentes
//

// cria uma pesquisa --- para obter o número de provas e os provadores usados.
$sqlDem = "SELECT proverId
             FROM demonstrations
            WHERE teoId='$pTeoId'";

$resultadoDem = mysqli_query($ligacao,$sqlDem);
$nLinhasDem =mysqli_num_rows($resultadoDem);

if ($nLinhasDem==0) { // caso em que não há provas
  echo "<tr>";
  echo "<td width='100%' colspan='8' align='center'><span class='titulo'>$pTeoName - No Proofs</span></td>";
  echo "</tr>";
}
else { // caso em que há pelo menos uma prova
  
  echo "<tr>";
  echo "<td width='100%' colspan='8' align='center'><span class='titulo'>$pTeoName - Proofs Info</span></td>";
  echo "</tr>";
  
  // mostra os detalhes para cada uma das demonstrações
  $nDem=0; // inicializa contador a zero
  while ($linhaDem = mysqli_fetch_assoc($resultadoDem)) {
    
    $nDem=$nDem+1; // incrementa o contador das demonstrações
    
    if ($nDem>1) // linha de separação entre as demonstrações
      echo "<tr><td colspan='8'><hr></td></tr>";

    // O restante processamento é dependente do provador escolhido
    // vai obter o nome do Provador
    $pPrvId = trim($linhaDem['proverId']);

    if ($pPrvId==2) { // GCLCprover
      require('formGeoThmGCLCprover.php');
    }
    elseif ($pPrvId==3) { // GCLCprover+euk2gclc 
      // ---> tenho de ver isto com mais cuidado
      require('formGeoThmGCLCproverEuk.php');
    }
    elseif ($pPrvId==4) { //Coq+JNarboux (por antecipação)
      require('formGeoThmCoqJN.php');
    }
    // Fim do ciclo
  }
  echo "</table>";
}
?>

<hr/>

<?php
  require_once($entradaFILE.'footer.php');
?>
