		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-function

Process a target function fn among t1, ..., tp.

Signature
(atc-process-function fn previous-fns uncalled-fns wrld) → (mv erp new-previous-fns new-uncalled-fns)
Arguments: fn — Guard (symbolp fn).; previous-fns — Guard (symbol-listp previous-fns).; uncalled-fns — Guard (symbol-listp uncalled-fns).; wrld — Guard (plist-worldp wrld).
Returns: new-previous-fns — Type (symbol-listp new-previous-fns), given (and (symbolp fn) (symbol-listp previous-fns)).; new-uncalled-fns — Type (symbol-listp new-uncalled-fns), given (and (symbolp fn) (symbol-listp uncalled-fns)).

Here we perform some of the checks prescribed in atc, namely the ones that are easy to perform without analyzing the body of the function in detail. The remaining checks are performed during code generation, where it is more natural to perform them, as the functions' bodies are analyzed and translated to C.

The previous-fns parameter lists the symbols of all the target functions that precede fn in (t1 ... tp). This list is used to ensure that there are no duplicate target functions.

The uncalled-fns parameter lists the symbols of all the recursive target functions that precede fn in (t1 ... tp) and that are not called by any of the functions that precede fn in (t1 ... tp). This list is used to ensure that all the recursive target functions, which represent C loops, are called by some other target functions (that follow them). The reason for checking this is that C loops may only occur in C functions; if this check were not satisfied, there would be some C loop, represented by a recursive target function, that does not appear in the generated C code. As we process fn, we remove from uncalled-fns all the functions called by fn. If fn is recursive, we add it to uncalled-fns. We return the updated list of uncalled functions.

When this input processing function is called, fn is already known to be a function name. See atc-process-target.

Definitions and Theorems

Function: atc-process-function

(defun atc-process-function (fn previous-fns uncalled-fns wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (symbol-listp previous-fns)
                             (symbol-listp uncalled-fns)
                             (plist-worldp wrld))))
 (declare (xargs :guard (function-symbolp fn wrld)))
 (let ((__function__ 'atc-process-function))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil)
    (previous-fns (cons fn previous-fns))
    (desc (msg "The target function ~x0" fn))
    ((unless (logicp fn wrld))
     (reterr (msg "~@0 must be in logic mode." desc)))
    ((unless (acl2::guard-verified-p fn wrld))
     (reterr (msg "~@0 must be guard-verified." desc)))
    ((unless (acl2::definedp fn wrld))
     (reterr (msg "~@0 must be defined." desc)))
    ((when (ffnnamep fn (uguard+ fn wrld)))
     (reterr
      (msg
       "The target function ~x0 is used in its own guard. ~
                      This is currently not supported in ATC."
       fn)))
    (rec (irecursivep+ fn wrld))
    ((when (and rec (> (len rec) 1)))
     (reterr
      (msg
       "The recursive target function ~x0 ~
                      must be singly recursive, ~
                      but it is mutually recursive with ~x1 instead."
       fn (remove-eq fn rec))))
    ((when (and rec
                (not (equal (well-founded-relation+ fn wrld)
                            'o<))))
     (reterr
      (msg
       "The well-founded relation ~
                      of the recursive target function ~x0 ~
                      must be O<, but it ~x1 instead. ~
                      Only recursive functions with well-founded relation O< ~
                      are currently supported by ATC."
       fn (well-founded-relation+ fn wrld))))
    (uncalled-fns
         (atc-remove-called-fns uncalled-fns (ubody+ fn wrld)))
    (uncalled-fns (if rec (cons fn uncalled-fns)
                    uncalled-fns)))
   (retok previous-fns uncalled-fns))))

Theorem: symbol-listp-of-atc-process-function.new-previous-fns

(defthm symbol-listp-of-atc-process-function.new-previous-fns
 (implies
    (and (symbolp fn)
         (symbol-listp previous-fns))
    (b* (((mv acl2::?erp
              ?new-previous-fns ?new-uncalled-fns)
          (atc-process-function fn previous-fns uncalled-fns wrld)))
      (symbol-listp new-previous-fns)))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-process-function.new-uncalled-fns

(defthm symbol-listp-of-atc-process-function.new-uncalled-fns
 (implies
    (and (symbolp fn)
         (symbol-listp uncalled-fns))
    (b* (((mv acl2::?erp
              ?new-previous-fns ?new-uncalled-fns)
          (atc-process-function fn previous-fns uncalled-fns wrld)))
      (symbol-listp new-uncalled-fns)))
 :rule-classes :rewrite)

Theorem: true-listp-of-atc-process-function.new-previous-fns

(defthm true-listp-of-atc-process-function.new-previous-fns
 (implies
    (true-listp previous-fns)
    (b* (((mv acl2::?erp
              ?new-previous-fns ?new-uncalled-fns)
          (atc-process-function fn previous-fns uncalled-fns wrld)))
      (true-listp new-previous-fns)))
 :rule-classes :type-prescription)

Theorem: true-listp-of-atc-process-function.new-uncalled-fns

(defthm true-listp-of-atc-process-function.new-uncalled-fns
 (implies
    (true-listp new-uncalled-fns)
    (b* (((mv acl2::?erp
              ?new-previous-fns ?new-uncalled-fns)
          (atc-process-function fn previous-fns uncalled-fns wrld)))
      (true-listp new-uncalled-fns)))
 :rule-classes :type-prescription)