Graphiti: Add option to show unknown edges (teorth#440)

As per [1], add the ability to graph unknown implications with dotted edges, and make it easy to navigate to this graph from the equation explorer. ![65](https://github.com/user-attachments/assets/cfaf9026-304e-465e-9919-25fd5c17865f) [1] https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Equation.2065.20-.3E.20left.20cancellability/near/475352370
b-mehta · Oct 8, 2024 · 5e82e8e · 5e82e8e
1 parent a326d6d
commit 5e82e8e
Show file tree

Hide file tree

Showing 4 changed files with 109 additions and 32 deletions.
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
@@ -153,7 +153,8 @@ jobs:
       - name: Generate home_page/graphiti/graph.json
         run: |
           ~/.elan/bin/lake exe extract_implications --json > /tmp/implications.json
-          ruby scripts/generate_graphiti_data.rb /tmp/implications.json > home_page/graphiti/graph.json
+          ~/.elan/bin/lake exe extract_implications unknowns > /tmp/unknowns.json
+          ruby scripts/generate_graphiti_data.rb /tmp/implications.json /tmp/unknowns.json > home_page/graphiti/graph.json
 
       - name: Build website using Jekyll
         if: github.event_name == 'push' && env.HOME_PAGE_EXISTS == 'true'

diff --git a/home_page/graphiti/index.html b/home_page/graphiti/index.html
@@ -7,15 +7,6 @@
     <title>Graphiti</title>
 
     <style>
-      /* Styling for the links */
-      .node a {
-        text-decoration: none; /* Remove underline */
-        color: blue; /* Link color */
-      }
-      .node a:hover {
-        color: red; /* Change color on hover */
-      }
-
       body {
         font-family: Arial, sans-serif;
         margin: 0;
@@ -28,11 +19,28 @@
         background: white;
         padding: 20px;
         border-radius: 5px;
+        display: flex;
+        align-items: left;
+      }
+      input[type="text"] {
+        width: 100%; /* Make text inputs take up full width */
+        box-sizing: border-box; /* Ensure padding and border are included in the element's width */
+      }
+      button {
+        width: 100%; /* Make text inputs take up full width */
+        box-sizing: border-box; /* Ensure padding and border are included in the element's width */
+      }
+
+      .checkbox-container {
+        display: flex;
+        flex-direction: row; /* Ensures checkbox and label are in a row */
+        align-items: center;
       }
 
       form {
         display: flex;
         flex-direction: column;
+        align-items: flex-start; /* Aligns all form elements to the left */
       }
 
       label {
@@ -130,6 +138,17 @@
         >
         <input type="text" id="highlight_blue" name="highlight_blue" /><br />
 
+        <div class="checkbox-container">
+          <input
+            type="checkbox"
+            id="show_unknowns_conjectures"
+            name="show_unknowns_conjectures"
+          />
+          <label for="show_unknowns_conjectures"
+            >Show unknowns and conjectures</label
+          >
+        </div>
+
         <button type="submit">Submit</button>
       </form>
 
@@ -158,7 +177,7 @@
         <li>
           <a
             href="#"
-            onclick="fillForm({implies: '43', max_variables: '3', hightlight_red: '43'})"
+            onclick="fillForm({implies: '43', max_variables: '3', highlight_red: '43'})"
             >Equations up to 3 variables implied by the commutative law</a
           >
         </li>
@@ -231,7 +250,11 @@ <h1 id="message"></h1>
         const inputs = form.getElementsByTagName("input");
 
         for (let input of inputs) {
-          if (input.type != "hidden") {
+          if (input.type == "hidden") {
+            continue;
+          } else if (input.type === "checkbox") {
+            input.checked = false; // Uncheck all checkboxes
+          } else {
             input.value = ""; // Clear all fields
           }
         }
@@ -240,7 +263,11 @@ <h1 id="message"></h1>
         Object.keys(params).forEach((key) => {
           const inputField = form.querySelector(`input[name="${key}"]`);
           if (inputField) {
-            inputField.value = params[key];
+            if (inputField.type === "checkbox") {
+              inputField.checked = params[key]; // Set checkbox value
+            } else {
+              inputField.value = params[key];
+            }
           }
         });
       }
@@ -273,14 +300,15 @@ <h1 id="message"></h1>
       function populateForm() {
         const params = new URLSearchParams(window.location.search);
 
-        // Loop through all input elements in the form
-        const inputs = document.querySelectorAll(
-          "#searchForm input, #searchForm textarea",
-        );
-        inputs.forEach((input) => {
-          const name = input.name; // Get the name of the input field
-          if (params.has(name)) {
-            input.value = params.get(name); // Set the value from the query string
+        // Iterate over the query string parameters
+        params.forEach((value, key) => {
+          let input = document.querySelector(`[name="${key}"]`);
+          if (input) {
+            if (input.type === "checkbox") {
+              input.checked = value === "on"; // Convert string to boolean for checkboxes
+            } else {
+              input.value = value; // Set text input value
+            }
           } else {
             input.value = ""; // Optional: clear if not in query string
           }
@@ -414,8 +442,6 @@ <h1 id="message"></h1>
           document.body.appendChild(a);
           a.click();
           document.body.removeChild(a);
-
-          console.log(55);
         };
 
         img.src = url;
@@ -505,6 +531,12 @@ <h1 id="message"></h1>
         );
 
         let vertices_to_delete = new Set();
+
+        // These mess up rendering now with the unknowns, get rid of them.
+        vertices_to_delete.add(5105)
+        vertices_to_delete.add(28393)
+        vertices_to_delete.add(374794)
+
         if (params.max_variables) {
           max_var = Number(params.max_variables);
           for (const [eqNumStr, eqStr] of Object.entries(
@@ -577,9 +609,9 @@ <h1 id="message"></h1>
         }
 
         dotFile = `
-graph G {
+digraph G {
   layout = dot
-  rankdir = TB
+  rankdir = BT
   graph [ pad="0.2", ranksep="0.75", nodesep="0.35" ];
   node [ shape="none" ]
 `;
@@ -661,7 +693,21 @@ <h1 id="message"></h1>
 
         for (const [v, neighbors] of Object.entries(reduced_graph)) {
           for (const n of neighbors) {
-            dotFile += `  ${n} -- ${v}\n`;
+            dotFile += `  ${v} -> ${n} [arrowhead="none"]\n`;
+          }
+        }
+
+        if (params.show_unknowns_conjectures == "on") {
+          for (const scc_name of Object.keys(scc_to_node_map)) {
+            if (!graph_json.unknowns[scc_name]) {
+              continue;
+            }
+
+            graph_json.unknowns[scc_name]
+              .filter((x) => x in scc_to_node_map)
+              .forEach((x) => {
+                dotFile += `  ${scc_name} -> ${x} [style="dotted"]\n`;
+              });
           }
         }
 

diff --git a/home_page/implications/script.js b/home_page/implications/script.js
@@ -271,8 +271,6 @@ function renderImplications(index) {
 	    selectedEquationDual.innerHTML = "";
     }
 
-  selectedEquationGraphitiLinks.innerHTML = `(Visualize <a target="_blank" href="${GRAPHITI_BASE_URL}?render=true&implies=${index+1}&highlight_red=${index+1}">implied</a> and <a target="_blank" href="${GRAPHITI_BASE_URL}?render=true&implied_by=${index+1}&highlight_red=${index+1}">implied by</a> equations) `
-
     // Add this section to display equivalent equations
     const equivalentClass = equiv.find(cls => cls.includes(index)) || [index];
     const equivalentEquations = equivalentClass
@@ -293,9 +291,11 @@ function renderImplications(index) {
     const implies = [];
     const antiImplies = [];
     const unknownImplies = [];
+    const unknownImpliesEqNum = [];
     const impliedBy = [];
     const antiImpliedBy = [];
     const unknownImpliedBy = [];
+    const unknownImpliedByEqNum = [];
 
     let seenClasses = new Set();
     implications.forEach((row, i) => {
@@ -326,10 +326,21 @@ function renderImplications(index) {
 		statusIndex === 0 ? antiImpliedBy.push(item) : antiImplies.push(item);
             } else if (isUnknown(status, treatConjecturedAsUnknown)) {
 		statusIndex === 0 ? unknownImpliedBy.push(item) : unknownImplies.push(item);
+		statusIndex === 0 ? unknownImpliedByEqNum.push(i) : unknownImpliesEqNum.push(i);
             }
 	});
     });
 
+  selectedEquationGraphitiLinks.innerHTML = `<br>(Visualize <a target="_blank" href="${GRAPHITI_BASE_URL}?render=true&implies=${index+1}&highlight_red=${index+1}">implied</a> and <a target="_blank" href="${GRAPHITI_BASE_URL}?render=true&implied_by=${index+1}&highlight_red=${index+1}">implied by</a> of the equation)`
+  if (unknownImpliesEqNum.length > 0) {
+    const implies = unknownImpliesEqNum.map(x => x + 1)
+    selectedEquationGraphitiLinks.innerHTML += `<br />(Visualize <a target="_blank" href="${GRAPHITI_BASE_URL}?render=true&implies=${index+1},${implies.join(",")}&highlight_red=${index+1}&highlight_blue=${implies.join(",")}&show_unknowns_conjectures=on">implied</a> and <a target="_blank" href="${GRAPHITI_BASE_URL}?render=true&implied_by=${index+1},${implies.join(",")}&highlight_red=${index+1}&highlight_blue=${implies.join(",")}&show_unknowns_conjectures=on">implied by</a> of the equation+unknowns+conjectures</a>)`
+  }
+  if (unknownImpliedByEqNum.length > 0) {
+    const impliedby = unknownImpliedByEqNum.map(x => x + 1)
+    selectedEquationGraphitiLinks.innerHTML += `<br />(Visualize <a target="_blank" href="${GRAPHITI_BASE_URL}?render=true&implies=${index+1},${impliedby.join(",")}&highlight_red=${index+1}&highlight_blue=${impliedby.join(",")}&show_unknowns_conjectures=on">implied</a> and <a target="_blank" href="${GRAPHITI_BASE_URL}?render=true&implied_by=${index+1},${impliedby.join(",")}&highlight_red=${index+1}&highlight_blue=${impliedby.join(",")}&show_unknowns_conjectures=on">implied by</a> of the equation+unknown bys+conjectured bys</a>)`
+  }
+
     impliesList.innerHTML = implies.join('') || 'None';
     antiImpliesList.innerHTML = antiImplies.join('') || 'None';
     unknownImpliesList.innerHTML = unknownImplies.join('') || 'None';

diff --git a/scripts/generate_graphiti_data.rb b/scripts/generate_graphiti_data.rb
@@ -1,12 +1,13 @@
 # lake exe extract_implications --json equational_theories > /tmp/implications.json
-# ruby scripts/generate_graphiti_data.rb /tmp/implications.json > home_page/graphiti/graph.json
+# lake exe extract_implications unknowns > /tmp/unknowns.json
+# ruby scripts/generate_graphiti_data.rb /tmp/implications.json /tmp/unknowns.json > home_page/graphiti/graph.json
 # python -m http.server 8000 --directory home_page/graphiti
 
 require 'json'
 require File.join(__dir__, 'graph')
 
-if ARGV.length != 1
-  $stderr.puts "Usage: scripts/generate_graphiti_data.rb <implications json>"
+if ARGV.length != 2
+  $stderr.puts "Usage: scripts/generate_graphiti_data.rb <implications json> <unknowns json>"
   exit 1
 end
 
@@ -36,11 +37,29 @@
 condensed = {}
 condensed_closure.adj_list.each { |k, v| condensed[k] = v.to_a }
 
+unknowns = {}
+JSON.parse(File.read(ARGV[1])).each { |unknown|
+  unknown_lhs_eq = unknown["lhs"][8, unknown["lhs"].length].to_i
+  unknown_rhs_eq = unknown["rhs"][8, unknown["rhs"].length].to_i
+
+  unknown_lhs_scc = node_to_scc_map[unknown_lhs_eq]
+  unknown_rhs_scc = node_to_scc_map[unknown_rhs_eq]
+
+  if !unknown_lhs_scc || !unknown_rhs_scc
+    $stderr.puts "Unknown LHS/RHS mapping to SCC"
+    exit 1
+  end
+
+  unknowns[unknown_lhs_scc] ||= []
+  unknowns[unknown_lhs_scc] << unknown_rhs_scc
+}
+
 puts JSON.generate({
   "timestamp" => Time.now.utc.to_i,
   "commit_hash" => `git rev-parse HEAD`.chomp,
   "condensed_graph" => condensed,
   "scc_to_node_map" => scc_to_node_map,
   "node_to_scc_map" => node_to_scc_map,
-  "equations" => equations
+  "equations" => equations,
+  "unknowns" => unknowns
 })