[opentheory-users] a standalone tactic translating numeral encodings

[Ramana Kumar]

I've written a Haskell program that acts as a conversion between Norrish
numerals and binary numerals.
It reads an OpenTheory article encoding a Norrish numeral n[N] (made with
bit1, bit2, and zero) and writes an article that proves the theorem:
|- n[N] = n[B]
where n[B] is the binary encoding of n (made with bit0, bit1, and zero).
You can access it as a "standalone tactic" at http://cam.xrchz.net/n2b.cgi.
It may use up to 6 theorems as axioms (which are all proved in the standard
library).

The Haskell source code is here
https://github.com/xrchz/typed-conv/blob/master/numeral/n2b.hs (around 500
lines).
I'm pretty new to Haskell, so I'd very much appreciate any comments on the
design.
A lot of the infrastructure should be resuable by future standalone tactics
in Haskell.

Specific design questions I have:
 - would it be better to somehow write articles without going via a type of
proofs (i.e. just directly log as theorems are built)? I tried to figure
out a way to do that but failed, and also stopped thinking it would be
better
 - would it be more efficient to store conclusions with proofs rather than
computing them with concl? but I think Haskell memoises anyway...
 - is there a better algorithm for converting between these numeral
encodings?
 - my articles always leave tonnes of stuff on the stack because they just
def everything... is there an efficient algorithm for only deffing things
you'll actually use (and maybe removing them after you won't any more)?
 - probably lots of obvious things I'm doing less nicely than is possible...
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120217/25b64d30/attachment.htm>