Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9411021735.AA26727@deneb.cs.cornell.edu>
To: Konrad Slind <slind@informatik.tu-muenchen.de>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: bhogan@bedlam: HOL90 on a PC
In-Reply-To: Your message of "Wed, 02 Nov 1994 13:02:25 +0100." <94Nov2.130228met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 02 Nov 1994 12:35:14 -0500
From: Chet Murthy <murthy@cs.cornell.edu>


Why not try to port it to caml-light?  I mean, caml-light will soon
have a functor-style module system, and it already has separate
compilation (so if you only instanciate functors a few times, you can
do it with cp/sed).  There is a *fantastic* package for writing
parsers and pretty-printers which is *small*.  And there's work in the
CAML group on syntactic extension in the style of the old CAML
toplevel -- much more powerful than anything else available.

In sum, functors are on the way (and even in their absence, you can do
a *lot* -- I know, since I did this for *many* modules), parsing and
pretty-printing is a beautifully-solved problem, and quotations are on
their way, too.

MoSML, sorry to say, would be a step backwards.  The equality test in
MoSML is coded in ML, rather than in C, so if you use equality a lot,
it gets *slow* (it was the only way to get SML's semantics for
ref-equality out of a caml-light bytecode machine).  Whatever.

There's no support for separate compilation, and I'm sure that a
million other things are still not working.  A better solution would
be a simple SML->CAML-light translator.  You could then translate
mechanically, fixup by hand where it was needed, and get running
pretty easily.

Again, I did this in both directions with lots of code, *by hand*, and
found that the two languages were almost identical for large bodies of
code.  People just don't take advantage of the left-to-right
evaluation order (the only place where caml-light differs -- its
right-to-left), and when they do, they usually are playing tricks, and
are more than willing to make the code more linear.  This happened in
the Constructions code corpus exactly *once*, and in the corpus of
Chan's decision procedure exactly *3* times.

I was never bitten by the fact that equality on refs in caml-light is
structural.

--chet--

>>>>> "KS" == Konrad Slind <slind@informatik.tu-muenchen.de> writes:

    KS> 1. Usage of the ML module system would have to be stripped
    KS> out.

    KS> 2. Parsers for types, terms, theories, and library
    KS> descriptions would have to be hand-written if the bulky
    KS> implementation of ML-Yacc was not desired.

    KS> 3. Automatic prettyprinting of types, terms, and theorems
    KS> ought to be available, but Moscow ML doesn't supply these
    KS> sorts of hooks (in the interest of purity).

    KS> 4. Support for quotations would be nice, although Moscow ML
    KS> doesn't supply them. Probably running it piped through a
    KS> filter that expands quotations out would suffice.


    KS> John Harrison has done some work in this vein, using
    KS> CAML-Light.