|
|
|---|
|
|
|
|---|
Tips for dealing with symbol package issues when using the ACL2s interface
When using any of the ACL2s interface functions from inside of a package other than "ACL2", you may run into problems because the symbols inside of any query literals will default to being interned in that package. This is mainly problematic when it comes to writing expressions that call ACL2 functions.
The simplest way to solve this problem while still working in a non-ACL2 package is to fully specify the names of all functions inside your queries. For example, one would write (acl2s-compute '(acl2::expt 2 3)) instead of (acl2s-compute '(expt 2 3)).
This gets painful when writing queries containing many function calls. In this case, depending on your host Lisp, you may be able to use extended package prefix notation. For example, in SBCL, one could write (acl2s-compute 'acl2::(expt 2 (expt 2 3))) instead of (acl2s-compute '(acl2::expt 2 (acl2::expt 2 3))).
Note that using extended package prefix notation with a backquoted value will also affect any evaluated subexpressions. The following example shows one way of getting around this, by providing the full name of the argument
(in-package :foo) ;; assume we've defined a package named foo in Common Lisp (defun baz-ok-1 (x) (acl2s-compute `(acl2::expt 2 (acl2::expt 2 ,x)))) (defun baz-bad (x) (acl2s-compute `acl2::(expt 2 (expt 2 ,x)))) ;; ,x here will evaluate acl2::x instead of foo::x. (defun baz-ok-2 (x) (acl2s-compute `acl2::(expt 2 (expt 2 ,foo::x)))) ;; we can just override the default package to fix this