[Agda] Ring Solver (looking for feedback)

[Donnacha Oisín Kidney]

https://oisdk.github.io/agda-ring-solver/README.html <https://oisdk.github.io/agda-ring-solver/README.html>

Hi all! For the past few months I’ve been working on a new ring solver to replace the one in the standard library. It’s part of my undergrad final year project, but I’m hoping to also submit it to a conference or something over the next few weeks.

The focus is on ease-of-use, but it’s also faster than the old solver (on more complex equations—the base-level time to solve things like 1 ≈ 1 is ~5 seconds, versus the standard library’s ~2).

At the moment, I’m the only person who’s used it, so I’m interested in hearing about more use cases and how it fits in. Also, any insight on type-checking performance would be great: the vast majority of speed gains in the solver came from places I wasn’t expecting (carefully arranging things to prevent reduction and encourage syntactic equality, for instance).

Anyway, this is what the interface looks like:

    lemma : ∀ x y → x + y * 1 + 3 ≈ 3 + 1 + y + x + - 1
    lemma = solve Int.ring

Oisín Kidney.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190127/2e22f070/attachment.html>