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

[Dmytro Kondratiuk]

Thanks for quick reply - I’ll try that one then.

On Fri, Oct 2, 2020 at 3:17 AM Ulf Norell <ulfn at chalmers.se> wrote:

> 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/20201002/8e985e67/attachment.html>