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

[Ulf Norell]

Yes, probably Agda.Syntax.Concrete(.Pretty) is your best bet. This is the
AST before desugaring, scope checking and type checking, so it will give
you the most flexibility.

/ Ulf

On Thu, Oct 1, 2020 at 9:49 PM Dmytro Kondratiuk <dmytro.kondratiuk at iohk.io>
wrote:

> 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
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20201001/8879f01d/attachment.html>