-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
22211ae
commit c6b3841
Showing
10 changed files
with
817 additions
and
86 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -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> | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,229 @@ | ||
| <script lang="ts"> | ||
| import { onMount } from 'svelte' | ||
| import * as d3 from 'd3' | ||
| import type { Property, Trait, Theorem } from '@/models' | ||
| import { formula } from '@pi-base/core' | ||
| import * as katex from 'katex' | ||
| import type { Writable } from 'svelte/store' | ||
| export let selected: Writable<Property | Theorem> | ||
| export let property: Property | ||
| export let traits: [Property, Trait][] | ||
| export let theorems: Theorem[] | ||
| function renderLatex(s: string) { | ||
| return s.replaceAll(/\$[^$]+\$/g, p => { | ||
| return (katex as any).default.renderToString(p.replaceAll('$', '')) | ||
| }) | ||
| } | ||
| type DragEvent = d3.D3DragEvent<HTMLElement, unknown, Node> | ||
| type Node = d3.SimulationNodeDatum & { | ||
| property: Property | ||
| trait?: Trait | ||
| degree: number | ||
| pinned?: { x?: number; y?: number } | ||
| } | ||
| type Link = d3.SimulationLinkDatum<Node> & { theorem: Theorem } | ||
| let nodes: Node[] | ||
| let links: Link[] | ||
| let el: SVGSVGElement | ||
| const width = 600 | ||
| const height = 600 | ||
| const bound = 200 | ||
| const textWidth = 500 | ||
| $: { | ||
| // Build graph | ||
| // - one node per property | ||
| // - theorems correspond to edges linking "when" and "then" () | ||
| const inodes: Record<string, Node> = {} | ||
| links = [] | ||
| for (const theorem of theorems) { | ||
| for (const a of formula.properties(theorem.when)) { | ||
| inodes[a.id] ||= { property: a, degree: 0 } | ||
| inodes[a.id].degree++ | ||
| for (const c of formula.properties(theorem.then)) { | ||
| inodes[c.id] ||= { property: c, degree: 0 } | ||
| inodes[c.id].degree++ | ||
| links.push({ | ||
| source: a.id.toString(), | ||
| target: c.id.toString(), | ||
| theorem, | ||
| }) | ||
| } | ||
| } | ||
| } | ||
| for (const [property, trait] of traits) { | ||
| inodes[property.id] ||= { property, degree: 0 } | ||
| inodes[property.id].trait = trait | ||
| inodes[property.id].fx = -1 * bound | ||
| inodes[property.id].pinned = { x: -1 * bound } | ||
| } | ||
| inodes[property.id].fx = bound | ||
| inodes[property.id].fy = 1 | ||
| inodes[property.id].pinned = { x: bound, y: 1 } | ||
| nodes = Object.values(inodes) | ||
| } | ||
| onMount(() => { | ||
| const color = d3.scaleOrdinal(d3.schemeTableau10) | ||
| const simulation = d3 | ||
| .forceSimulation(nodes) | ||
| .force( | ||
| 'link', | ||
| d3.forceLink<Node, Link>(links).id(d => d.property.id.toString()), | ||
| ) | ||
| .force( | ||
| 'charge', | ||
| d3.forceManyBody<Node>().strength(d => -100 * (d.pinned ? 10 : 1)), | ||
| ) | ||
| .force( | ||
| 'x', | ||
| d3.forceX().strength(d => { | ||
| const x = d.x || 0 | ||
| return Math.min((x / bound) * (x / bound), 1) | ||
| }), | ||
| ) | ||
| 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%;') | ||
| const text = svg | ||
| .append('g') | ||
| .attr('class', 'labels') | ||
| .selectAll('foreignObject') | ||
| .data(nodes) | ||
| .enter() | ||
| .append('foreignObject') | ||
| .attr( | ||
| 'requiredFeatures', | ||
| 'http://www.w3.org/TR/SVG11/feature#Extensibility', | ||
| ) | ||
| .attr('width', `${textWidth}px`) | ||
| .attr('height', '2em') | ||
| const link = svg | ||
| .append('g') | ||
| .attr('stroke', '#777') | ||
| .attr('stroke-opacity', 0.6) | ||
| .selectAll('path') | ||
| .data(links) | ||
| .join('path') | ||
| .attr('stroke-width', 2) | ||
| .attr('marker-mid', 'url(#arrowhead)') | ||
| .on('mouseover', function () { | ||
| const datum = d3.select(this).datum() as { theorem: Theorem } | ||
| if (datum.theorem) { | ||
| $selected = datum.theorem | ||
| } | ||
| }) | ||
| text | ||
| .append('xhtml:div') | ||
| .html(d => (d.degree > 2 || d.pinned ? renderLatex(d.property.name) : '')) | ||
| .style('width', '100%') | ||
| .style('text-align', 'center') | ||
| const node = svg | ||
| .append('g') | ||
| .selectAll('circle') | ||
| .data(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'))) | ||
| .on('mouseover', function () { | ||
| const datum = d3.select(this).datum() as { property: Property } | ||
| if (datum.property) { | ||
| $selected = datum.property | ||
| } | ||
| }) | ||
| node.append('title').text(d => d.property.name) | ||
| node.call( | ||
| d3 | ||
| .drag<any, Node, unknown>() | ||
| .on('start', dragstarted) | ||
| .on('drag', dragged) | ||
| .on('end', dragended), | ||
| ) | ||
| simulation.on('tick', () => { | ||
| link.attr('d', ({ source, target }: Link) => { | ||
| const { x: x1 = 0, y: y1 = 0 } = source as Node | ||
| const { x: x2 = 0, y: y2 = 0 } = target as Node | ||
| const mx = (x2 - x1) / 2 + x1 | ||
| const my = (y2 - y1) / 2 + y1 | ||
| return `M${x1},${y1}L${mx},${my}L${x2},${y2}` | ||
| }) | ||
| node.attr('cx', (d: Node) => d.x!).attr('cy', (d: Node) => d.y!) | ||
| text | ||
| .attr('x', (d: Node) => d.x! - textWidth / 2) | ||
| .attr('y', (d: Node) => d.y! + 8) | ||
| }) | ||
| 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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.