[Agda] hello, I've done something terrible...

[Perikov Pavel]

Congrats! I'm about to make doing terrible things with Agda my main job:)


On 26.07.2011, at 8:58, Jeremy Shaw wrote:

> Hello,
> 
> I am ashamed to admit that I have done something horrible ... I have written an irc bot in Agda.
> 
> That's right! A program that you can not only type-check -- but even run! And it is a pretty big hack job too... probably even buggy!
> 
> I have forever tarnished the good name of Agda.
> 
> You can attempt to browse the source here:
> 
> http://patch-tag.com/r/stepcut/agdabot/snapshot/current/content/pretty
> 
> But unicode support is apparently busted -- so it is a bit tough to read. 
> 
> darcs get should be fine though:
> 
> darcs get http://patch-tag.com/r/stepcut/agdabot
> 
> Current it only supports one command: hi
> 
> Here is a sample session:
> 
> <stepcut> agdabot: hi
> <agdabot> hello!
> 
> The most 'interesting' part of the code is perhaps the unit tests. For example, here is a unit test that checks that messages are decoded properly:
> 
> test-decode-1 : decode ":adams.freenode.net NOTICE * :*** Looking up your hostname..." ≡ just (record { prefix = just (server "adams.freenode.net") ; command = "NOTICE" ; params = "*" ∷ "*** Looking up your hostname..." ∷ [] })
> test-decode-1 = refl
> 
> There the unit test is in the type signature and checked at compile time. Obviously that is old hat to a seasoned Agda programmer, but crazy talk to a Haskell user :)
> 
> The thing that makes the code especially ugly is that I have not figured out how to handle the equivalent of nested case statements yet. So, I have a bunch of helper functions that use 'with f x' to work around that. That is probably the first thing I will fix.
> 
> The biggest known flaw is that the many1 parser does not prove termination, so I had to enable --no-termination-check. That is probably the second thing I will look at.
> 
> patches and flames welcome!
> 
> - jeremy
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110728/de5e9cfc/attachment.html