		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-measure-name

Process the :measure-name input.

Signature
(defarbrec-process-measure-name measure-name fn$ update-names$ terminates-name$ terminates-witness-name terminates-rewrite-name ctx state) → (mv erp measure-name$ state)
Arguments: fn$ — Guard (symbolp fn$).; update-names$ — Guard (symbol-listp update-names$).; terminates-name$ — Guard (symbolp terminates-name$).; terminates-witness-name — Guard (symbolp terminates-witness-name).; terminates-rewrite-name — Guard (symbolp terminates-rewrite-name).
Returns: measure-name$ — A symbolp.

Return the name to use for the measure function.

Definitions and Theorems

Function: defarbrec-process-measure-name

(defun defarbrec-process-measure-name
       (measure-name fn$ update-names$
                     terminates-name$ terminates-witness-name
                     terminates-rewrite-name ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn$)
                             (symbol-listp update-names$)
                             (symbolp terminates-name$)
                             (symbolp terminates-witness-name)
                             (symbolp terminates-rewrite-name))))
 (let ((__function__ 'defarbrec-process-measure-name))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-symbol$ measure-name
                              "The :MEASURE-NAME input" t nil))
    (symbol (or measure-name
                (add-suffix-to-fn fn$ "-MEASURE")))
    (description
     (msg
      "The name ~x0 of the measure function, ~
                          determined (perhaps by default) by ~
                          the :MEASURE-NAME input,"
      symbol))
    ((er &)
     (ensure-symbol-new-event-name$ symbol description t nil))
    ((er &)
     (ensure-symbol-different$
          symbol fn$
          (msg "the name ~x0 of the function to generate"
               fn$)
          description t nil))
    ((er &)
     (ensure-value-is-not-in-list$
      symbol update-names$
      (if
       (= 1 (len update-names$))
       (msg
        "the name ~x0 of ~
                          the iterated argument update function, ~
                          determined (perhaps by default) by ~
                          the :UPDATE-NAMES input"
        (car update-names$))
       (msg
        "the name ~&0 of ~
                        the iterated argument update functions, ~
                        determined (perhaps by default) by ~
                        the :UPDATE-NAMES input"
        update-names$))
      description t nil))
    ((er &)
     (ensure-symbol-different$
      symbol terminates-name$
      (msg
       "the name ~x0 of the termination testing predicate, ~
                      determined (perhaps by default) by ~
                      the :TERMINATES-NAME input"
       terminates-name$)
      description t nil))
    ((er &)
     (ensure-symbol-different$
      symbol terminates-witness-name
      (msg
       "the name ~x0 of the witness function associated to ~
                      the termination testing predicate, ~
                      determined (perhaps by default) by ~
                      the :TERMINATES-NAME input"
       terminates-witness-name)
      description t nil))
    ((er &)
     (ensure-symbol-different$
      symbol terminates-rewrite-name
      (msg
       "the name ~x0 of the rewrite rule associated to ~
                      the termination testing predicate, ~
                      determined (perhaps by default) by ~
                      the :TERMINATES-NAME input"
       terminates-rewrite-name)
      description t nil)))
   (value symbol))))