Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Wed, 11 May 94 19:10:25 EDT
From: reetz <reetz@ira.uka.de>
To: info-hol@cs.uidaho.edu
Subject: RE: does there exists a hol-lex?
Message-Id: <"i80fs2.ira.797:11.04.94.17.10.28"@ira.uka.de>

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.

>? Isn't the way to do this to define a set of (mutually) recursive
>types to handle 2 and then use an mlyacc grammar to generate 3).

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.

>I don't think this is a very sensible thing to do! It will take a vast amount
>of code and be very slow.

I'm not sure about that. Nobody has tried. Functional parsing is currently
a hot topic in the ``theoretical corner''. And beside that, if proving for
VHDL needs quite a lot of time, a not-so-fast parser won't make things
much worse. Especially if there's no decision procedure, the time needed
by the human prover is probably the biggest problem here. So,
terms, which are better to read, might help.