Draw derived proofs

packages/viewer/package.json

@@ -20,12 +20,14 @@
     "@pi-base/core": "workspace:*",
     "@sentry/browser": "^7.75.1",
     "bootstrap": "^4.6.2",
+    "d3": "^7.8.5",
     "debug": "^4.3.4",
     "fromnow": "^3.0.1",
     "fuse.js": "^6.6.2",
     "hast-to-hyperscript": "^10.0.3",
     "hyperscript": "^2.0.2",
     "jquery": "1.12.4",
+    "katex": "^0.16.9",
     "rehype-katex": "^6.0.3",
     "remark-rehype": "^10.1.0",
     "unified": "^10.1.2",
@@ -37,6 +39,7 @@
     "@sveltejs/kit": "^1.27.1",
     "@sveltejs/vite-plugin-svelte": "^2.4.6",
     "@tsconfig/svelte": "^3.0.0",
+    "@types/d3": "^7.4.3",
     "@types/debug": "^4.1.10",
     "@types/hyperscript": "0.0.6",
     "@types/katex": "^0.16.5",

packages/viewer/public/global.css

@@ -46,3 +46,14 @@
 .description {
   margin-bottom: 1rem;
 }
+
+.links line {
+  stroke: #999;
+  stroke-opacity: 0.6;
+}
+
+.nodes circle {
+  stroke: #fff;
+  stroke-width: 1.5px;
+}
+

packages/viewer/src/app.html

@@ -4,25 +4,25 @@
     <meta charset="utf-8" />
     <meta name="viewport" content="width=device-width" />
 
-	  <title>π-Base</title>
+	<title>π-Base</title>
 
-	  <meta name="author" content="James Dabbs" />
-	  <meta name="description"
-	  	content="A community database of topological theorems and spaces, with powerful search and automated proof deduction." />
-	  <meta property="og:type" content="website" />
-	  <meta property="og:site_name" content="π-Base" />
-	  <meta property="og:url" name="twitter:url" content="https://topology.pi-base.org" />
-	  <meta property="og:title" name="twitter:title" content="π-Base" />
-	  <meta property="og:description" name="twitter:description"
-	  	content="A community database of topological theorems and spaces, with powerful search and automated proof deduction." />
-	  <meta property="og:image" content="%sveltekit.assets%/pi-base.png" />
-	  <meta name="twitter:site" content="π-Base" />
-	  <meta name="twitter:creator" content="@jamesdabbs" />
+	<meta name="author" content="James Dabbs" />
+	<meta name="description"
+		content="A community database of topological theorems and spaces, with powerful search and automated proof deduction." />
+	<meta property="og:type" content="website" />
+	<meta property="og:site_name" content="π-Base" />
+	<meta property="og:url" name="twitter:url" content="https://topology.pi-base.org" />
+	<meta property="og:title" name="twitter:title" content="π-Base" />
+	<meta property="og:description" name="twitter:description"
+		content="A community database of topological theorems and spaces, with powerful search and automated proof deduction." />
+	<meta property="og:image" content="%sveltekit.assets%/pi-base.png" />
+	<meta name="twitter:site" content="π-Base" />
+	<meta name="twitter:creator" content="@jamesdabbs" />
 
     <link rel="icon" href="%sveltekit.assets%/favicon.ico" />
 
-	  <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-Xi8rHCmBmhbuyyhbI88391ZKP2dmfnOl4rT9ZfRI7mLTdk1wblIUnrIq35nqwEvC" crossorigin="anonymous">
-	  <link rel='stylesheet' href='/global.css'>
+	<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-Xi8rHCmBmhbuyyhbI88391ZKP2dmfnOl4rT9ZfRI7mLTdk1wblIUnrIq35nqwEvC" crossorigin="anonymous">
+	<link rel='stylesheet' href='/global.css'>
 
     %sveltekit.head%
   </head>

packages/viewer/src/components/Theorems/Table.svelte

@@ -1,11 +1,14 @@
 <script lang="ts">
-  import type { Theorem } from '@/models'
+  import type { Property, Theorem } from '@/models'
   import { Formula, Link } from '../Shared'
+  import type { Readable } from 'svelte/store'
 
   export let theorems: Theorem[] = []
