Add DDAR example in the javascript interface and fix some code style.

Author: hzhangxyz

examples/ddar.ejs

@@ -0,0 +1,74 @@
+<%
+
+const ddar_data = `
+perp A B C D, perp C D E F, ncoll A B E => para A B E F
+cong O A O B, cong O B O C, cong O C O D => cyclic A B C D
+eqangle A B P Q C D P Q => para A B C D
+cyclic A B P Q => eqangle P A P B Q A Q B
+eqangle6 P A P B Q A Q B, ncoll P Q A B => cyclic A B P Q
+cyclic A B C P Q R, eqangle C A C B R P R Q => cong A B P Q
+midp E A B, midp F A C => para E F B C
+para A B C D, coll O A C, coll O B D => eqratio3 A B C D O O
+perp A B C D, perp E F G H, npara A B E F => eqangle A B E F C D G H
+eqangle a b c d m n p q, eqangle c d e f p q r u => eqangle a b e f m n r u
+eqratio a b c d m n p q, eqratio c d e f p q r u => eqratio a b e f m n r u
+eqratio6 d b d c a b a c, coll d b c, ncoll a b c => eqangle6 a b a d a d a c
+eqangle6 a b a d a d a c, coll d b c, ncoll a b c => eqratio6 d b d c a b a c
+cong O A O B, ncoll O A B => eqangle O A A B A B O B
+eqangle6 A O A B B A B O, ncoll O A B => cong O A O B
+circle O A B C, perp O A A X => eqangle A X A B C A C B
+circle O A B C, eqangle A X A B C A C B => perp O A A X
+circle O A B C, midp M B C => eqangle A B A C O B O M
+circle O A B C, coll M B C, eqangle A B A C O B O M => midp M B C
+perp A B B C, midp M A C => cong A M B M
+circle O A B C, coll O A C => perp A B B C
+cyclic A B C D, para A B C D => eqangle A D C D C D C B
+midp M A B, perp O M A B => cong O A O B
+cong A P B P, cong A Q B Q => perp A B P Q
+cong A P B P, cong A Q B Q, cyclic A B P Q => perp P A A Q
+midp M A B, midp M C D => para A C B D
+midp M A B, para A C B D, para A D B C => midp M C D
+eqratio O A A C O B B D, coll O A C, coll O B D, ncoll A B C, sameside A O C B O D => para A B C D
+para A B A C => coll A B C
+midp M A B, midp N C D => eqratio M A A B N C C D
+eqangle A B P Q C D U V, perp P Q U V => perp A B C D
+eqratio A B P Q C D U V, cong P Q U V => cong A B C D
+cong A B P Q, cong B C Q R, cong C A R P, ncoll A B C => contri* A B C P Q R
+cong A B P Q, cong B C Q R, eqangle6 B A B C Q P Q R, ncoll A B C => contri* A B C P Q R
+eqangle6 B A B C Q P Q R, eqangle6 C A C B R P R Q, ncoll A B C => simtri A B C P Q R
+eqangle6 B A B C Q R Q P, eqangle6 C A C B R Q R P, ncoll A B C => simtri2 A B C P Q R
+eqangle6 B A B C Q P Q R, eqangle6 C A C B R P R Q, ncoll A B C, cong A B P Q => contri A B C P Q R
+eqangle6 B A B C Q R Q P, eqangle6 C A C B R Q R P, ncoll A B C, cong A B P Q => contri2 A B C P Q R
+eqratio6 B A B C Q P Q R, eqratio6 C A C B R P R Q, ncoll A B C => simtri* A B C P Q R
+eqratio6 B A B C Q P Q R, eqangle6 B A B C Q P Q R, ncoll A B C => simtri* A B C P Q R
+eqratio6 B A B C Q P Q R, eqratio6 C A C B R P R Q, ncoll A B C, cong A B P Q => contri* A B C P Q R
+para a b c d, coll m a d, coll n b c, eqratio6 m a m d n b n c, sameside m a d n b c => para m n a b
+para a b c d, coll m a d, coll n b c, para m n a b => eqratio6 m a m d n b n c
+`;
+
+function statementToTerm(statement) {
+    const [predicate, ...objects] = statement.split(" ").map(s => s.trim());
+    return `(${predicate} ${objects.map(s => `\`${s}`).join(" ")})`;
+}
+
+for (let line of ddar_data.trim().split("\n")) {
+    const trimmedLine = line.trim();
+    if (trimmedLine !== "") {
+        const [premisesStr, conclusionStr] = trimmedLine.split(" => ");
+        const premises = premisesStr.split(",").map(p => p.trim());
+        const conclusion = conclusionStr.trim();
+        for (let premise of premises) {
+-%>
+    <%- statementToTerm(premise) %>
+<%
+}
+-%>
+-----------------------------------
+<%-
+statementToTerm(conclusion)
+%>
+
+<%
+}
+}
+%>

examples/ddar.mjs

@@ -0,0 +1,39 @@
+import express from "express";
+import ejs from "ejs";
+import { search } from "./search.mjs";
+
+const rules = await ejs.renderFile("examples/ddar.ejs");
+
+const app = express();
+
+app.use(express.text({ type: "*/*" }));
+
+app.post("/", (req, res) => {
+    const terms = req.body
+        .split(/[,;\n]/)
+        .map((x) => x.trim())
+        .filter((x) => x.length > 0)
+        .map((x) => `(${x})`)
+        .join("\n\n");
+    const data = [rules, terms]
+        .join("\n\n")
+        .split("\n\n")
+        .map((x) => x.trim())
+        .filter((x) => x.length > 0);
+    const result = [];
+    const generator = search(data, req.query.size || 1024, (candidate) => {
+        if (candidate.length() === 0) {
+            const str = candidate.conclusion().toString();
+            const toAppend = str.slice(1, -1);
+            result.push(toAppend);
+        }
+    });
+    while (true) {
+        if (generator.next().done) {
+            break;
+        }
+    }
+    res.type("text/plain").send(`${result.join(req.query.sep || ",")}\n`);
+});
+
+app.listen(3000);

examples/engine.mjs

@@ -7,9 +7,10 @@ import { search } from "./search.mjs";
 
 async function read_file_to_string_array(file_path) {
     const content = await readFile(file_path, "utf-8");
-    const sections = content.split(/\n\n/);
-    const results = sections.filter((section) => section.trim().length > 0).map((section) => section.trim());
-    return results;
+    return content
+        .split("\n\n")
+        .map((x) => x.trim())
+        .filter((x) => x.length > 0);
 }
 
 function default_callback(candidate) {

package.json

@@ -19,13 +19,16 @@
         "all": "run-s build test"
     },
     "devDependencies": {
+        "@rollup/plugin-commonjs": "^28.0.6",
+        "@rollup/plugin-json": "^6.1.0",
         "@rollup/plugin-node-resolve": "^16.0.1",
         "@rollup/plugin-terser": "^0.4.4",
         "@rollup/plugin-typescript": "^12.1.4",
         "@types/jest": "^30.0.0",
         "@web/rollup-plugin-copy": "^0.5.1",
         "cross-env": "^7.0.3",
         "ejs": "^3.1.10",
+        "express": "^5.1.0",
         "jest": "^30.0.5",
         "npm-run-all": "^4.1.5",
         "rollup": "^4.45.1",

rollup.config.mjs

@@ -1,4 +1,6 @@
+import json from "@rollup/plugin-json";
 import terser from "@rollup/plugin-terser";
+import commonjs from "@rollup/plugin-commonjs";
 import typescript from "@rollup/plugin-typescript";
 import nodeResolve from "@rollup/plugin-node-resolve";
 import { copy } from "@web/rollup-plugin-copy";
@@ -10,6 +12,7 @@ export default {
         example: "examples/main.mjs",
         search: "examples/search.mjs",
         engine: "examples/engine.mjs",
+        ddar: "examples/ddar.mjs",
     },
     output: {
         dir: "dist",
@@ -18,7 +21,9 @@ export default {
         entryFileNames: "[name].mjs",
     },
     plugins: [
+        json(),
         terser(),
+        commonjs(),
         typescript(),
         nodeResolve(),
         copy({