		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-expand-input-lines

Extend stv-expand-input-entry across a list of lines.

Signature
(stv-expand-input-lines lines gensyms usersyms) → (mv new-lines gensyms usersyms)
Arguments: lines — Guard (true-list-listp lines).
Returns: new-lines — Type (true-list-listp new-lines).

Definitions and Theorems

Function: stv-expand-input-lines

(defun
 stv-expand-input-lines
 (lines gensyms usersyms)
 (declare (xargs :guard (true-list-listp lines)))
 (let
  ((__function__ 'stv-expand-input-lines))
  (declare (ignorable __function__))
  (b*
   (((when (atom lines))
     (mv nil gensyms usersyms))
    (line1 (car lines))
    ((cons name1 entries1) line1)
    ((unless (and (consp name1) (atom-listp name1)))
     (raise
      "Expected all input line names to be already expanded to ~
                non-empty lists of E bits, but found ~x0."
      name1)
     (mv nil gensyms usersyms))
    ((mv new-entries1 gensyms usersyms)
     (stv-expand-input-entries name1 (len name1)
                               0 entries1 gensyms usersyms nil))
    (new-car (cons name1 new-entries1))
    ((mv new-cdr gensyms usersyms)
     (stv-expand-input-lines (cdr lines)
                             gensyms usersyms)))
   (mv (cons new-car new-cdr)
       gensyms usersyms))))

Theorem: true-list-listp-of-stv-expand-input-lines.new-lines

(defthm true-list-listp-of-stv-expand-input-lines.new-lines
        (b* (((mv ?new-lines ?gensyms ?usersyms)
              (stv-expand-input-lines lines gensyms usersyms)))
            (true-list-listp new-lines))
        :rule-classes :rewrite)

Theorem: stv-expand-input-lines-mvtypes-0

(defthm
     stv-expand-input-lines-mvtypes-0
     (true-listp
          (mv-nth 0
                  (stv-expand-input-lines lines gensyms usersyms)))
     :rule-classes :type-prescription)

Theorem: true-listp-of-stv-expand-input-lines-gensyms

(defthm true-listp-of-stv-expand-input-lines-gensyms
        (let ((ret (stv-expand-input-lines lines gensyms usersyms)))
             (implies (true-listp gensyms)
                      (true-listp (mv-nth 1 ret)))))