Split a term into component terms.
(atc-uterm-to-components uterm comps) → (mv uterms varps bound-vars)
This is used in generation of type assertions in modular proofs, precisely in atc-gen-term-type-formula. A term may return one or more results, in general. For terms that represent C constructs, each result has a C type, and the type assertions in modular theorems say just that. This ACL2 function turns a term into one or more terms, one for each returned result: the resulting terms represent the results of the term, and can be individually used as arguments of type predicates in the generated theorems.
A seemingly easy way to do this would be to apply mv-nth
with increasing indices to the term if it returns two or more results,
and instead return the term unchanged if it returns a single result.
But then, because of the presence of the mv-nth in certain places,
the generated theorems would not be readily applicable as rewrite rules,
in subsequent theorems that depend on them.
We need to ``push'' the mv-nths into the term, but only to a point:
we push them through lets and mv-lets,
and also through mvs;
in all other cases, we apply the mv-nths.
This leads to the following recursive definition,
which includes some defensive checks.
The
We also return a list of the bound variables encountered along the way. We also return a list of boolean flags, one for each component, each of which says whether pushing the mv-nth through the corresponding term reached a variable. The purpose of this list of bound variables and of this list of boolean flags is explained in atc-gen-term-type-formula.
Function:
(defun atc-uterm-to-components-aux (uterm comps) (declare (xargs :guard (natp comps))) (let ((__function__ 'atc-uterm-to-components-aux)) (declare (ignorable __function__)) (cond ((zp comps) nil) (t (cons (cons 'mv-nth (cons (1- comps) (cons uterm 'nil))) (atc-uterm-to-components-aux uterm (1- comps)))))))
Theorem:
(defthm true-listp-of-atc-uterm-to-components-aux (b* ((uterms (atc-uterm-to-components-aux uterm comps))) (true-listp uterms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atc-uterm-to-components-aux (b* ((?uterms (atc-uterm-to-components-aux uterm comps))) (equal (len uterms) (nfix comps))))
Function:
(defun atc-uterm-to-components (uterm comps) (declare (xargs :guard (posp comps))) (let ((__function__ 'atc-uterm-to-components)) (declare (ignorable __function__)) (b* (((when (symbolp uterm)) (b* (((unless (eql comps 1)) (raise "Internal error: ~x0 components for ~x1." comps uterm) (mv nil nil nil))) (mv (list uterm) (list t) nil))) ((unless (and (true-listp uterm) (consp uterm))) (raise "Internal error: unexpected term ~x0." uterm) (mv nil nil nil)) ((when (eq (car uterm) 'list)) (b* ((uterms (cdr uterm)) ((unless (eql (len uterms) comps)) (raise "Internal error: ~x0 components for ~x1." comps uterm) (mv nil nil nil))) (mv uterms (atc-symbolp-list uterms) nil))) ((when (member-eq (car uterm) '(let let*))) (b* (((unless (and (consp (cdr uterm)) (consp (cddr uterm)) (endp (cdddr uterm)))) (raise "Internal error: malformed LET or LET* ~x0." uterm) (mv nil nil nil)) (bindings (cadr uterm)) ((unless (and (alistp bindings) (symbol-listp (strip-cars bindings)))) (raise "Internal error: malformed LET or LET* bindings ~x0." bindings) (mv nil nil nil)) (vars (strip-cars bindings)) (body-uterm (caddr uterm)) ((mv body-uterms varsp body-bound-vars) (atc-uterm-to-components body-uterm comps))) (mv (atc-make-lets-of-uterms (car uterm) bindings body-uterms) varsp (append vars body-bound-vars)))) ((when (eq (car uterm) 'mv-let)) (b* (((unless (and (consp (cdr uterm)) (consp (cddr uterm)) (consp (cdddr uterm)) (endp (cddddr uterm)))) (raise "Internal error: malformed MV-LET ~x0." uterm) (mv nil nil nil)) (vars (cadr uterm)) ((unless (symbol-listp vars)) (raise "Internal error: MV-LET bound variables not symbols." vars) (mv nil nil nil)) (vars-uterms (caddr uterm)) (body-uterm (cadddr uterm)) ((mv body-uterms varsp body-bound-vars) (atc-uterm-to-components body-uterm comps))) (mv (atc-make-mv-lets-of-uterms vars vars-uterms body-uterms) varsp (append vars body-bound-vars))))) (if (eql comps 1) (mv (list uterm) (list nil) nil) (mv (rev (atc-uterm-to-components-aux uterm comps)) (repeat comps nil) nil)))))
Theorem:
(defthm true-listp-of-atc-uterm-to-components.uterms (b* (((mv ?uterms ?varps ?bound-vars) (atc-uterm-to-components uterm comps))) (true-listp uterms)) :rule-classes :type-prescription)
Theorem:
(defthm boolean-listp-of-atc-uterm-to-components.varps (b* (((mv ?uterms ?varps ?bound-vars) (atc-uterm-to-components uterm comps))) (boolean-listp varps)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-uterm-to-components.bound-vars (b* (((mv ?uterms ?varps ?bound-vars) (atc-uterm-to-components uterm comps))) (symbol-listp bound-vars)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atc-uterm-to-components.varps (b* (((mv ?uterms ?varps ?bound-vars) (atc-uterm-to-components uterm comps))) (equal (len varps) (len uterms))))