Refactor node handling and HTML generation

1. Added `topsString` variable:
   - This variable is used to pass the top formula from the dialog.

2. Added unique ID attribute to node HTML:
   - Each node now has a unique ID to facilitate inserting new top nodes' HTML.
   - Created a new variable `topsElementId` to represent the location where new nodes will be inserted. This ID is determined in the `turnstileFunction()`.

3. Removed original `addNodeToTop` function from `sequentAst.js`:
   - The logic previously in `addNodeToTop` has been moved to the `handleSubmitAnswer` function in `App.vue`.

4. Renamed `generateProofTreeHTML` to `generateNodeHTML` in `sequentAst.js`:
   - The new `generateNodeHTML` function now only generates the node and `bottomLatex`.
   - The rule and the bar are now generated in the `handleSubmitAnswer()` function in `App.vue`.

5. Enhanced `handleSubmitAnswer()` function in `App.vue`:
   - This function now also handles the insertion of the new node HTML into the target `tops`.

src/App.vue

@@ -23,7 +23,7 @@
         </div>
       </el-main>
     </el-container>
-    <proof-step-dialog v-model:visible="isDialogVisible" v-model:statement="currentStatement" v-model:conclusionString="currentString" @submit-answer="handleSubmitAnswer" @next-answer="handleNextAnswer" />
+    <proof-step-dialog v-model:visible="isDialogVisible" v-model:statement="currentStatement" v-model:conclusionString="currentString" @submit-answer="handleSubmitAnswer" />
   </el-container>
 </template>
 
@@ -33,9 +33,9 @@ import 'katex/dist/katex.min.css';
 import renderMathInElement from 'katex/dist/contrib/auto-render';
 const ast = require('./utils/expAst.js');
 const { parse } = require("../src/utils/parser.js");
-//const { generateProofTreeHTML } = require("../src/utils/sequentAst.js");
+//const { generateNodeHTML } = require("../src/utils/sequentAst.js");
 
