		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-const-name-aux

Signature
(atc-process-const-name-aux target-fns prog-const wrld) → (mv erp fn-thms fn-limits fn-body-limits)
Arguments: target-fns — Guard (symbol-listp target-fns).; prog-const — Guard (symbolp prog-const).; wrld — Guard (plist-worldp wrld).
Returns: fn-thms — Type (symbol-symbol-alistp fn-thms), given (symbol-listp target-fns).; fn-limits — Type (symbol-symbol-alistp fn-limits), given (symbol-listp target-fns).; fn-body-limits — Type (symbol-symbol-alistp fn-body-limits), given (symbol-listp target-fns).

Definitions and Theorems

Function: atc-process-const-name-aux

(defun atc-process-const-name-aux (target-fns prog-const wrld)
 (declare (xargs :guard (and (symbol-listp target-fns)
                             (symbolp prog-const)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-process-const-name-aux))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil nil)
    ((when (endp target-fns))
     (retok nil nil nil))
    (fn (car target-fns))
    (fn-thm (packn (list prog-const "-" (symbol-name fn)
                         "-CORRECT")))
    (msg? (acl2::fresh-namep-msg-weak fn-thm nil wrld))
    ((when msg?)
     (reterr
      (msg
       "The generated theorem name ~x0 ~
                         for the correctness theorem of the function ~x1 ~
                         is invalid: ~@2"
       fn-thm fn msg?)))
    ((erp fn-thms fn-limits fn-body-limits)
     (atc-process-const-name-aux (cdr target-fns)
                                 prog-const wrld))
    (fn-limit (packn (list prog-const "-" (symbol-name fn)
                           "-LIMIT")))
    (msg? (acl2::fresh-namep-msg-weak fn-limit 'function
                                      wrld))
    ((when msg?)
     (reterr
      (msg
       "The generated function name ~x0 ~
                         for the limit of the function ~x1 ~
                         is invalid: ~@2"
       fn-limit fn msg?)))
    ((when (not (irecursivep+ fn wrld)))
     (retok (acons fn fn-thm fn-thms)
            (acons fn fn-limit fn-limits)
            fn-body-limits))
    (fn-body-limit (packn (list prog-const "-" (symbol-name fn)
                                "-BODY-LIMIT")))
    (msg? (acl2::fresh-namep-msg-weak fn-body-limit 'function
                                      wrld))
    ((when msg?)
     (reterr
      (msg
       "The generated function name ~x0 ~
                         for the body limit of the function ~x1 ~
                         is invalid: ~@2"
       fn-body-limit fn msg?))))
   (retok (acons fn fn-thm fn-thms)
          (acons fn fn-limit fn-limits)
          (acons fn fn-body-limit fn-body-limits)))))

Theorem: symbol-symbol-alistp-of-atc-process-const-name-aux.fn-thms

(defthm symbol-symbol-alistp-of-atc-process-const-name-aux.fn-thms
 (implies
     (symbol-listp target-fns)
     (b* (((mv acl2::?erp
               ?fn-thms ?fn-limits ?fn-body-limits)
           (atc-process-const-name-aux target-fns prog-const wrld)))
       (symbol-symbol-alistp fn-thms)))
 :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atc-process-const-name-aux.fn-limits

(defthm symbol-symbol-alistp-of-atc-process-const-name-aux.fn-limits
 (implies
     (symbol-listp target-fns)
     (b* (((mv acl2::?erp
               ?fn-thms ?fn-limits ?fn-body-limits)
           (atc-process-const-name-aux target-fns prog-const wrld)))
       (symbol-symbol-alistp fn-limits)))
 :rule-classes :rewrite)

Theorem: symbol-symbol-alistp-of-atc-process-const-name-aux.fn-body-limits

(defthm
  symbol-symbol-alistp-of-atc-process-const-name-aux.fn-body-limits
 (implies
     (symbol-listp target-fns)
     (b* (((mv acl2::?erp
               ?fn-thms ?fn-limits ?fn-body-limits)
           (atc-process-const-name-aux target-fns prog-const wrld)))
       (symbol-symbol-alistp fn-body-limits)))
 :rule-classes :rewrite)