Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <19614.9406141435@frogland.inmos.co.uk>
Subject: Re: Improved error messages
To: Brian.Graham@cl.cam.ac.uk (Brian Graham)
Date: Tue, 14 Jun 1994 15:35:01 +0100 (BST)
Cc: hol2000@leopard.cs.byu.edu, leonard@ricks.enet.dec.com
In-Reply-To: <"swan.cl.cam.:149770:940614140705"@cl.cam.ac.uk> from "Brian Graham" at Jun 14, 94 03:06:48 pm
Content-Type: text
Content-Length: 2044

Brian Graham has said:
> When I was porting the conversions for the revised list theory
> from hol88 to hol90, I looked at the exception handling in 
> a few other places, and generally thought that it didn't provide
> much helpful information.  (Note: not yet released.)
> 
> I attempted to provide a trace in the exception by concatenating
> the origin function to the front of the message of the exception,
> so that as the exception gets passed from handler to handler you
> end up with a path of function names.  It may be primitive,
> but it seemed more helpful to give some indication of the origin
> of possibly obscure exceptions.
> 
> I think there should be a documented standard procedure for the
> handling of exceptions in HOL90, so that we might get a more 
> uniform treatment in the system.  Perhaps Konrad could tell us
> what scheme he used to organize exception handling; there are
> significant differences in exception handling between classic 
> ml and sml, so I doubt it was a simple carryover of existing code.

I don't think you need to do this concatenating if you use the
following discipline (which I admit I don't).

1) use the Raise function in execeptions.sml instead of the primitive
raise in SML

2) put a final exception handler round all "significant" functions
which flag an exception inside that function.

i.e.

fun f x y z =
    ....
    ....
handle _ => Raise(HOL_ERR{origin_structure="<struct_name>",
                          origin_function="f",
                          message="internal exception traceback"})
;

Then any exception generated will firstly print out its message
at the point of generation and then succesively be handled by these
exception trace handlers all the way back up through the code.


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."