[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it
Michael Norrish
Michael Norrish <Michael.Norrish@nicta.com.au>
Fri, 1 Apr 2005 10:29:35 +1000
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.