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: <4104.9405111201@frogland.inmos.co.uk>
Subject: Re: does there exists a hol-lex?
To: reetz@ira.uka.de (reetz)
Date: Wed, 11 May 1994 13:01:54 +0100 (BST)
Cc: info-hol@leopard.cs.byu.edu
In-Reply-To: <"i80fs2.ira.490:11.04.94.11.27.50"@ira.uka.de> from "reetz" at May 11, 94 01:27:47 pm
Content-Type: text
Content-Length: 1448

reetz has said:
> I wonder about a lex for the logic hol,
> i.e. a sml-function, which takes something
> like a list of (regular expression,term:ty_token)
> for input/output and constructs a definition for an
> equivalent finite transductor, which maps a term 
> of type string into tokens formalised by an
> arbitrary type ty_token (normally an enumeration 
> of type constructors as defined by define_type).
> 
> Frankly, I don't want to rediscover the wheel ;-)
> So, did anybody program such function for 
> HOL90.{5,6} and is willing to share the code?

Assuming you have SMLofNJ, look in the tools directory
at the mlyacc and lexgen directories. These basically do what you
want.

I assume what you are wanting to do is to generate code that parses a
grammar into a HOL term. In which case lexgen/mlyacc will do the job. I
knocked together a parser for a (trivially) simple sequential  language
using VHDL-style syntax into an SML type in about a couple of days
starting from no knowledge of mlyacc. Assuming you already  have the
necessary hol type structure (just as I had to predefine the SML types)
then going into a HOL term would be much the same.


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