		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-fn-of-terms

Generate a function to generate certain kinds of terms.

The function generated by this macro generates the list ((fn1 term1) (fn2 term2) ...), where (term1 term2 ...) is the terms input of the function, and where each fnk is one of either oldpk, newpk, forthk, and backk or oldp_rk, newp_rk, forth_rk, and back_rk. The choice of the fnk functions is the input of the macro. The arg/res-isomaps input of the generated function may be arg-isomaps or res-isomaps.

Macro: isodata-gen-fn-of-terms

(defmacro isodata-gen-fn-of-terms (fn)
 (declare (xargs :guard (member-eq fn '(oldp newp forth back))))
 (b* ((name (packn (list 'isodata-gen- fn '-of-terms)))
      (string (str::downcase-string (symbol-name fn)))
      (selector (packn (list 'isodata-isomap-> fn))))
  (cons
   'define
   (cons
    name
    (cons
     '((terms pseudo-term-listp)
       (arg/res-isomaps isodata-symbol-isomap-alistp))
     (cons
      ':guard
      (cons
       '(= (len terms) (len arg/res-isomaps))
       (cons
        ':returns
        (cons
         '(new-terms "A @(tsee pseudo-term-listp).")
         (cons
          ':verify-guards
          (cons
           'nil
           (cons
            ':short
            (cons
             (str::cat
              "Apply the @('"
              string "k') or @('" string
              "_rk') function
                            to the corresponding term
                            in a list of terms of length equal to
                            the number of formals or results of @('old').")
             (cons
              (cons
               'b*
               (cons
                (cons
                 '((when (endp terms)) nil)
                 (cons
                  '(term (car terms))
                  (cons
                   '(isomap (cdar arg/res-isomaps))
                   (cons
                    (cons fn
                          (cons (cons selector '(isomap)) 'nil))
                    (cons
                     (cons
                         'new-term
                         (cons (cons 'apply-term* (cons fn '(term)))
                               'nil))
                     (cons
                      (cons
                       'new-terms
                       (cons
                         (cons name
                               '((cdr terms) (cdr arg/res-isomaps)))
                         'nil))
                      'nil))))))
                '((cons new-term new-terms))))
              'nil))))))))))))))