Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Wed, 9 Dec 1992 11:11:37 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13910; Wed, 9 Dec 92 01:41:08 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13905; Wed, 9 Dec 92 01:40:30 -0800 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Wed, 9 Dec 1992 09:38:42 +0000 To: chou@edu.ucla.cs (Ching-Tsun Chou) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: **** RELEASE OF HOL 2.01 **** In-Reply-To: Your message of Tue, 08 Dec 92 16:35:39 -0800. <9212090035.AA12293@maui.cs.ucla.edu> Date: Wed, 09 Dec 92 09:38:36 +0000 From: Richard Boulton Message-Id: <"nene.cl.ca.809:09.12.92.09.38.44"@cl.cam.ac.uk> Ching Tsun writes: > o Renaming of REWRITE_CONV to REWR_CONV (see below); there is an entry > "newrw" in "contrib" to update code with respect to this change. > > What is the rationale behind this change? This may not be the whole story, but this is how I see it: Prior to Version 2.01, HOL featured (amongst others) three functions to do with rewriting: REWRITE_CONV REWRITE_TAC REWRITE_RULE REWRITE_CONV took a single theorem and tried to apply it at the top-level of the term *only*; it would fail if the theorem was not an applicable rewrite. REWRITE_TAC and REWRITE_RULE, on the other hand, did a TOP_DEPTH_CONV on the goal or theorem (respectively), that is to say they tried to apply the rewrite rule (theorem) at all levels, and repeatedly. They also took a list of theorems, used the list of basic rewrites, and would not fail due to inapplicability of the rewrites. It is probably fair to say that most users encounter REWRITE_TAC first. It is therefore reasonable for them to expect REWRITE_CONV to take a list of theorems and do a top-depth conversion, as REWRITE_TAC and REWRITE_RULE do. In Version 2.01 this is the case, but unfortunately in order to do this the old REWRITE_CONV has had to be renamed REWR_CONV. Obviously this will be the source of some irritation, but I think you'll find it is easy to change your source files by a global replacement of `REWRITE_CONV' with `REWR_CONV'. To make it really easy a utility has been provided in contrib. I see several advantages to the change: o New users are presented with a more uniform naming scheme. o A top-depth rewriting conversion that uses the basic rewrites is now available, built-in. o It is now sensible to have a family of depth rewriting conversions, just as there are tactics, e.g. ONCE_REWRITE_CONV. o The primitive rewriting function now has a shorter name which is convenient when writing complicated conversions because one tends to get less line breaks. Just my biased view. Richard.