<?php

require '../FirstOrderLogicProp.inc.php';

class FOLP_HTML extends FOLPChecker
{
    function FOLP_HTML ($formula=NULL,$expand=FALSE) { parent::FirstOrderLogicProp($formula,$expand); }
    function printValuesTable ($border=1, $attrs='')
    {
        $formula = parent::toString();
        $table = parent::valuesTable();
        $vars = $table['vars'];
        $vals = $table['values'];
        echo '<table border="'.$border.'" '.$attrs.'>';
        echo '<tr>';
        foreach ($vars as $var) echo '<td align="center"><b style="color:darkblue">'.htmlentities($var).'</b></td>';
        echo '<td align="center"><b style="color:darkred">'.htmlentities($formula).'</b></td></tr>';
        foreach ($vals as $v) {
            echo '<tr>';
            foreach ($vars as $var) echo '<td align="center"><span style="color:darkblue">'.htmlentities($v['values'][$var]).'</span></td>';
            echo '<td align="center"><b style="color:darkred">'.$v['result'].'</b></td></tr>';
        }
        echo '</table>';
    }
}

function check ( $p )
{
    echo 'checking <b>'.htmlentities($p->toString()).'</b>...<br>';
    $p->check();
    if ($p->theorem) {
        echo 'This is a theorem !';
    }
    else {
        echo 'This is not a theorem. Here is a counterexample:<br>';
        echo 'If you affect ';
        foreach ($p->counterexample as $aff) {
            $var = $aff[0];
            $val = $aff[1]->toString();
            echo $val.' to "'.$var.'", ';
        }
        echo 'then the proposition becomes false.';
    }
}

$default = '(a <!> c) & (b -> c)';
$formula = isset($_POST['formula']) ? $_POST['formula'] : $default;
$p = new FOLP_HTML;//($formula);
$p->addSyntaxFile('syntax.litteral');
$p->parse($formula) or $formula = $default;
$p->printValuesTable();

if (isset($_POST['cunj'])) {
    $q = &$p->clone();
    $q->conjunctiveForm();
    echo 'Forme conjonctive: <b>'.htmlentities($q->toString()).'</b><br>';
    $q->destroy();
    unset($q);
}

if (isset($_POST['disj'])) {
    $q = &$p->clone();
    $q->disjunctiveForm();
    echo 'Forme disjonctive: <b>'.htmlentities($q->toString()).'</b><br>';
    $q->destroy();
    unset($q);
}

if (isset($_POST['check'])) check($p);

$p->destroy();
unset($p);


?>

<form method="post">
    <input type="text" value="<?php echo $formula; ?>" name="formula">
    <input type="submit" value="Envoyer"><br>
    <input type="checkbox" name="cunj">Afficher la forme conjonctive<sup style="color:red">*</sup><br>
    <input type="checkbox" name="disj">Afficher la forme disjonctive<sup style="color:green">*</sup><br>
    <input type="checkbox" name="check">Exécuter le prouveur sur la proposition<sup style="color:green">*</sup><br>
</form>
<sup style="color:green">*</sup> <small>le temps de calcul peut être important</small><br>
<sup style="color:red">*</sup> <small>ATTENTION le temps de calcul peut être TRES important</small><br>
<hr>
<b>Syntaxes:</b><br>
<ul>
    <li>TRUE: "TRUE" ou "1"
    <li>FALSE: "FALSE" ou "0"
    <li>NOT: "NOT" ou "!"
    <li>AND: "AND" ou "&"
    <li>NAND: "NAND" ou "!&"
    <li>OR: "OR" ou "|"
    <li>NOR: "NOR" ou "!|"
    <li>XOR: "XOR" ou "&lt;!&gt;"
    <li>IMPLIES: "IMPLIES" ou "-&gt;"
    <li>NOT_IMPLIES: "NOT_IMPLIES" ou "-!&gt;"
    <li>IMPLIED:        "IMPLIED_BY" ou "&lt;-"
    <li>NOT_IMPLIED:    "NOT_IMPLIED_BY" ou "&lt;!-"
    <li>IFF:            "IF_ONLY_IF" ou "&lt;-&gt;"
</ul>