David,
I've also sent this to the mailing list in case any other users have comments.
If you write your own read-eval-print loop using PolyML.compiler, you may want to treat exceptions raised during the eval stage specially. However you can't currently stop Poly/ML printing out the exception. It seems appropriate to me to use negative values of the error depth control to do this.
I get the effect I want with the following patch:
--- mlsource/MLCompiler/COMPILER_BODY.ML- 2006-11-06 13:20:50.000000000 +0000 +++ mlsource/MLCompiler/COMPILER_BODY.ML 2008-02-12 13:22:56.000000000 +0000 @@ -641,14 +641,17 @@ val pstream = prettyPrint (77, lexPrint lex);
in - ppBeginBlock pstream (3, false); - ppAddString pstream "Exception-"; - ppBreak pstream (1, 0); - VALUEOPS.printStruct (exceptionData, - TYPETREE.exnType, ! errorDepth, pstream, printEnv); - ppBreak pstream (1, 0); - ppAddString pstream "raised"; - ppEndBlock pstream (); + if ! errorDepth >= 0 + then ( + ppBeginBlock pstream (3, false); + ppAddString pstream "Exception- "; + ppBreak pstream (1, 0); + VALUEOPS.printStruct (exceptionData, + TYPETREE.exnType, ! errorDepth, pstream, printEnv); + ppBreak pstream (1, 0); + ppAddString pstream "raised"; + ppEndBlock pstream () + ) else ();
(* print out timing info *) printTimes (parseTime,pass2Time,treeTime,codeTime,endRunTime)
I note that the error depth also influences syntax-checking and type-checking error messages, but I can't see why anyone would want to suppress those.
Regards,
Rob.
On Sun, 2 Mar 2008, Rob Arthan wrote:
If you write your own read-eval-print loop using PolyML.compiler, you may want to treat exceptions raised during the eval stage specially. However you can't currently stop Poly/ML printing out the exception.
In Isabelle we do have our own toplevel loop (for the Isar theory and proof language). ML is also embedded here, and passed down via PolyML.compiler. Exceptions are handled the regular way, and printed with General.exnMessage (more specific output for one of our key exceptions). We also managed to get PolyML.exception_trace, PolyML.profiling, and interrupt management through our toplevel.
If you are curious see Isabelle/src/Pure/ML-Systems/polyml.ML and Isabelle/src/Pure/Isar/toplevel.ML for the gory details.
Makarius
Rob Arthan wrote:
If you write your own read-eval-print loop using PolyML.compiler, you may want to treat exceptions raised during the eval stage specially. However you can't currently stop Poly/ML printing out the exception. It seems appropriate to me to use negative values of the error depth control to do this.
I note that the error depth also influences syntax-checking and type-checking error messages, but I can't see why anyone would want to suppress those.
Rob, Would it make sense to use print_depth rather than error_depth here and leave error_depth for compiler error messages? Then setting print_depth to zero could have the effect of suppressing the printing of exceptions in the same way that it suppresses the printing of top-level declarations. So print_depth applies to printing run-time values and error_depth to compile-time.
Actually, I think the code in COMPILER_BODY that prints out the exception information was written before General.exnMessage existed. From what I can tell it should be possible to remove that code and instead print the exception information in the Poly/ML read-eval-print loop. That would allow your own read-eval-print loop to do what it liked. Since the depth of any structure printed by General.exnMessage is affected by print_depth rather than error_depth if I made this change I would also use print_depth to suppress exception printing.
Regards, David
David,
On 4 Mar 2008, at 18:29, David Matthews wrote:
Rob Arthan wrote:
If you write your own read-eval-print loop using PolyML.compiler, you may want to treat exceptions raised during the eval stage specially. However you can't currently stop Poly/ML printing out the exception. It seems appropriate to me to use negative values of the error depth control to do this. I note that the error depth also influences syntax-checking and type-checking error messages, but I can't see why anyone would want to suppress those.
Rob, Would it make sense to use print_depth rather than error_depth here and leave error_depth for compiler error messages? Then setting print_depth to zero could have the effect of suppressing the printing of exceptions in the same way that it suppresses the printing of top-level declarations. So print_depth applies to printing run-time values and error_depth to compile-time.
No, that definitely wouldn't make sense for me. ProofPower wraps a pre- and post-processor around the ML read-eval-print loop, essentially to extend the lexis so that object language quotations become part of the language. Any ML value can be returned, so I need the compiler to pretty-print the value.
However, exceptions are different: I can print them myself and sometimes I just want to catch them and take special action. E.g., there is an exception to terminate my read-eval-print loop and return to the Poly/ML one - in that case it is slightly confusing to the user to see the exception message printed by the compiler.
Actually, I think the code in COMPILER_BODY that prints out the exception information was written before General.exnMessage existed. From what I can tell it should be possible to remove that code and instead print the exception information in the Poly/ML read-eval-print loop.
That would be a much better solution I think, since most users won't want to suppress exception messages altogether but may want to limit the amount of information in them. Your read-eval-print loop would also then provide a fully-featured prototype for anyone trying to write their own.
That would allow your own read-eval-print loop to do what it liked. Since the depth of any structure printed by General.exnMessage is affected by print_depth rather than error_depth if I made this change I would also use print_depth to suppress exception printing.
Regards,
Rob.
Rob Arthan wrote:
Actually, I think the code in COMPILER_BODY that prints out the exception information was written before General.exnMessage existed. From what I can tell it should be possible to remove that code and instead print the exception information in the Poly/ML read-eval-print loop.
That would be a much better solution I think, since most users won't want to suppress exception messages altogether but may want to limit the amount of information in them. Your read-eval-print loop would also then provide a fully-featured prototype for anyone trying to write their own.
Rob, I've spent a while this week reorganising the interface between the compiler and the read-eval-print loop. Up till now the read-eval-print loop has been compiled as part of the compiler. That has limited the extent to which it has been possible to replace the loop with your own version since many of the hooks weren't available. I've now changed it so that only a limited version of the loop is used when compiling the basis library and the final, fully featured, version is compiled in at the end. The new version is in basis/FinalPolyML.sml in the current CVS.
As part of this I've changed PolyML.compiler to include all the arguments it needs and removed PolyML.compilerEx. This is an incompatible change which will affect Isabelle. The new version of PolyML.compiler has type: {getChar: unit -> char option, fileName: string, nameSpace: PolyML.NameSpace.nameSpace, putString: string -> unit, lineNumber: unit -> int} -> unit -> unit
getChar is used for the input stream. Unlike the old PolyML.compiler this returns a char option rather than a string. NONE is used to signal end-of-file. putString is, as before, the output stream. fileName is the name of the file used in error message. The empty string indicates an interactive stream. lineNumber is used indicate the source line in an error message. Returning zero suppresses this. 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. PolyML.make works by interposing between the compiler and the global space. When a structure, functor or signature name is looked up it checks whether the entity is up-to-date and may recursively invoke the compiler before eventually returning the recompiled entity. It might be possible to use this for some form of quotation or anti-quotation.
This is still experimental but I think it's going in the right direction. I've produced updated versions of the import files for x86-32 and x86-64. I still need to do that for the other architectures.
Regards, David.
On Fri, 14 Mar 2008, David Matthews wrote:
I've spent a while this week reorganising the interface between the compiler and the read-eval-print loop. Up till now the read-eval-print loop has been compiled as part of the compiler. That has limited the extent to which it has been possible to replace the loop with your own version since many of the hooks weren't available. I've now changed it so that only a limited version of the loop is used when compiling the basis library and the final, fully featured, version is compiled in at the end. The new version is in basis/FinalPolyML.sml in the current CVS.
As part of this I've changed PolyML.compiler to include all the arguments it needs and removed PolyML.compilerEx. This is an incompatible change which will affect Isabelle.
We have now catched up with these changes. So far it works without any problems.
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.
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.
Makarius
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.
On Wed, 26 Mar 2008, David Matthews wrote:
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
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 "?".
Apart from the print functions the only other case where the global environment is used is the "debug" function. This is set using setDebugShell.
Maybe the above PolyML.printPretty with explicit name space argument will help a little bit for the particular problem of printing exceptions. But I also realize now that general print/makestring functionality is not fully addressed by this extra argument: the name space is not the actual environment value, only the record of access functions to an implicitly mutable table. So we need to manage the latter using ``setmp'' tricks anyway.
So a global configuration of the default name space, like PolyML.setPrintEnv but also for PolyML.compiler, could do the job. This is then a bit like configuring the global signal handler for the runtime system.
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.
This looks like a good idea independently of the above issues.
| FileName of string (* Default is empty string i.e. interactive *) | LineNumber of unit->int (* Default is no line numbering *)
How about just one argument to produce an error message, depending on the present line number, e.g. MakeError of int -> string -> string or PutError of int -> string -> unit. This would allow to wrap up the position information in a way that the user interface understands, cf. the uniform Position.str_of (with optional markup) that we are using in Isabelle. (That function would include the constant file name information by itself.)
Makarius
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
rda＠lemma-one.com