Re: [Gcl-devel] proclaim error

[Camm Maguire]

Greetings!  A followup from my last note.  Stable versions 2.6.1-10 and
above, cvs versions 2.7.0-4 and above, should have this problem
fixed.  Please let me know if not.  Retrieval instructions (partially
under construction) at http://people.debian.org/~camm/gcl.

Take care,

<address@hidden> writes:

> 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>>
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Gcl-devel mailing list
> address@hidden
> http://mail.gnu.org/mailman/listinfo/gcl-devel
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah