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; Fri, 27 Jan 1995 18:53:00 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA03787;
          Fri, 27 Jan 1995 11:26:27 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from bobcat.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA03780;
          Fri, 27 Jan 1995 11:26:26 -0700
Received: from localhost by bobcat.cs.byu.edu (1.38.193.4/CS-Client) id AA11023;
          Fri, 27 Jan 1995 11:26:44 -0700
Message-Id: <9501271826.AA11023@bobcat.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: bug in let_CONV ????
Date: Fri, 27 Jan 1995 11:26:43 -0700
From: Phil Windley <windley@lal.cs.byu.edu>


I'm using HOL88 2.02 compiled with AKCL 1.609.  I had originally thought
this was a HOL bug, then thought it was an AKCL/GCL bug and have not gone
full circle to believe it is a HOL bug.  

I'm attaching a small example that produces the error.
The error message is  

    Error: The function NIL is undefined.
    Fast links are on: do (use-fast-links nil) for debugging
    Error signalled by FUN%297%102.
    Backtrace:  > funcall > lambda > cons > FUN%297%102
    evaluation failed     lisp error

I get this the first time I run the last expressions (let EXPANDED_M_RULES
= map (CONV_RULE (DEPTH_CONV let_CONV))...), but if you keep trying,
eventually it works.

Can someone verify that they get this same behavior.  What LISP are you
using?  Do you get the same behavior with something beside AKCL?  

--phil--

unlink `test.th`;;

new_theory `test`;;

let M_LDI = new_definition
   (`M_LDI`,
    "M_LDI s = 
        let reg     = FST s and
            pc      = (FST o SND) s and
            nextpc  = (FST o SND o SND) s and
            nextnextpc  = (FST o SND o SND o SND) s and
            imem     = (FST o SND o SND o SND o SND) s and
            dmem     = (SND o SND o SND o SND o SND)  s in
        let a = reg + pc and
	    i = imem + 2 in
        let result = a - i in
        let new_reg = a and
            new_pc = nextpc and
            new_nextpc = nextnextpc and
            new_nextnextpc = pc + 1 in
        let new_dmem = dmem + 3 in
	(new_reg, new_pc, new_nextpc, new_nextnextpc, imem, new_dmem)"
   );;




let EXPANDED_M_RULES = map (CONV_RULE (DEPTH_CONV let_CONV))
    [M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
     M_LDI;
   ];;