Check if a term
(atc-affecting-term-for-let-p term prec-fns) → yes/no
This is explained in the user documentation. Here we perform a shallow check, because we examine the term in full detail when recursively generating C code from it. In essence, here we check that the term is either (i) an if whose test is not mbt or (ii) a call of a (preceding) target function.
Function:
(defun atc-affecting-term-for-let-p (term prec-fns) (declare (xargs :guard (and (pseudo-termp term) (atc-symbol-fninfo-alistp prec-fns)))) (let ((__function__ 'atc-affecting-term-for-let-p)) (declare (ignorable __function__)) (case-match term (('if test . &) (b* (((mv mbtp &) (check-mbt-call test))) (not mbtp))) ((fn . &) (and (symbolp fn) (consp (assoc-eq fn prec-fns)))) (& nil))))
Theorem:
(defthm booleanp-of-atc-affecting-term-for-let-p (b* ((yes/no (atc-affecting-term-for-let-p term prec-fns))) (booleanp yes/no)) :rule-classes :rewrite)