		Search-engine friendly clone of the ACL2 documentation.

Std/util

Defenum

Introduce an enumeration type, like an enum in C.

General form:

(defenum name
  elements
  &key mode         ; current defun-mode by default
       parents      ; nil by default
       short        ; nil by default
       long         ; nil by default
       )

For example,

(defenum day-p
  (:monday :tuesday :wednesday :thursday :friday :saturday :sunday))

results in a new function, (day-p x), that recognizes :monday, :tuesday, etc.

Usage and Options

I often use keyword symbols as the elements, but any objects (even conses) can be used.

The optional :mode keyword can be set to :logic or :program to introduce the recognizer in logic or program mode. The default is whatever the current default defun-mode is for ACL2, i.e., if you are already in program mode, it will default to program mode, etc.

The optional :parents, :short, and :long parameters are like those in defxdoc.

If keyword :disable-fc is set, it causes the generated forward chaining rule to be disabled, which can make the admission of the defenum form and subsequent proofs much faster when the number of elements is large.

If keyword :member is set, then the body of the recognizer uses a member-eq check rather than an or. This can speed up compilation when the number of elements is large. It is probably necessary to have some rules about member-equal available; loading the std/lists/sets should be sufficient.

Performance Notes

The recognizer just tests its argument against the elements, in order. Because of this, you might want to order your elements so that the most common elements come first. For instance, day-p will be fastest on :monday and slowest on :sunday.

The recognizer uses eq or eql checks where possible, so if your enumeration includes a mix of, say, conses and atom like symbols, you may wish to put the atoms first.

Checking the argument against each element is probably a perfectly good strategy when the number of elements is small (perhaps fewer than 20) and when the equality checks are relatively fast (e.g., symbols, characters, numbers). It is probably is not a good strategy otherwise. If you want to use defenum for something more complex, it might be best to modify it to adaptively use a fast alist or other schemes, based on the elements it is given.