Return-Path: 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 12:40:09 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA17623; Wed, 11 May 1994 05:25:22 -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 AA17619; Wed, 11 May 1994 05:25:08 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Wed, 11 May 1994 13:21:45 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <24488-0@i80fs2.ira.uka.de>; Wed, 11 May 1994 13:27:48 +0200 Date: Wed, 11 May 94 13:27:47 EDT From: reetz To: info-hol@leopard.cs.byu.edu Subject: does there exists a hol-lex? Message-Id: <"i80fs2.ira.490:11.04.94.11.27.50"@ira.uka.de> 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? Thanks for reply! (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research *) (* reetz@informatik.uni-karlsruhe.de society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)