Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Wed, 8 Jul 92 02:52:40 MDT
From: slind@ca.ucalgary.cpsc (Konrad Slind)
Message-Id: <9207080852.AA01690@fsa.cpsc.ucalgary.ca>
To: info-hol@edu.uidaho.cs.ted

Sree re-raises the question of the re-use of constant names. As Phil
points out, this can be regarded as a parsing problem. As such, and as
noted by John Harrison in the previous incarnation of this discussion,
the question of how this affects type inference needs to be addressed.

In one approach, the idea is that a constant name "x" is really an
abbreviation for a constant name "th.x", where "th" is the name of the
theory where "x" is defined. An implementation will need to maintain at
least the following information for a constant:

    Name : string
    Definings : {Theory : string, Ty : hol_type} list

where Definings gives the theory and the most general type for each
definition of a constant with the given name. Then we require that the
type inference algorithm insist that the context constrain any
occurrence of the constant to be an instance of exactly one of the
constants denoted by Definings. If this is satisfied, then the constant
will get made, with its name being the concatenation of the theory name,
a dot, and the constant name, e.g., "th.x". On being prettyprinted, only
"x" will get printed unless a flag has been set.

It would be an error to attempt to define a constant with an
already-existing name and a type that is unifiable with a Ty in
Definings. Otherwise parsing could not uniquely assign a theory to the
name.

(Note that "mk_const" and "dest_const" will retain their old types.
However, just as in type inference, the type passed to "mk_const" must
be an instance of only one of the set of most general types of the
constant. This restriction on types could be lifted if the long
identifer, e.g., "th.x", were given.)

This is approximately the solution that SML has adopted for overloading
resolution, as explained on p. 54 of the Commentary on Standard ML.

I am planning on implementing this solution for hol90, but am eager to
hear of other alternatives. In the previous discussion, Tobias Nipkow
pointed out a more general solution that I think has been implemented
in Isabelle.

By the way, just to clarify a point of Sree's:

> In HOL-88, for security, a constant defined in a theory may not be 
> (re)defined in another theory, when both theories are loaded into 
> the same HOL environment irrespective of them being ancestors of each other.

You may define a constant c in theories A and B, if neither is an
ancestor of the other, but you can not make A and B both ancestors of
another theory. The proposed change would fix this.

Konrad.