ProofWidgets for Lean 4

The PenroseCanvas component renders interactive Penrose diagrams. It supports embedding React nodes (like custom UI or math expressions) directly into the diagram at specific locations defined in the Penrose substance program.

Requirements for Embedding Nodes

To successfully embed a React node using the embedNodes prop:

1. Substance Program: The object must exist in your Penrose substance program.
2. Style Program: The object must be assigned a name.textBox : Rectangle field in your Penrose style program. The component uses this field to determine the dimensions and position for the embedded React node.
3. Positioning: The component automatically calculates the offset of the named element and positions the React node absolutely over the textBox area.

Props

• trio: A PenroseTrio object containing the dsl, sty, and sub strings.
• maxOptSteps: A number representing the maximum number of optimization steps allowed. This prevents the optimizer from running indefinitely if a diagram fails to converge.
• embedNodes: A Map<string, React.ReactNode> where the key is the name of the object in the Penrose program and the value is the React element to render at that location.

import { PenroseCanvas } from './path/to/penroseCanvas';

// Example usage
<PenroseCanvas
  trio={{
    dsl: 'domain code...',
    sty: 'style code with name.textBox : Rectangle...',
    sub: 'substance code...'
  }}
  maxOptSteps={100}
  embedNodes={new Map([
    ['myObjectName', <div className="custom-widget">Hello World</div>]
  ])}
/>

The ForceGraphDisplay component is a React component used to visualize a graph using a force-directed simulation (powered by D3). It supports interactive elements like dragging vertices, zooming, panning, and clicking elements to show details.

To use it, provide a Graph object containing vertices and edges, along with configuration for the simulation forces.

import ForceGraphDisplay from './forceGraphDisplay';

// Define your graph data
const vertices = [
  { id: 'v1', label: { text: 'Node 1' }, boundingShape: { circle: { radius: 10 } } },
  { id: 'v2', label: { text: 'Node 2' }, boundingShape: { circle: { radius: 10 } } }
];

const edges = [
  { source: 'v1', target: 'v2', attrs: [['stroke', 'black']] }
];

// Define simulation forces
const forces = [
  { center: { x: 0, y: 0, strength: 0.1 } },
  { manyBody: { strength: -30 } },
  { link: { distance: 50 } }
];

// Render the component
<ForceGraphDisplay 
  vertices={vertices} 
  edges={edges} 
  defaultEdgeAttrs={[['stroke', 'gray']]} 
  forces={forces} 
  showDetails={true} 
/>

The GraphvizDisplay component is a React component used to render Graphviz diagrams using d3-graphviz. It accepts DOT syntax strings and provides options for layout, sizing, and interactivity.

Important Performance Note: To prevent unnecessary re-renders and layout thrashing, you must memoize the options, attributer, and event handler props (onClickNode, onPointerEnterNode, onPointerLeaveNode). If these references change on every render, the component will re-render the entire graph.

Props Reference

import GraphvizDisplay from './GraphvizDisplay';

// Example usage with memoized props
const options = React.useMemo(() => ({ width: 800, height: 600 }), []);
const onClick = React.useCallback((ev, d) => console.log('Clicked:', d), []);

function MyGraph() {
  return (
    <GraphvizDisplay
      dot="digraph { A -> B }"
      options={options}
      renderDebounceMs={100}
      onClickNode={onClick}
    />
  );
}

The forces prop accepts an array of objects, where each object defines a specific D3 force type. Supported force types include:

• center: { x?: number, y?: number, strength?: number } - Positions the center of the simulation.
• collide: { radius?: number, strength?: number, iterations?: number } - Prevents nodes from overlapping.
• link: { distance?: number, strength?: number, iterations?: number } - Constrains edges to a specific distance.
• manyBody: { strength?: number, theta?: number, distanceMin?: number, distanceMax?: number } - Simulates electrostatic forces (repulsion/attraction).
• x: { x: number, strength?: number } - Forces nodes toward a specific X coordinate.
• y: { y: number, strength?: number } - Forces nodes toward a specific Y coordinate.
• radial: { radius: number, x?: number, y?: number, strength?: number } - Forces nodes into a radial pattern.

// Example of multiple forces
const forces = [
  { center: { x: 0, y: 0 } },
  { manyBody: { strength: -100 } },
  { collide: { radius: 20 } },
  { link: { distance: 100 } }
];