<?php
/*
 * Geothms/Forms/formGeoThmCoqAM.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.
 */

  
// Caso em que a prova foi feita pelo Coq + Area Method by J. Narboux

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

// vai obter a restante informação
$sqlDemPrv = "SELECT demId,code,proof,proofXML,dateSubmission,userId,status
                FROM demonstrations
               WHERE teoId='$pTeoId' 
                 AND proverId='$pPrvId'";

$resultadoDemPrv = mysqli_query($ligacao,$sqlDemPrv); 
$linhaDemPrv = mysqli_fetch_assoc($resultadoDemPrv);


$pDemId          = trim($linhaDemPrv['demId']);
$pCode           = trim($linhaDemPrv['code']);
$pDateSubmission = trim($linhaDemPrv['dateSubmission']);
$pUserIdPrv      = trim($linhaDemPrv['userId']);
//$pBibrefPrv      = trim($linhaDemPrv['bibrefId']);
$pStatus         = trim($linhaDemPrv['status']);

// Obtém o nome do Provador
$sqlPrv = "SELECT name,version
             FROM provers
            WHERE proverId='$pPrvId'";
$resultadoPrv = mysqli_query($ligacao,$sqlPrv);
$linhaPrv = mysqli_fetch_assoc($resultadoPrv);
  
// Obtém o identificador do Utilizador
$sqlUsr = "SELECT name,email
             FROM users
            WHERE userId='$pUserIdPrv'";
$resultadoUsr = mysqli_query($ligacao,$sqlUsr);
$linhaUsr = mysqli_fetch_assoc($resultadoUsr);


$pPrvName    = trim($linhaPrv['name']);
$pPrvVersion = trim($linhaPrv['version']);

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


// obtêm os dados sobre as Medidas de eficiência

$sqlProofMeasures = "SELECT timeCPU,CPU
                       FROM measures
                 INNER JOIN computer USING(computerId)   
                      WHERE measuresId='$pDemId'";

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


$linhaProofMeasures = mysqli_fetch_assoc($resultadoProofMeasures);

$vTimeCPU       = trim($linhaProofMeasures['timeCPU']);
$vComputerSpecs = trim($linhaProofMeasures['CPU']);


// a tabela
echo "<tr>";
echo "<tr>";
echo "<td width='25%' colspan='2'><span class='ficha'>Prover Name</span></td>";
echo "<td width='25%' colspan='2'>$pPrvName</td>";
echo "<td width='25%' colspan='2'><span class='ficha'>Prover Version</span></td>";
echo "<td width='25%' colspan='2'>$pPrvVersion</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='25%' colspan='2'>$pUserName</td>";
echo "</tr>";
echo "<tr>";
echo "<td width='25%' colspan='2'><span class='ficha'>Bibliographic Reference</span></td>"; 
echo "<td width='75%' colspan='6'>$pBibrefPrv"; 
// 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"; 

$sqlBibDem = "SELECT demonstrations.demId,teoId,bibrefId 
                FROM demonstrations INNER JOIN bibproofs 
                     ON demonstrations.demId=bibproofs.demId  
               WHERE teoId='$pTeoId'";

$resultadoBibDem = mysqli_query($ligacao,$sqlBibDem);


$nlinhasBibDem =  mysqli_num_rows($resultadoBibDem);

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

    echo "<td>$pBibRefDem"; 

    if ($nBibDem<$nlinhasBibDem) // coloca um ";" a separar as diferentes referências bibliográficas
      echo ";</td>";
    else
      echo "</td>";
  }
}
echo "</tr>\n";    
echo "</table>\n"; 
echo "</td>\n";
// Fim das refs bibs
echo "<tr>";
echo "<td width='12.5%' colspan='1'><span class='ficha'>Proof Status</span></td>";
if ($pStatus=='Proved')
  echo "<td width='87.5%' colspan='7'><font color='green'><b>$pStatus</b></font></td>";
else
  echo "<td width='87.5%' colspan='7'><font color='red'><b>$pStatus</b></font></td>";
echo "</tr>";
echo "<tr>";
echo "<td width='100%' colspan='8' align='center'><b>Measures of efficiency</b></td>";
echo "</tr>";
echo "<tr>";
echo "<td width='25%' colspan='2'><span class='ficha'>Time spent (seconds)</span></td>";
echo "<td width='25%' colspan='2' align='left'>$vTimeCPU</td>";
echo "<td width='50%' colspan='4' align='left'>$vComputerSpecs</td>";
echo "</tr>";

?>