A very fine alternative to defun.
define is an extension of defun/defund with:
- Richer formals lists that permit keyword/optional arguments, embedded
guards and documentation, automatically infer ACL2::stobj declarations,
- A more concise xargs syntax that also adds control over other
settings like set-ignore-ok, set-irrelevant-formals-ok, and
- A concise syntax for naming return values, documenting them, and proving
basic theorems (e.g., type-like theorems) about them.
- Integration with xdoc with function signatures derived and a defsection-like ability to associate related theorems with your function.
- Automatic binding of __function__ to the name of the function, which
can be useful in error messages (see, e.g., raise) and, on CCL at least,
appears to produce identical compiled output when __function__ isn't used
in the body.
The general form of define is:
(define name formals
[/// other-events]) ;; optional, starts with the symbol ///
There's nothing special about the name, it's just the name of the new
function to be defined, as in defun. The other parts all have their own
syntax and features to cover, and we address them in turn.
The formals have many features; see extended-formals. Besides the
ordinary extended-formals utilities, they can also include :type
declarations (see ACL2::type-spec) and XDOC descriptions. For instance:
(x oddp :type integer)
(y evenp :type (integer 0 *))
(z stringp "The name of something.")
The Main Stuff
After the formals we get to the main part of the definition. This section
is a mixed list that may contain:
- Extended options of the form :name value
- Declarations of the form (declare ...)
- Traditional documentation strings, i.e., "..."
- The function's body, a term
Except for the extended options, this is just like defun.
Extended options can go anywhere between the formals and the special
separator /// (if any) or the end of the define. Here is a contrived
(define parse-foo (channel n &optional (state 'state))
:parents (parser) ;; extended option
;; declarations/docstrings must come before body, as in defun
(declare (type integer n))
(declare (ignorable channel))
"Traditional doc string that the xdoc system ignores."
(declare (xargs :normalize nil))
:guard (< 17 n) ;; extended option
(b* ((next (peek-char channel state)) ;; function's body
(mv result state))
:measure (file-measure channel state) ;; more extended opts.
:hints (("Goal" ...))
How does this work, exactly? Ordinarily, defun distinguishes the
function's body from documentation strings and declarations using a simple
rule: the last item is the function's body, and everything before it must be a
declaration or documentation string. For define, we simply add a
- First, all of the extended options are extracted.
- Then, the remaining parts are handled using the ordinary defun rule.
There is one special case where this approach is incompatible with
defun: if your function's body is nothing more than a keyword symbol,
(defun returns-foo (x)
(declare (ignore x))
then it cannot be converted into a define since the body looks like
a (malformed) extended option. I considered workarounds to avoid this, but
decided that it is better to just live with not being able to define these
kinds of functions. They are very weird, anyway.
Basic Extended Options
All xargs are available as extended options (though we provide an
additional option for :verify-guards --- see below). In practice this
just makes things more concise and better looking, e.g., compare:
(defun strpos-fast (x y n xl yl)
(declare (xargs :guard (and ...)
:measure (nfix ...)))
(define strpos-fast (x y n xl yl)
:guard (and ...)
:measure (nfix ...)
See define-guards for discussion of the various ways guards can be
Some additional minor options include:
- :enabled val
- By default the function will be disabled after the other-events are
processed. If :enabled t is provided, we will leave it enabled,
- :ignore-ok val
- Submits (set-ignore-ok val) before the definition. This option is
local to the define only and does not affect the other-events.
- :irrelevant-formals-ok val
- Submits (set-irrelevant-formals-ok val) before the definition; local
to this define only and not to any other-events.
- :inline val
- By default val is :default and we produce an ordinary function
that is neither inline or notinline. When :inline t is provided, we
create an inline function as in defun-inline; the function will
have an ugly name like foo$inline, so we'll also set up a foo macro
and appropriate macro aliases. When :inline nil is provided, we create a
notinline function as in defun-notinline; the function will have
an ugly name like foo$notinline, so we will again set up a macro and
appropriate macro aliases.
- :parents, :short, :long
- These are defxdoc-style options for documenting the function. They
are passed to a defsection for this definition.
- :prepwork events
- These are any arbitrary events you want to put before the definition
itself, for instance it might include -aux functions or local lemmas
needed for termination.
- :t-proof val
- By default, the termination proof is lost after admitting a function.
But if :t-proof t is provided, we will create a theorem without
any rule-classes that holds the proof of termination for this function and
- :verify-guards val
- The value val can be one of the following: t, nil, or
:after-returns. The first two correspond to what is described in xargs, but the third option is specific to define. The keyword
:after-returns indicates that the guards of the function are to be
verified after the returns-specifiers.
- :no-function bool
- (Advanced/obscure) By default, define will automatically bind
__function__ to the name of your function. This binding can change how
ACL2 classifies :definition rules by promoting :definition into
:abbreviation rules. When porting legacy libraries to define, this
difference can sometimes cause problems in later theorems. Setting
:no-function t will avoid binding __function__ for better backwards
- :hooks hooks
- (Advanced feature). Override which post-define-hooks are to be
executed. For instance, :hooks nil can be used to disable all such
A configuration object can also be defined to specify some extended options;
here's an example.
As of now, the following options can be set through the configuration
A configuration object can be used to set these options across multiple
defines. However, a configuration object's settings are local to a
book. Of course, the object can be changed inside a book as many times as
Extended options provided in a define will override those set by the
configuration object. Additionally, the :hooks option in the
configuration object will override any default post-define hook specified using
The Other Events
The final part of a define is an area for any arbitrary events to be
put. These events will follow the function's definition, but will be submitted
before disabling the function.
Any event can be included here, but this space is generally intended for
theorems that are "about" the function that has just been defined. The
events in this area will be included in the xdoc, if applicable, as if
they were part of the same defsection.
Any strings that appear after the /// symbol are appended to the
:long section of the define's xdoc, in between the events around
To distinguish the other-events from the main-stuff, we use the
special symbol /// to separate the two.
Why do we use this goofy symbol? In Common Lisp, /// has a special
meaning and is used by the Lisp read-eval-print loop. Because of that, ACL2
does not allow you to bind it in let statements or use it as a formal in
a definition. Because of that, we can be sure that /// is not the
body of any function definition, so it can be reliably used to separate the
rest-events. As bonus features, /// is already imported by any package that imports
*common-lisp-symbols-from-main-lisp-package*, and even sort of looks like
some kind of separator!
- A concise way to name, document, and prove basic type-like theorems
about a function's return values.
- Extended syntax for function arguments that allows for built-in
guards, documentation, and macro-like keyword/optional arguments.
- Prove additional theorems about a defined
function, implicitly binding the return variables.
- Discussion of how guards are given in define.
- Prove additional theorems about a mutual-recursion created using defines, implicitly binding the return variables.
- A way to extend define to carry out additional behaviors.
- Prove additional return-value theorems about a defined
- Shorthand for causing hard errors.