		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-remove-extobj-args

Remove from a list of argument terms the ones that are external objects.

Signature
(atc-remove-extobj-args args formals extobjs) → filtered-args
Arguments: args — Guard (expr-listp args).; formals — Guard (symbol-listp formals).; extobjs — Guard (symbol-listp extobjs).
Returns: filtered-args — Type (expr-listp filtered-args), given (expr-listp args).

While ACL2 functions have explicit arguments for external objects, the corresponding C functions do not, because they access them directly. Thus, when generating code for C function calls, we must omit the ACL2 function arguments that are external objects. Those arguments are removed using this code.

Definitions and Theorems

Function: atc-remove-extobj-args

(defun atc-remove-extobj-args (args formals extobjs)
  (declare (xargs :guard (and (expr-listp args)
                              (symbol-listp formals)
                              (symbol-listp extobjs))))
  (let ((__function__ 'atc-remove-extobj-args))
    (declare (ignorable __function__))
    (b* (((when (endp args))
          (b* (((unless (endp formals))
                (raise "Internal error: extra formals ~x0."
                       formals)))
            nil))
         ((unless (consp formals))
          (raise "Internal error: extra arguments ~x0."
                 args))
         (arg (car args))
         (formal (car formals)))
      (if (member-eq formal extobjs)
          (atc-remove-extobj-args (cdr args)
                                  (cdr formals)
                                  extobjs)
        (cons arg
              (atc-remove-extobj-args (cdr args)
                                      (cdr formals)
                                      extobjs))))))

Theorem: expr-listp-of-atc-remove-extobj-args

(defthm expr-listp-of-atc-remove-extobj-args
 (implies
   (expr-listp args)
   (b*
     ((filtered-args (atc-remove-extobj-args args formals extobjs)))
     (expr-listp filtered-args)))
 :rule-classes :rewrite)