[MLton] MLton HOL

[Stephen Weeks]

> So my question to you is, assuming I have read in a large collection
> of theorems to a suitable data-structure, is it possible to write
> something like
>
> val theorem_1 = DB.fetch "theorem_1";
> val theorem_2 = DB.fetch "theorem_2";
> ...
> val theorem_n = DB.fetch "theorem_n";
> 
> in such a way that it won't generate vast amounts of code and 
> variables in MLton?

I don't see that the way you've written it would be that bad.  One
reason MLton has been choking on your code is that the literal
construction of each theorem_i was expressed as ML code, and each of
those constructions created lots of basic blocks, lots of liveness
info, etc.  But it was really our problem to fix, not yours.

One thing you could do is to put them all in an array and refer to
them by subscripting.

val theorems = 
   Array.fromList [DB.fetch "theorem_1", ..., DB.fetch "therorem_n]

But, this does keep them all alive for the duration of the program.  I
don't know how big they are so I can't tell if it will hurt or not.


Don't worry too much about trying to please MLton.  If there are
performance bugs, we'll fix them.  Your code has already helped us
find five or so performance bugs already.