88 lines
2.6 KiB
JavaScript
88 lines
2.6 KiB
JavaScript
// Based on:
|
|
// https://github.com/plug-obp/obp3-algos/blob/1f15cf8c829c7ecd08adb7180aa3c3aefa4f9466/src/main/java/obp3/fixer/Fixer.java
|
|
// which is in turn based on:
|
|
// 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>
|
|
|
|
// 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.
|
|
|
|
let inactive = true;
|
|
|
|
const ensureTransient = node => {
|
|
if (mTransient.has(node)) return;
|
|
mTransient.set(node, lattice.bottom());
|
|
mWorkset.push(node);
|
|
}
|
|
|
|
const solve = current => {
|
|
if (mFixed.get(current) !== undefined) return;
|
|
const currentChildren = [];
|
|
const alive = [true];
|
|
const requestFunction = node => {
|
|
if (!alive[0]) throw new Error("must be alive!");
|
|
const property = mFixed.get(node);
|
|
if (property !== undefined) return property;
|
|
ensureTransient(node);
|
|
currentChildren.push(node);
|
|
return mTransient.get(node);
|
|
}
|
|
const newProperty = eqsFunction(current)(requestFunction);
|
|
alive[0] = false;
|
|
|
|
const isMaximal = lattice.isMaximal(newProperty);
|
|
if (!isMaximal) {
|
|
for (const child of currentChildren) {
|
|
const parents = mParents.get(child);
|
|
if (parents === undefined) {
|
|
mParents.set(child, [current]);
|
|
} else {
|
|
parents.push(current);
|
|
}
|
|
}
|
|
|
|
if (!lattice.equality(mTransient.get(current), newProperty)) {
|
|
mTransient.set(current, newProperty);
|
|
mWorkset.push(...(mParents.get(current) || []));
|
|
}
|
|
}
|
|
else {
|
|
mFixed.set(current, newProperty);
|
|
const oldProperty = mTransient.get(current);
|
|
mTransient.delete(current);
|
|
if (!lattice.equality(oldProperty, newProperty)) {
|
|
mWorkset.push(...(mParents.get(current) || []));
|
|
}
|
|
}
|
|
}
|
|
|
|
const get = node => {
|
|
const property = mFixed.get(node);
|
|
if (property !== undefined) return property; // return from cache
|
|
|
|
if (!inactive) throw new Error("must be inactive!");
|
|
inactive = false;
|
|
|
|
ensureTransient(node);
|
|
|
|
while (mWorkset.length > 0) {
|
|
const current = mWorkset.pop(); // LIFO
|
|
solve(current);
|
|
}
|
|
|
|
for (const [key, value] of mTransient) {
|
|
mFixed.set(key, value);
|
|
}
|
|
mTransient.clear();
|
|
inactive = true;
|
|
return mFixed.get(node);
|
|
}
|
|
|
|
return get;
|
|
}
|