[MLton] MLton HOL

[Stephen Weeks]

Hi Joe.  I added to MLton the idea that Matthew and I mentioned about
pretty printing top-level exceptions.  The actual name that I settled
on was MLton.Exn.addExnMessager (this may change).

On line 5905 of psl1.sml, immediately after the declaration of
HOL_ERR, I inserted code to print HOL_ERR nicely.

val () =
  MLton.Exn.addExnMessager
    (fn HOL_ERR {origin_structure, origin_function, message} =>
        SOME (concat ["HOL_ERR: {origin_structure = ", origin_structure,
                      ", origin_function = ", origin_function,
                      "message = ", message, "}"])
      | _ => NONE)

I also fixed one quadratic performance bug in our code generator that
Matthew found.  It turns out that this bug caused the bulk of the
slowdown in the 8.6 hour compile.  As a result, my latest compile of
HOL took 1.3 hours.  Here's what the executable now displays.

% 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: {origin_structure = Type, origin_function = mk_thy_typemessage = Expecting 2 arguments for path}

Hopefully this is enough to let your work continue at last!

BTW, all these improvements are checked in to the MLton CVS.  So, if
you want to, you can build MLton from CVS and start using it on HOL
immediately.  Else, let me know when you need it and I'll package up
an experimental release.