There was this paper a while ago, not sure where the software can be downloaded: <a href="http://ittc.ku.edu/~andygill/papers/IntroHERA06.pdf">http://ittc.ku.edu/~andygill/papers/IntroHERA06.pdf</a><br><br><div class="gmail_quote">On Mon Jan 19 2015 at 8:43:49 AM Mathieu Boespflug <<a href="mailto:mboes@tweag.net">mboes@tweag.net</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Could Hermit be of any relief?<br>
<br>
<a href="http://ku-fpg.github.io/software/hermit/" target="_blank">http://ku-fpg.github.io/<u></u>software/hermit/</a><br>
<br>
It doesn't work on the surface syntax, only on the core syntax AFAIK,<br>
but some would call that a feature (simpler traversals). So long as<br>
you're happy doing this reasoning at the level of Core, this should be<br>
workable. I'm not sure that it would be easy to map the result back to<br>
surface syntax, but maybe Andy can comment.<br>
<br>
Best,<br>
<br>
Mathieu<br>
<br>
On 19 January 2015 at 00:46, Christopher Done <<a href="mailto:chrisdone@gmail.com" target="_blank">chrisdone@gmail.com</a>> wrote:<br>
> Hi<br>
><br>
> I quite enjoy doing equational reasoning to prove that my functions satisfy<br>
> some laws, I like to type out each substitution step until I get back what I<br>
> started with. The only trouble is that it's rather manual and possibly error<br>
> prone.<br>
><br>
> Is there any tooling anywhere out there that can take in a Haskell<br>
> expression and reduce it by one step? I only know of stepeval:<br>
><br>
> <a href="http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr=foldr+%28%2B%29+0+%5B1%2C2%2C3%5D+%3D%3D+6" target="_blank">http://bm380.user.srcf.net/<u></u>cgi-bin/stepeval.cgi?expr=<u></u>foldr+%28%2B%29+0+%5B1%2C2%<u></u>2C3%5D+%3D%3D+6</a><br>
><br>
> But it's just a prototype and works on a teeny weeny subset of Haskell. As<br>
> much as I like doing tooling, my bandwidth for this area is already full.<br>
><br>
> It seems quite hard to implement such a tool with existing tooling. Real<br>
> compilers and interpreters tend to be distinctly far away from a simple<br>
> substitution model or retaining the original source code and being able to<br>
> print valid source back out.<br>
><br>
> If such a tool existed, though, it'd be super handy and you could probably<br>
> include it as another check for your build process like your type checking,<br>
> your quickcheck properties and your unit tests. I would personally invest a<br>
> little bit of time to add interactive Emacs support for such a tool.<br>
><br>
> Ciao<br>
><br>
> ______________________________<u></u>_________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
><br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>