		Search-engine friendly clone of the ACL2 documentation.

Extended-formals

Extended syntax for function arguments that allows for built-in guards, documentation, and macro-like keyword/optional arguments.

Macros like define accept an extended formals syntax. This syntax properly extends the normal syntax for a function's arguments used by defun, so you can still use a plain list of variable names if you like. But there are also some more interesting extensions.

Basic examples of some extended formals in a define:

(define split-up-string
  ((x stringp "The string to split")
   (separators (and (consp separators)
                    (character-listp separators))
    "Letters to split on -- <b>dropped from the result!</b>")
   &key
   (limit (or (not limit)
              (natp limit))
    "Where to stop, @('nil') means @('(length x)')"))
  ...)

The general syntax for extended formals is:

Formals ::= (Formal*                 ; ordinary formals
             [&optional OptFormal*]  ; optional positional formals
             [&key OptFormal*]       ; optional keyword formals
             )

OptFormal ::= Formal          ; optional formal w/NIL default
            | (Formal 'val)   ; optional formal w/custom default

Formal  ::= (varname Item*)

Item    ::= xdoc       ; documentation string
          | guard      ; guard specifier
          | :key val   ; other additional options

&key and &optional arguments

You can use &key and &optional as in macro-args. (Other lambda-list keywords like &rest aren't supported.) When macros like define see these keywords, then instead of just producing a defun we will generate:

A function, name-fn,
A wrapper macro, name,
A macro alias associating name-fn with name

The default values for these parameters work just like in ordinary macros. The explicit quote serves to separate these from Items.

Inline Documentation

You can optionally describe your formals with some xdoc documentation. This description will be embedded within some generated <dl>/<dt>/<dd> tags that describe your function's interface. You can freely use xdoc::markup and xdoc::preprocessor directives. Typically your descriptions should be short and should not include document-structuring tags like <p>, <ul>, <h3>, and so forth.

Inline Guards

As a convenient shorthand, the guard may be a single non-keyword symbol, e.g., in split-up-string above, the guard for x is (stringp x). To be more precise:

t and nil are treated literally, and
Any other symbol g is treated as short for (g var)

For more complex guards, you can also write down arbitrary terms, e.g., above separators must be a non-empty character list. We put a few sensible restrictions here. We require that a guard term must be at least a cons to distinguish it from documentation, symbol guards, and keywords. We also require that it is not simply a quoted constant. This ensures that guards can be distinguished from default values in macro arguments. For example, compare:

    &key (x 'atom)     ;; x has no guard, default value 'atom
vs. &key (x atom)      ;; x has guard (atom x), default value nil
vs. &key ((x atom) '3) ;; x has guard (atom x), default value 3

Keyword/Value Options

To make the formals syntax more flexible, other keyword/value options can be embedded within the formal.

The valid keywords and their interpretations can vary from macro to macro. For instance, define doesn't accept any keyword/value options, but defaggregate fields have a :rule-classes option.

Additional Features

Some other features of extended formals are not evident in their syntax.

We generally expect macros that take extended formals to automatically recognize ACL2::stobjs and insert appropriate (declare (xargs :stobjs ...)) forms.

Future work (not yet implemented): certain guards like stringp and (unsigned-byte-p 32 x), are recognized as ACL2::type-specs and result in type declarations for the Lisp compiler. This may occasionally improve efficiency.