		Search-engine friendly clone of the ACL2 documentation.

Defvisitors

Defvisitor

Generate visitor functions for one type or one mutually-recursive clique of types.

Defvisitor first requires that you have a visitor template defined using defvisitor-template. The defvisitor form then instantiates that template to create a visitor function for a type, or for each type in a mutually-recursive clique of types. See also defvisitors, which generates several defvisitor forms in order to traverse several types, and defvisitor-multi, which combines defvisitor and defvisitors forms into a mutual recursion.

For example, the following visitor template was described in defvisitor-template:

(defvisitor-template collect-strings ((x :object))
  :returns (names (:join (append names1 names)
                   :tmp-var names1
                   :initial nil)
                  string-listp)
  :type-fns ((string list))
  :fnname-template collect-strings-in-<type>)

If we have a type defined as follows:

(deftagsum simple-tree
  ;; Some simple kind of structure
  (:leaf ((name  stringp)
          (value natp)
          (cost  integerp)))
  (:branch ((left   simple-tree)
            (right  simple-tree)
            (hint   booleanp)
            (family stringp)
            (size   natp))))

then to create a visitor for the simple-tree type, we can do:

(defvisitor collect-strings-in-simple-tree-definition
            ;; optional event name, for tags etc

  ;; type or mutually-recursive clique of types to visit
  :type simple-tree

  ;; template to instantiate
  :template collect-strings)

This creates (essentially) the following function definition:

(define collect-strings-in-simple-tree ((x simple-tree-p))
  :returns (names string-listp)
  :measure (simple-tree-count x)
  (simple-tree-case x
    :leaf   (b* ((names (list x.name)))
               names)
    :branch (b* ((names (collect-strings-in-simple-tree x.left))
                 (names1 (collect-strings-in-simple-tree x.right))
                 (names (append names1 names))
                 (names1 (list x.family))
                 (names (append names1 names)))
               names)))

Additionally, defvisitor modifies the collect-strings template so that future instantiations of the template will, by default, use collect-strings-in-simple-tree when visiting a simple-tree object. (The pair (simple-tree collect-strings-in-simple-tree) is added to the :type-fns of the template; see defvisitor-template.)

If we instead have a mutually-recursive clique of types, like the following:

(deftypes mrec-tree
  (deftagsum mrec-tree-node
     (:leaf ((name stringp)
             (value natp)
             (cost integerp)))
     (:branch ((children mrec-treelist)
               (family stringp)
               (size natp))))
  (deflist mrec-treelist :elt-type mrec-tree-node))

then we can create a mutual recursion of visitors for these types as follows:

(defvisitor collect-mrec-tree-strings
   :type mrec-tree   ;; the deftypes form name, not one of the type names
   :template collect-strings)

This creates a definition like this:

(defines collect-strings-in-mrec-tree
  (define collect-strings-in-mrec-tree-node ((x mrec-tree-node-p))
     :returns (names string-listp)
     :measure (mrec-tree-node-count x)
     (mrec-tree-node-case x
       :leaf ...    ;; similar to the simple-tree above
       :branch ...))
  (define collect-strings-in-mrec-treelist ((x mrec-treelist-p))
     :returns (names string-listp)
     :measure (mrec-treelist-count x)
     (if (atom x)
         nil
       (b* ((names (collect-strings-in-mrec-tree-node (car x)))
            (names1 (collect-strings-in-mrec-treelist (cdr x)))
            (names (append names1 names)))
         names))))

The general form of defvisitor is:

(defvisitor [ event-name ]
   :type type-name
   :template template-name
   other-keyword-args
   mrec-defines
   ///
   post-events)

One or more additional define forms may be nested inside a defvisitor form; this means they will be added to the mutual-recursion with the generated visitor functions. This can be used to specialize the visitor's behavior on some field so that when visiting that field the function is called, which then calls other visitor functions from the clique.

The available keyword arguments (other than :type and :template) are as follows:

:type-fns, :field-fns, :prod-fns -- these add additional entries to the corresponding arguments of the template; see defvisitor-template. When the defvisitor event finishes, these entries are left in the updated template.
:fnname-template, :renames -- these override the corresponding arguments of the template, but only for the current defvisitor; i.e., they are not stored in the updated template.
:omit-types, :include-types -- when defining visitors for a mutually-recursive clique of types, :omit-types may be used to skip creation of a visitor for some of the types, or :include-types may be used to only create visitors for the listed types.
:measure -- Template for generating the measure for the functions; defaults to :count. In the template, :count is replaced by the count function for each type visited, and :order is replaced by the current order value (see below). E.g., (two-nats-measure :count 0) is often a useful measure template, and (two-nats-measure :order :count) is sometimes useful inside defvisitor-multi.
:defines-args, define-args -- Extra keyword arguments provided to defines or :define respectively; defines-args is only applicable when there is a mutual recursion.
:order specifies the order value for this clique, which is useful when combining multiple defvisitor cliques into a single mutual recursion with defvisitor-multi.