[Top][All Lists]

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

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

From: Matt Kaufmann
Subject: [Gcl-devel] Re: Problem to get a Function Admitted by ACL2
Date: Fri, 12 Dec 2003 09:13:52 -0600

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;



   >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))
         (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))) 
                  (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 
            (post-alist3 (lisp::new-alist post-alist3 old new)))

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

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

                                     (make-certificate-file full-book-name
                                     (let ((bdir (si::getenv "BUILDDIR"))
                                           (fdir (si::getenv "FINALDIR")))
                                       (when (and bdir fdir)

   "Matt Kaufmann" <address@hidden> writes:

   > Camm --
   > In case Bogo's excellent reply didn't fully answer your particular 
   > I'm wondering if the following is the sort of problem you found, where you 
   > 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

   > 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."  --  

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

reply via email to

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