• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
        • Defstv
        • Stv-compile
          • Stv-expand-input-entry
          • Stv-expand-output-entry
          • Stv-restrict-alist
          • Stv-extraction-alists
          • Stv-expand-input-lines
          • Stv-expand-input-entries
          • Stv-expand-output-entries
          • Stv-expand-output-lines
          • Stv-expand-internal-lines
          • Stv-expand-internal-line
          • Stv-forge-state-bit
          • Stv-gensyms
          • Safe-pairlis-onto-acc
        • Symbolic-test-vector-format
        • Stv-implementation-details
        • Compiled-stv-p
        • Stv-run-for-all-dontcares
        • Stv-run
        • Stv-process
        • Stv-run-check-dontcares
        • Symbolic-test-vector-composition
        • Stv-expand
        • Stv-easy-bindings
        • Stv-debug
        • Stv-run-squash-dontcares
        • Stvdata-p
        • Stv-doc
        • Stv2c
        • Stv-widen
        • Stv-out->width
        • Stv-in->width
        • Stv-number-of-phases
        • Stv->outs
        • Stv->ins
        • Stv-suffix-signals
        • Stv->vars
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

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