<?php 
session_start();
/*
 * Interaction/insertCodeProver.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');
}

// coloca o valor para a página de ajuda apropriada
$_SESSION['helpsection']='interaction';

require_once($entradaFILE.'dbLogin.php');

?>

<?php



  // carregar das funções do bloco de notas
require_once($entradaFILE."Scrapbook/functionsScrapbook.php");


$argumento = $_GET['argumento'];


if (isset($_GET['teoId'])) {
  $vTeoId = $_GET['teoId'];
}
else {
  $vTeoId = 'GEO0000'; // valor por omissão
}
     
$insercao  = $_GET['insercao']; // primeira vez, ou actualização

// selecciona o Id de utilizador para poder referênciar o ficheiro
// escrito na fase da avaliação.
$username = $_SESSION['username'];
// cria uma pesquisa
$sqlUserId = "SELECT userId
                FROM users
               WHERE username ='$username'";

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

$pUserId     = trim($linhaUserId['userId']);

$vNameProofPDF = 'proof'.$pUserId.'.pdf';

// Testa se é uma nova sessão ou se já estamos a re-introduzir código
// temos três casos
// i) entrada a partir do menu de opções => primeira vez
// ii) entrada após a escolha de um resultado da BD 
// iii) entrada a partir da secção de interacção com as figuras
if (!isset($_GET['argumento'])) { 
  // i) primeira vez
  // pode ser a primeira de todas ou então a escolha de um resultado da BD
  // em ambos os casos o ficheiro é chamado sem argumentos "get".

  $insercao=1; // coloca inserção a verdade para marcar que passa a
	       // ser uma escolha de um resultado da BD
  // nesse caso apaga o ficheiro anterior
  system("rm proof*");
  $pTeoIdName = $_POST['TeoIdName'];


  //GEO0004 -- Thales' Theorem -- (21,GCLC, Area Method)

  $pCodeTmpIdName = $_SESSION['CodeTmpIdName']; // escolha de uma
						// construção do bloco
						// de notas


  // vai fazer a agora a separação entre i e (ii ou iii)
  if (isset($_POST['TeoIdName']) || isset($_POST['filename'])) { 
    if (isset($pTeoIdName)) { // neste caso já é a escolha de um
			     // resultado dado que a variável "post"
			     // já tem um valor
      preg_match("#([A-Z0-9]+) -- ([A-Za-z0-9\\\' _.-]+) \(([0-9]+)#",$pTeoIdName,$matches);
      
      $vTeoId = $matches[1];
      $vDemId = $matches[3];
      //$vTeoName = $matches[2];

      // get the prover's code
      $sqlProofCode = "SELECT code,proverId
                         FROM demonstrations
                        WHERE demId='$vDemId'";
      $resultadoProofCode = mysqli_query($ligacao,$sqlProofCode);
      $linhaProofCode = mysqli_fetch_assoc($resultadoProofCode);
      $pCode      = trim($linhaProofCode['code']);
      $pPrvId     = trim($linhaProofCode['proverId']);
    }
    else { // caso em que o código vem da secção da interacção com os DGSs
      // é necessário fazer a leitura a partir do ficheiro auxiliar

      $vNameAux=$_POST['filename'];
      // get the figure's code

      $codefile=fopen($vNameAux,"r");
      $pCode=fread($codefile, filesize($vNameAux));
      fclose($codefile);  

      $pCode      = trim($pCode);
      // acrescenta uma linha de separação entre o código da figura e
      // a conjectura
      $pCode = $pCode."\n\n\n%------conjecture------%\n\n\n";
      $pDrwId     = trim($_POST['drawerId']);
      if ($pDrwId==2) {// Eukleides 
          $pPrvId=3; // GCLCprover+euk2eps
      }
      elseif ($pDrwId==3) {// GCLC 
          $pPrvId=2; // GCLCprover Area Method
      }
      else // outros DGSs (no futuro)
          $pPrvId=1; // sem provador associado
      $vTeoId='GEO0000'; // uma nova conjectura
    }
  } elseif (isset($pCodeTmpIdName)) { // o resultado vem é do bloco de notas
    
    preg_match("§([0-9]+) - ([A-Za-z0-9 _.]+)§",$pCodeTmpIdName,$matches);
    
    
    $pCodeTmpId = $matches[1];
    
    $scrapbookMode="prover";
    scrapbook_get_code($scrapbookMode,$pCodeTmpId,$ligacao,$pCode,$pDrwId);
  } // senão (vazio) é a primeira de todas
    // este caso não é importante dado que aqui é o começo de todo o
    // processo, isto é, neste caso a textarea está vazia e, é tudo.
 }
 else {
   $insercao=0; // falso
  
   // cria uma pesquisa
   $sqlPrvCodeTmp = "SELECT code,proverId,proof,proofResults
                       FROM codeTmp
                      WHERE codeTmpId ='$argumento'";

   $resultadoPrvCodeTmp = mysqli_query($ligacao,$sqlPrvCodeTmp);
   $linhaPrvCodeTmp = mysqli_fetch_assoc($resultadoPrvCodeTmp);

   $pPrvId        = trim($linhaPrvCodeTmp['proverId']);
   $pCode         = trim($linhaPrvCodeTmp['code']);
   $pCodeTmpId    = $argumento;
   $pProof        = trim($linhaPrvCodeTmp['proof']);
   $pProofResults = trim($linhaPrvCodeTmp['proofResults']);
}

if ($pPrvId==2) { // 2=GCLCprover -> GCLC
  // Inicialização da janela de textarea/javascript

  echo "<script language=\"Javascript\" type=\"text/javascript\">\n";
  echo "editAreaLoader.init({
        id: \"ProverCode\"	// id of the textarea to transform		
          ,start_highlight: true	// if start with highlight
          ,allow_resize: \"both\"
          ,allow_toggle: false
          ,language: \"en\"
          ,syntax: \"gclc\"	
      });\n";
  echo "</script>\n\n";
}
elseif ($pPrvId==3) { // 3=GCLCproverEuk -> Eukleides
  // Inicialização da janela de textarea/javascript
  
  echo "<script language=\"Javascript\" type=\"text/javascript\">\n";
  echo "editAreaLoader.init({
        id: \"ProverCode\"	// id of the textarea to transform		
          ,start_highlight: true	// if start with highlight
          ,allow_resize: \"both\"
          ,allow_toggle: false
          ,language: \"en\"
          ,syntax: \"eukleides\"	
      });\n";
  echo "</script>\n\n";
}
else { // 4 = COQareaMethod -> tenho ainda de fazer um estilo próprio (O coqam=gclc)
  // Inicialização da janela de textarea/javascript
  
  echo "<script language=\"Javascript\" type=\"text/javascript\">\n";
  echo "editAreaLoader.init({
        id: \"ProverCode\"	// id of the textarea to transform		
          ,start_highlight: true	// if start with highlight
          ,allow_resize: \"both\"
          ,allow_toggle: false
          ,language: \"en\"
          ,syntax: \"coqam\"	
      });\n";
  echo "</script>\n\n";
}

// cria uma pesquisa - para a lista de provers
$sql = "SELECT proverId,name,version
          FROM provers";

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

$ncampos =mysqli_num_fields($resultado);


$linha = mysqli_fetch_assoc($resultado);

// uma forma bacoca de retirar o primeiro valor "No prover selected"
$pProverId       = $linha['proverId'];
$pName           = $linha['name'];
$pVersion        = $linha['version'];


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'>Geometric Prover Workbench</span></td>";
echo "</tr>";
if (1) { // Isto é o que se chama fazer as coisas à bruta !?!?!?
  echo "<form action='insertCodeProver.php' method='post'>";
  echo "<tr>";
  //  echo "<td width='25%' colspan='2'>&nbsp;</td>";
  echo "<td width='12.5%' colspan='1' align='right'><span class='ficha'>Proofs Listing</span></td>";
  // select a theorem from the database - only those that do have a
  // demonstration
  $sqlListaBD = "SELECT teoName,theorems.teoId,demonstrations.proverId,
                        demonstrations.demId
                   FROM theorems,demonstrations 
                  WHERE theorems.teoId=demonstrations.teoId
                    AND level=0
               ORDER BY teoId";
  $resultadoListaBD = mysqli_query($ligacao,$sqlListaBD);
  echo "<td width='62.5%' colspan='5'><span class='entrada'><SELECT NAME='TeoIdName'>";
  $pTeoIdAux='GEO0000';
  $pTeoNameAux='New Conjecture';
  print "<option selected>$pTeoIdAux -- $pTeoNameAux</option>\n"; 
  while ($linhaListaBD = mysqli_fetch_assoc($resultadoListaBD)){
    $pTeoIdAux=trim($linhaListaBD['teoId']);
    $pTeoNameAux=trim($linhaListaBD['teoName']);
    $pPrvCodeAux=trim($linhaListaBD['proverId']); 
    $pDemIdAux=trim($linhaListaBD['demId']);
    //
    // Os nomes dos provadores aqui são "hardcoded" 
    //
    if ($pPrvCodeAux=='2') $pPrvNameAux='GCLC, Area Method';
    elseif ($pPrvCodeAux=='3') $pPrvNameAux='GCLCproverEuk';
    elseif ($pPrvCodeAux=='4') $pPrvNameAux='Coq Area Method';
    elseif ($pPrvCodeAux=='5') $pPrvNameAux='GCLC, Method of Wu';
    elseif ($pPrvCodeAux=='6') $pPrvNameAux='GCLC, Groebner Basis Method';
    if ($vTeoId==$pTeoIdAux && $vDemId==$pDemIdAux)
      print "<option selected>$pTeoIdAux -- $pTeoNameAux ($pDemIdAux,$pPrvNameAux)</option>\n"; 
    else
      print "<option>$pTeoIdAux -- $pTeoNameAux -- ($pDemIdAux,$pPrvNameAux)</option>\n"; 
  };
  echo "</SELECT>";
  echo "</td>";
  echo "<td width='25%' colspan='2' align='center'><input type='submit' value='&nbsp;&nbsp;&nbsp;choose a Theorem&nbsp;&nbsp;&nbsp;'></td>";
  echo "</tr>\n";
  echo "</form>";
 }
// linha de separação
echo "<tr><td colspan='8'><hr></td></tr>";

// ================================================
// Bloco de Notas - Guardar & Seleccionar & Apagar
// ================================================

// Uma linha da tabela


// =====================================
// Introdução da barra do Bloco de Notas
// =====================================
echo "<tr>\n";
echo "<td colspan='8'>\n";
$pathToScrapbook = "../Scrapbook";
$nameCallingForm="Interaction/insertCodeProver.php";
$scrapbookMode="prover";
$saveActive=1;
$selectActive=1;
$deleteActive=1;
require_once($entradaFILE."Scrapbook/scrapbook.php");
echo "</td>\n";
echo "</tr>\n";


// ================================================
// Formulário respeitante à (re)avaliação do código
// ================================================
echo "<form enctype='multipart/form-data' action='iInsertCodeProver.php' method='post'>";

echo "<tr>";
echo "<td width='12.5%' colspan='1'>\n";
echo "<table>\n";
echo "<tr>
       <td align='right'>
        <span class='ficha'>Code</span>
       </td>
      </tr>\n";
echo "<tr>
       <td>&nbsp;</td>
      </tr>\n";
echo "<tr>
       <td>&nbsp;</td>
      </tr>\n";
echo "<tr>\n";
echo "<td align='center'>
        <span class='ficha'>Prover</span>\n";
// select a Prover form a list of Provers
$sql_prover_idnameversion = "SELECT proverId,name,version
                               FROM provers
                              WHERE NOT(name='No prover selected')
                           ORDER BY proverId";
$resultado_prover_idnameversion = mysqli_query($ligacao,$sql_prover_idnameversion);
echo "<span class='entrada'><SELECT NAME='PrvIdNameVersion'>";
while ($linha = mysqli_fetch_assoc($resultado_prover_idnameversion)){
  $pProverId=trim($linha['proverId']);
  $pProverName=trim($linha['name']);
  $pProverVersion=trim($linha['version']);
  if ($pPrvId==$pProverId)
    print "<option selected>$pProverId -- $pProverName -- $pProverVersion</option>\n";
  else
    print "<option>$pProverId -- $pProverName -- $pProverVersion</option>\n"; 
 };
echo "</SELECT>";
echo "</td>";
echo "</tr>  ";
echo "<tr>
       <td>&nbsp;</td>
      </tr>\n";
echo "<tr>
       <td>&nbsp;</td>
      </tr>\n";
echo "<tr>
       <td align='center'>
        <input type='submit' value='&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(re)evaluate the code&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;'>
       </td>
      </tr>\n";
echo "</table>\n";
echo "</td>\n";
echo "<td width='37.5%' colspan='3'>
       <TEXTAREA id='ProverCode' NAME='ProverCode' ROWS='30' COLS='60'>$pCode</TEXTAREA>
      </td>";

$filename = $vNameProofPDF;
$texfile=fopen($filename,"w");
fwrite($texfile,$pProof); 
fclose($texfile);  

if  (file_exists($filename) and filesize($filename)>0) { // re-avaliação
  // o ficheiro da prova existe e é não nulo
  echo "<td width='50%' colspan='4' align='center'>\n";
  echo "<table>";
  echo "<tr>";
  echo "<td colspan='6' align='center'><hr></td>";
  echo "</tr>";
  echo "<tr>";

  // O mostrar dos resultados está dependente do provador utilizado

  if ($pPrvId == 2) { // GCLCprover, Area Method
    require('showResultsGCLCprover.php');
  }
  elseif ($pPrvId == 3) { // GCLCprover+euk2gclc 
    // ---> tenho de ver isto com mais cuidado
    require('showResultsGCLCproverEuk.php');
  }
  elseif ($pPrvId == 4) { //Coq+JNarboux
    require('showResultsCoqJN.php');
  }
  elseif ($pPrvId == 5) { // GCLCprover, Method of Wu
    require('showResultsGCLCproverWM.php');
  }
  elseif ($pPrvId == 6) { // GCLCprover, Groebner Basis Method
    require('showResultsGCLCproverGBM.php');
  }
}
else // É a primeira vez - o ficheiro da prova não existe ou é nulo
echo "<td width='50%' colspan='4' align='center'>Proof Results</td>";
echo "</tr>";
echo "<input type='hidden' name='insercao' value=$insercao>";
echo "<input type='hidden' name='CodeTmpId' value=$pCodeTmpId>";
echo "<input type='hidden' name='TeoId' value=$vTeoId>";
echo "</form>";
// // se se trata de uma nova conjectura 
// //  e o utilizador é um contribuidor
// //  e já foi introduzido um dado código
// // então
// //  vai-se oferecer a possibilidade de incluir o novo resultado na base
// // de dados
// if ($vTeoId=="GEO0000" && $pTipoUtilizador!="anonymous" && $pCode!="") {
//   echo "<tr>";
//   // inserir um novo resultado na base de dados.
//   // grava-se o resultado num ficheiro e passa-se o nome do ficheiro
//   // através do método POST
//   echo "<form enctype='multipart/form-data' action='../Geothms/insertGeoThmFigPrf.php' method='post'>";  
//   echo "<input type='hidden' name='teoId' value=$vTeoId>";
//   // a identificação do provador usado passa escondida
//   echo "<input type='hidden' name='proverId' value=$pPrvId>";

//   // escreve um ficheiro auxiliar com o código
//   $vNameAux = 'auxProof'.$pUserId.'.code';

//   $filename = $vNameAux;
//   $texfile=fopen($filename,"w");
//   fwrite($texfile,$pCode); 
//   fclose($texfile);  
//   // passa (escondido) o nome do ficheiro escrito 
//   echo "<input type='hidden' name='filename' value=$vNameAux>";
//   echo "<td width='100%' colspan='8' align='right'><input type='submit' value='&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Go to the \"New Result Form\" section to submit a new result to the database&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;'></td>";
//   echo "</tr>";echo "<tr>";
//   echo "</tr>  ";
//   echo "</form>";
// }
echo "</table>";

?>

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