		Search-engine friendly clone of the ACL2 documentation.

Event-macro-input-processors

Def-process-input-fresh-function-name

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 :auto (which cannot be a function name). In the latter case, the function name to use is generated according to some method described in the user documentation of the event macro. In either case, the name must be valid for a function and must be fresh, i.e. (1) not already in the ACL2 world and (2) distinct from the names of other event being generated by the event macro.

This macro generates an input processor for this kind of inputs. See the implementation for details, which uses a readable backquote notation. The input argument of this macro is the name of the input being processed. The :macro argument is the name of the event macro. The :other-args argument is a list of zero or more additional define-style parameters for the input processor, needed to construct the function name when the input is :auto. The :auto-code argument is the code to use to construct the function name when the input is :auto; this must refer to the additional parameters just described. The :prepwork argument consists of zero or more preparatory events, as in define.

Macro: def-process-input-fresh-function-name

(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))))))))))))))