[Agda-dev] Fwd: Agda as a target language

[Dmytro Kondratiuk]

Hi agda-devs!

I'd like to use Agda as a target language in a code generator. Here's a
short description of the problem:
I have logic (written in Haskell) that allows me to generate business rules
in a given target language, which is currently an embedded DSL.

I'd like to prove certain properties about those rules, but I'd prefer to
avoid rewriting them manually in Agda (it is a large ever growing
specification with tons of formulas from the financial domain).
Instead my goal is to generate Agda code automatically and then create
proofs on top of the generated code.

Is there a convenient API in Agda's compiler that would allow me to safely
generate Agda syntax tree and pretty-print it into .agda file? Any examples?

P.S. Agda.Syntax.Concrete.Pretty seems like a good candidate, though I'm
not sure if it is the right way to do it.

Thanks in advance,
Dmytro Kondratiuk
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20201002/6c501bea/attachment.html>