Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sat, 11 Jun 1994 17:35:42 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA09808;
          Sat, 11 Jun 1994 10:32:35 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA09804;
          Sat, 11 Jun 1994 10:32:33 -0600
Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA02734;
          Sat, 11 Jun 1994 10:33:02 -0600
Message-Id: <9406111633.AA02734@jaguar.cs.byu.edu>
To: reetz <reetz@ira.uka.de>
Cc: hol2000@leopard.cs.byu.edu
Subject: Re: pretty printing versus mk_const
In-Reply-To: Your message of Sat, 11 Jun 1994 14:33:32 -0400. <"i80fs2.ira.089:11.05.94.12.33.38"@ira.uka.de>
Date: Sat, 11 Jun 1994 10:33:01 -0600
From: Phil Windley <windley@lal.cs.byu.edu>


On Sat, 11 Jun 94 14:33:32 EDT reetz writes
+--------------------
| Consider the values of type ==`:num`== and type ==`:string`==,
| --`5`-- or --`"blabla"`--. As far as I know, these are represented
| WITHIN the logic as a constant, which itself is contructed by mk_thm. 
| What are the reasons for it? As I see it:

I should point out, that Ralf brought up this same topic on info-hol about
a year ago and we had some pretty good discussion on it.  Look on the
<A HREF="http://lal.cs.byu.edu/cgi-bin/info-hol_search">info-hol search</A>
with the PERL expression "numerals.by.pretty" to see the discussion.  

This seems like a good topic for HOL2000.

As I understand it, the summary of the discussion is:

a.) HOL now does *not* convert a constant such as 5 to the unary
representation via the pretty printer.  The conversion num_CONV does this
using mk_thm.

b.) HOL *could* use the pretty printer to convert a constant to an internal
representation based on lists.

The advantage of the latter is that one can easily make the mechanism
flexible enough to handle base n numbers.  The same general mechanism, as
Ralf points out, can be used for strings.

Of course, the way HOL does it now hasn't stopped people from adding new
constants.  Perhaps Tim Leonard could explain how he did hex constants?

--phil--

Phillip J. Windley, Asst. Professor              |  windley@cs.byu.edu
Laboratory for Applied Logic	                 |  
Dept. of Computer Science, TMCB 3370             |
Brigham Young University                         |  Phone: 801.378.3722
Provo UT                  84602-6576             |  Fax:   801.378.7775
------------------------------------------------------------------------
If you use WWW, I'm <A HREF="http://lal.cs.byu.edu/people/windley/windley.html">here</A>.