<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Congrats! I'm about to make doing terrible things with Agda my main job:)<div><br></div><div><br><div><div>On 26.07.2011, at 8:58, Jeremy Shaw wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Hello,<div><br></div><div>I am ashamed to admit that I have done something horrible ... I have written an irc bot in Agda.</div><div><br></div><div>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!</div><div><br></div><div>I have forever tarnished the good name of Agda.</div><div><br></div><div>You can attempt to browse the source here:</div><div><br></div><div><a href="http://patch-tag.com/r/stepcut/agdabot/snapshot/current/content/pretty">http://patch-tag.com/r/stepcut/agdabot/snapshot/current/content/pretty</a></div><div><br></div><div>But unicode support is apparently busted -- so it is a bit tough to read. </div><div><br></div><div>darcs get should be fine though:</div><div><br></div><div><span class="Apple-style-span" style="color: rgb(34, 34, 34); font-family: courier; font-size: 12px; line-height: 18px; ">darcs get <a href="http://patch-tag.com/r/stepcut/agdabot">http://patch-tag.com/r/stepcut/agdabot</a></span></div><div><span class="Apple-style-span" style="color: rgb(34, 34, 34); font-family: courier; font-size: 12px; line-height: 18px; "><br></span></div><div><span class="Apple-style-span" style="color: rgb(34, 34, 34); font-family: courier; font-size: 12px; line-height: 18px; ">Current it only supports one command: hi</span></div><div><span class="Apple-style-span" style="color: rgb(34, 34, 34); font-family: courier; font-size: 12px; line-height: 18px; "><br></span></div><div><span class="Apple-style-span" style="color: rgb(34, 34, 34); font-family: courier; font-size: 12px; line-height: 18px; ">Here is a sample session:</span></div><div><span class="Apple-style-span" style="color: rgb(34, 34, 34); font-family: courier; font-size: 12px; line-height: 18px; "><br></span></div><div><div style="font-family: courier; font-size: 12px; line-height: 18px; margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 119px; text-indent: -119px; font: normal normal normal 12px/normal Courier; color: rgb(58, 58, 58); "><span style="color: #848484"><stepcut> </span>agdabot: hi</div><div style="font-family: courier; font-size: 12px; line-height: 18px; margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 119px; text-indent: -119px; font: normal normal normal 12px/normal Courier; "><font class="Apple-style-span" color="#222222"><</font><span style="color: rgb(105, 30, 108); ">agdabot></span> <font class="Apple-style-span" color="#222222">hello!</font></div><div style="font-family: courier; font-size: 12px; line-height: 18px; color: rgb(34, 34, 34); "><br></div><div style="font-family: courier; font-size: 12px; line-height: 18px; color: rgb(34, 34, 34); ">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:</div><div style="font-family: courier; font-size: 12px; line-height: 18px; color: rgb(34, 34, 34); "><br></div><div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;">test-decode-1 : decode ":<a href="http://adams.freenode.net">adams.freenode.net</a> NOTICE * :*** Looking up your hostname..." ≡ just (record { prefix = just (server "<a href="http://adams.freenode.net">adams.freenode.net</a>") ; command = "NOTICE" ; params = "*" ∷ "*** Looking up your hostname..." ∷ [] })</span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;">test-decode-1 = refl</span></font></div></div></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;"><br></span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;">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 :)</span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;"><br></span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;">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.</span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;"><br></span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;">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.</span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;"><br></span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;">patches and flames welcome!</span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;"><br></span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;">- jeremy</span></font></div><div><font class="Apple-style-span" color="#222222" face="courier"><span class="Apple-style-span" style="line-height: 18px;"><br></span></font></div></div>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></blockquote></div><br></div></body></html>