[Agda] Example Runnable Agda Programs

[Alan Jeffrey]

I've written some executable agda:

An FRP library, compiling down to JavaScript
https://github.com/agda/agda-frp-js
http://asaj.org/papers/padl13.pdf

An IO library based on transducers, compiling down to Haskell
https://github.com/agda/agda-system-io
http://asaj.org/papers/csl11.pdf

A.

On 12/12/2014 09:13 AM, Aaron Stump wrote:
> Hello, Philipp.  I have written an executable program in Agda called
> fore.  It is a type checker and translator for System F plus global
> positive-recursive type definitions.  I am using this for research on
> typed lambda encodings (Church, Parigot, a new one of ours).  It parses
> input -- using a parser produced by our gratr parser-generator, which
> targets OCaml and Agda -- then type checks it, and translates it to
> Racket and Haskell.  You can find the code, and examples, here:
>
> http://www.cs.uiowa.edu/~astump/software/fore.zip
>
> It's about 2kloc of Agda.  Let me know if you have any questions about
> this example.
>
> It is great if you will improve the Agda compiler!
>
> Best wishes,
> Aaron
>
> On 12/12/2014 08:47 AM, Philipp Hausmann wrote:
>> Hi,
>>
>> I am looking for example programs to test the Agda compilers. Just by
>> searching github, google & co I couldn't find many Agda programs which
>> can actually be run and do something interesting.
>>
>> To give a bit of context, we are working on a new backend for Agda and
>> would like to have some regression tests. We have some simple
>> HelloWorld-style programs. but we are missing some more complicated
>> examples. Currently we are porting the Eliza [1] example from GHC's
>> nofib testsuite, but adding already existing Agda programs would be much
>> less work....  Especially interesting would also be examples where the
>> current MAlonzo backend fails or produces bad code. I remember seeing
>> some emails about them on the mailing list [2, 3, 4], but I don't
>> remember seeing any actual code example for reproducing these errors.
>>
>> As the behaviour of Agda programs should not really depend on the
>> backend, I think the test programs would be useful for the MAlonzo
>> backend as well.
>>
>> Long story short, does anyone have actual runnable Agda programs we
>> could use for testing?
>>
>> Cheers,
>> Philipp
>>
>> [1]
>> https://github.com/phile314/agda/blob/compiler-tests/test/exec/with-stdlib/Eliza.agda
>>
>> [2] https://lists.chalmers.se/pipermail/agda/2012/004423.html
>> [3] https://lists.chalmers.se/pipermail/agda/2013/005229.html
>> [4] https://lists.chalmers.se/pipermail/agda/2014/006990.html
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda