Hi Makarius,
I am trying to adapt the Isabelle system (http://isabelle.in.tum.de) to
work with Alice (using the current CVS version instead of 1.3, due to
availability of signature includes). After some renaming of identifiers to
avoid clashes with the extra keywords of Alice, I've managed to compile
the static part of Isabelle/Pure.
Excellent! I'm glad to here that.
I'm always astonished how many people are brave enough to build Alice from
CVS... :-)
(The release of 1.4 will happen within the next 3 or 4 weeks, btw.)
To make the system really work, we now need a way to invoke the compiler
at runtime within the current toplevel environment, where normal execution
should continue afterwards. Unlike the 'use' command of Alice, which
appears to queue compilation requests to be fulfilled by the Alice
toplevel later, we need more something like EVAL in various versions of
LISP, or a string version of the 'use' of other ML implementations
(notably Poly/ML, SML/NJ, MosML).
After studying the Compiler structure (and further toplevel modules) of
Alice, I am still puzzled how this could work out. On the other hand,
with all the extra dynamic concepts of packages/components/pickles/...
available, I'd be surprised if plain old EVAL would be out of reach.
I'm afraid it is - Compiler.evalWith is as close as you can get. The reason
is not so much lack of dynamism, but the non-priviledged status and
functional purity of compiler and toplevel in the Alice system. Let me
explain. (If you already discussed this with Priya and Alan then there
probably won't be much news in here.)
All systems I'm aware of that support the feature you ask for are so-called
image systems. In these systems, the compiler is more or less an integral
part of the runtime system, and the interactive toplevel tends to be the
primary mode of operation. In particular, the compiler maintains - as
global, mutable state - a "current" environment within the runtime.
Eval-like functions can access - and modify - this environment.
Alice is not such a system, even though its toplevel may give the illusion.
The Alice runtime is just a bare VM and does not know anything about
compilation. The Compiler structure has no special status whatsoever, it is
an ordinary component that just happens to be able to produce component
values.
The interactive toplevel is even less magic. It is an ordinary application,
written all in plain ML, on top of the Compiler structure. Roughly, all it
does is running an interactive loop invoking Compiler.evalWith and threading
the environment (plus a few other things, e.g. installing its own component
manager to enable the reset functionality). Thus the "current" environment
can only be updated after complete processing of an input, not in-between.
IOW, all input has to be sequentialised - that is what the "use" queue
accomplishes.
Consequently, while it would be possible to give access to the toplevel's
"current" environment, there is no useful way to *modify* it during
evaluation - like with "use", modifications would not take effect before the
next input, and in addition, would conflict with the result from the current
input, as only one can survive.
As you see, the lack of the functionality you ask for is due to fundamental
design choices. It cannot easily be retrofitted into the system. Nor do I
think it would be a good idea - since Alice ML is focussed on concurrency, a
mechanism so heavily relying on global state does not appear advisable. I
guess the morale is that the toplevel isn't really intended for such use
(for that, Alice ML provides its dynamic component system).
Having said that, let's see how we can solve the issue with Isabelle. The
problem is that a file calling "use" won't see its effect. Only code
executed later does, including code invoked through subsequent calls to
"use". So a possible solution is to put the continuation of a specific call
to use into a separate file and use that. For example, say you have:
(* a.sml *)
val a = 33
(* b.sml *)
use "a.sml";
val b = a+1
To make this work, you can transform b.sml into:
(* b.sml *)
use "a.sml";
use "b'.sml";
(* b'.sml *)
val b = a+1
Of course, this becomes more difficult if the continuation is more complex,
in particular, if "use" was called inside some non-trivial function. But in
principle, it should always be possible - essentially you do some sort of
CPS transformation. I don't know how complex this would become for Isabelle.
I hope this helps,
- Andreas
_______________________________________________
alice-users mailing list
[email protected]
http://www.ps.uni-sb.de/mailman/listinfo/alice-users
