[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] proclaim error
From: |
Camm Maguire |
Subject: |
Re: [Gcl-devel] proclaim error |
Date: |
24 Sep 2003 12:47:50 -0400 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
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