• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • Macro-libraries
          • B*
          • Defunc
          • Fty
            • Deftagsum
            • Defprod
            • Defflexsum
            • Defbitstruct
            • Deflist
            • Defalist
            • Defbyte
            • Deffixequiv
            • Defresult
            • Deffixtype
            • Defoption
            • Fty-discipline
            • Fold
            • Fty-extensions
            • Defsubtype
            • Deftypes
            • Specific-types
            • Defset
            • Defflatsum
            • Deflist-of-len
            • Defbytelist
            • Defomap
            • Fty::basetypes
            • Defvisitors
              • Defvisitor-template
              • Defvisitor
              • Defvisitor-multi
              • Deffixtype-alias
              • Deffixequiv-sk
              • Defunit
              • Multicase
              • Deffixequiv-mutual
              • Fty::baselists
              • Def-enumcase
              • Defmap
            • Apt
            • Std/util
            • Defdata
            • Defrstobj
            • Seq
            • Match-tree
            • Defrstobj
            • With-supporters
            • Def-partial-measure
            • Template-subst
            • Soft
            • Defthm-domain
            • Event-macros
            • Def-universal-equiv
            • Def-saved-obligs
            • With-supporters-after
            • Definec
            • Sig
            • Outer-local
            • Data-structures
          • Trans1
          • Defmacro-untouchable
          • Set-duplicate-keys-action
          • Add-macro-alias
          • Magic-macroexpand
          • Defmacroq
          • Trans!
          • Remove-macro-fn
          • Remove-macro-alias
          • Add-binop
          • Untrans-table
          • Trans*-
          • Remove-binop
          • Tcp
          • Tca
        • Mailing-lists
        • Interfacing-tools
      • Macro-libraries
        • B*
        • Defunc
        • Fty
          • Deftagsum
          • Defprod
          • Defflexsum
          • Defbitstruct
          • Deflist
          • Defalist
          • Defbyte
          • Deffixequiv
          • Defresult
          • Deffixtype
          • Defoption
          • Fty-discipline
          • Fold
          • Fty-extensions
          • Defsubtype
          • Deftypes
          • Specific-types
          • Defset
          • Defflatsum
          • Deflist-of-len
          • Defbytelist
          • Defomap
          • Fty::basetypes
          • Defvisitors
            • Defvisitor-template
            • Defvisitor
            • Defvisitor-multi
            • Deffixtype-alias
            • Deffixequiv-sk
            • Defunit
            • Multicase
            • Deffixequiv-mutual
            • Fty::baselists
            • Def-enumcase
            • Defmap
          • Apt
          • Std/util
          • Defdata
          • Defrstobj
          • Seq
          • Match-tree
          • Defrstobj
          • With-supporters
          • Def-partial-measure
          • Template-subst
          • Soft
          • Defthm-domain
          • Event-macros
          • Def-universal-equiv
          • Def-saved-obligs
          • With-supporters-after
          • Definec
          • Sig
          • Outer-local
          • Data-structures
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Defvisitors

      Defvisitor-multi

      Put defvisitor, defvisitors, and define forms togeher into a single mutual recursion.

      In a few cases it is useful to have visitors for several types (or perhaps several different kinds of visitors) together in a mutual recursion. Here is an example showing how this can work.

      ;; We have sum of product terms.  Each literal in the sum of products is
      ;; either a constant or a variable, which refers to another sum of products
      ;; term via a lookup table.
      (deftagsum literal
        (:constant ((value natp)))
        (:variable ((name symbolp))))
      
      (defprod product
        ((first  literal-p)
         (second literal-p)
         (third  literal-p)))
      
      (defprod sum
        ((left  product-p)
         (right product-p)))
      
      ;; Lookup table mapping each variable to a sum-of-products.
      (defalist sop-env :key-type symbolp :val-type sum-p)
      
      ;; Suppose we have a lookup table and we want to collect all the dependencies
      ;; of some expression -- i.e., when we get to a variable we want to collect
      ;; it, then look up its formula and collect its dependencies too.  If the
      ;; table doesn't have some strict dependency order, then we might not
      ;; terminate, so we'll use a recursion limit.
      
      (defvisitor-template collect-deps ((x :object)
                                         (env sop-env-p)
                                         (rec-limit natp))
        :returns (deps (:join (append deps1 deps)
                        :tmp-var deps1 :initial nil)
                        symbol-listp)
      
        ;; We'll call the function to apply to variable names
        ;; collect-and-recur-on-var.  Note that this hasn't been defined yet -- it
        ;; needs to be mutually recursive with the other functions in the clique.
        :prod-fns ((variable (name collect-and-recur-on-var)))
      
        :fnname-template <type>-collect-deps)
      
      ;; A defvisitor-multi form binds together some defvisitor and defvisitors
      ;; forms into a mutual recursion with some other functions.  Here, we'll just have
      ;; the one defvisitors form inside.
      (defvisitor-multi sum-collect-deps
      
         (defvisitors :template collect-deps :types (sum)
           ;; Normally this defvisitors form would create a visitor for a literal,
           ;; then product, then sum.  Inside a defvisitor-multi, it instead puts
           ;; all of those definitions into one mutual recursion.
      
           ;; We have to do something special with the measure.  Defvisitors
           ;; assigns an order to each of the types so that calling from one
           ;; visitor to another can generally reduce the measure.  Therefore, we
           ;; only need to decrease the rec-limit when calling from a lower-level
           ;; type to a higher-level one -- e.g. when we reach a variable and will
           ;; recur on a sum.
           :measure (two-nats-measure rec-limit :order)
      
           ;; Since our lowest-level visitor (literal-collect-deps) is going to
           ;; call an intermediate function (collect-and-recur-on-var) which then
           ;; calls our highest-level visitor (sum-collect-deps), it's convenient
           ;; to set the order of the lowest-level to 1 so that
           ;; collect-and-recur-on-var can use 0 as the order in its measure.
           :order-base 1)
      
         ;; This function goes in the mutual recursion with the others.
         (define collect-and-recur-on-var ((x symbolp)
                                           (env sop-env-p)
                                           (rec-limit natp))
            :returns (deps symbol-listp)
            :measure (two-nats-measure rec-limit 0)
            (b* ((x (mbe :logic (symbol-fix x) :exec x))
                 (lookup (hons-get x (sop-env-fix env)))
                 ((unless lookup) (list x))
                 ((when (zp rec-limit))
                  (cw "Recursion limit ran out on ~x0~%" x)
                  (list x)))
              (cons x (sum-collect-deps (cdr lookup) env (- rec-limit 1))))))

      A defvisitor-multi form's syntax is as follows:

      (defvisitor-multi event-name
         defvisitor-defvisitors-define-forms
         keyword-args
         ///
         post-events)

      The only keyword arguments currently accepted are :defines-args and :fixequivs, which are described in defvisitor. All the usual arguments to defvisitor and defvisitors are accepted, except for these two. An additional difference from non-nested forms is that the nested defvisitor and defvisitors forms may not have an event name as the first argument.