		Search-engine friendly clone of the ACL2 documentation.

Std/util

Define

A very fine alternative to defun.

Introduction

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, etc.
A more concise xargs syntax that also adds control over other settings like set-ignore-ok, set-irrelevant-formals-ok, and inlining.
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
  main-stuff
  [/// 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 example:

(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" ...))
  :guard-debug t)

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 preprocessing step:

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, e.g.,

(defun returns-foo (x)
  (declare (ignore x))
  :foo)

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 ...)))
  ...)
vs.
(define strpos-fast (x y n xl yl)
  :guard (and ...)
  :measure (nfix ...)
  ...)

See define-guards for discussion of the various ways guards can be given, additionally.

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, instead.
: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 measure.
: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 compatibility.
:hooks hooks: (Advanced feature). Override which post-define-hooks are to be executed. For instance, :hooks nil can be used to disable all such hooks.

Configuration Object

A configuration object can also be defined to specify some extended options; here's an example.

(make-define-config
    :inline t
    :no-function t)

As of now, the following options can be set through the configuration object:

(:inline :t-proof
         :no-function :non-executable
         :enabled :verbosep
         :progn :ignore-ok
         :irrelevant-formals-ok :mode
         :normalize :split-types
         :well-founded-relation :hooks
         :ruler-extenders :verify-guards
         :ret-patbinder :parents)

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 you want.

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 add-default-post-define-hook.

Returns Specifications

See returns-specifiers.

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

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!

Subtopics

Returns-specifiers: A concise way to name, document, and prove basic type-like theorems about a function's return values.
Extended-formals: Extended syntax for function arguments that allows for built-in guards, documentation, and macro-like keyword/optional arguments.
Defret: Prove additional theorems about a defined function, implicitly binding the return variables.
Define-guards: Discussion of how guards are given in define.
Defret-mutual: Prove additional theorems about a mutual-recursion created using defines, implicitly binding the return variables.
Post-define-hook: A way to extend define to carry out additional behaviors.
More-returns: Prove additional return-value theorems about a defined function.
Raise: Shorthand for causing hard errors.