search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.48k stars 345 forks source link

ToTreeless: allow backends to define custom pipelines #7273

Closed omelkonian closed 4 months ago

omelkonian commented 4 months ago

When developing backends, the translation from internal syntax to treeless syntax currently only exports toTreeless with a fixed pipeline of optimization passes (compilerPipeline).

This PR introduces toTreelessWith to allow backends to tweak that and use a custom pipeline (I already need that in agda2rust), while also exporting necessary utilities to build those pipelines.

andreasabel commented 2 months ago

I am adding a changelog entry; this is a noteworthy change of the API.