Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: chou@cs.ucla.edu
Cc: info-hol@ted.cs.uidaho.edu, Paul.Curzon@cl.cam.ac.uk
Subject: Re: HOL90 is faster, for me
In-Reply-To: Your message of "Tue, 22 Jun 93 21:34:45 PDT." <9306230434.AA17035@maui.cs.ucla.edu>
Date: Wed, 23 Jun 93 10:48:53 +0100
From: Paul Curzon <Paul.Curzon@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:023600:930623094906"@cl.cam.ac.uk>

>Now that we are on the subject of HOL90, has anyone translated `res_quan`
>and `more_lists` to HOL90?  And in general, how hard is it to translate
>HOL88 libraries to HOL90?  Note that `res_quan` consists predominantly
>of ML procedures, while `more_lists` is mostly theorems and proofs.
>How hard would the translation be in each case?  Is there an automatic
>procedure for doing the translation?  It seems plausible to me that we
>can have a program that can automatically translate "Classic ML" into
>Standard ML.  Or perhaps I'm just dreaming?
>
>- Ching Tsun


I have just translated to HOL90 the more_arithmetic, more_lists and
res_quan (including conditional rewriting as a separate library)
libraries, and also Wai Wong's new word library. I haven't tested
everything yet so there may be bugs, but if anyone wants them I can
make them available. res_quan (and so words) require restricted quantifiers
to be in the main system. They arent in v. 90.5, so Konrad added them
to v. 90.6 for me (which may not be officially released yet?).
 
I used a mixture of automatic and hand translation. The automatic
parts were done with an extended version of Kondrads emacs
ml-to-sml function. I then went over them by hand. Much of the hand
translation was very routine but depended on local context. It took me a
couple of weeks to do all the above.  The proofs took longer, mainly
due to the fact that theorems don't autoload, so I had to keep
finding which theories theorems I had long taken for
granted were in. Also there were lots of theorems to translate, and
I did it first so I had to get used to SML.
The lists library translation was also slow because I removed
the dependancies on the auxiliary library (so a few theorems are
missing and I redid the proofs of lots more). The procedures were
generally quicker. However, there may still be bugs! The main thing 
that I didn't do automatically that was time consuming was the
conversion of things that in HOL88 return pairs but in HOL90 return
records (eg dest_comb) so I had to find out the names of the record
fields and which corresponded to the first and which the second
element of the HOL88 pair. HOL90 usually but not always prints the
type the other way round which was confusing at times:
- dest_comb;
val it = fn : term -> {Rand:term, Rator:term}
Procedures that used the more esoteric Classic ML control
structures were also occasionally a problem.

Paul Curzon.
(pc@cl.cam.ac.uk)