gcl-devel
[Top][All Lists]
Advanced

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

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


From: Camm Maguire
Subject: [Gcl-devel] Re: Problem to get a Function Admitted by ACL2
Date: 12 Dec 2003 10:01:53 -0500
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

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




reply via email to

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