Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Wed, 21 Oct 1992 13:03:06 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17506; Wed, 21 Oct 92 04:47:08 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA17501; Wed, 21 Oct 92 04:46:57 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Wed, 21 Oct 1992 12:45:33 +0100 To: kimdam@dk.tfl (Kim Dam Petersen) Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: Error in variant -- Can anyone explain... In-Reply-To: Your message of Mon, 19 Oct 92 17:05:00 +0700. Date: Wed, 21 Oct 92 12:45:10 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.219:21.09.92.11.45.40"@cl.cam.ac.uk> kimdam> According to the Reference Manual kimdam> kimdam> variant : term list -> term -> term kimdam> kimdam> never fails. Nevertheless the simple application: kimdam> kimdam> variant ["T"] (mk_var(`x`,":num"));; kimdam> kimdam> yields the error message: kimdam> kimdam> evaluation failed VARIANT Sorry about that, but the REFERENCE entry for variant that was distributed with version 2.0 of the system is just wrong. The modified version 2.01 REFERENCE manual entry is attached. Note the updated failure conditions. It is, by the way, not in any case necessary include constants in the term list supplied to the variant function. A call to variant [list] "x" creates a variant of x which is distinct from all variables in [list], and *which has a name distinct from that of any (unhidden) constant*. Tom ============================================================================= variant : (term list -> term -> term) SYNOPSIS Modifies a variable name to avoid clashes. DESCRIPTION When applied to a list of variables to avoid clashing with, and a variable to modify, variant returns a variant of the variable to modify, that is, it changes the name as intuitively as possible to make it distinct from any variables in the list, or any (non-hidden) constants. This is normally done by adding primes to the name. The exact form of the variable name should not be relied on, except that the original variable will be returned unmodified unless it is itself in the list to avoid clashing with. FAILURE CONDITIONS variant l t fails if any term in the list l is not a variable or if t is neither a variable nor a constant. EXAMPLES The following shows a couple of typical cases: #variant ["y:bool"; "z:bool"] "x:bool";; "x" : term #variant ["x:bool"; "x':num"; "x'':num"] "x:bool";; "x'''" : term while the following shows that clashes with the names of constants are also avoided: #variant [] (mk_var(`T`,":bool"));; "T'" : term USES The function variant is extremely useful for complicated derived rules which need to rename variables to avoid free variable capture while still making the role of the variable obvious to the user. SEE ALSO genvar, hide_constant. () : void