Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 11 May 1994 13:54:07 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA17842;
          Wed, 11 May 1994 06:37:56 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from irafs1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA17838;
          Wed, 11 May 1994 06:37:27 -0600
Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP);
          Wed, 11 May 1994 14:23:23 +0200
Received: from ira.uka.de by i80fs2.ira.uka.de id <24784-0@i80fs2.ira.uka.de>;
          Wed, 11 May 1994 14:29:22 +0200
Date: Wed, 11 May 94 14:29:21 EDT
From: reetz <reetz@ira.uka.de>
To: David <des@inmos.co.uk>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: does there exists a hol-lex?
Message-Id: <"i80fs2.ira.786:11.04.94.12.29.26"@ira.uka.de>

Using lexgen/mlyacc seems be a good idea. 
However, I would like to note to things:

1) lexgen/mlyacc
won't work well for a set of states large than
255, because then, it switches to integer arrays
to represent them and there is a known bug with
integer arrays, which causes SML/NJ to increase
memory to 100MB or even more. So, for large grammars
lexgen/mlyacc won't work very well up to now.

2) Another application I additionally had in mind
is making logic terms more readable. I would like
to call in ones mind the discussion about overloading
constants a few weeks ago. Or, e.g. think of expressions of
VHDL. One might like to read a term like e.g.

--`
"(BOOLEAN'POS (['0','1','1'] and ['1','0','1'])) * (-6)"
`--

instead of something like

--`
TRANSLATOR
(BOOLEAN_POS ((WORD [F,T,T]) bit_vector_and (WORD[T,F,T])) plus (neg(INT 6)))
`--

(I'm sorry if there's any mistake here ;)