Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Subject: Preterms and term location specifications
In-Reply-To: Your message of "Sun, 09 Apr 1995 13:47:36 +0200." <95Apr9.134749met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Tue, 11 Apr 1995 19:38:46 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:292930:950411183854"@cl.cam.ac.uk>


I am wondering whether the internals of the preterm signature in hol90
should be publically available or not.  (It isn't at the moment.)

This problem arose when trying to use terms and/or preterms
as "term location" specifications.  For example:

"!_. _ /\ _ /\ P /\ _"
"!_. (_ = [P;_]) /\ _ /\ Q"

[Note "_" is allowed as a variable name in hol90.  A small
problem with the term lexical analyser actually means the above
won't pass syntax checking, but a term such as
	(--`_ /\ _ /\ P /\ _`--)
will.  The problem is with the !_.

Also note that the second would not type check as a term, as a tyoe
clash would occur on the variable "_".]

Here P and Q indicate terms on which to apply an operation.  For 
instance, such a location specifier could be used 
as an argument to a tactic

	type term_locator = Parse.Parse_support.Preterm.preterm
	PATH_CONV_TAC: conv -> term_locator -> tactic

They could also be used as window opening specifications in
the window inference library.

Using preterms for these seems suitable, as I don't care about type inference.
Another option would be to use lambdas, but there is no parse
support for these.  A third option, and perhaps the best, would
be to tweek the term type checker so that setting a flag
would let conflicting types be inferred for variables (or just
the variable _), and also assume polymorphic types for
all unconstrained type variables.   These would
still be type-correct terms, after all.  Then we could define
a new term parser, say "-|"
	-|`!_. _ /\ _ /\ P /\ _`|-

To be honest, such parser behaviour would be useful in other situations 
too.  I often want to know a general type for a polymorphic constant,
as in
	type_of (-|`$RES_FORALL`|-)

 
Don

-----------------------------------------------------------------------------
At the lab:							     At home:
The Computer Laboratory                                      c/o Trinity Hall
New Museums Site                                                      CB2 1TJ
University of Cambridge                                         Cambridge, UK
CB4 3BD
Cambridge, UK
-----------------------------------------------------------------------------