From mboxrd@z Thu Jan 1 00:00:00 1970 Received: by pauillac.inria.fr; Mon, 30 May 94 18:56:30 +0200 Received: from margaux.inria.fr by pauillac.inria.fr; Mon, 30 May 94 16:50:08 +0200 Received: from concorde.inria.fr by margaux.inria.fr, Mon, 30 May 1994 16:50:07 +0200 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by concorde.inria.fr (8.6.9/8.6.9) with ESMTP id QAA14025 for ; Mon, 30 May 1994 16:50:05 +0200 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 30 May 1994 15:49:52 +0100 To: caml-list@margaux.inria.fr Cc: John.Harrison@cl.cam.ac.uk Subject: Re: Irrelevant variables in patterns In-Reply-To: Your message of "Sat, 28 May 94 12:43:29 +0200." <29438.770121809@pauillac.inria.fr> Date: Mon, 30 May 94 15:49:46 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:029090:940530144959"@cl.cam.ac.uk> Sender: weis@pauillac.inria.fr Chet writes: | Exceptions in ML are a programming mechanism. They are not used | anymore for exceptional conditions. We need a new mechanism for that. In the HOL theorem prover we use exceptions to indicate that certain inference rules are inapplicable. It's quite common for code to trap failures at certain subterms and conclude "we have rewritten this subterm as much as possible, so return it". In the present code (including hol90 in SML) most of the exceptions are caught completely indiscriminately, i.e. `_' not `HOL_ERR(_)'. This means there are situations where exceptional conditions just get driven over. Really the code should be rewritten, but as Chet remarks, there's something to be said for a separate signal mechanism. | Moreover, even if I _do_ write the code in handle_exceptions_generally | to treat Out_of_memory, etc, I get many warnings telling me that I am | catching the exception. Which raises another point. Is there a way to suppress the incredibly irritating (and I seem to recall not very accurate) "match not exhaustive" messages in CAML Light (in general expression matching as well as exceptions)? I find myself putting in redundant clauses to avoid them, which is hardly good style. It's especially pointless when the match is actually done at toplevel, e.g. let [x;y] = [1;2];; As Christophe says: | [...] Then what you really needs is a compiler | option to discard a particular warning (or class or warning) so you only get | the warnings which are relevant to you programming style. I agree completely. John.