[MLton] HOL's Moscow ML implementation, and pushing MLton to
emulate it
Andreas Rossberg
rossberg@ps.uni-sb.de
Tue, 05 Apr 2005 11:28:28 +0200
>> 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