Hello,
Here is my problem. The code below, that is the code of the page called "index.php" works. < https://www.vidal-rosset.net/fCube/ > But I would be happy to have this prover in this web page < https://www.vidal-rosset.net/fcube_an_efficient_prover_for_intuitionistic_propositional_logic.html > that I have made from org-mode. Unfortunately, all my efforts to integrate this code to export failed, and finally I get a JSON.parse error, ( json-parse-unexpected-character-at-line-1-column-1-of-the-json-data ) that I suspect to be a PHP error code. Your help is welcome. Best wishes, and Merry Christmas ! Jo. PS: the code to export from an org-mode file would be this one (that of index.php file, presently): <?php if ($f_encoded = ($_POST['formula'] ?? null)) { $formula = urldecode($f_encoded); // swipl will need the full path, so // assume quineweb.pl is in the same folder as this php script $fcube = __DIR__ . '/fcubeweb.pl'; $descp = [ 0 => ['pipe','r'], 1 => ['pipe','w'], //2 => null ]; $proc = proc_open("swipl -g fcube -g halt $fcube", $descp, $pipes); if (is_resource($proc)) { fwrite($pipes[0], $formula); fclose($pipes[0]); $Proof = stream_get_contents($pipes[1]); fclose($pipes[1]); $return_value = proc_close($proc); header('Content-type: application/json'); echo json_encode(['proof'=>$Proof,'formula'=>'TBD']); } exit; } ?> <!DOCTYPE html> <html lang="en"> <head> <!-- 2020-08-13 jeu. 09:08 --> <meta charset="utf-8"> <meta name="viewport" content="width=device-width, initial-scale=1"> <title>index</title> <meta name="generator" content="Org mode"> <link rel="stylesheet" type="text/css" href="css/org.css"/> <link rel="stylesheet" type="text/csl" href="ieee.csl"/> <link rel="icon" href="ico/favicon.ico" type="image/x- icon"> <script type="text/javascript"> /* @licstart The following is the entire license notice for the JavaScript code in this tag. Copyright (C) 2012-2020 Free Software Foundation, Inc. The JavaScript code in this tag is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License (GNU GPL) as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. The code is distributed WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU GPL for more details. As additional permission under GNU GPL version 3 section 7, you may distribute non-source (e.g., minimized or compacted) forms of that code without the copy of the GNU GPL normally required by section 4, provided you include this license notice and a URL through which recipients can access the Corresponding Source. @licend The above is the entire license notice for the JavaScript code in this tag. */ <!--/*--><![CDATA[/*><!--*/ function CodeHighlightOn(elem, id) { var target = document.getElementById(id); if(null != target) { elem.cacheClassElem = elem.className; elem.cacheClassTarget = target.className; target.className = "code-highlighted"; elem.className = "code-highlighted"; } } function CodeHighlightOff(elem, id) { var target = document.getElementById(id); if(elem.cacheClassElem) elem.className = elem.cacheClassElem; if(elem.cacheClassTarget) target.className = elem.cacheClassTarget; } /*]]>*///--> </script> </head> <body> <div id="content"> <div class="head"> <div class="title"> <p> <a href= "https://www.swi-prolog.org/";><img src="swi-prolog-logo.png" width="50" height="50"></a> <a href="index.html">FCUBE 4.1 WITH INFIX NOTATION</a> </p> </div> </nav> <div> <div> </script> <script> MathJax = { loader: { load: ['[tex]/bussproofs'] }, tex: { packages: {'[+]': ['bussproofs']}, tags: 'ams' } }; </script> <script id="MathJax-script " async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js";> </script> </head> <body> <div id="content"> <h3>Syntax for input formulas: ~a , a & b, a | b ,a =>b , a <=> b (for, respectively, negation, conjunction, disjunction, conditional and biconditional . </h3> <label> <p> Choose a formula in the list below, or input your one</p> <?=formulae_predef()?> </label> </div> <textarea id=formula rows=1 cols=100% title='enter your formula here, or select one predefined above'> </textarea> <div> <button id=decide_formula><img src="swi-prolog-logo.png" width="35" height="35"> <b> ? - </b></button> <pre id=proof_show>Either an intuitionistic proof or an intuitionistic refutation will show here</pre> </div> </div> <?=css()?> <?=js()?> </html> <?php function formulae_predef() { ob_start();?> <select id=formulae_predef> <option> ~ a | a /* Excluded Middle */ </option> <option> ~ ~ a => a /* Double Negation Elimination */ </option> <option>((a => b) => a) => a /* Pierce Formula */ </option> <option>((~ a => b) & (a => b)) => b /* Dilemma */ </option> <option>(a => b) | (b => a) /* Dummett Formula */ </option> <option>~(a & b) => (~ a | ~ b) /* Classical de Morgan Implication */</option> <option>(~ a | ~ b) => ~(a & b) /* Intuitionistic de Morgan Implication */</option> <option>~(a | b) <=> (~ a & ~ b) /* Intuitionistic De Morgan Equivalence */</option> <option>(~ a => a) <=> ~ ~ a /* Intuitionistic Equivalence */</option> <option> ( ( p | ( q & r ) ) <=> ( ( p | q ) & ( p | r ) ) ) /* Pelletier Problem 13 SYN045+1 */</option> <option> ( ( ( p & ( q => r ) ) => s ) <=> ( ( ~ p | q | s ) & ( ~ p | ~ r | s ) ) ) /* Pelletier Problem 17 SYN047+1 */ </option> <option>((a | b) => c) <=> ((a => c) & (b => b)) </option> <option>((a & b) => c) <=> ((a => c) | (b => c)) </option> <!-- add more, to illustrate accepted syntax --> </select> <?php return ob_get_clean(); } function css() { ob_start();?> <style> </style> <?php return ob_get_clean(); } function js() { ob_start();?> <script> window.onload = () => { const request = (url,formula) => fetch(url,{ method: 'POST', headers: { 'Content-Type': 'application/x-www-form-urlencoded;charset=UTF-8' }, body: 'formula='+encodeURIComponent(formula) }).then(r => r.json()) decide_formula.onclick = async (ev) => { let f = formula.value.trim() if (!f.endsWith('.')) f += '.' try { let result = await request("<?=$_SERVER['REQUEST_URI']?>", f) if (result.proof) proof_show.textContent = result.proof else proof_show.innerHTML = 'there was a problem:<b>'+JSON.stringify(result)+'<b>' } catch(e) { alert(e.message) } } formulae_predef.onchange = (ev) => { formula.value = ev.target.value } } </script><?php return ob_get_clean(); }
