Re: [Gcl-devel] More on proclaim error

[Camm Maguire]

OK, this is in now, stable and head.

typep works, subtypep returns nil nil.

Take care,

<address@hidden> writes:

> 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)))
> (loop
> (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

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