Makarius wrote:
On Fri, 14 Mar 2008, David Matthews wrote:
The new argument is nameSpace. In most cases this can just be set to PolyML.globalNameSpace which will look up values in the normal ML name space and enter them there, but it is possible to set up your own name space or interpose one between the compiler and the global space.
This sounds very interesting. It looks like it will finally enable proper management of ML bindings invoked within Isabelle, observing the hierarchical structure of theories, admitting proper undo/redo, and working smoothly with multithreading.
That would be good. I hadn't thought about rolling back the name space but of course that's perfectly possible.
The only concern is the global PolyML.setPrintEnv for General.exnMessage and PolyML.print. Is there an easy way to get a purely functional interface for passing the name space? Otherwise we need to apply the usual tricks with our setmp and CRITICAL markup.
I've experimented with adding equivalent functions to the present PolyML.print and PolyML.makestring (from which General.exnMessage is derived) but with the name space to be used as an additional argument. The most general form would be something like: PolyML.printPretty: { value: 'a, nameSpace: nameSpace, stream: string->unit, depth: int, lineLength: int } -> () PolyML.formatAsString: 'a * nameSpace -> string
As well as the name space this would also take the output stream and print depth as arguments. Would this do what you want? Note that printPretty pretty-prints its argument whereas displayAsString just produces a linear string.
PolyML.print and PolyML.makestring are both relics of an early draft of Standard ML that didn't make it into the published standard. They are infinitely overloaded functions rather like '=' and '<>'. printPretty and formatAsString would be just the same. Because the compiler treats them specially this restricts the way they can usefully be incorporated into other functions. For example it's not possible to define fun makestring a = PolyML.formatAsString(PolyML.globalNameSpace, a) because this would capture the type of "a" as 'a and so it would only ever print "?". It is possible to define val exnMessage: exn->string = PolyML.makestring which is actually how it is defined, or val exnMessageInSpace: exn*namespace->string = PolyML.formatAsString because they make use of the identifier in an exception packet to search the name space for an exception with that identifier and use the type information they find.
Apart from the print functions the only other case where the global environment is used is the "debug" function. This is set using setDebugShell. This could be improved by having it use the namespace used when the code to be debugged was compiled. Alternatively, it could also be passed in as a parameter to PolyML.compiler but that is adding yet more arguments. But since most of the arguments to PolyML.compiler have sensible defaults I'm wondering whether it would be better to change the type of PolyML.compiler to use something like the threadAttribute settings in Thread.Thread.fork. PolyML.compiler would have type: (unit->char option) * compilerArgument list -> unit -> unit so the only compulsory argument would be the input stream and the others could be given in the list or left to default.
compilerArgument would be defined as datatype compilerArgument = PutString of string -> unit (* Default is TextIO.print *) | FileName of string (* Default is empty string i.e. interactive *) | LineNumber of unit->int (* Default is no line numbering *) | NameSpace of nameSpace (* Default is PolyML.globalNameSpace *) | Debugger of nameSpace->unit (* Default is no debugging. *) | PrintDepth of int ref (* Reference to use for print depth: default PolyML.print_depth *) | various other compiler options. This would make it fairly easy to add additional options without affecting existing code and make the compiler as close to purely functional as possible.
David.