-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Rough library version of use_e build and evaluation
- Loading branch information
Showing
13 changed files
with
924 additions
and
720 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,115 @@ | ||
// e init (tree) => e-graph | ||
// e match (pattern, e-graph) => e-node[] | ||
// e sub (result, e-node, e-graph) => e-graph | ||
|
||
let nodeIdCounter = 0; | ||
const nodes = new Map(); | ||
|
||
const node = (value, ...children) => { | ||
const hash = value + children.map((c) => ":" + c.id).join(""); | ||
if (nodes.has(hash)) return nodes.get(hash); | ||
const res = { | ||
isNode: true, | ||
value, | ||
children: children, | ||
parents: [], | ||
id: nodeIdCounter++, | ||
hash, | ||
}; | ||
nodes.set(hash, res); | ||
for (const child of children) child.parents.push(res); | ||
return res; | ||
}; | ||
const vari = (v, ...children) => { | ||
const res = { | ||
isNode: true, | ||
var: v, | ||
children: children, | ||
parent: null, | ||
}; | ||
for (const child of children) child.parent = res; | ||
return res; | ||
}; | ||
const nodeEq = (n1, n2) => n1.hash === n2.hash; | ||
|
||
const a = node("f", node(1), node(2)); | ||
const b = node("f", node(1), node(2)); | ||
|
||
console.log("nodeEq!", nodeEq(a, b)); | ||
console.log("nodes!", nodes); | ||
|
||
let idCounter = 0; | ||
const eClasses = new Set(); | ||
const eNodes = new Map(); | ||
|
||
const eNode = (value, ...children) => { | ||
const hash = value + children.map((c) => ":" + c.id).join(""); | ||
if (eNodes.has(hash)) return nodes.get(hash); | ||
const res = { | ||
isENode: true, | ||
value, | ||
children: children, | ||
parents: [], | ||
id: nodeIdCounter++, | ||
hash, | ||
}; | ||
nodes.set(hash, res); | ||
for (const child of children) child.parents.push(res); | ||
return res; | ||
}; | ||
|
||
const eNodes = new Map(); | ||
let eClassIdCounter = 0; | ||
const eClassFromNode = (node, parentENode = null) => { | ||
const eNode = { isENode: true, value: node.value }; | ||
eNode.children = node.children.map((n) => eClassFromNode(n, eNode)); | ||
const id = node.value + eNode.children.map((c) => "c" + c.id).join(); | ||
eNodes.set(id, eNode); | ||
return { | ||
isEClass: true, | ||
eNodes: [eNode], | ||
parents: [parentENode], | ||
id: eClassIdCounter++, | ||
}; | ||
}; | ||
|
||
console.log("eClassFromNode!", eClassFromNode(a)); | ||
|
||
const eClassMatches = (patternNode, eClass) => { | ||
return eClass.eNodes.flatMap((en) => eNodeMatches(patternNode, en)); | ||
}; | ||
const eNodeMatches = (patternNode, eNode) => { | ||
if (patternNode.var === undefined && eNode.value !== patternNode.value) | ||
return []; | ||
else if (patternNode.children.length !== eNode.children.length) return []; | ||
else { | ||
const childrenMatches = eNode.children.map((ec, i) => | ||
eClassMatches(patternNode.children[i], ec) | ||
); | ||
return [ | ||
...gogo( | ||
childrenMatches, | ||
patternNode.var ? { [patternNode.var]: eNode.value } : {} | ||
), | ||
]; | ||
} | ||
}; | ||
|
||
const gogo = function* (childrenMatches, match) { | ||
if (childrenMatches.length === 0) { | ||
yield { ...match }; | ||
return; | ||
} | ||
for (const matches1 of childrenMatches[0]) { | ||
for (const matches2 of gogo(childrenMatches.slice(1))) { | ||
yield { ...match, ...matches1, ...matches2 }; | ||
} | ||
} | ||
}; | ||
|
||
console.log( | ||
"eClassMatches!", | ||
eClassMatches(vari("go", vari("1"), node(2)), eClassFromNode(a)) | ||
); | ||
|
||
// Aside: the implicit lifting language could maybe really help simplify this. |
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,69 @@ | ||
import { makeSet, find, union } from "./union_find.js"; | ||
// map canonical e-nodes to e-class ids | ||
// i.e. e-node 𝑛 ∈ 𝑀 [𝑎] ⇐⇒ 𝐻 [canonicalize(𝑛)] = find(𝑎) | ||
const hashcons = new Map(); | ||
const parents = new Map(); | ||
const worklist = new Set(); | ||
const mk_enode = (op, children) => ({ | ||
op, | ||
children, | ||
hash: op + children.map((c) => "c" + c.id).join(), | ||
}); | ||
// TODO: fix canonicalize to respect hashcons | ||
const canonicalize = (eNode) => mk_enode(eNode.op, eNode.children.map(find)); | ||
const lookup = (eNode) => hashcons.get(eNode.hash); | ||
// eNode -> eClassId | ||
const add = (eNode) => { | ||
const en = canonicalize(eNode); | ||
if (lookup(en)) | ||
return lookup(en); | ||
else { | ||
const eClassId = makeSet(); | ||
for (const child of eNode.children) | ||
parents.set(child, parents.get(child)?.set(en, eClassId) ?? new Map([[en, eClassId]])); | ||
hashcons.set(en.hash, eClassId); | ||
return eClassId; | ||
} | ||
}; | ||
const merge = (eClassId1, eClassId2) => { | ||
if (find(eClassId1) === find(eClassId2)) | ||
return find(eClassId1); | ||
const newEClassId = union(eClassId1, eClassId2); | ||
worklist.add(newEClassId); | ||
return newEClassId; | ||
}; | ||
const rebuild = () => { | ||
while (worklist.size > 0) { | ||
const todo = [...worklist]; | ||
worklist.clear(); | ||
for (const eClassId of todo) | ||
repair(find(eClassId)); | ||
} | ||
}; | ||
const repair = (eClassId) => { | ||
for (const [peNode, peClassId] of parents.get(eClassId) ?? []) { | ||
hashcons.delete(peNode.hash); | ||
const newPeNode = canonicalize(peNode); | ||
hashcons.set(newPeNode.hash, peClassId); | ||
} | ||
const newParents = new Map(); | ||
for (const [peNode, peClassId] of parents.get(eClassId) ?? []) { | ||
const newPeNode = canonicalize(peNode); | ||
if (newParents.has(newPeNode)) { | ||
merge(peClassId, newParents.get(newPeNode)); | ||
} | ||
newParents.set(newPeNode, find(peClassId)); | ||
} | ||
parents.set(eClassId, newParents); | ||
}; | ||
//const ematch = (pattern) => [subts, eClass][] | ||
// To apply a rewrite l → 𝑟 to an e-graph, | ||
// ematch finds tuples (𝜎,𝑐) where e-class 𝑐 represents l[𝜎]. | ||
// Then, for each tuple, merge(𝑐, add(𝑟 [𝜎])) adds 𝑟 [𝜎] to the e-graph | ||
// and unifies it with the matching e-class c. | ||
add(mk_enode("1", [])); | ||
add(mk_enode("2", [])); | ||
add(mk_enode("+", [hashcons.get("1"), hashcons.get("2")])); | ||
add(mk_enode("+", [hashcons.get("1"), hashcons.get("2")])); | ||
rebuild(); | ||
console.log(hashcons); |
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,37 @@ | ||
import { | ||
node, | ||
vari, | ||
merge, | ||
printEClasses, | ||
runRules, | ||
e, | ||
checkEq, | ||
unhash, | ||
eClassMatches, | ||
} from "./e_graph.js"; | ||
import { setFromId, find } from "./union_find.js"; | ||
|
||
const rules = [ | ||
{ | ||
from: [node("a")], | ||
to: ({}, ec) => merge(ec, e("b")), | ||
}, | ||
{ | ||
from: [node("b")], | ||
to: ({}, ec) => merge(ec, e("a")), | ||
}, | ||
]; | ||
|
||
e("+", e("a")); | ||
e("+", e("b")); | ||
|
||
printEClasses(); | ||
|
||
runRules(rules); | ||
|
||
printEClasses(); | ||
|
||
console.log( | ||
"CHECK", | ||
checkEq(node("a"), node("+", node("-", node("b"), node("c")), node(0))) | ||
); |
Oops, something went wrong.