		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-algo-name

Process the :algo-name input.

Signature
(schemalg-process-algo-name algo-name ?f ?f1...?fp acl2::names-to-avoid ctx state) → (mv acl2::erp acl2::result state)
Arguments: ?f — Guard (symbolp ?f).; ?f1...?fp — Guard (symbol-listp ?f1...?fp).; acl2::names-to-avoid — Guard (symbol-listp acl2::names-to-avoid).
Returns: acl2::result — A (tuple (fn symbolp) (updated-names-to-avoid symbol-listp) result).

Definitions and Theorems

Function: schemalg-process-algo-name-aux

(defun schemalg-process-algo-name-aux (?f1...?fp)
 (declare (xargs :guard (symbol-listp ?f1...?fp)))
 (let ((__function__ 'schemalg-process-algo-name-aux))
  (declare (ignorable __function__))
  (cond
    ((endp ?f1...?fp) nil)
    (t (append (list #\[)
               (explode (symbol-name (car ?f1...?fp)))
               (list #\])
               (schemalg-process-algo-name-aux (cdr ?f1...?fp)))))))

Function: schemalg-process-algo-name

(defun schemalg-process-algo-name
       (algo-name ?f ?f1...?fp
                  acl2::names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp ?f)
                             (symbol-listp ?f1...?fp)
                             (symbol-listp acl2::names-to-avoid))))
 (let ((__function__ 'schemalg-process-algo-name))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-symbol$ algo-name
                              (msg "The ~x0 input" :algo-name)
                              t nil))
    (acl2::fn
        (if (eq algo-name :auto)
            (b* ((??f-chars (explode (symbol-name ?f)))
                 (algo-chars (if (and (consp ?f-chars)
                                      (eql (car ?f-chars) #\?))
                                 (cdr ?f-chars)
                               ?f-chars))
                 ([?f1]...[?fp]-chars
                      (schemalg-process-algo-name-aux ?f1...?fp)))
              (intern-in-package-of-symbol
                   (implode (append algo-chars [?f1]...[?fp]-chars))
                   ?f))
          algo-name))
    ((er acl2::names-to-avoid)
     (ensure-symbol-is-fresh-event-name$
      acl2::fn
      (msg
       "The name ~x0 specified (perhaps by default) by the ~x1 input"
       acl2::fn :algo-name)
      'function
      acl2::names-to-avoid t nil)))
   (value (list acl2::fn acl2::names-to-avoid)))))