Filter external objects out of the formals, for passing to exec-fun.
(atc-filter-exec-fun-args formals prec-objs) → args
In the generated correctness theorem for each non-recursive function, we generally pass to exec-fun an argument for each formal of the function. Except for formals that represent external objects: those are accessed in the computation state. Thus, here we filter, out of a list of formals, the ones that represent external objects.
Function:
(defun atc-filter-exec-fun-args (formals prec-objs) (declare (xargs :guard (and (symbol-listp formals) (atc-string-objinfo-alistp prec-objs)))) (let ((__function__ 'atc-filter-exec-fun-args)) (declare (ignorable __function__)) (b* (((when (endp formals)) nil) (formal (car formals))) (if (assoc-equal (symbol-name formal) prec-objs) (atc-filter-exec-fun-args (cdr formals) prec-objs) (cons formal (atc-filter-exec-fun-args (cdr formals) prec-objs))))))
Theorem:
(defthm symbol-listp-of-atc-filter-exec-fun-args (implies (symbol-listp formals) (b* ((args (atc-filter-exec-fun-args formals prec-objs))) (symbol-listp args))) :rule-classes :rewrite)