		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-uterm-to-components

Split a term into component terms.

Signature
(atc-uterm-to-components uterm comps) → (mv uterms varps bound-vars)
Arguments: uterm — An untranslated term.; comps — Guard (posp comps).
Returns: uterms — Untranslated terms.
Type (true-listp uterms).; varps — Type (boolean-listp varps).; bound-vars — Type (symbol-listp bound-vars).

This is used in the 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 comps input is the number of results.

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.

Definitions and Theorems

Function: atc-uterm-to-components-aux

(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: true-listp-of-atc-uterm-to-components-aux

(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: len-of-atc-uterm-to-components-aux

(defthm len-of-atc-uterm-to-components-aux
  (b* ((?uterms (atc-uterm-to-components-aux uterm comps)))
    (equal (len uterms) (nfix comps))))

Function: atc-uterm-to-components

(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 (alistp bindings))
        (raise "Internal error: malformed LET or LET* bindings ~x0."
               bindings)
        (mv nil nil nil))
       (vars (strip-cars bindings))
       ((unless (symbol-listp vars))
        (raise "Internal error: malformed LET or LET* bindings ~x0."
               bindings)
        (mv nil nil nil))
       (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: true-listp-of-atc-uterm-to-components.uterms

(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: boolean-listp-of-atc-uterm-to-components.varps

(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: symbol-listp-of-atc-uterm-to-components.bound-vars

(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: len-of-atc-uterm-to-components.varps

(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))))