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
Cc: elsa@research.att.com (Elsa Gunter), jhr@research.att.com, 
    Richard.Boulton@cl.cam.ac.uk
Subject: Re: renaming things in core hol
Date: Tue, 09 May 1995 17:07:55 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:133230:950509160826"@cl.cam.ac.uk>

I responded to Elsa Gunter's recent message on info-hol about changes to the
pervasive environment of Standard ML by asking which implementations of SML
were actually going to go along with the changes and by further suggesting
that hol90 be made as portable as possible across different SML
implementations. Elsa's response can be found below. It addresses my concerns
satisfactorily. The only question remaining is what position the implementors
of PolyML are taking. If anyone from Abstract Hardware Ltd reads this,
perhaps they could comment?

Richard Boulton.


------- Forwarded Message

Date: Tue, 9 May 95 11:07 EDT
From: elsa@research.att.com (Elsa Gunter)
To: Richard.Boulton@cl.cam.ac.uk
In-reply-to: <"swan.cl.cam.:286910:950509090321"@cl.cam.ac.uk> (message from Richard Boulton on Tue, 09 May 1995 10:02:53 +0100)
Subject: Re: renaming things in core hol

Dear Richard,
  If you find it acceptable, would you please forward this message to
info-hol.  Since I am quoting a private message you sent me I would
prefer you agreed to it's being posted before it gets sent.

  In response to your reply to my recent message to info-hol:

> Are the implementors/supporters of PolyML and MoscowSML going along with this
> extension? I think the move to having a separate type of characters is a good
> one but only if it is universal. I do not want to see hol90 become even more
tied in to SML/NJ than it already is, but rather the converse. It is in the
interest of the HOL community to have as wide a choice as possible of SML's.

I'm not sure about PolyML, but certianly MoscowML is, and the group at
Edinburgh is. I think there is at least one other implementor (other
than PolyML) that is as well.  MoscowML is also changing to
accommodate our quotation/antiquotation mechanism.  Peter Sestoft, who
is an implementor of MoscowML, is visting here at Bell Labs, and is
quite keen to have hol90 running under MoscowML.  The only thing
preventing it at this moment is the fact that MoscowML does not
support functors or substructures in the module system (and they
don't yet support a mechanism for installing pretty-printers).  Hol90
uses the full module system of Standard ML, and it would be painful
(although not impossible) to flatten everying.
  As for your comment about strings versus characters, and your
comment:

> To be a bit more constructive: perhaps effort would better be spent making
> the code of hol90 more portable than making changes to fit in with new SML
> developments. 
I said:
>> I am also creating a
>> compatability module to try to ease the process of upgrading, but it
>> is biased toward encouraging the use of the new system features.

I have factored all of the system dependencies through a single
structure Sml_system.  (This is not quite accurate.  I don't factor
the infix :: for lists or any of the operations on numbers or the
special syntax for strings ("") or the special syntax for frag lists
(``, the way we get quotation/antiquotation)).  To port hol90 to
another SML only requires that the version of SML support
quotation/antiquotation and be able to give some implementation of the
structure Sml_system.  In particular, for those systems with have only
strings, I already have in implementation that does the job.  It
enables one to build the system under the old SML-NJ version 0.93.
You just make both the type of characters and the type string be the
same type.  It is further my hope that my factoring could be of use to
others wishing to write code portable across multiple implementations.

> Perhaps quotations could be
> included in the proposed new pervasive environment? Or has this already been
> done? 

I belive it is not being included in the new standard basis, but I
believe the main players have all doing it anyway.  I will suggest it.

There is also the less important point of providing support for the
automatic pretty-printing of user defined types by the system
top-lever.  I will ask whether it has been considered whether to
include such a capability in the basis or not.  I'm pretty sure they
have not.  This is less important, however, for thue user can apply
there own printing function.  Still, it's nice to have.

If you are interested in seeing what the new basis will look like, the
is a (still changing) draft of a manual describing it, which I could
send you.
				---Elsa

------- End of Forwarded Message