[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it

[Andreas Rossberg]

 >> Now we just need that embedded SML interpreter for our script (=
 >> theory-generation) files.
 >
 > Maybe Hamlet?  Andreas reads this list; perhaps he could comment.

Sorry, I wasn't following the discussion, since I had a week off.

I don't know what exactly you require from an embedded interpreter, but 
Hamlet implements full SML and runs fine on MLton. It is easy to extend 
it with new "primitives" provided by the host environment. It's 
certainly not adequate for something performance-critical, but since you 
say scripting that does not seem to be an issue. Let me know if you want 
more specific information.

Cheers,

   - Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB