		Search-engine friendly clone of the ACL2 documentation.

Stv-widen

Stv-widen-lines

Rewrite lines of an STV, repeating the last entry in each line to extend it to the desired number of phases.

Signature
(stv-widen-lines lines number-of-phases warn-non-blank) → widened-lines
Arguments: lines — Guard (true-list-listp lines).; number-of-phases — Guard (natp number-of-phases).; warn-non-blank — Guard (booleanp warn-non-blank).
Returns: widened-lines — Type (true-list-listp widened-lines), given the guard.

The warn-non-blank is intended to be set for :output lines and :internals lines. When it is set, we cause an error if an attempt is made to replicate any element other than _, since it doesn't make sense to replicate simulation variables.

Definitions and Theorems

Function: stv-widen-lines

(defun stv-widen-lines (lines number-of-phases warn-non-blank)
 (declare (xargs :guard (and (true-list-listp lines)
                             (natp number-of-phases)
                             (booleanp warn-non-blank))))
 (let ((__function__ 'stv-widen-lines))
  (declare (ignorable __function__))
  (b*
   (((when (atom lines)) nil)
    (line1 (car lines))
    (line1-name (car line1))
    (line1-phases (cdr line1))
    (- (or (consp line1-phases)
           (er hard? 'stv-widen-lines
               "No phases were provided for ~x0.~%"
               line1-name)))
    (line1-nphases (len line1-phases))
    (line1-widened-phases
     (cond
      ((= line1-nphases number-of-phases)
       line1-phases)
      ((< line1-nphases number-of-phases)
       (b* ((repeat-me (car (last line1-phases))))
        (or
         (not warn-non-blank)
         (eq repeat-me '_)
         (er
          hard? 'stv-widen-lines
          "The line for ~x0 needs to be extended, but it ends ~
                          with ~x1.  We only allow output and internal lines ~
                          to be extended when they end with an underscore."
          line1-name repeat-me))
        (append line1-phases
                (replicate (- number-of-phases line1-nphases)
                           repeat-me))))
      (t
       (prog2$
        (er hard? 'stv-widen-lines
            "Entry for ~x0 is longer than the max number of phases?"
            line1-name)
        (take number-of-phases line1-phases))))))
   (cons (cons line1-name line1-widened-phases)
         (stv-widen-lines (cdr lines)
                          number-of-phases warn-non-blank)))))

Theorem: true-list-listp-of-stv-widen-lines

(defthm true-list-listp-of-stv-widen-lines
 (implies
   (and (true-list-listp lines)
        (natp number-of-phases)
        (booleanp warn-non-blank))
   (b*
     ((widened-lines
           (stv-widen-lines lines number-of-phases warn-non-blank)))
     (true-list-listp widened-lines)))
 :rule-classes :rewrite)