Re: [Gcl-devel] proclaim error

[Camm Maguire]

Greetings!  OK, I'm still testing this, but it looks good so far:

=============================================================================
Index: gcl_predlib.lsp
===================================================================
RCS file: /cvsroot/gcl/gcl/lsp/gcl_predlib.lsp,v
retrieving revision 1.1.2.1
diff -u -r1.1.2.1 gcl_predlib.lsp
--- gcl_predlib.lsp     14 Sep 2003 02:30:35 -0000      1.1.2.1
+++ gcl_predlib.lsp     20 Sep 2003 15:22:17 -0000
@@ -117,6 +117,9 @@
           (atom . atom)
           (cons . consp)
           (list . listp)
+          (fixnum . fixnump)
+          (integer . integerp)
+          (rational . rationalp)
           (number . numberp)
           (character . characterp)
           (package . packagep)
@@ -132,7 +135,8 @@
           )
         (cdr l)))
     ((endp l))
-  (si:putprop (caar l) (cdar l) 'type-predicate))
+  (si:putprop (caar l) (cdar l) 'type-predicate)
+  (si:putprop (cdar l) (caar l) 'predicate-type))
 
 (defun class-of (object)
   (declare (ignore object))
@@ -256,6 +260,10 @@
 ;;; The result is always a list.
 (defun normalize-type (type &aux tp i )
   ;; Loops until the car of type has no DEFTYPE definition.
+  (when (and (consp type) (eq (car type) 'satisfies))
+    (unless (setq tp (get (cadr type) 'predicate-type))
+      (error "Cannot process type ~S~%" type))
+    (setq type tp))
   (loop
     (if (atom type)
         (setq tp type i nil)
@@ -264,12 +272,20 @@
         (setq type (apply (get tp 'deftype-definition) i))
         (return-from normalize-type (if (atom type) (list type) type)))))
 
+;(defun nnormalize-type (type &aux tp) 
+;  (when (and (consp type) (eq (car type) 'satisfies))
+;    (unless (setq tp (get (cadr type) 'predicate-type))
+;      (error "Cannot process type ~S~%" type))
+;    (setq type tp))
+;  (normalize-type type)
+;)
 
 ;;; KNOWN-TYPE-P answers if the given type is a known base type.
 ;;; The type may not be normalized.
+;; FIXME this needs to be more robust
 (defun known-type-p (type)
   (when (consp type) (setq type (car type)))
-  (if (or (equal (string type) "ERROR")
+  (if (or (and (stringp type) (equal (string type) "ERROR"))
          (member type
                   '(t nil boolean null symbol keyword atom cons list sequence
                      signed-char unsigned-char signed-short unsigned-short
@@ -292,7 +308,7 @@
                      style-warning synonym-stream two-way-stream 
structure-object
                      type-error unbound-slot unbound-variable 
undefined-function
                      warning ))
-          (get type 's-data))
+          (and (symbolp type) (get type 's-data)))
       t
       nil))
 
@@ -311,10 +327,20 @@
                       (values t t) (values nil t))))
     (when (or c1 c2)
       (return-from subtypep (values nil t))))
-  (setq t1 (normalize-type type1))
-  (setq type1 (if (eq (car t1) 'satisfies) (list type1) t1))
-  (setq t2 (normalize-type type2))
-  (setq type2 (if (eq (car t2) 'satisfies) (list type2) t2))
+  (setq type1 (normalize-type type1))
+  (setq type2 (normalize-type type2))
+;  (setq type1 (if (eq (car t1) 'satisfies) (list type1) t1))
+;  (when (eq (car t1) 'satisfies)
+;    (unless (setq t1 (get (cadr t1) 'predicate-type))
+;      (return-from subtypep (values nil nil)))
+;    (setq t1 (list t1)))
+;  (setq type1 t1)
+;  (setq type2 (if (eq (car t2) 'satisfies) (list type2) t2))
+;  (when (eq (car t2) 'satisfies)
+;    (unless (setq t2 (get (cadr t2) 'predicate-type))
+;      (return-from subtypep (values nil nil)))
+;    (setq t2 (list t2)))
+;  (setq type2 t2)
 ;  (setq type1 (normalize-type type1))
 ;  (setq type2 (normalize-type type2))  
   (when (equal type1 type2)
=============================================================================

If you want to try this out, apply this patch to gcl_predlib.lsp in
the lsp subdirectory after you have build your GCL, go into that
directory and type 'make'.  Then go into ../unixport and type 'make
saved_gcl' or make 'saved_ansi_gcl' depending on your configure
options.

If you'd rather wait, then this or equivalent will be committed to
both 2.6.1 and HEAD shortly if all tests pass.

I'm alo probably missing some predicates.  Anyone have a complete
'list'?


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