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; Fri, 2 Jun 1995 20:10:38 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA267697412; Fri, 2 Jun 1995 12:23:32 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from cheetah.cs.byu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA267657409; Fri, 2 Jun 1995 12:23:30 -0600 From: Clark Barrett Received: by cheetah.cs.byu.edu (1.37.109.15/CS-Client) id AA241457356; Fri, 2 Jun 1995 12:22:36 -0600 Message-Id: <199506021822.AA241457356@cheetah.cs.byu.edu> Subject: Compiler bug To: info-hol@leopard.cs.byu.edu Date: Fri, 02 Jun 1995 12:22:36 MDT X-Mailer: Elm [revision: 109.14] Running HOL88 Version 2.02 on HP700 platform using ACL4.2: The parser library did not function correctly. After some experimentation, I produced the following code which demonstrates a bug in the compiler: % ===================================================================== % % preprocess_args: Go through the argument list putting together the % % various sequences of calls. % % ===================================================================== % letrec preprocess_args ch calls pops args file prdn gen_num prev call start pop_ctr t_par = if ch = `}` then ( failwith ch ) else failwith `not if`;; This code, when compiled, always fails with the input character instead of `not if`, regardless of what character is input. The key seems to be in having 12 or more parameters, as deleting one of the dummy parameters results in correct operation. Clark Barrett barrett@lal.cs.byu.edu