Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Cc: reetz@ira.uka.de
Subject: better error messages in hol90?
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Fri, 03 Nov 1995 12:57:59 +0100
From: reetz <reetz@ira.uka.de>
Message-Id: <"iraun1.ira.572:03.11.95.11.58.28"@ira.uka.de>

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

Now you have a complicated program code for f which dozens of list_mk_comb.
Try to find out WHERE the error happened - you only know WHAT kind of error
happened. For my on stuff, I found it very useful to write error messages,
which included the term like

raise HOL_ERROR
{origin_structure = "bla",
 origin_function  = "f",
 message          =
 "f fails because subterm "^(term_to_string t)^" is blablabla"};

However, there are a lot of situations where constructors/decontructors of
structure Term fail because you programed a bug. Thus this better sort
of error messages especially in structure Term would be nice to have (there
are other error messages of hol90, which could be better, too, of course).

Ralf


(*******************************************************************)
(*                                                                 *)
(*  Ralf Reetz                                                     *)
(*                                                                 *)
(*  University of Karlsruhe                                        *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany              *)
(*                                                                 *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html       *)
(*  fax:    +49 721 370455                                         *)
(*  tel:    +49 721 6084220                                        *)
(*                                                                 *)
(*******************************************************************)