[Gcl-devel] Re: Problem to get a Function Admitted by ACL2

[Matt Kaufmann]

Right: DO and WHEN and especially PUSH, SETF, and NREVERSE are not supported in
ACL2, which is fully applicative (functional).  An ACL2-style definition of
new-alist would, I think, use recursion, and would definitely avoid assignment
(e.g., with SETF) and destructive operations (like PUSH and NREVERSE).

There is a pending issue in ACL2 for supporting changing of directories for
.cert files.  That might be relevant for what you're trying to do.  Please feel
free to email me directly if you want to discuss this further.

-- Matt
   cc: address@hidden, address@hidden,
      "Michael Bogomolny" <address@hidden>, address@hidden
   From: "Camm Maguire" <address@hidden>
   Date: 12 Dec 2003 10:01:53 -0500
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   X-WSS-ID: 13C707EC4929876-01-01
   Content-Type: text/plain;
    charset=us-ascii

   Greetings!

   >camm,

   >can you give a few more details about what exactly you want to do?
   >Maybe the function definition that was rejected would be useful.


   Unfortunately I doubt my attempted function would be of much use to
   anyone.  I was looking into the possibility of shipping working,
   pre-built .cert files for acl2's "books" in the Debian ACL2 package.
   Its quite simple in principle if I can navigate around ACL2's
   restrictions on lisp:

   ;; in other-events.lisp...

   (defun new-alist (alist old new)
     (let (new-list)
       (do ((al alist (cdr al)))
           ((not (consp al))
            (let ((res (nreverse new-list)))
              (when al
                (setf (cdr (last res)) al))
              res))
         (let ((a (car al)))
           (cond ((consp a)
                  (push (new-alist a old new) new-list))
                 ((and (stringp a)
                       (> (length a) (length old))
                       (equal old (subseq a 0 (length old))))
                  (push (concatenate 'string new (subseq a (length old))) 
new-list))
                 (t
                  (push a new-list)))))))


   (defun make-certificate-file-with-final-path (file portcullis post-alist1 
post-alist2 state old new)

    (let* ((certification-file (convert-book-name-to-cert-name file))
            (post-alist3 (mark-local-included-books post-alist1 post-alist2))
           ;;;
           ;;; only changed lines are below
           ;;;
            (certification-file (concatenate 'string certification-file 
".final"))
            (post-alist3 (lisp::new-alist post-alist3 old new)))

   ;; rest same as make-certificate-file
   ;; ......
   ))

   ;; Then in certify-book-fn:
   ;; ....

                                    (er-progn
                                     (make-certificate-file full-book-name
                                                            portcullis
                                                            post-alist1
                                                            post-alist2
                                                            state)
                                     (let ((bdir (si::getenv "BUILDDIR"))
                                           (fdir (si::getenv "FINALDIR")))
                                       (when (and bdir fdir)
                                         (make-certificate-file-with-final-path
                                                            full-book-name
                                                            portcullis
                                                            post-alist1
                                                            post-alist2
                                                            state
                                                            bdir
                                                            fdir)))




   "Matt Kaufmann" <address@hidden> writes:

   > Camm --
   > 
   > In case Bogo's excellent reply didn't fully answer your particular 
question:
   > I'm wondering if the following is the sort of problem you found, where you 
use
   > a function defined in Common Lisp that is unknown to ACL2.
   > 
   >   ACL2 !>(defun my-princ (x)
   >       (princ x))
   > 
   > 
   >   ACL2 Error in ( DEFUN MY-PRINC ...):  The symbol PRINC (in package
   >   "COMMON-LISP") has neither a function nor macro definition in ACL2.
   >   Please define it.
   > 

   Yep.  If I recall, this was triggered in the example above with "DO".
   Also, I couldn't figure out how to try a simple change to
   other-events.lisp, and recompile only that file -- instead each
   modification required a rebuild of all of ACL2 from what I could
   discern. 


   > Perhaps we should create a documentation topic ("lisp-analogues"?) that
   > associates ACL2 functions with Common Lisp functions, e.g.:
   > 
   >   princ   -->   princ$
   >   format  -->   fms, fmt, fmt1
   >   pairlis -->   pairlis$
   > 
   > and so on.  Would anyone find that useful?
   > 

   Might be helpful, but please don't launch this solely on my account,
   as I imagine my application here is a bit uncommon.

   Take care,

   > -- Matt
   >    cc: address@hidden
   >    From: "Camm Maguire" <address@hidden>
   >    Date: 11 Dec 2003 21:02:43 -0500
   >    User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   >    Reply-to: address@hidden
   >    Sender: address@hidden
   >    X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
   >    X-WSS-ID: 13C7FE754525471-01-01
   >    Content-Type: text/plain;
   >     charset=us-ascii
   > 
   >    Greetings!  On an unrelated issue, I too was trying to write a lisp
   >    function for use inside ACL2, and ran into the "~ not defined for use
   >    in ACL2" error message.  Anyway, I too would like to know how to do
   >    this (i.e. write lisp functions for use in ACL2). 
   > 
   >    Take care,
   >    -- 
   >    Camm Maguire                                            address@hidden
   >    
==========================================================================
   >    "The earth is but one country, and mankind its citizens."  --  
Baha'u'llah
   > 
   > 
   > 
   > 

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