Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Wed, 5 Oct 1994 10:06:52 +0100
From: terra@diku.dk
Message-Id: <199410050906.AA17922@tyr.diku.dk>
To: info-hol@leopard.cs.byu.edu
Cc: terra@diku.dk
Subject: Release: Automatic Conversion Generating Tool for Hol-90


Hi!

As I promised a couple of you in Valetta I have made a black-box
tool for generating very efficient conversions.

It is available as ftp.diku.dk:/pub/diku/users/terra/convgen.sml
and contains both usage and copying instructions within.  If any
of you can think of a better place for it, feel free to put it
there.

So what is it?  Well, it is a program that takes a list of
equality theorems and produces a conversion that will rewrite
a term with respect to one of the theorems.  This is more or
less what GEN_REWRITE_CONV does, but when I said `produces a
conversion' above I should have said `produces SML-code for a
conversion' because the output is genuine, readable SML-code.
This difference, among other things, makes the conversions a
lot faster.  I have appended a sample session below.

I believe that the code works for any list of theorem; there
are no longer problems with non-linear patterns (like in
|- !x. (x=x)=T ) or polymorphism.

Without having done formal timings (but see my article in the
Supplementary HOL-94 proceedings) I can say that you should
expect conversions generated this way to be at least twice as
fast as the GEN_REWRITE_CONV-produced ones.

I am open to suggestions on improvements (dare I say bug fixes?)
if you have any.  Note that I am not on the info-hol mailing
list as I get way to much mail as it is.


Morten Welinder
terra@diku.dk

------------------------------------------------------------------------
For information on the free Republic of Macedonia, ftp to ftp.uts.edu.au
Australia and check out the /pub/MAKEDON directory.
------------------------------------------Morten Welinder, terra@diku.dk


---------------------------------------------------------------------------


          HHH                 LL
          HHH                  LL
          HHH                   LL
          HHH                    LL
          HHH          OOOO       LL
          HHHHHHH     OO  OO       LL
          HHHHHHH     OO  OO       LLL
          HHH          OOOO        LLLL
          HHH                     LL  LL
          HHH                    LL    LL
          HHH                   LL      LL
          HHH                  LL        LL90.6

Created on Mon Apr 11 10:48:36 METDST 1994
using: Standard ML of New Jersey, Version 0.93, February 15, 1993


The library "HOL" is loaded.
- use "convgen.sml";
[opening convgen.sml]
val conversion_generator = fn : string -> string -> (thm * string) list -> unit
val convgen = fn : (thm * string) list -> unit

Usage: conversion_generator file_name func_name [(thm,"thm"),...]
or     convgen [(thm,"thm"),...]

val it = () : unit
- val ADD = definition "arithmetic" "ADD";
val ADD = |- (!n. 0 + n = n) /\ (!m n. SUC m + n = SUC (m + n)) : thm
- val ADD1 = CONJUNCT1 ADD;
val ADD1 = |- !n. 0 + n = n : thm
- val ADD2 = CONJUNCT2 ADD;
val ADD2 = |- !m n. SUC m + n = SUC (m + n) : thm

- local
=   fun mk_add x y =
=     mk_comb {Rator = mk_comb {Rator = --`$+`--, Rand = x}, Rand = y};
= in
=   fun fib 0 = --`SUC 0`--
=     | fib 1 = --`SUC 0`--
=     | fib n = mk_add (fib (n-2)) (fib (n-1));
= end;

val fib = fn : int -> term

- convgen [(ADD1,"ADD1"),(ADD2,"ADD2")];
------------------------------------------------------------------------------
Hi, I'm the MW Conversion Generator version 0,10!

I will now generate a file called "temp.sml" containing the source code
for a rewriting conversion corresponding to the 2 theorems you gave me.
The name of the conversion will be "conv".

If you put conversions generated this way to any serious use, you should
mail Morten Welinder (terra@diku.dk) and tell him; that might cheer him up.
------------------------------------------------------------------------------
val it = () : unit
- use "temp.sml";
[opening temp.sml]
val save_System_Control_interp = true : bool
temp.sml:52.3-52.31 Warning: binding not exhaustive
          thm_2_1 :: nil = ...
val conv = fn : conv
val it = () : unit

- REDEPTH_CONV conv (fib 5);
val it =
  |- (SUC 0 + SUC 0 + SUC 0) + (SUC 0 + SUC 0) + SUC 0 + SUC 0 + SUC 0 =
     SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) : thm
-