[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] More on proclaim error
From: |
Camm Maguire |
Subject: |
Re: [Gcl-devel] More on proclaim error |
Date: |
05 Dec 2003 19:37:44 -0500 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings! OK, luckily this is pretty easy to handle, depending on
what you are trying to accomplish. What do you intend the
proclamation to achieve? Without some sort of mapping from a
predicate function to a known type, all the subtypep and typep calls
will return nil, and it is these calls that the compiler uses in
writing/optimizing functions. GCL makes this mapping for known
predicates via the symbol-plist of the predicate and the type,
i.e. (get 'predicate 'si::predicate-type) -> type, (get 'type
'si::type-predicate) -> predicate. You can install these yourself if
you'd like with si::putprop. You can also look at deftype.
If you just want the syntax to be parsed, you can apply this diff:
--- 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)
Perhaps Paul can let us know what the proper behavior should be for
user defined predicates. I'm reasonably confident we'll be able to
implement that pretty simply.
Take care,
<address@hidden> writes:
> 1. ( ) text/plain (*) text/html
>
>
>
> Hi, I'm David Hardin, and I'm working with Dave Greve and Matt Wilding on
> some ACL2 projects. On 18 September, Dave
> reported an error with proclaim that appeared somewhere between GCL 2.2.2 and
> GCL 2.5.0, and that persisted in GCL
> 2.6.1. Dave reported in
> http://mail.gnu.org/archive/html/gcl-devel/2003-09/msg00117.html
> that the form:
> (proclaim
> '(ftype (function
> ((satisfies integerp))
> t)
> foo))
> results in the error:
> Error: (satisfies integerp) is not of type STRING
> Camm noted in
> http://mail.gnu.org/archive/html/gcl-devel/2003-09/msg00158.html
> that a preliminary fix had been made to gcl_predlib.lsp. I applied this fix
> to my gcl-2.6.1-9 environment, and confirmed
> that Dave's original example problem was now fixed. However, the real
> problem we are seeing in our ACL2 models is with
> user-defined predicates. So, if I alter Dave's example slightly:
> (defun mypredp (x) t)
> (proclaim
> '(ftype (function
> ((satisfies mypredp))
> t)
> foo))
> and run with the most recent gcl_predlib.lsp fix, I still get an error:
> Fast links are on: do (si::use-fast-links nil) for debugging
> Error signalled by PROCLAIM.
> Broken at SYSTEM::NORMALIZE-TYPE. Type :H for Help.
> BTW, clisp 2.31 digests this latter example correctly, returning nil.
> This problem is currently impeding our progress in a number of places, so any
> additional help would be appreciated. We
> can't really go back to an older gcl where the problem does not occur (e.g.,
> gcl 2.2.2 on Solaris), because we have moved
> from Solaris to Linux, and the older gcl's won't build on Linux. BTW, we
> really need to use GCL, and not clisp or CMU CL,
> because we need C source code generation.
> Thanks,
> David
> _______________________________________________
> 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
Re: [Gcl-devel] More on proclaim error, dshardin, 2003/12/17