Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <27341.9306230929@frogland.inmos.co.uk>
Subject: Re: HOL90 is faster, for me
To: chou@cs.ucla.edu
Date: Wed, 23 Jun 1993 10:29:42 +0100 (BST)
Cc: info-hol@ted.cs.uidaho.edu
In-Reply-To: <9306230434.AA17035@maui.cs.ucla.edu> from "chou@cs.ucla.edu" at Jun 22, 93 09:34:45 pm
Content-Type: text
Content-Length: 1860

chou@cs.ucla.edu has said:
> 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.

On the whole its not too difficult to do a translation - a bit tedious
but there are few complications. Some of the "global" changes 
(e.g. ;; -> ; -  ` -> " - %...% -> (*...*) ) can be done via
replace(-regexp) in emacs. Things like proofs and theorems should
work directly as the tactics rules etc are (virtually) identical.

> 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?

I'm sure it could be done automatically, but its probably not worth
the effort (assuming the hol90 community co-ordinates translation work
then the effort can be shared a bit). Also, when moving to hol90/SML there 
are various bits and pieces that can be tidied up. Firstly, tying in
failures to to the standard hol90 exception (and thus providing more
useful error messages) then there's various places where hol88 code tends
to say

let f l = if l=[] then ....
          else let (l.t) = l in .....


where in SML you'd use pattern matching and have

fun f []     = ...
  | f (l::t) = ...


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley