		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Make-mv-let-call

Build a translated call of mv-let.

Signature
(make-mv-let-call mv-var vars indices mv-term body-term) → term
Arguments: mv-var — Guard (symbolp mv-var).; vars — Guard (symbol-listp vars).; indices — Guard (or (nat-listp indices) (eq indices :all)).; mv-term — Guard (pseudo-termp mv-term).; body-term — Guard (pseudo-termp body-term).
Returns: term — Type (pseudo-termp term), given the guard.

In translated form, (mv-let (var1 ... varn) mv-term body-term) is

((lambda (mv)
         ((lambda (var1 ... varn) body-term-trans)
          (mv-nth '0 mv)
          ...
          (mv-nth 'n-1 mv)))
 mv-term-trans)

where mv-term-trans and body-term-trans are the translations of mv-term and body-term.

This utility creates a translated term of the form above from its constituents.

For greater flexibility, we allow the mv variable to be a symbol different from the symbol `mv': as explained in check-mv-let-call, a translated mv-let may have a different symbol from `mv', and so this flexibility is useful, for example, to reconstruct an mv-let call, possibly with some modification, from another one whose mv variable is another symbol. The parameter mv-var of this utility is the symbol to use.

Also for greater flexibilty, we allow some mv-nth calls to be missing. As explained in check-mv-let-call, while translated terms obtained directly from mv-let calls always have all the mv-nth calls, a term subjected to some transformations may not. To use this utility to reconstruct this kind of transformed term, the indices parameter lets the caller specify which indices should be present. As a convenience, :all stands for all contiguous indices from 0 to the number of bound variables minus 1. If a list of indices is supplied, it must consist of strictly increasing natural numbers, and its length must match the number of bound variables. The second condition is expressed by the guard, but the first condition is checked at run time, causing an error if not satisfied.

This utility is essentially the inverse of check-mv-let-call.

Definitions and Theorems

Function: make-mv-let-call-aux1

(defun make-mv-let-call-aux1 (index n mv-var)
  (declare (xargs :guard (and (natp index)
                              (natp n)
                              (symbolp mv-var))))
  (let ((__function__ 'make-mv-let-call-aux1))
    (declare (ignorable __function__))
    (if (or (not (mbt (natp index)))
            (not (mbt (natp n)))
            (>= index n))
        nil
      (cons (cons 'mv-nth
                  (cons (cons 'quote (cons index 'nil))
                        (cons mv-var 'nil)))
            (make-mv-let-call-aux1 (1+ index)
                                   n mv-var)))))

Theorem: pseudo-term-listp-of-make-mv-let-call-aux1

(defthm pseudo-term-listp-of-make-mv-let-call-aux1
  (implies (symbolp mv-var)
           (b* ((terms (make-mv-let-call-aux1 index n mv-var)))
             (pseudo-term-listp terms)))
  :rule-classes :rewrite)

Theorem: len-of-make-mv-let-call-aux1

(defthm len-of-make-mv-let-call-aux1
  (b* ((?terms (make-mv-let-call-aux1 index n mv-var)))
    (implies (and (natp index) (natp n))
             (equal (len terms)
                    (nfix (- n index))))))

Function: make-mv-let-call-aux2

(defun make-mv-let-call-aux2 (indices mv-var)
 (declare (xargs :guard (and (nat-listp indices)
                             (symbolp mv-var))))
 (let ((__function__ 'make-mv-let-call-aux2))
  (declare (ignorable __function__))
  (cond
   ((endp indices) nil)
   ((endp (cdr indices))
    (list (cons 'mv-nth
                (cons (cons 'quote (cons (car indices) 'nil))
                      (cons mv-var 'nil)))))
   (t
    (if (< (car indices) (cadr indices))
        (cons (cons 'mv-nth
                    (cons (cons 'quote (cons (car indices) 'nil))
                          (cons mv-var 'nil)))
              (make-mv-let-call-aux2 (cdr indices)
                                     mv-var))
     (prog2$
      (raise
       "The list of indices ~x0 ~
                                is not strictly increasing."
       indices)
      (make-list (len indices)
                 :initial-element nil)))))))

Theorem: pseudo-term-listp-of-make-mv-let-call-aux2

(defthm pseudo-term-listp-of-make-mv-let-call-aux2
  (implies (symbolp mv-var)
           (b* ((terms (make-mv-let-call-aux2 indices mv-var)))
             (pseudo-term-listp terms)))
  :rule-classes :rewrite)

Theorem: len-of-mv-let-call-aux2

(defthm len-of-mv-let-call-aux2
  (b* ((?terms (make-mv-let-call-aux2 indices mv-var)))
    (equal (len terms) (len indices))))

Function: make-mv-let-call

(defun make-mv-let-call (mv-var vars indices mv-term body-term)
 (declare (xargs :guard (and (symbolp mv-var)
                             (symbol-listp vars)
                             (or (nat-listp indices)
                                 (eq indices :all))
                             (pseudo-termp mv-term)
                             (pseudo-termp body-term))))
 (declare (xargs :guard (or (equal indices :all)
                            (equal (len indices) (len vars)))))
 (let ((__function__ 'make-mv-let-call))
  (declare (ignorable __function__))
  (cons
   (cons
        'lambda
        (cons (cons mv-var 'nil)
              (cons (cons (cons 'lambda
                                (cons vars (cons body-term 'nil)))
                          (if (eq indices :all)
                              (make-mv-let-call-aux1 0 (len vars)
                                                     mv-var)
                            (make-mv-let-call-aux2 indices mv-var)))
                    'nil)))
   (cons mv-term 'nil))))

Theorem: pseudo-termp-of-make-mv-let-call

(defthm pseudo-termp-of-make-mv-let-call
 (implies
  (and (symbolp mv-var)
       (symbol-listp vars)
       (if (nat-listp indices)
           (nat-listp indices)
         (eq indices ':all))
       (pseudo-termp mv-term)
       (pseudo-termp body-term)
       (if (equal indices ':all)
           (equal indices ':all)
         (equal (len indices) (len vars))))
  (b*
   ((term (make-mv-let-call mv-var vars indices mv-term body-term)))
   (pseudo-termp term)))
 :rule-classes :rewrite)