		Search-engine friendly clone of the ACL2 documentation.

Defvisitors

Defvisitor-template

Create a template that says how to make visitor functions.

This is used in combination with defvisitors and defvisitor to automatically generate "visitor" functions, i.e. functions that traverse a data structure and do something at specified locations in it. E.g., they can be used to transform all fields of a certain type, or to collect some information about all occurrences of a certain product field, etc. The types that these visitors may traverse are those defined by deftypes and related macros defprod, deftagsum, deflist, defalist, defoption, deftranssum, and defflexsum.

Visitor templates can be used by defvisitor, defvisitors, and defvisitor-multi to automatically generate immense amounts of boilerplate code for traversing complicated datatypes, especially when the operation you want to do only really has to do with a few fields or component types.

Here is a simple example from visitor-tests.lisp, annotated:

(defvisitor-template

  ;; Name of the template.  This gets referred to later when this template is
  ;; used by defvisitor/defvisitors.
  collect-strings

  ;; Formals, similar to the formals in std::define.  Here :object stands for
  ;; the type predicate of whatever kind of object we're currently visiting; we'll
  ;; typically instantiate this template with several different :object types.
  ((x :object))

  ;; Return specifiers.  These are also like in std::define, but after each return name
  ;; is a description of how the return value gets constructed.  The names here are
  ;; a "join" value, which means they get constructed by combining,
  ;; pairwise, the corresponding values returned by sub-calls.  In this case, the
  ;; value (names1) returned from the most recent subcall is appended onto the
  ;; previous value (names).  The initial value is nil, i.e. this is what a
  ;; visitor function returns when run on an empty list or an object with no fields.
  :returns (names (:join (append names1 names)
                   :tmp-var names1
                   :initial nil)
                  string-listp)

  ;; Now we describe what is a base case and what we return in base cases.
  ;; This says, for any string field x, just produce (list x).  (The value
  ;; bound in the alist is a lambda or function that gets applied to the
  ;; formals, in this case just x.)
  :type-fns ((string list))

  ;; Describes how the functions we produce should be named.  Here, <type> gets
  ;; replaced by the type of object each separate visitor function operates on.
  :fnname-template collect-strings-in-<type>)

Besides join values, there are two other kinds of visitor return values: accumulators and updaters. The following example shows how to use an accumulator:

(defvisitor-template collect-names-acc   ;; template name
    ;; formals:
    ((x :object)
     (names string-listp)) ;; accumulator formal

    ;; Names the return value and declares it to be an accumulator, which
    ;; corresponds to the formal NAMES.  The :fix is optional but is needed if
    ;; the return type of your accumulator output is unconditional.
    :returns  (names-out (:acc names :fix (string-list-fix names))
                         string-listp)

    ;; Base case specification.  This says that when visiting a
    ;; simple-tree-leaf product, use the function CONS as the visitor for the
    ;; NAME field.  That is, instead of recurring on name, use (cons x names),
    ;; i.e., add the name to the accumulator.
    :prod-fns ((simple-tree-leaf  (name cons))))

This shows how to use an updater return value:

(defvisitor-template incr-val  ((x :object)
                                (incr-amount natp))

  ;; In an :update return value, the type is implicitly the same as :object.
  ;; It can optionally be specified differently.  This means that new-x gets
  ;; created by updating all the fields that we recurred on (or that were base
  ;; cases) with the corresponding results.
  :returns (new-x :update)

  ;; This says that when we visit a simple-tree-leaf, we replace its value field with
  ;; the field's previous value plus (lnfix incr-amount).  (We could just use
  ;; + here instead of the lambda, but this would violate the fixing convention for
  ;; incr-amount.)
  :prod-fns ((simple-tree-leaf  (value (lambda (x incr-amount) (+ x (lnfix incr-amount)))))))

The general form of a defvisitor-template call is:

(defvisitor-template template-name formals ... keyword-args)

where the accepted keywords are as follows:

:returns, required, describing the values returned by each visitor function and how they are constructed from recursive calls. The argument to :returns is either a single return tuple or several return tuples inside an (mv ...), and each return tuple is similar to a define returnspec except that it has an extra form after the return name and before the rest of the arguments, describing how it is constructed -- either a :join, :acc, or :update form, as in the examples above.
:type-fns specify base cases for fields of certain types. The argument is a list of pairs (type function), where the function applied to the visitor formals gives the visitor values for fields of that type. Alternatively, function may be :skip, meaning that we don't recur on fields of this type. (This is the default for field types that were not defined by deftypes.) The :type-fns entry is only used if there is no applicable entry in :field-fns or :prod-fns, below.
:prod-fns specify base cases for certain fields of certain products. The argument is a list of entries (prod-name (field-name1 function1) (field-name2 function2) ...), where the functions work the same way as in :type-fns. :prod-fns entries override :type-fns and :field-fns entries.
:field-fns specify base cases for fields with certain names. The argument is a list of pairs (field-name function), where function is as in the :type-fns. This is similar to using :prod-fns, but applies to fields of the given name inside any product. :field-fns entries override :type-fns entries, but :prod-fns entries override both.
:fnname-template describes how the generated functions should be named. The argument is a symbol containing the substring <TYPE>, and function names are generated by replacing this with the name of the type.
:renames allows you to specify function names that differ from the ones described by the :fnname-template. The argument is a list of pairs (type function-name). It is also possible to use :skip as the function name, in which case the function won't be generated at all.
:fixequivs -- true by default, says whether to prove congruence (deffixequiv) theorems about the generated functions.
:reversep -- false by default, says whether to reverse the order in which fields are processed.
:wrapper -- :body by default; gives a form in which to wrap the generated body of each function, where :body is replaced by that generated body. Advanced use.

See also defvisitor, defvisitors, and defvisitor-multi.