Show proof status on the left bar: complete, complete with Z3, incomplete, unprovable

Author: joom

index.html

@@ -116,9 +116,12 @@
         border-bottom: 1px solid white;
         padding: 1em 0.2em 1em 0.2em;
       }
-      #left-bar ol li span {
+      #left-bar ol li span.conclusion {
         cursor: pointer;
       }
+      span.resultOk { color: #4cd625; }
+      span.resultBad { color: #dc3545; }
+      span.resultIncomplete { color: #FFA500; }
       .selected {
         background: #0d6efd;
       }

src/app.js

@@ -182,14 +182,27 @@ const refreshList = () => {
   let ol = document.querySelector('#left-bar ol')
   ol.innerHTML = ''
   proofs.forEach((entry, i) => {
+    let status = entry.proof.status()
+    let result = ``
+    if (status instanceof Unprovable) {
+      result = `<span class="resultBad">✖</span>`
+    } else if (status instanceof Incomplete) {
+      result = `<span class="resultIncomplete">✎</span>`
+    } else if (status instanceof CompleteWithZ3) {
+      result = `<span class="resultOk">✓*</span>`
+    } else if (status instanceof Complete) {
+      result = `<span class="resultOk">✓</span>`
+    }
+
     ol.innerHTML += `<li value="${i}" class="${entry.selected ? 'selected' : ''}">
-                        <span onclick="javascript:selectProof(${i})">
+                        <span class="conclusion" onclick="javascript:selectProof(${i})">
                         ${entry.proof.conclusion.unicode()}
                         </span>
                         <br>
                         <button onclick="javascript:giveLatex(${i})" class="latex">L<sup>a</sup>T<sub>e</sub>X</button>
                         <button onclick="javascript:removeProof(${i})">✖ Delete</button>
                         <button onclick="javascript:saveProof(${i})">💾 Save</button>
+                        ${result}
                      </li>`
   })
 }

src/schema.js

@@ -18,6 +18,12 @@ const deepEqual = (x, y) => {
 // Check if argument (arr) is array of objects type (cl)
 const arrayOf = (arr, cl) => arr instanceof Array && arr.every(a => a instanceof cl)
 
+class Status { }
+class Complete extends Status { }
+class CompleteWithZ3 extends Status { }
+class Incomplete extends Status { }
+class Unprovable extends Status { }
+
 class Term {
   constructor () {
     if (new.target === Term) {
@@ -548,6 +554,14 @@ ${rule}
         throw new TypeError(`Don't know how to typeset a judgment with ${this.premises.length} premises`)
     }
   }
+
+  status () {
+    let prems = this.premises.map(p => p.status())
+    if(prems.some(s => s instanceof Unprovable)) { return new Unprovable() }
+    if(prems.some(s => s instanceof Incomplete)) { return new Incomplete() }
+    if(prems.some(s => s instanceof CompleteWithZ3)) { return new CompleteWithZ3() }
+    return new Complete()
+  }
 }
 
 // Beginning of LK rules
@@ -1189,13 +1203,24 @@ class Z3Rule extends LKProofTree {
         canvas.remove(obj)
       })
       proofs.map(p => p.proof.draw())
+      refreshList()
 
     })
   }
 
   reconstructor () {
     return `new Z3Rule(${this.conclusion.reconstructor()})`
   }
+
+  status () {
+    if (this.z3Response === true) {
+      return new CompleteWithZ3()
+    } else if (this.z3Response === false) {
+      return new Unprovable()
+    } else {
+      return new Incomplete()
+    }
+  }
 }
 
 class LKIncomplete extends LKProofTree {
@@ -1224,6 +1249,14 @@ class LKIncomplete extends LKProofTree {
       return `new LKIncomplete(${this.conclusion.reconstructor()})`
     }
   }
+
+  status () {
+    if (this.completer) {
+      return this.completer.status()
+    } else {
+      return new Incomplete()
+    }
+  }
 }
 
 // End of LK rules
@@ -1577,6 +1610,14 @@ ${rule}
         throw new TypeError(`Don't know how to typeset a judgment with ${this.premises.length} premises`)
     }
   }
+
+  status () {
+    let prems = this.premises.map(p => p.status())
+    if(prems.some(s => s instanceof Unprovable)) { return new Unprovable() }
+    if(prems.some(s => s instanceof Incomplete)) { return new Incomplete() }
+    if(prems.some(s => s instanceof CompleteWithZ3)) { return new CompleteWithZ3() }
+    return new Complete()
+  }
 }
 
 /*
@@ -1805,6 +1846,14 @@ class HoareIncomplete extends HoareProofTree {
       return `new HoareIncomplete(${this.conclusion.reconstructor()})`
     }
   }
+
+  status () {
+    if (this.completer) {
+      return this.completer.status()
+    } else {
+      return new Incomplete()
+    }
+  }
 }
 
 // If a tree is set as toDelete, delete the tree and its premises