-const { sequentNode, generateProofTreeHTML } = require("../src/utils/sequentAst.js");
+const { sequentNode, generateNodeHTML } = require("../src/utils/sequentAst.js");
 
 export default {
   components: {
@@ -48,8 +48,8 @@ export default {
       currentStatement: '', // rendered statement to dialog
       currentString: '', // original input string to dialog
       errorMsg: '',
-      proofTree: null,
       isDialogVisible: false,
+      topsElementId: '',
     };
   },
   methods: {
@@ -63,42 +63,11 @@ export default {
       try {
         const targetAst = parse(this.givenStatement);
         this.latexStatement = ast.astsToLateX(targetAst);
-        this.proofTree = new sequentNode(this.latexStatement, this.givenStatement, null, []);
-
-
-        // this.proofTree = {
-        //   rule: "rule6",
-        //     bottomString: "X & (Y -> Z)",
-        //       bottomLatex: "\\vdash \\mathit{X} \\land (\\mathit{Y} \\rightarrow \\mathit{Z})",
-        //         topsLatex: [
-        //           {
-        //             rule: "rule3",
-        //             bottomLatex: "\\vdash \\mathit{X} \\land (\\mathit{Y} \\rightarrow Z)",
-        //             bottomString: "X & (Y -> Z)",
-        //             topsLatex: [
-        //               {
-        //                 rule: "",
-        //                 bottomLatex: "\\vdash \\mathit{X} \\land (\\mathit{Y} \\rightarrow \\mathit{Z})",
-        //                 bottomString: "X & (Y -> Z)",
-        //                 topsLatex: []
-        //               },
-        //               {
-        //                 rule: "",
-        //                 bottomLatex: "\\vdash \\mathit{X} \\land (\\mathit{Y} \\rightarrow \\mathit{Z})",
-        //                 bottomString: "X & (Y -> Z)",
-        //                 topsLatex: []
-        //               }
-        //             ]
-        //           },
-        //           {
-        //             rule: "",
-        //             bottomLatex: "\\vdash \\mathit{X} \\land (\\mathit{Y} \\rightarrow \\mathit{Z})",
-        //             bottomString: "X & (Y -> Z)",
-        //             topsLatex: []
-        //           }
-        //         ]
-        // };
+        const root = new sequentNode(this.latexStatement, this.givenStatement);
+        const rootHTML = generateNodeHTML(root);
 
+        // Insert the generated HTML into the page
+        document.getElementById('proof-tree').innerHTML = rootHTML;
 
         this.renderProofTree();
 
@@ -108,11 +77,6 @@ export default {
       }
     },
     renderProofTree() {
-      // Use this function to generate HTML
-      const proofTreeHTML = generateProofTreeHTML(this.proofTree);
-
-      // Insert the generated HTML into the page
-      document.getElementById('proof-tree').innerHTML = proofTreeHTML;
 
       // Call KaTeX directly to render
       renderMathInElement(document.getElementById('proof-tree'), {
@@ -121,7 +85,8 @@ export default {
           { left: "\\[", right: "\\]", display: true }
         ]
       });
-      this.turnstileFunction()
+
+      this.turnstileFunction();
     },
 
     // Hover effect
@@ -139,8 +104,32 @@ export default {
             const annotationElement = nodeElement ? nodeElement.querySelector('.katex-mathml') : null;
             let statement = annotationElement ? annotationElement.innerText : '';
 
+            // find the topsLatex of the nearst node
+            const topsElement = nodeElement.querySelector('.topsLatex');
+
+            console.log('topsElement', topsElement);
+            
+
+            if (!topsElement) {
+              this.errorMsg = 'topsLatex element not found.';
+              return;
+            }
+
+            console.log('topsElement.innerHTML', topsElement.innerHTML);
+
+            if (topsElement.innerHTML != "") {
+              this.errorMsg = 'This statement cannot be chosen: its top is full.';
+              return;
+            }
+
+            // get the id of the topsLatex element
+            this.topsElementId = topsElement.getAttribute('id');
+
+            
+            // start the proof
             this.openProofStepDialog(statement, originalInputString);
-            // do the add statement to node
+            
+            
           });
         }
       });
@@ -152,12 +141,66 @@ export default {
       this.currentString = originalInputString;
       this.isDialogVisible = true;
     },
-    handleSubmitAnswer(/* { rule, answer } */) {
-      // 处理提交的答案
-      this.isDialogVisible = false;
+
+
+    ruleToLatex(value) {
+      switch (value) {
+      case 'andIntroduction':
+          return '\\land \\mathit{I}';
+      case 'negationIntroduction':
+          return '\\neg \\mathit{I}';
+      case 'negationElimination':
+          return '\\neg \\mathit{E}';
+      case 'andRightElimination':
+          return '\\land \\mathit{E}_\\mathit{R}';
+      case 'andLeftElimination':
+          return '\\land \\mathit{E}_\\mathit{L}';
+      case 'orRightIntroduction':
+          return '\\lor \\mathit{I}_\\mathit{R}';
+      case 'orLeftIntroduction':
+          return '\\lor \\mathit{I}_\\mathit{L}';
+      case 'orElimination':
+          return '\\lor \\mathit{E}';
+      case 'implyIntroduction':
+          return '\\rightarrow \\mathit{I}';
+      case 'implyElimination':
+          return '\\rightarrow \\mathit{E}';
+      case 'contradiction':
+          return '\\mathit{Pbc}';
+      default:
+        return '';
+      }
     },
-    handleNextAnswer(/* { rule, answer } */) {
-      // 处理下一个答案的逻辑
+
+    handleSubmitAnswer(input) {
+
+    
+      const topsStrings = input.standardAnswer;
+      const rule = this.ruleToLatex(input.rule);
+
+      console.log("back from dialog, now is App");
+      console.log("input", input);
+      console.log("topsStrings", topsStrings);
+      // added new node to the top
+      console.log("this.topsElementId", this.topsElementId);
+      console.log("document.getElementById(this.topsElementId)", document.getElementById(this.topsElementId));
+      console.log("this.renderProofTree(topsStrings)", this.renderProofTree(topsStrings));
+      console.log("document.getElementById(this.topsElementId).innerHTML", document.getElementById(this.topsElementId).innerHTML);
+
+      const topsAsts = topsStrings.map(topsString => parse(topsString));
+
+      const topsLatexs = topsAsts.map(topsAst => ast.astsToLateX(topsAst));
+
+      for (let i = 0; i < topsLatexs.length; i++) {
+        const tops = new sequentNode(topsLatexs[i], topsStrings[i]);
+        document.getElementById(this.topsElementId).innerHTML += generateNodeHTML(tops);
+      }
+      document.getElementById(this.topsElementId).innerHTML += `<div class="bar"><div class="rule">\\(${rule}\\)</div></div>`;
+
+    
+      this.isDialogVisible = false;
+
+      this.renderProofTree();
     },
   },
 };

