Re: [Gcl-devel] More on proclaim error

[Camm Maguire]

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