Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
To: reetz <reetz@ira.uka.de>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: better error messages in hol90?
In-Reply-To: Your message of "Fri, 03 Nov 1995 12:57:59 +0100." <"iraun1.ira.572:03.11.95.11.58.28"@ira.uka.de>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Mon, 20 Nov 1995 16:34:25 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:242190:951120163440"@cl.cam.ac.uk>


Ralf writes:

> I would like to propose that error messages in hol90 include the term, which
> causes the error. Why? Consider the following situtation: you write a
> function "f",  which, applied to some parameter "p", produces a LARGE term
> and unfortunately, there's a bug in "f" like e.g.
> 
> (f g;()) handle e print_HOL_ERR e;
> 
> Exception raised at Term.list_mk_comb:
> incompatible types
> val it = () : unit

It is certainly reasonable to ask for better exception reporting
from hol90.  Konrad, Richard, myself and a few others have had
discussions about exceptions before, and these suggestions came up:
	- add a delayed evaluation field to HOL_ERR (like Rob suggested)
	- add a field which stores an exception value, so the
whole heirarchy of exceptions is returned and they can be 
unravalled one by one.  This is my preference.

To demonstrate how the second could work if we could ignore
compatibility issues:
	exception WRAPPED_ERR = (string * exn)
	fun WRAP_ERR (f,e) = raise WRAPPED_ERR (f,e)

used as follows:
	fun my_function a b =
           ...
           list_mk_comb(...)
           ...
           handle e => WRAP_ERR("my_function",e);

The product of a failure deep in the code would be an exception
of kind WRAPPED_ERR, which contains another exception of kind
WRAPPED_ERR, and so on all the way down to the "real" error,
of any kind. Note WRAP_ERR would be only used 
for "unexpected" errors.

To unwrap the exception stack, you just rais ethe exception,
handling the special case where the exception is a WRAP_ERR
by raising the exception it contains, and printing out
information on the way.  See below for an example.

The problem then is that NJSML doesn't print out top level exceptions,
(which is hopeless, but we have to live with it).  It would
be fairly easy to modify the SMLNJ system slightly so that it could
print certain exceptions like WRAPPED_ERR and HOL_ERR. 
In fact I think I will put a modified version of SMLNJ suitable
for using with HOL up for ftp sooner or later.  I had a look
at this problem a while ago, and decided it would only need a one
line change to get HOL_ERR's displayed.  It's really quite ridiculous
that the user can't see the contents of an exception!

In the short term, it is possible that HOL_ERR will have an "exception"
value field added.  See the code below for how this could
be done without too much pain - the exception could be renamed
HOL_EXN and a compatibility function HOL_ERR could be supported
which produces a HOL_EXN.  This can be made fairly backward compatible,
but not completely.  The only non-compatible case
would be if people had code of the form
       ...
	handle HOL_ERR (origin_structure,origin_function,message} => ...

which could be changed to:
       ...
	handle HOL_EXN (origin_structure,origin_function,message,exn} => ...

But there shouldn't be much of this sort of code around - 
why would anyone want to handle a HOL_ERR 
explicitly, instead of using Raise?? I'm interested in 
knowing how bad this compatibility problem would be.


Cheers,
Don Syme


---------------------------------------------------------------------------
Example code:

exception HOL_EXN of {
       structure:string,
       function:string,
       message:string,
       exn:exn option
}

fun ERR str (func,mesg) =
    raise HOL_EXN {
        structure=str,
        function=func,
        message=mesg,
        exn=NONE 
    }

fun WRAP_ERR str (func,exn) =
    raise HOL_EXN {
        structure=str,
        function=func,
        message="",
        exn=SOME exn
    }

fun print_exn (HOL_EXN {origin_structure,origin_function,message,exn}) = 
     (say structure; say "."; 
      say function; say " - "; 
      say message;
      case exn of
         NONE => ()
       | SOME exn => print_exn exn);

 | print_exn (Fail s) = say s
 | print_exn (Io s) = say ("Io error: "^s)
    etc.
 | print_exn _ = say ("Unknown exception");

fun Raise e = (say "Exception raised: "; print_exn e; raise e)


(* HOL_ERR for compatibility *)

val print_HOL_ERR = print_exn;
fun HOL_ERR {origin_structure,origin_function,message} =
    HOL_EXN {
       structure=origin_structure,
       function=origin_function,
       message=message,
       exn = NONE
    }