Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Interaction Net graph dumping and visualization #435

Open
wants to merge 15 commits into
base: main
Choose a base branch
from
Open
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ examples/**/main
examples/**/*.c
examples/**/*.cu
.out.hvm
dots.js

# nix-direnv
/.direnv/
Expand Down
31 changes: 31 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -72,3 +72,34 @@ don't worry, it isn't meant to. [Bend](https://github.com/HigherOrderCO/Bend) is
the human-readable language and should be used both by end users and by languages
aiming to target the HVM. If you're looking to learn more about the core
syntax and tech, though, please check the [PAPER](./paper/HVM2.pdf).

Interaction Net graph dumping and visualization
-----------------------------------------------

With the rust interpreter (`hvm run`), every evaluation step can be dumped with
the `--dump` command line option. You can dump in sequential mode (only one
redex is evaluated in each step) or, with the `--parallel` option,
in parallel mode (all redexes are evaluated in each step).

The dump will be written to the file `dots.js` in the current directory.

You can view the graph dump with `index.html` as follows:

Copy the file `dots.js` to the HVM directory. Then start a http server in the
HVM directory:

```sh
cd HVM
python3 -m http.server
```

Now you can visit `http://127.0.0.1:8000` and step through the graph with
the wasd keys on your keyboard.

How parallel is my Bend/HVM program?
------------------------------------

With the `--parallel` option, HVM also calculates the average number of regexes
in each step, thus giving a measurement of how parallel a given bend program is.

You can use the `--parallel` option without the `--dump` option as well.
97 changes: 97 additions & 0 deletions index.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@
<!DOCTYPE html>
<meta charset="utf-8">
<body>
<style type="text/css">
html, body {
margin: 0;
padding: 0;
}
#graph {
position: absolute;
display: block;
width: 100%;
height: 100%;
}
</style>
<script src="https://d3js.org/d3.v7.min.js"></script>
<script src="https://unpkg.com/@hpcc-js/[email protected]/dist/graphviz.umd.js"></script>
<script src="https://unpkg.com/[email protected]/build/d3-graphviz.js"></script>
<script src="./dots.js"></script>
<div id="graph"></div>
<script>

const div = document.getElementById("graph");
var offset = 0;
var dotIndex = 0;
readHash();
var graphviz = d3.select("#graph").graphviz()
.transition(function () {
return d3.transition("main")
.ease(d3.easeLinear)
.duration(200);
})
.logEvents(false)
.width(div.clientWidth)
.height(div.clientHeight)
.fit(false)
.tweenPaths(false)
.tweenShapes(false)
.growEnteringEdges(false)
.fade(true)
.on("initEnd", render);

window.addEventListener("keydown", function (e) {
old = offset;
if (e.code === "KeyW") {
offset = 10;
} else if (e.code === "KeyS") {
offset = -10;
} else if (e.code === "KeyA") {
offset = -1;
} else if (e.code === "KeyD") {
offset = 1;
}
if (old === 0) {
update();
}
});

window.addEventListener("keyup", function (e) {
offset = 0;
});

window.addEventListener("hashchange", function (e) {
readHash();
render();
});

function readHash() {
if (window.location.hash) {
dotIndex = parseInt(window.location.hash.slice(1), 10);
if (isNaN(dotIndex)) {
dotIndex = 0;
}
}
}

function render() {
graphviz.renderDot(dots[dotIndex]);
graphviz.on("end", update);
}

function update() {
if (offset === 0) {
return;
}

dotIndex += offset;
if (dotIndex < 0) {
dotIndex += dots.length;
} else if (dotIndex >= dots.length) {
dotIndex -= dots.length;
}
window.location.hash = "#" + dotIndex;
render();
}

</script>
Loading