Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 8 Sep 1993 19:25:47 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA23338; Wed, 8 Sep 93 11:19:53 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from tuminfo2.informatik.tu-muenchen.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA23334; Wed, 8 Sep 93 11:19:48 -0700 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57666>; Wed, 8 Sep 1993 20:19:41 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8081>; Wed, 8 Sep 1993 20:19:16 +0200 From: Konrad Slind To: info-hol@cs.uidaho.edu In-Reply-To: Manish's message of Wed, 8 Sep 1993 19:20:49 +0200 <9309081720.AA13573@domain_csci> Subject: Is there a HOL grammar available ? Message-Id: <93Sep8.201916met_dst.8081@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 8 Sep 1993 20:19:11 +0200 hol90 uses an ML-yacc grammar (and an ML-Lex lexer) to build its parsers. "hol_lex" and "hol_yak" are the relevant files; they can be found in src/0 of the hol90 distribution. More detailed information can be found in doc/parsing.doc. One should note that the language isn't fixed: new infix operators can be declared by the user. As a result, there is a post-parsing pass that uses the user-declared precedences of infixes to shuffle the abstract syntax trees into their final shape. This gives a type of "preterms". Then a side-effecting version of Milner's type inference algorithm is used to map preterms into real terms. The type of preterms is abstract, but functions exist to manipulate it in the structure "Parse_support". Unfortunately, these functions are not yet documented, nor is how to build the hol90 parser in the first place. Contact me if you want these sort of details. Konrad.