fixpoint algorithm: parameterize the Map to use

This commit is contained in:
Joeri Exelmans 2025-05-22 14:31:26 +02:00
parent ea878975be
commit 47786ae792
3 changed files with 58 additions and 10 deletions

View file

@ -4,10 +4,12 @@
// FRANCOIS POTTIER,<a href="https://gallium.inria.fr/~fpottier/publis/fpottier-fix.pdf"> Lazy Least Fixed Points in ML</a>
// <a href="https://gitlab.inria.fr/fpottier/fix">OCAML Code</a>
export const fixer = (eqsFunction, lattice) => {
const mFixed = new Map();
const mTransient = new Map();
const mParents = new Map();
// eqsFunction: V -> (V -> P) -> P
// elemCmp: (V -> V -> Ordering)
export const fixer = (eqsFunction, dictType, lattice) => {
const mFixed = dictType();
const mTransient = dictType();
const mParents = dictType();
const mWorkset = []; // Note: we use a Stack (LIFO), but FIFO queue or any other collection would also work.
@ -16,7 +18,6 @@ export const fixer = (eqsFunction, lattice) => {
const ensureTransient = node => {
if (mTransient.has(node)) return;
mTransient.set(node, lattice.bottom());
mParents.set(node, []);
mWorkset.push(node);
}
@ -47,7 +48,7 @@ export const fixer = (eqsFunction, lattice) => {
}
if (!lattice.equality(mTransient.get(current), newProperty)) {
mTransient.put(current, newProperty);
mTransient.set(current, newProperty);
mWorkset.push(...(mParents.get(current) || []));
}
}

View file

@ -29,3 +29,46 @@ export class RBTreeWrapper {
return this.tree.keys.map(key => [key, this.tree.get(key)]);
}
}
// Can be used as drop-in replacement for Map
// Why create a mutable adapter for a purely-functional data structure?
// Because the builtin Map does not allow custom comparison functions and this one does.
export class MutableRBTree {
constructor(tree, printf = defaultPrintf) {
this.tree = tree;
this[inspect.custom] = printf;
}
static new(cmp) {
return new MutableRBTree(createRBTree(cmp));
}
set(key, value) {
this.tree = this.tree.remove(key).insert(key, value);
}
delete(key) {
this.tree = this.tree.remove(key);
}
get(key) {
return this.tree.get(key);
}
has(key) {
return this.tree.get(key) !== undefined;
}
clear() {
this.tree = createRBTree(this.tree._compare);
}
*[Symbol.iterator]() {
const iter = this.tree.begin;
while (iter !== undefined && iter.valid) {
yield [iter.key, iter.value];
iter.next();
}
}
}