Rewrite lines of an STV, repeating the last entry in each line to extend it to the desired number of phases.
(stv-widen-lines lines number-of-phases warn-non-blank) → widened-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)))))
(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)