Add variable node

localgraphs/forallprover.html

@@ -17,7 +17,11 @@
         <button id="tool_move">Move</button>
         <button id="tool_arrow">Orient</button>
         <button id="tool_label">Label</button>
-        <button id="tool_boxwindow">Box</button>
+        <button id="tool_box">Box</button>
+        <button id="tool_forallbox">For All</button>
+        <button id="tool_outputbox">Output</button>
+        <button id="tool_eitherbox">Either</button>
+        <button id="tool_varnode">Variable</button>
         <button id="reset">Reset</button>
         <button id="undo">Undo</button>
         <button id="redo">Redo</button>

localgraphs/src/graph.ts

@@ -52,13 +52,32 @@ export function createEdge<T>(graph: Graph<T>, a: GraphNode<T>, b: GraphNode<T>,
     return edge
 }
 
-export function clearEdges<T>(graph: Graph<T>) {
+export function clearAllEdges<T>(graph: Graph<T>) {
     for (let node of graph.nodes) {
         node.neighbors.clear()
     }
     graph.edges = []
 }
 
+export function clearNeighbors<T>(graph: Graph<T>, node: GraphNode<T>) {
+    for (let neighbor of node.neighbors) {
+        neighbor.neighbors.delete(node)
+    }
+    node.neighbors.clear()
+    graph.edges = graph.edges.filter(e => e.a !== node && e.b !== node)
+}
+
+export function deleteEdge<T>(graph: Graph<T>, a: GraphNode<T>, b: GraphNode<T>) {
+    graph.edges = graph.edges.filter(e => !(e.a === a && e.b === b) && !(e.a === b && e.b === a))
+    a.neighbors.delete(b)
+    b.neighbors.delete(a)
+}
+
+export function deleteNode<T>(graph: Graph<T>, node: GraphNode<T>) {
+    clearNeighbors(graph, node)
+    graph.nodes = graph.nodes.filter(n => n !== node)
+}
+
 // copies the given nodes with data transformed by mapping and the edges between them to targetGraph
 // returns a map from old nodes to new nodes
 export function mapSubgraphTo<S,T>(nodes: Iterable<GraphNode<S>>, targetGraph: Graph<T>, mapping: (value: S) => T): Map<GraphNode<S>, GraphNode<T>> {

localgraphs/src/interaction/graphsim.ts

@@ -42,6 +42,8 @@ export function moveSlightly(node: GraphNode<unknown>, strength: number = 3) {
     // prevents nodes on same position and wakes them from sleep
     node.vx += (Math.random()*2.-1.) * strength
     node.vy += (Math.random()*2.-1.) * strength
+    node.x += node.vx * 0.2
+    node.y += node.vy * 0.2
 }
 
 export function dragNodes(nodes: Iterable<GraphNode<unknown>>, dx: number, dy: number, deltaTime: number) {

localgraphs/src/interaction/physics.ts

@@ -119,18 +119,25 @@ function applyLayoutForces<T>(
     }
 }
 
-export class GraphLayoutPhysics implements LayoutPhysics<unknown> {
-    constructor(private layoutStyle: LayoutConfig) {}
+export class GraphLayoutPhysics<T> implements LayoutPhysics<T> {
+    constructor(
+        private layoutStyle: LayoutConfig,
+        private customForces: ((dt: number, graph: Graph<T>, w: number, h: number) => unknown)[] = []
+    ) {}
     step(
-        graph: Graph<unknown>,
+        graph: Graph<T>,
         width: number,
         height: number,
         dt: number,
     ) {
         let activeNodes = findActiveNodes(graph, this.layoutStyle.sleepVelocity)
+
+        for (let custom of this.customForces) {
+            custom(dt, graph, width, height);
+        }
+
         applyVelocityStep(graph.nodes, this.layoutStyle.dampening, dt)
         applyLayoutForces(graph, this.layoutStyle, activeNodes, width, height, dt)
-
         // count at the end again, in case nodes started moving this step
         let activeNodesCount = activeNodes.size;
         activeNodesCount += findActiveNodes(graph, this.layoutStyle.sleepVelocity).size;

localgraphs/src/interaction/tools.ts

@@ -15,10 +15,14 @@ export class BuildGraphInteraction<T> implements GraphInteraction<T> {
     constructor(private buildNode: (graph: Graph<T>, x: number, y: number) => GraphNode<T>, private buildEdge: (graph: Graph<T>, a: GraphNode<T>, b: GraphNode<T>) => unknown) {
     }
 
+    findNode(x: number, y: number, visible: Iterable<GraphNode<T>>): GraphNode<T> | null {
+        return findClosestNode(x, y, visible)
+    }
+
     onMouseDown(graph: Graph<T>, visible: GraphNode<T>[], mouseX: number, mouseY: number): void {
         this.startX = mouseX
         this.startY = mouseY
-        this.startNode = findClosestNode(mouseX, mouseY, visible)
+        this.startNode = this.findNode(mouseX, mouseY, visible)
         this.hasMoved = false
     }
     checkHasMoved(mouseX: number, mouseY: number): boolean {
@@ -43,7 +47,7 @@ export class BuildGraphInteraction<T> implements GraphInteraction<T> {
             drawCtx.strokeStyle = "black"
             drawCtx.lineWidth = 1
             drawCtx.beginPath()
-            let endNode = findClosestNode(mouseX, mouseY, visible)
+            let endNode = this.findNode(mouseX, mouseY, visible)
             if (endNode !== null && !this.shouldCreateEndpoint(mouseX, mouseY, endNode)) {
                 drawCtx.moveTo(endNode.x, endNode.y)
                 drawCtx.quadraticCurveTo(mouseX, mouseY, this.startNode.x, this.startNode.y)
@@ -61,7 +65,7 @@ export class BuildGraphInteraction<T> implements GraphInteraction<T> {
     }
     onMouseUp(graph: Graph<T>, visible: Iterable<GraphNode<T>>, endX: number, endY: number): void {
         if (this.startNode !== null && this.hasMoved) {
-            let endNode = findClosestNode(endX, endY, visible)
+            let endNode = this.findNode(endX, endY, visible)
             if (endNode === null || this.shouldCreateEndpoint(endX, endY, endNode)) {
                 endNode = this.buildNode(graph, endX, endY)
             }

localgraphs/src/interaction/windows.ts

@@ -3,9 +3,11 @@ import { ensured } from "../../../shared/utils";
 import { AnimationFrame, InteractiveSystem, MouseDownResponse, PointerId, SleepState } from "./controller";
 
 function drawWindowFrame(ctx: CanvasRenderingContext2D, window: WindowBounds, titleArea: Rect) {
+    ctx.save()
     const cornerRadius = 4
-    ctx.strokeStyle = "darkblue";
-    ctx.fillStyle = `rgba(200, 220, 255, 0.6)`;
+    ctx.strokeStyle = window.borderColor;
+    //ctx.fillStyle = `rgba(200, 220, 255, 0.6)`;
+    ctx.fillStyle = `color-mix(in srgb, ${window.borderColor} 10%, rgba(255, 255, 255, 0.8))`;
     ctx.lineWidth = 1;
     ctx.beginPath()
     ctx.roundRect(window.bounds.left, titleArea.top, Rect.width(window.bounds), Rect.height(titleArea), [cornerRadius, cornerRadius, 0, 0]);
@@ -27,15 +29,18 @@ function drawWindowFrame(ctx: CanvasRenderingContext2D, window: WindowBounds, ti
         }
         ctx.stroke();
     }
+    ctx.restore()
 }
 
-export function drawWindowTitle(ctx: CanvasRenderingContext2D, titleBounds: Rect, title: string): number {
-    ctx.fillStyle = "darkblue";
+export function drawWindowTitle(ctx: CanvasRenderingContext2D, titleBounds: Rect, title: string, color: string): number {
+    ctx.save()
+    ctx.fillStyle = color;
     ctx.font = "15px monospace";
     ctx.textBaseline = "middle";
     ctx.textAlign = "left";
     const left = titleBounds.left + 12
     ctx.fillText(title, left, titleBounds.top + Rect.height(titleBounds) / 2);
+    ctx.restore()
     const measured = ctx.measureText(title);
     return left + measured.width
 }
@@ -49,6 +54,7 @@ export type WindowBounds = {
         minWidth: number,
         minHeight: number,
     } | false
+    borderColor: string
 }
 
 export function satisfyMinBounds(window: WindowBounds) {