		Search-engine friendly clone of the ACL2 documentation.

Defvisitors

Generate visitor functions across types using a visitor template.

To use defvisitors, first see defvisitor-template and defvisitor. Defvisitors automates the generation of several defvisitor forms that create a system of visitor functions that works on a nest of types.

For example, suppose we have the following types:

(defprod employee
   ((name stringp)
    (salary natp)
    (title stringp)))

(deflist employees :elt-type employee)

(defprod group
  ((lead employee)
   (members employees)
   (budget natp)
   (name stringp)
   (responsibilities string-listp)))

(defprod division
  ((head employee)
   (operations  group)
   (engineering group)
   (sales       group)
   (service     group)
   (black-ops   group)))

Suppose we want to total up the salaries of all the employees in a division, including the division head, group leads, and group members. A visitor template for this operation might look like this:

(defvisitor-template salary-total ((x :object))
  :returns (total (:join (+ total1 total)
                   :tmp-var total1
                   :initial 0)
                  natp :rule-classes :type-prescription
                  "The total salary of all employees")
  :type-fns ((employee employee->salary)))

Now we need visitor functions for the employees, group, and division types, so we can do:

(defvisitor :type employees :template salary-total)
(defvisitor :type group     :template salary-total)
(defvisitor :type division  :template salary-total)

However, we can automate this more by using defvisitors instead of defvisitor. This doesn't seem worthwhile to get rid of just three defvisitor forms, but oftentimes the type hierarchy is much more specialized than this, and changes frequently. Using defvisitors can prevent the need to modify the code if you add a type to the hierarchy. To invoke it:

(defvisitors division-salary-total ;; optional event name
  :types (division)
  :template salary-total)

This searches over the field types of the division type and creates a graph of the types that need to be visited, then arranges them in dependency order and creates the necessary defvisitor forms.

The options for defvisitors are somewhat more limited than for defvisitor. The available keyword arguments are as follows:

:template -- the name of the visitor template to instantiate.
:types, :dep-types -- controls the top-level types to visit. Those listed in dep-types are not themselves visited, but their children are. Note that these are type names, NOT deftypes names as in defvisitor. (For a single type, the type name and deftypes name is likely the same, but for a mutually-recursive clique of types, the deftypes name refers to the whole clique.)
:measure -- measure form to use for each defvisitor form; this is mostly only useful in the context of a defvisitor-multi form.
:order-base -- starting index from which the order indices assigned to the deftypes forms are generated; also mostly only useful in the context of a defvisitor-multi form. Defvisitors assigns a different order index to each defvisitor form it submits, with earlier forms having lower indices. When the measure is properly formulated in terms of the order, this allows them to be used together in a mutual recursion.
:debug -- print some information about the graph traversals.

Subtopics

Defvisitor-template: Create a template that says how to make visitor functions.
Defvisitor: Generate visitor functions for one type or one mutually-recursive clique of types.
Defvisitor-multi: Put defvisitor, defvisitors, and define forms togeher into a single mutual recursion.