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: <4457.9405111543@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 16:43:35 +0100 (BST)
Content-Type: text
Content-Length: 2507

reetz has said:
> Konrad writes:
> 
>     A. Write your own parser for all HOL terms, including your new
>        language.
>  
>     B. Write a parser for your new language, and somehow insert its
>        results into HOL terms.
> 
> Well, I don't want to use A., because what if HOL90.whateverversion
> changes its syntax, again? I'm afraid my own stuff won't be
> compatible. So, what about B in detail? Embedding an own language,
> one has to formally embed typechecking, too. So one can even
> reason about typechecking... So, polymorphy won't be a problem.
> I didn't understand what Konrad wrote about antiquotation.
> Can somebody give me further details? My idea was to represent
> sentences of the new language as a string in hol and define
> a parser as a hol constant, which maps strings into the semantics
> of the new language (or into an error, if e.g. typechecking fails).

I see! You want to write 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.

What Konrad means with antiquotation is that you would be able to
put in terms like (in the case of, say, a VHDL parser)

(--`VHDL_semantics ^(parse_vhdl"PROCESS BEGIN out <= inp; END PROCESS;")
    ==> ! t. out t = inp t`--);

where parse_vhdl is an SML function that parses a string into a term
representing VHDL programs in HOL.

> IMHO, in my point of view, most(?) people have formalised languages
> in HOL completly by hand. For small languages, that's just fine.
> But what about some sort of ``baroque'' languages? You get stuck in
> doing everything by hand. However, looking at compiler building,
> we might like to get tools, which are formalised within
> the logic (see typechecking above), which completly automate some stuff
> like syntax and which produces better-to-read results.

For a language you need

1) a grammar
2) a representation that you will parse to
3) a parser to take 1) into 2)

? 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).

I expect from a bare bones grammar you could probably generate
a good approximation of 2) along with production rules to generate
3).


--------------------------------------------------------------------------
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."