[Agda] Example Runnable Agda Programs

[Andreas Abel]

The Agda Prelude has two runnable examples in

   https://github.com/fkettelhoit/agda-prelude/tree/master/Examples

Cheers,
Andreas

On 12.12.2014 21:47, Alan Jeffrey wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/