		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-terminates-name

Process the :terminates-name input.

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

Return the names to use for the termination testing predicate, the associated witness, and the associated rewrite rule.

Since the predicate is introduced via a defun-sk, we must ensure that the associated witness name and rewrite rule name are also new and distinct from other names introduced by defarbrec.

For now we use, for witness and rewrite rule, the same names that defun-sk would generate by default. But this might change in the future.

Definitions and Theorems

Function: defarbrec-process-terminates-name

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