Skip to content

Commit

Permalink
Merge pull request #10 from anoma/fozkvm
Browse files Browse the repository at this point in the history 
String Diagrams and ZKVMs post
  • Loading branch information
@AHartNtkn
AHartNtkn authored Jul 16, 2024
2 parents 4e9061e + 85f84b5 commit 744050a
Show file tree
Hide file tree
Showing 10 changed files with 1,001 additions and 1 deletion.
2 changes: 1 addition & 1 deletion anthony/arithmetizing-computable-programs.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,7 @@ If we only care about normal forms, we can implement the tree calculus over them
app Leaf z = Branch z
app (Branch y) z = Fan y z
app (Fan Leaf y) z = y
app (Fan (Branch x) y) z = app (app y z) (app x y)
app (Fan (Branch x) y) z = app (app y z) (app x z)
app (Fan (Fan w x) y) z = app (app z w) x
```

Expand Down
337 changes: 337 additions & 0 deletions anthony/embeds/tree-binder-graph.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,337 @@
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>Interactive Tree Visualizer with Binders - Fixed V7</title>
<script src="https://cdnjs.cloudflare.com/ajax/libs/react/17.0.2/umd/react.development.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/react-dom/17.0.2/umd/react-dom.development.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/babel-standalone/6.26.0/babel.min.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/d3/5.16.0/d3.min.js"></script>
<script src="https://unpkg.com/react-force-graph-2d"></script>
<style>
body, html {
margin: 0;
padding: 0;
height: 100%;
overflow: hidden;
}
.button {
margin: 5px;
padding: 5px 10px;
background-color: #f0f0f0;
border: 1px solid #AB0000;
border-radius: 4px;
cursor: pointer;
color: #AB0000;
}
.button:hover {
background-color: #e0e0e0;
}
.examples-text {
color: #AB0000;
}
</style>
</head>
<body>
<div id="root"></div>

<script type="text/babel">
const TreeVisualizer = () => {
const [inputText, setInputText] = React.useState('apply(lam(x. f(x)), a)');
const [graphData, setGraphData] = React.useState({ nodes: [], links: [] });

const examples = [
{ name: 'Simple', tree: 'lam(x. f(x))' },
{ name: 'Duplication', tree: 'lam(x. f(x, x))' },
{ name: 'Multibinding', tree: 'lam(x y. f(x, y))' },
{ name: 'Non-Scoping', tree: 'foo(a, bar(a. x))' },
{ name: 'Complex', tree: 'apply(lam(x y. add(x,y)), a, b)' }
];

const parseTree = (input) => {
const tokenize = (str) => {
const tokens = [];
let current = '';
for (let char of str) {
if ('(.),'.includes(char)) {
if (current) tokens.push(current);
tokens.push(char);
current = '';
} else if (char === ' ') {
if (current) tokens.push(current);
current = '';
} else {
current += char;
}
}
if (current) tokens.push(current);
return tokens;
};

const parse = (tokens) => {
const nodes = [];
const stack = [{ id: -1, name: 'root', args: [], binders: [] }];
let id = 0;

for (let token of tokens) {
if (token === '(') {
const newNode = { id: id++, name: stack[stack.length - 1].args.pop(), args: [], binders: [] };
stack.push(newNode);
} else if (token === ')') {
if (stack.length > 1) {
const node = stack.pop();
nodes.push(node);
stack[stack.length - 1].args.push(node);
}
} else if (token === '.') {
stack[stack.length - 1].binders = stack[stack.length - 1].args;
stack[stack.length - 1].args = [];
} else if (token === ',') {
// Do nothing, just separates arguments
} else {
stack[stack.length - 1].args.push(token);
}
}

while (stack.length > 1) {
const node = stack.pop();
nodes.push(node);
stack[stack.length - 1].args.push(node);
}

return nodes;
};

const processNodes = (nodes) => {
const binderNames = new Set(nodes.flatMap(node => node.binders));
let processedNodes = nodes.filter(node => !binderNames.has(node.name)).map(node => ({
id: node.id,
name: node.name,
args: node.args,
binders: node.binders.map(binder => ({ name: binder, locs: [] })),
loc: null
}));

let id = processedNodes.length;

// First pass: add all nodes and set locations
processedNodes.forEach((node) => {
node.args.forEach((arg, argIndex) => {
if (typeof arg === 'string' && !binderNames.has(arg)) {
const newNode = {
id: id++,
name: arg,
args: [],
binders: [],
loc: [node.id, argIndex + 1 + node.binders.length]
};
processedNodes.push(newNode);
} else if (typeof arg === 'object') {
const childNode = processedNodes.find(n => n.id === arg.id);
if (childNode) {
childNode.loc = [node.id, argIndex + 1 + node.binders.length];
}
}
});
});

// Second pass: process binders
processedNodes.forEach(node => {
node.args.forEach((arg, argIndex) => {
if (typeof arg === 'string' && binderNames.has(arg)) {
const binderNode = processedNodes.find(n => n.binders.some(b => b.name === arg));
if (binderNode) {
const binder = binderNode.binders.find(b => b.name === arg);
binder.locs.push([node.id, argIndex + 1 + node.binders.length]);
}
}
});
});

return processedNodes;
};

const createGraph = (processedNodes) => {
const nodes = [];
const links = [];
const dupNodeCounter = {};

processedNodes.forEach(node => {
nodes.push({
id: node.id,
name: node.name,
childCount: node.args.length + node.binders.length
});

if (node.loc) {
links.push({
source: node.id,
target: node.loc[0],
sourcePort: 0,
targetPort: node.loc[1]
});
}

node.binders.forEach((binder, index) => {
if (binder.locs.length > 1) {
const dupNodeId = `dup_${binder.name}_${dupNodeCounter[binder.name] || 0}`;
dupNodeCounter[binder.name] = (dupNodeCounter[binder.name] || 0) + 1;
nodes.push({ id: dupNodeId, name: '', isDup: true });

links.push({
source: node.id,
target: dupNodeId,
sourcePort: index + 1,
targetPort: 0
});

binder.locs.forEach(loc => {
links.push({
source: dupNodeId,
target: loc[0],
sourcePort: 0,
targetPort: loc[1]
});
});
} else if (binder.locs.length === 1) {
links.push({
source: node.id,
target: binder.locs[0][0],
sourcePort: index + 1,
targetPort: binder.locs[0][1]
});
}
});
});

return { nodes, links };
};


const tokens = tokenize(input);
const parsedNodes = parse(tokens);
const processedNodes = processNodes(parsedNodes);
return createGraph(processedNodes);
};

React.useEffect(() => {
const newGraphData = parseTree(inputText);
setGraphData(newGraphData);
}, [inputText]);

const nodeRadius = 20;

const drawNode = (node, ctx, globalScale) => {
const label = node.name;
const fontSize = 12/globalScale;
const scaledNodeRadius = nodeRadius/globalScale;

if (node.isDup) {
// Draw duplication node
ctx.beginPath();
ctx.arc(node.x, node.y, scaledNodeRadius / 2, 0, 2 * Math.PI, false);
ctx.fillStyle = '#AB0000';
ctx.fill();
} else {
// Draw main circle
ctx.beginPath();
ctx.arc(node.x, node.y, scaledNodeRadius, 0, 2 * Math.PI, false);
ctx.fillStyle = 'white';
ctx.fill();
ctx.strokeStyle = '#AB0000';
ctx.stroke();

// Draw text
ctx.font = `${fontSize}px Sans-Serif`;
ctx.textAlign = 'center';
ctx.textBaseline = 'middle';
ctx.fillStyle = 'black';
ctx.fillText(label, node.x, node.y);

// Draw ports
const portRadius = 3/globalScale;
for (let i = 0; i <= node.childCount; i++) {
const angle = (i * 2 * Math.PI) / (node.childCount + 1) - Math.PI/2;
const portX = node.x + scaledNodeRadius * Math.cos(angle);
const portY = node.y + scaledNodeRadius * Math.sin(angle);

ctx.beginPath();
ctx.arc(portX, portY, portRadius, 0, 2 * Math.PI, false);
ctx.fillStyle = i === 0 ? '#AB0000' : 'white';
ctx.fill();
ctx.strokeStyle = '#AB0000';
ctx.stroke();
}
}
};

const getPortPosition = (node, portIndex, globalScale) => {
if (node.isDup) {
return { x: node.x, y: node.y };
}
const scaledNodeRadius = nodeRadius / globalScale;
const angle = (portIndex * 2 * Math.PI) / (node.childCount + 1) - Math.PI/2;
return {
x: node.x + scaledNodeRadius * Math.cos(angle),
y: node.y + scaledNodeRadius * Math.sin(angle)
};
};

return (
<div style={{ display: 'flex', height: '100vh' }}>
<div style={{ width: '33%', padding: '1rem', display: 'flex', flexDirection: 'column' }}>
<textarea
style={{ width: '100%', height: '70%', padding: '0.5rem', border: '1px solid #AB0000', borderRadius: '4px', marginBottom: '1rem', backgroundColor: '#3F3F3F', color: 'white' }}
value={inputText}
onChange={(e) => setInputText(e.target.value)}
placeholder="Enter tree structure (e.g., b(b(b(b(x)))))"
/>
<div>
<h4 className="examples-text">Examples:</h4>
<div style={{ display: 'flex', flexWrap: 'wrap' }}>
{examples.map((example, index) => (
<button
key={index}
className="button"
onClick={() => setInputText(example.tree)}
>
{example.name}
</button>
))}
</div>
</div>
</div>
<div style={{ width: '67%' }}>
<ForceGraph2D
graphData={graphData}
nodeCanvasObject={(node, ctx, globalScale) => drawNode(node, ctx, globalScale)}
nodePointerAreaPaint={(node, color, ctx) => {
ctx.fillStyle = color;
const size = node.isDup ? nodeRadius : 2 * nodeRadius;
ctx.fillRect(node.x - size / 2, node.y - size / 2, size, size);
}}
linkColor={() => '#AB0000'}
linkWidth={2}
linkCanvasObject={(link, ctx, globalScale) => {
const start = getPortPosition(link.source, link.sourcePort, globalScale);
const end = getPortPosition(link.target, link.targetPort, globalScale);

ctx.beginPath();
ctx.moveTo(start.x, start.y);
ctx.lineTo(end.x, end.y);
ctx.strokeStyle = '#AB0000';
ctx.lineWidth = 2 / globalScale;
ctx.stroke();
}}
linkDirectionalArrowLength={0}
/>
</div>
</div>
);
};

ReactDOM.render(<TreeVisualizer />, document.getElementById('root'));
</script>
</body>
</html>
Loading

0 comments on commit 744050a

Please sign in to comment.