Better `rewrite` engine

antalsz / hs-to-coq

Convert Haskell source code to Coq source code

https://hs-to-coq.readthedocs.io

MIT License

279 stars 27 forks source link

Better `rewrite` engine #124

Open antalsz opened 5 years ago

antalsz commented 5 years ago

Our rewrite engine is a bare-bones version of something more honest. For example, what about real support for variable binding, or handling nonlinear patterns gracefully?

antalsz commented 5 years ago

This also extends to improving the Coq parser, such as by supporting let 'pair x y := ... in ....

antalsz commented 5 years ago

And being consistent in where we apply rewrites – for instance, we don't currently rewrite all generated matches