[Gcl-devel] proclaim error

[dagreve]

Camm,

  Just wanted to report the following GCL bug.
I am running gcl-2.6.1 on linux and Matt reports
that it is also an issue for gcl-2.5.0 on SunOS 5.9.

The form:

(proclaim
 '(ftype (function
               ((satisfies integerp))
               t)
              foo))Thanks,

results in the error:

Error: (satisfies integerp) is not of type STRING.

 BTW: is 2.6.1 considered the most recent stable
release of gcl?

Thanks,
Dave



Dave --

Would you (1) execute this in your GCL, and if it fails, then (2) send a
bug
report to address@hidden with CC to me and to address@hidden  You
can
add that this also fails on GCL 2.5.0 running on SunOS 5.9.

(proclaim
 '(ftype (function
               ((satisfies integerp))
               t)
              foo))

Thanks --
-- Matt
   From: <address@hidden>
   Date: Thu, 18 Sep 2003 15:57:25 -0500
   X-MIMETrack: Serialize by Router on
CollinsCRSMTP02/CedarRapids/RockwellCollins(Release
    5.0.10 |March 22, 2002) at 09/18/2003 03:57:25 PM
   Content-type: text/plain; charset="us-ascii"


   Matt,

     The following simple function definition results
   in a certify-book crash.  The extended :bt below
   seems to point to a GCL bug.

   Dave


   (in-package "ACL2")

   (defun remove-list (list target)
     (declare (type (satisfies eqlable-listp) list target))
     (if (consp list)
              (remove-list (cdr list) (remove (car list) target))
       target))

   Form:  ( DEFUN REMOVE-LIST ...)
   Rules: ((:COMPOUND-RECOGNIZER EQLABLEP-RECOG)
                (:DEFINITION ENDP)
                (:DEFINITION EQL)
                (:DEFINITION EQLABLE-LISTP)
                (:DEFINITION NOT)
                (:DEFINITION REMOVE)
                (:ELIM CAR-CDR-ELIM)
                (:EXECUTABLE-COUNTERPART CONSP)
                (:EXECUTABLE-COUNTERPART EQLABLE-LISTP)
                (:FAKE-RUNE-FOR-TYPE-SET NIL)
                (:FORWARD-CHAINING ATOM-LISTP-FORWARD-TO-TRUE-LISTP)
                (:FORWARD-CHAINING EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP)
                (:REWRITE CAR-CONS)
                (:REWRITE CDR-CONS)
                (:TYPE-PRESCRIPTION ATOM-LISTP)
                (:TYPE-PRESCRIPTION EQLABLE-LISTP)
                (:TYPE-PRESCRIPTION REMOVE))
   Warnings:  None
   Time:  0.07 seconds (prove: 0.04, print: 0.02, other: 0.01)
   REMOVE-LIST

   * Step 3:  That completes the admissibility check.  Each form read
   was an embedded event form and was admissible. We now retract back
   to the initial world and try to include the book.  This may expose
   local incompatibilities.

   Error: (SATISFIES EQLABLE-LISTP) is not of type STRING.
   Error signalled by SYSTEM::KNOWN-TYPE-P.
   Broken at COND.  Type :H for Help.
   ACL2>>:bt

   #0   KNOWN-TYPE-P {loc0=((satisfies eqlable-listp)),loc1=(satisfies
   eqlable-listp)} [ihs=26]
   #1   SUBTYPEP {loc0=(satisfies eqlable-listp),loc1=fixnum,loc2
=(satisfies
   eqlable-listp),loc3=...} [ihs=25]
   #2   TYPE-FILTER {loc0=(satisfies eqlable-listp)} [ihs=24]
   #3   FUNCTION-ARG-TYPES {loc0=(#0=(satisfies eqlable-listp)
#0#),loc1=nil}
   [ihs=23]
   #4   ADD-FUNCTION-PROCLAMATION {loc0=remove-list,loc1=((#0=(satisfies
   eqlable-listp) #0#) nil),loc2=(remove-lis...} [ihs=22]
   #5   PROCLAIM {loc0=(ftype (function (#0=# #0#) nil) remove-list),loc1
=(#0
   =(satisfies eqlable-...} [ihs=21]
   #6   PROCLAIM-FORM {form=nil,g1387=nil,x=nil,loc3=#<compiled-function
   proclaim>} [ihs=20]
   #7   PROCLAIM-FILE {name
   ="/accts/dagreve/CVS/linux/proofs/symbols/simple.lisp",file=#<input
stream
   ...} [ihs=19]
   #8   INCLUDE-BOOK-FN {state
   ="simple",state-global-let*-cleanup-lst=acl2_invisible::|The Live State
   It...} [ihs=18]
   #9   CERTIFY-BOOK-FN {state

="simple",state-global-let*-cleanup-lst=0,g12590=t,state-global-let*-clean...}


   [ihs=17]
   #10   CERTIFY-BOOK-FN {} [ihs=16]
   #11   RAW-EV-FNCALL {w=certify-book-fn,*1*fn=("simple" 0 t
...),applied-fn
   =((state . acl2_invisible:...} [ihs=15]
   #12   EV-FNCALL {x=certify-book-fn,y=("simple" 0 t
...),w=acl2_invisible::
   |The Live State Itself...} [ihs=14]
   #13   EV {loc0=(certify-book-fn (quote "simple") (quote 0) ...),loc1
   =((state . acl2_invis...} [ihs=13]
   #14   TRANS-EVAL {loc0=(certify-book "simple"
   0),loc1=top-level,loc2=acl2_invisible::|The Live St...} [ihs=12]
   #15   LD-READ-EVAL-PRINT {state=acl2_invisible::|The Live State
   Itself|,revert-world-on-error-temp=(acl2_...} [ihs=11]
   #16   LD-LOOP {loc0=acl2_invisible::|The Live State Itself|} [ihs=10]
   #17   LD-FN-BODY

{loc0=acl2-input-channel::standard-object-input-0,loc1=nil,loc2=acl2_invisible::...}


   [ihs=9]
   #18   LD-FN {alist=((standard-oi .
   acl2-input-channel::standard-object-input-0) (standard-co...} [ihs=8]
   #19   LP {args=nil,cb1=#<compiled-function 09b13b20>,cfb1=(lp),cb2
   =(lp),cfb2=#\),loc5=#<"...} [ihs=7]
   #20   EVAL {loc0=nil,loc1=nil,loc2=nil,loc3=#<compiled-function lp>}
   [ihs=6]
   #21   TOP-LEVEL
   {loc0=nil,loc1=0,loc2=0,loc3=nil,loc4=nil,loc5=nil,loc6=nil,loc7
="Licensed
   under...} [ihs=5]
   #22   FUNCALL {loc0=#<compiled-function system:top-level>} [ihs=4]
   ACL2>>