Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <4627.9405111736@frogland.inmos.co.uk>
Subject: RE: does there exists a hol-lex?
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Wed, 11 May 1994 18:36:50 +0100 (BST)
Content-Type: text
Content-Length: 1903

reetz has said:
> David Shepherd has said:
> 
> >For a language you need
> >
> >1) a grammar
> >2) a representation that you will parse to
> >3) a parser to take 1) into 2) 
> 
> I completly agree on that. But 2) is
> the problem. A representation of VHDL in HOL
> is really hard to read. antiquotation doesn't
> solve that problem, as far as I can see. The 
> result of antiquotation is a term which is hard 
> to read.

If reading is the problem then what you need is a pretty printer.

I'm fairly certain that I talked to Konrad about this a few months
ago and he said that there is a hook into the hol term pretty printer.
In this way you just write a pretty printer for terms of type :vhdl
and add a function into this hook that calls this printer whenever
it meets something of that type

> Yes, you usually represent syntax in HOL by a set of (mutually
> recursive types. But what does that mean? You define the type
> of all parse trees, so you don't define the set of all
> sentences of the language, but the set of all parse trees of
> the sentences of the language (in fact, I have written a function
> which takes a context free grammar and maps it into the appropriate
> mutually recursive types automatically). So, you need to read parse trees
> and that's IMHO not fun. The sentences would be pretty much better 
> to read. But to get sentences as a representation, you need a parser
> *in* HOL.

nope, you need a parser and a pretty printer outside HOL to do the
interfacing for you.

If you don't like this approach then I assume you always write

--`$! \x. P x`-- 

instead of

--`! x. P x`--

:-)

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."