src/components/ProofStepDialog.vue

@@ -129,7 +129,13 @@ export default {
       this.clean();
     },
 
-    // 新增的方法
+    submitStandardAnswerToApp() {
+      // 提交答案逻辑
+      this.$emit('submit-answer', { standardAnswer: this.standardAnswer, rule: this.selectedRule });
+      this.clean();
+    },
+
+    
     submitExpression() {
       if (this.currentExpression) {
         this.expressions.push(parse(this.currentExpression));
@@ -213,6 +219,10 @@ export default {
 
       this.msg = 'Correct answer';
 
+      
+
+      this.submitStandardAnswerToApp();
+
       return;
     },
 

src/utils/sequentAst.js

@@ -13,23 +13,21 @@ function addRule(node, rule) {
     node.rule = rule;
 }
 
-function generateProofTreeHTML(node) {
+let nodeIdCounter = 0;
+
+
+// top is empty list
+function generateNodeHTML(node) {
+
     if (!node) return '';
 
-    // Generate the HTML for the current node
-    let html = '<div class="node" original-input-string="' + node.bottomString + '">';
-
-    
-    html += '<div class="topsLatex">';
-    if (node.rule) {
-        
-        // Recursively process prerequisite nodes
-        node.topsLatex.forEach(childNode => {
-            html += generateProofTreeHTML(childNode);
-        });
-        
-        html += `<div class="bar"><div class="rule">\\(${node.rule}\\)</div></div>`;
-    }
+    // Generate a unique id
+    const uniqueId = `tops-${nodeIdCounter++}`;
+
+    // Generate HTML for the current node
+    let html = `<div class="node" original-input-string="${node.bottomString}">`;
+
+    html += `<div class="topsLatex" id="${uniqueId}">`;
     html += '</div>';
 
     html += `<div class="bottomLatex"><span class="math">\\(${node.bottomLatex}\\)</span></div>`;
@@ -39,24 +37,7 @@ function generateProofTreeHTML(node) {
 }
 
 
-// existingNode and newNodeHTML are a rendered proof tree HTML string
-function addNodeToTop(existingNode, newNodeHTML) {
-    // 获取现有节点的 topsLatex 部分
-    const topsLatexElement = existingNode.querySelector('.topsLatex');
 
-    if (!topsLatexElement) {
-        console.error('topsLatex element not found.');
-        return;
-    }
-
-    if (!topsLatexElement.innerHTML) {
-        console.error('This node is already full, cannot add more html.');
-        return;
-    }
-
-    // 插入新节点
-    topsLatexElement.innerHTML = newNodeHTML;
-}
 
 
 // Define isSequentNode function to check if an object is an instance of sequentNode
@@ -88,7 +69,6 @@ module.exports = {
     sequentNode,
     isSequentNode,
     linkSequentNode,
-    generateProofTreeHTML,
+    generateNodeHTML,
     addRule,
-    addNodeToTop
 };
\ No newline at end of file