Generate a function to generate certain kinds of terms.
The function generated by this macro
generates the list
Macro:
(defmacro expdata-gen-fn-of-terms (fn) (declare (xargs :guard (member-eq fn '(oldp newp forth back)))) (b* ((name (packn (list 'expdata-gen- fn '-of-terms))) (string (str::downcase-string (symbol-name fn))) (selector (packn (list 'expdata-surjmap-> fn)))) (cons 'define (cons name (cons '((terms pseudo-term-listp) (arg/res-surjmaps expdata-symbol-surjmap-alistp)) (cons ':guard (cons '(= (len terms) (len arg/res-surjmaps)) (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 '(surjmap (cdar arg/res-surjmaps)) (cons (cons fn (cons (cons selector '(surjmap)) '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-surjmaps))) 'nil)) 'nil)))))) '((cons new-term new-terms)))) 'nil))))))))))))))