| title |
|---|
Egglog0 |
A prototype implementation. You may be looking for https://github.com/egraphs-good/egglog
<script type="module"> export { run }; import init, { run_wasm } from './pkg/egglog.js'; async function run() { await init(); var query = document.getElementById("query").value; var proof = document.getElementById("proofmode").checked; var graph = false; const result = run_wasm(query, proof, graph); console.log(result); document.getElementById("result").value = result; } window.run = run; //run(); </script> <script> function pickerbox(select){ var xhr = new XMLHttpRequest(); xhr.open('GET', `/egglog0/examples/${select.value}`, true); // If specified, responseType must be empty string or "text" xhr.responseType = 'text'; xhr.onload = function () { if (xhr.readyState === xhr.DONE) { if (xhr.status === 200) { //console.log(xhr.response); //console.log(xhr.responseText); document.getElementById("query").value = xhr.responseText; } } }; xhr.send(null); } window.onload = () => { urlParams = new URLSearchParams(window.location.search); url_eaxmple = urlParams.get('example'); picker = document.getElementById("examplepicker") if(url_eaxmple != null){ picker.value = url_eaxmple; } pickerbox(picker) } </script> <textarea spellcheck="false" id="query" rows="20" style="width:100%"> </textarea>Run
PLDI Talk
Basics
Datalog
SKI Combinators
Lists
Arithmetic
Memory/Arrays
Pullback of Monic is Monic
Uniqueness of Identity
Composition of Pullbacks
Proofs (Experimental)
<textarea id="result" rows="20" style="width:100%"> </textarea>
A prolog like syntax for interfacing with the egg egraph library.
<iframe width="560" height="315" src="https://www.youtube.com/embed/dbgZJyw3hnk?start=2725" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture" allowfullscreen></iframe>Github repo: https://github.com/philzook58/egglog0 Read more here:
- Talk abstract
- https://www.philipzucker.com/egglog-checkpoint/ - Early version of egglog, motivations.
- https://www.philipzucker.com/egglog2-monic/ - A simple category theory theorem about pullbacks.
- https://www.philipzucker.com/egglog-3/ - Arithmetic, SKI combinator, datalog, lists examples