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

[Michael Norrish]

Stephen Weeks writes:
 
> > I'd really like to write
 
> >   val ADD_COMM = DB "arithmetic" "ADD_COMM"
> >   fun solve_system s = .... ADD_COM ....
 
> > But this won't work because the binding for ADD_COMM will happen as
> > the executable starts up, in an arithmetic-free context, and DB will
> > raise an exception.  (We need to support such a context precisely so
> > that our tool can itself be used for the development of the arithmetic
> > theory in the first place). 
 
> I don't understand the problem with this approach.  Why can't you
> guarantee that the DB has the necessary theorem, either from an
> earlier invocation of a different executable, or earlier in the
> startup of this executable?

I guess you are suggesting the use of a series of executables.  In the
initial stages, monolith0 is used:

  monolith0  -- creates -->   theories of booleans, relations, natural
                                          numbers, arithmetic on them

Now that we have theory of arithmetic to hand, the code above that
quotes ADD_COMM will work so we create monolith1, which links in the
additional code:

  monolith1  -- creates -->   theories of integers, lists

Now that we have a theory of integers, we can include the code for
deciding integer problems too, creating monolith2

  monolith2  -- create -->    theories of real numbers 

Now that we have a theory of real numbers, we can include the code for
real number decision problems, creating monolith3

etc etc 

The last monolith would necessarily load all of the theories its code
depended on, but we could ensure that the users of this code had
theories with the correct theory ancestry (i.e., not necessarily
everything) by being careful with our internal data management.  (This
is the insight: I had assumed that if you were initialising the theory
of arithmetic from disk, then you were committing to making all
subsequent work dependent on that theory, which we wouldn't want.)

If users wanted to include code of their own, they would create their
own monoliths. 

I think that's a nice story, thanks!

Now we just need that embedded SML interpreter for our script (=
theory-generation) files.

Regards,
Michael.