Date: Thu, 28 Feb 91 17:01:15 GMT
From: John.Van-Tassel@uk.ac.cam.cl
Message-Id: <9102281701.AA05850@uk.ac.cam.cl.dipper>
To: cant@au.oz.dsto.itd, info-hol@edu.ucdavis.clover
Subject: Re: String to term conversion

Tony,

Sorry to have been a bit late in getting this answer to your query about a
string -> term converter out the door.  I'm following up to info-hol because
the answer might be of interest to the wider HOL community.

In the new release of the system (version 1.12 -- an announcement of
which should eminate from Sara Kalvala soon), there's a new library
called "parser".  It allows one to create recursive descent parsers
for use from within ML.  Included as one of the examples in the library
is a HOL term parser.  There is no antiquotation, but it seems to work 
on other stuff in the same fashion as the internal HOL term parser.

Here are some examples of it in action (Sun3 w/ Franz Lisp):

   #<< x /\ y >>;;
   "x /\ y" : term
   Run time: 0.1s
   
   #"x/\y";;
   "x /\ y" : term
   Run time: 0.0s
   
   #<< let a = \x,y.x+y and b = \w,z.w-z in (a,b) >>;;
   "let a (x,y) = x + y and b (w,z) = w - z in a,b" : term
   Run time: 0.6s
   
   #"let a = \x,y.x+y and b = \w,z.w-z in (a,b)";;
   "let a (x,y) = x + y and b (w,z) = w - z in a,b" : term
   Run time: 0.1s

The "<< >>" notation is also a new feature of the system.  In essence,
one may define special syntax blocks, and special delimiters for them.  
The ML parser then treats the text between these delimiters as a string to
be passed to a user-specified function.  So, in the above case, the
statement "new_syntax_block(`<<`,`>>`,`parse`);;" causes anything
between a << and a >> to be sent to the function "parse".  "parse" itself
is the hook into the generated parser for HOL terms.

This and other new tools (e.g. a pretty-printer generator) come with
Version 1.12.  Coming soon to an anonymous repository near you!


JVT

------------------------------------------------------------------------------
John Van Tassel			|  Tel: +44-223-334729
Univ. of Cambridge		|  Fax: +44-223-334678
Computer Laboratory		|  
Pembroke Street			|  Email: jvt@cl.cam.ac.uk
Cambridge CB2 3QG		|
England				|