Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, shaw@cs.ucdavis.edu
In-Reply-To: <199601270030.QAA01217@roma-cafe.cs.ucdavis.edu> (shaw@cs.ucdavis.edu)
Subject: Re: Blank Pattern in HOL90 ?
Message-Id: <96Jan27.160640met.8179@sunbroy14.informatik.tu-muenchen.de>
Date: 	Sat, 27 Jan 1996 16:06:29 +0100


> What kind of ident is blank, that it is not allowed in a let VSTRUCT 
> binding but can serve as variable?

Underscore ("_") is a fully fledged symbolic identifier in HOL90, unlike
SML, in which it can only be a component of a pattern. I decided to omit
symbolic identifiers from binding constructs, because they would have to
be renameable to avoid variable capture in substitution. In retrospect,
renaming symbolics should be possible; in fact, probably the (internal)
distinction between symbolic and alphanumeric should just go away.

That aside, what you are really looking for is proper pattern-match
translation, ala ML compilers, and they work by replacing each
occurrence of "_" in a pattern by a fresh variable. This translation
doesn't yet exist in HOL. One can work around this manually, or by
adding an "underscore-to-fresh-variable" pass to the parser between the
preterm parsing and type inference stages. And a reverse translation for
pretty printing would be nice too, I suppose. Currently, this would
involve some hacking, but I hope that tools are becoming available that
will make it easier to modify the system in such ways.

By the way, having underscore available outside of patterns is useful,
too. I think Don Syme and Jim Grundy were looking at declaring a
constant

    _ : 'a

and using it to stand for "dont-care" parts of term skeletons, although
a translation of underscores to fresh variables might mesh better with
operations such as matching.

Konrad.