Public
Edited
Sep 14, 2024
url2 = "https://www.github.com/neobourbaki/Library/tree/main/database/"
function nodeType(id) {
if (/^[0-9][0-9A-Z]{7}$/.test(id)) return 'def';
if (/^[A-Z][0-9A-Z]{7}$/.test(id)) return 'thm';
return null;
}
async function getNode(id, tree={}, generation=15, label='', args={}) {
if (generation <= 0) return null;
if (!tree[id]) {
tree[id] = {
type: /^[0-9]/.test(id) ? 'def' : 'thm',
label: label,
children: [],
inProcess: false,
failed: false,
};
}
if (!nodeType(id)) return null;
tree[id].inProcess = true;
try {
const response = await fetch(url + `${id}/${id}.json`);
if (response.ok) {
const data = await response.json();
tree[id].data = data;
if (tree[id].label === "") tree[id].label = data.name;
tree[id].inProcess = false;
tree[id].failed = false;
// Process dependencies for the current node
let dependents = data.dependencies || {};
if (data.type && typeof data.type === 'object') {
dependents = { ...dependents, ...data.type };
}
const sections = ['statements', 'proofs', 'definitions'];
sections.forEach(section => {
Object.values(data[section] || {}).forEach(item => {
if (item.dependencies) {
dependents = { ...dependents, ...item.dependencies };
}
});
});
for (let key in dependents) {
let depId = key;
let label = dependents[key];
if (!nodeType(key) && label[8] == ':') {
[depId, label] = label.split(':');
}
if (tree.hasOwnProperty(depId)) {
tree[depId].children.push(id);
if (label != tree[depId].label) {
tree[depId].label = tree[depId].data.name;
}
} else {
if (!nodeType(depId)) depId += ':' + label;
tree[depId] = {
type: /^[0-9]/.test(depId) ? 'def' : 'thm',
label: label,
children: [id],
inProcess: false,
failed: !nodeType(depId)
};
await getNode(depId, tree, generation-1, label);
}
}
} else {
tree[id].failed = true;
}
} catch (error) {
tree[id].failed = true;
} finally {
tree[id].inProcess = false;
}
return tree;
}
function replaceVariables(obj1, obj2, str1, str2) {
// Function to extract keys from the string pattern {key}
const extractKeys = (text) => {
const regex = /\{(\w+)\}/g;
let keys = [], match;
while ((match = regex.exec(text)) !== null) {
keys.push(match[1]);
}
return keys;
};
// Recursive function to resolve nested keys
const resolveNestedKeys = (value, obj) => {
let resolvedValue = value;
const nestedKeys = extractKeys(resolvedValue);
nestedKeys.forEach(nestedKey => {
if (obj[nestedKey]) {
resolvedValue = resolvedValue.replace(`{${nestedKey}}`, resolveNestedKeys(obj[nestedKey], obj));
}
});
return resolvedValue;
};
// Resolve the values for each key in obj1 first to handle deep nesting
for (let key in obj1) {
obj1[key] = resolveNestedKeys(obj1[key], obj1);
}
// Replace references in obj2 based on keys extracted from str1 and mapped in obj1
const keysInStr1 = extractKeys(str1);
const keysInStr2 = extractKeys(str2);
keysInStr2.forEach((key, index) => {
const obj1Key = keysInStr1[index]; // Corresponding key in obj1
if (obj1[obj1Key]) {
obj2[key] = resolveNestedKeys(obj1[obj1Key], obj1);
}
});
return obj2;
}
function digraph(tree) {
// Helper function to find all paths from source to target
function findAllPaths(source, target, tree, path = []) {
path = path.concat(source);
if (source === target) {
return [path];
}
if (!tree[source] || !tree[source].children) {
return [];
}
const paths = [];
tree[source].children.forEach(child => {
if (!path.includes(child)) { // Avoid cycles
const newPaths = findAllPaths(child, target, tree, path);
newPaths.forEach(newPath => {
paths.push(newPath);
});
}
});
return paths;
}
// Function to reduce graph by removing implied links
function reducedGraph(tree) {
const directLinks = {};
Object.entries(tree).forEach(([id, node]) => {
if (node.children) {
node.children.forEach(childId => {
directLinks[`${id}->${childId}`] = true; // Record direct link
});
}
});
Object.entries(directLinks).forEach(([link]) => {
const [source, target] = link.split('->');
const allPaths = findAllPaths(source, target, tree);
// if (tree[target] && tree[target].type !== 'def') {
// allPaths.forEach(path => {
// if (path.length > 2) { // Means there's an intermediate node, hence remove direct link
// delete directLinks[link];
// }
// });
// }
});
return Object.keys(directLinks).map(link => link.split('->'));
}
let dotstring = 'digraph dependencies {\n';
dotstring += 'rankdir=TB;\n'; // Adjust rankdir as needed
// Define nodes
Object.entries(tree).forEach(([id, node]) => {
const shape = node.type === 'def' ? 'box' : 'ellipse';
const label = typeof node.label === 'string' ? node.label.replace(/--/g, '\n ') : ''; // Escape double quotes in label
const color = node.failed ? 'red' : 'black';
dotstring += `"${id}" [label="${label}", tooltip="${id}:\n${label}", shape=${shape}, color=${color}];\n`;
});
// Use reducedGraph to define edges
const reducedEdges = reducedGraph(tree);
reducedEdges.forEach(([source, target]) => {
dotstring += `"${source}" -> "${target}";\n`;
});
dotstring += '}\n';
return dot`${dotstring}`;
}
nodes = getNode(focus_id)
greyblock = (x) => md`<div style="background-color:#eeeeee; padding-left: 10px; padding-right: 10px; padding-top: 1px; padding-bottom: 1px; border-radius: 8px; width:${Math.min(640, width)}px">${x}</div>`
Purpose-built for displays of data
Observable is your go-to platform for exploring data and creating expressive data visualizations. Use reactive JavaScript notebooks for prototyping and a collaborative canvas for visual data exploration and dashboard creation.
