[MLton] MLton HOL

[Stephen Weeks]

Hi Joe.  I'm pleased to report some progress on compiling HOL.  I left
a compile running last night that completed in 8.6 hours.  It produced
a 33M executable, which, when run, produces the following output in
4.5 minutes.

% psl1
<<HOL message: Couldn't define encode function for type string>>
<<HOL message: Couldn't define encode function for type semi_ring>>
<<HOL message: Couldn't define encode function for type ring>>
<<HOL message: Couldn't define encode function for type deep_form>>
<<HOL message: loading RealArith>>
<<HOL message: Couldn't define encode function for type regexp>>
unhandled exception: HOL_ERR

Perhaps you could look into this error while we continue to improve
the compile time.  I'm shooting for 20 minutes -- it should just take
some more efforts on improving quadratic algorithms to get there.