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

[Anton Setzer]

You might have a look at an example I have written some time ago, namely
 a drawing program written in Agda.
The way to overcome the problem with termination is to use coalgebras
(at some point called codata, currently implemented using Nisse's # and b).

http://www.cs.swan.ac.uk/~csetzer/software/agda2/IOLib/

Anton


On 26/07/11 05: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


-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
 
                    
  

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