Generate an input processor for an input that specifies a fresh function name.
Some event macros have inputs
to specify names of generated functions.
An input of this kind must be
either a symbol to use as the function name,
or the keyword
This macro generates an input processor for this kind of inputs.
See the implementation for details,
which uses a readable backquote notation.
The
Macro:
(defmacro def-process-input-fresh-function-name (input &key macro other-args auto-code prepwork) (declare (xargs :guard (and (symbolp input) (symbolp macro) (true-listp other-args)))) (b* ((input-processor-name (packn-pos (list macro '-process- input) macro)) (keyword (intern (symbol-name input) "KEYWORD")) (short (concatenate 'string "Process the @(':" (string-downcase (symbol-name input)) "') input."))) (cons 'define (cons input-processor-name (cons (cons input (append other-args '((names-to-avoid symbol-listp) ctx state))) (cons ':returns (cons '(mv erp (result "A @('(tuple (fn symbolp) (updated-names-to-avoid symbol-listp) result)').") state) (cons ':mode (cons ':program (cons ':short (cons short (cons (cons 'b* (cons (cons (cons '(er &) (cons (cons 'ensure-value-is-symbol$ (cons input (cons (cons 'msg (cons '"The ~x0 input" (cons keyword 'nil))) '(t nil)))) 'nil)) (cons (cons 'fn (cons (cons 'if (cons (cons 'eq (cons input '(:auto))) (cons auto-code (cons input 'nil)))) 'nil)) (cons (cons '(er names-to-avoid) (cons (cons 'ensure-symbol-is-fresh-event-name$ (cons 'fn (cons (cons 'msg (cons '"The name ~x0 specified (perhaps by default) by the ~x1 input" (cons 'fn (cons keyword 'nil)))) '('function names-to-avoid t nil)))) 'nil)) 'nil))) '((value (list fn names-to-avoid))))) (and prepwork (list :prepwork prepwork))))))))))))))