[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Gcl-devel] More on proclaim error

From: dshardin
Subject: Re: [Gcl-devel] More on proclaim error
Date: Wed, 17 Dec 2003 15:51:53 -0600

Camm wrote:

> 1) Could you please repost the patch I sent?

Here's the diff that you provided to address my proclaim problem.  This is in addition to the diff that you provided in
http://mail.gnu.org/archive/html/gcl-devel/2003-09/msg00137.html to address Dave Greve's original report of a proclaim problem.

--- gcl_predlib.lsp        2003-11-06 21:53:19.000000000 -0500
+++ /tmp/f.lisp        2003-12-05 19:25:07.000000000 -0500
@@ -261,9 +261,8 @@

(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))
+    (when (setq tp (get (cadr type) 'predicate-type))
+      (setq type tp)))

(if (atom type)

(setq tp type i nil)

> 2) I'd like to make sure that Paul agrees that handling user-defined
> predicates in a (satisfies...) type type specifier in this manner
> is acceptable (or even proper).

I believe it's acceptable given the current use we're making of it in ACL2, i.e. in guard proofs.  We don't need the user-defined predicate satisfaction information to be available in order to optimize code generation, for instance.  But, I'm no Common Lisp language lawyer, so I have no clue as to what's actually required for this case.

BTW, earlier GCL's, i.e. GCL 2.2.2, handled this situation adequately for our needs.  I don't know if any additional wisdom could be found by looking back at that version of the source.

Thanks again,

David Hardin

reply via email to

[Prev in Thread] Current Thread [Next in Thread]