+  export let small = false
+  export let selected: Readable<Theorem | Property> | undefined = undefined
 </script>
 
-<table class="table">
+<table class="table" class:table-sm={small}>
   <thead>
     <tr>
       <th>Id</th>
@@ -15,7 +18,7 @@
   </thead>
   <tbody>
     {#each theorems as theorem (theorem.id)}
-      <tr>
+      <tr class:table-warning={$selected === theorem}>
         <td>
           <Link.Theorem {theorem} />
         </td>

packages/viewer/src/components/Traits/Graph.svelte

@@ -0,0 +1,202 @@
+<script lang="ts">
+  import { onMount } from 'svelte'
+  import * as d3 from 'd3'
+  import type { Property, Theorem } from '@/models'
+  import type { Writable } from 'svelte/store'
+
+  import {
+    type Node,
+    type Link,
+    type Graph,
+    drawLinkWithMidpoint,
+    renderLatex,
+    pin,
+  } from './graph'
+
+  export let selected: Writable<Property | Theorem>
+  export let graph: Graph
+
+  let el: SVGSVGElement
+
+  const width = 600
+  const height = 600
+
+  // Assumptions will be snapped to x = -bound, while the derived trait
+  // will be located at x = +bound
+  const bound = 200
+
+  // Maximum width of node label text
+  const textWidth = 500
+
+  $: pin(graph, bound)
+
+  onMount(() => {
+    const color = d3.scaleOrdinal(d3.schemeTableau10)
+
+    const simulation = d3
+      .forceSimulation(graph.nodes)
+      // Space out properties
+      .force(
+        'charge',
+        d3.forceManyBody<Node>().strength(d => -100 * (d.pinned ? 10 : 3)),
+      )
+      // Keep linked properties close together
+      .force(
+        'link',
+        d3.forceLink<Node, Link>(graph.links).id(d => d.property.id.toString()),
+      )
+
+    // Setup the SVG palette and primary shape types
+    const svg = d3
+      .select(el)
+      .attr('width', width)
+      .attr('height', height)
+      .attr('viewBox', [-width / 2, -height / 2, width, height])
+      .attr('style', 'max-width: 100%; width: 100%; height: 100%;')
+
+    // Labeling property nodes is tricky, for a few reasons:
+    //
+    // While we'd _like_ labels to be middle-anchored text nodes, if we want
+    // them to contain katex-rendered math, we need to attach foreignObjects to
+    // hold HTML nodes.
+    //
+    // Because we can't middle-anchor those nodes, we kludge around it by
+    // providing the foreignObjects with a generous bounding box and
+    // text-aligning inside them.
+    //
+    // We _don't_ want these bounding boxes to intercept clicks or mouseovers on
+    // the graph, so we have to keep them first in SVG document order.
+    const text = svg
+      .append('g')
+      .attr('class', 'labels')
+      .selectAll('foreignObject')
+      .data(graph.nodes)
+      .enter()
+      .append('foreignObject')
+      .attr(
+        'requiredFeatures',
+        'http://www.w3.org/TR/SVG11/feature#Extensibility',
+      )
+      .attr('width', `${textWidth}px`)
+      .attr('height', '2em')
+
+    text
+      .append('xhtml:div')
+      .html(d => (d.degree > 2 || d.pinned ? renderLatex(d.property.name) : ''))
+      .style('width', '100%')
+      .style('text-align', 'center')
+
+    // Draw edges connecting properties which are related by a theorem
+    const link = svg
+      .append('g')
+      .attr('stroke', '#777')
+      .attr('stroke-opacity', 0.6)
+      .selectAll('path')
+      .data(graph.links)
+      .join('path')
+      .attr('stroke-width', 2)
+      .attr('marker-mid', 'url(#arrowhead)')
+
+    link.append('title').text(d => d.theorem.name)
+
+    // Draw nodes for each property
+    const node = svg
+      .append('g')
+      .selectAll('circle')
+      .data(graph.nodes)
+      .enter()
+      .append('circle')
+      .attr('stroke', '#888')
+      .attr('stroke-width', d => (d.pinned ? 3 : 1.5))
+      .attr('r', d => {
+        if (d.pinned) {
+          return 10
+        } else if (d.degree > 2) {
+          return 8
+        } else {
+          return 5
+        }
+      })
+      .attr('fill', d => (d.pinned || d.degree > 2 ? color('1') : color('2')))
+
+    node.append('title').text(d => d.property.name)
+
+    // Run the simulation and update elements
+    simulation.on('tick', () => {
+      link.attr('d', drawLinkWithMidpoint)
+
+      node.attr('cx', ({ x }) => x ?? null).attr('cy', ({ y }) => y ?? null)
+
+      // Position labels just under their corresponding nodes, and shifted so
+      // that centered internal text will appear middle-anchored
+      text
+        .attr('x', ({ x }) => (x ? x - textWidth / 2 : null))
+        .attr('y', ({ y }) => (y ? y + 8 : null))
+    })
+
+    // Allow hover-over
+    node.on('mouseover', function () {
+      const datum = d3.select(this).datum() as { property: Property }
+      if (datum.property) {
+        $selected = datum.property
+      }
+    })
+
+    link.on('mouseover', function () {
+      const datum = d3.select(this).datum() as Link
+      if (datum.theorem) {
+        $selected = datum.theorem
+      }
+    })
+
+    // Allow dragging non-pinned nodes
+
+    type DragEvent = d3.D3DragEvent<HTMLElement, unknown, Node>
+
+    node.call(
+      d3
+        .drag<any, Node, unknown>()
+        .on('start', dragstarted)
+        .on('drag', dragged)
+        .on('end', dragended),
+    )
+
+    function dragstarted({ active, subject }: DragEvent) {
+      if (!active) {
+        simulation.alphaTarget(0.3).restart()
+      }
+
+      subject.fx = subject.pinned?.x || subject.x
+      subject.fy = subject.pinned?.y || subject.y
+    }
+
+    function dragged({ subject, x, y }: DragEvent) {
+      subject.fx = subject.pinned?.x || x
+      subject.fy = subject.pinned?.y || y
+    }
+
+    function dragended({ active, subject }: DragEvent) {
+      if (!active) {
+        simulation.alphaTarget(0)
+      }
+
+      subject.fx = subject.pinned?.x
+      subject.fy = subject.pinned?.y
+    }
+  })
+</script>
+
+<svg xmlns="http://www.w3.org/2000/svg" bind:this={el}>
+  <defs>
+    <marker
+      id="arrowhead"
+      markerWidth="3"
+      markerHeight="3"
+      refX="0"
+      refY="1.5"
+      orient="auto"
+    >
+      <polygon points="0,0 3,1.5 0,3" fill="#888" />
+    </marker>
+  </defs>
+</svg>

packages/viewer/src/components/Traits/Proof.svelte

@@ -1,19 +1,32 @@
 <script lang="ts">
-  import { Link } from '../Shared'
+  import { writable } from 'svelte/store'
+  import { Icons, Link } from '../Shared'
   import { Table as Theorems } from '../Theorems'
+  import Graph from './Graph.svelte'
   import Value from './Value.svelte'
   import type { Property, Space, Theorem, Trait } from '@/models'
+  import { toGraph } from './graph'
 
   export let space: Space
+  export let property: Property
   export let theorems: Theorem[]
   export let traits: [Property, Trait][]
+
+  const selected = writable<Property | Theorem>()
+
+  $: graph = toGraph(property, traits, theorems)
 </script>
 
+<Icons.Robot />
+
 Automatically deduced from the following:
+
 <div class="row">
-  <div class="col">
-    <h5>Properties</h5>
-    <table class="table">
+  <div class="col-6">
+    <Graph {graph} {selected} />
+  </div>
+  <div class="col-6">
+    <table class="table table-sm">
       <thead>
         <tr>
           <th>Property</th>
@@ -22,7 +35,7 @@ Automatically deduced from the following:
       </thead>
       <tbody>
         {#each traits as [property, trait] (property.id)}
-          <tr>
+          <tr class:table-warning={$selected === property}>
             <td>
               <Link.Property {property} />
             </td>
@@ -35,9 +48,7 @@ Automatically deduced from the following:
         {/each}
       </tbody>
     </table>
-  </div>
-  <div class="col">
-    <h5>Theorems</h5>
-    <Theorems {theorems} />
+
+    <Theorems {theorems} small={true} {selected} />
   </div>
 </div>