• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
          • Scopestack
          • Hid-tools
          • Filtering-by-name
          • Vl-interface-mocktype
          • Stripping-functions
          • Genblob
          • Expr-tools
          • Extract-vl-types
          • Hierarchy
          • Range-tools
          • Finding-by-name
          • Stmt-tools
            • Vl-rebuild-caselist
              • Vl-stmt-atomicstmts
              • Vl-compoundstmt->stmts
              • Vl-compoundstmt->exprs
              • Vl-compoundstmt->vardecls
              • Change-vl-compoundstmt
              • Vl-compoundstmt->paramdecls
              • Vl-compoundstmt->ctrl
              • Vl-atomicstmtlist-p
              • Vl-stmt->atts
              • Vl-atomicstmt-p
              • Vl-timingstmt-p
              • Vl-repeatstmt-p
              • Vl-foreverstmt-p
              • Vl-assignstmt-p
              • Vl-whilestmt-p
              • Vl-waitstmt-p
              • Vl-nullstmt-p
              • Vl-ifstmt-p
              • Vl-forstmt-p
              • Vl-dostmt-p
              • Vl-casestmt-p
              • Vl-callstmt-p
              • Vl-exprlistlist
            • Modnamespace
            • Flat-warnings
            • Reordering-by-name
            • Datatype-tools
            • Syscalls
            • Allexprs
            • Lvalues
            • Port-tools
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Stmt-tools

    Vl-rebuild-caselist

    Signature
    (vl-rebuild-caselist x new-exprs new-stmts) → new-x
    Arguments
    x — Guard (vl-caselist-p x).
    new-exprs — Guard (vl-exprlist-p new-exprs).
    new-stmts — Guard (vl-stmtlist-p new-stmts).
    Returns
    new-x — Type (vl-caselist-p new-x).

    Definitions and Theorems

    Function: vl-rebuild-caselist

    (defun vl-rebuild-caselist (x new-exprs new-stmts)
     (declare (xargs :guard (and (vl-caselist-p x)
                                 (vl-exprlist-p new-exprs)
                                 (vl-stmtlist-p new-stmts))))
     (declare
         (xargs :guard
                (let ((x (vl-caselist-fix x)))
                  (and (same-lengthp new-exprs (flatten (alist-keys x)))
                       (same-lengthp new-stmts x)))))
     (let ((__function__ 'vl-rebuild-caselist))
      (declare (ignorable __function__))
      (b*
       ((x (vl-caselist-fix x))
        ((when (atom x)) nil)
        ((cons match-exprs ?stmt) (car x))
        (exprs1
         (mbe
            :logic
            (append
                 (vl-exprlist-fix (first-n (len match-exprs) new-exprs))
                 (acl2::final-cdr (caar x)))
            :exec
            (if (true-listp (caar x))
                (first-n (len match-exprs) new-exprs)
              (append (first-n (len match-exprs) new-exprs)
                      (acl2::final-cdr (caar x))))))
        (stmt1 (vl-stmt-fix (car new-stmts)))
        (exprs2 (rest-n (len match-exprs) new-exprs)))
       (cons (cons exprs1 stmt1)
             (vl-rebuild-caselist (cdr x)
                                  exprs2 (cdr new-stmts))))))

    Theorem: vl-caselist-p-of-vl-rebuild-caselist

    (defthm vl-caselist-p-of-vl-rebuild-caselist
      (b* ((new-x (vl-rebuild-caselist x new-exprs new-stmts)))
        (vl-caselist-p new-x))
      :rule-classes :rewrite)

    Theorem: vl-rebuild-caselist-identity

    (defthm vl-rebuild-caselist-identity
      (implies (vl-caselist-p x)
               (equal (vl-rebuild-caselist x (flatten (alist-keys x))
                                           (alist-vals x))
                      x)))

    Theorem: alist-vals-of-vl-rebuild-caselist

    (defthm alist-vals-of-vl-rebuild-caselist
      (implies (and (vl-caselist-p x)
                    (equal (len (alist-keys x))
                           (len stmts)))
               (equal (alist-vals (vl-rebuild-caselist x exprs stmts))
                      (vl-stmtlist-fix stmts))))

    Theorem: flatten-of-alist-keys-of-vl-rebuild-caselist

    (defthm flatten-of-alist-keys-of-vl-rebuild-caselist
     (implies
       (and (vl-caselist-p x)
            (same-lengthp exprs (flatten (alist-keys x))))
       (equal (flatten (alist-keys (vl-rebuild-caselist x exprs stmts)))
              (vl-exprlist-fix (list-fix exprs)))))

    Theorem: vl-rebuild-caselist-of-vl-caselist-fix-x

    (defthm vl-rebuild-caselist-of-vl-caselist-fix-x
      (equal (vl-rebuild-caselist (vl-caselist-fix x)
                                  new-exprs new-stmts)
             (vl-rebuild-caselist x new-exprs new-stmts)))

    Theorem: vl-rebuild-caselist-vl-caselist-equiv-congruence-on-x

    (defthm vl-rebuild-caselist-vl-caselist-equiv-congruence-on-x
     (implies (vl-caselist-equiv x x-equiv)
              (equal (vl-rebuild-caselist x new-exprs new-stmts)
                     (vl-rebuild-caselist x-equiv new-exprs new-stmts)))
     :rule-classes :congruence)

    Theorem: vl-rebuild-caselist-of-vl-exprlist-fix-new-exprs

    (defthm vl-rebuild-caselist-of-vl-exprlist-fix-new-exprs
      (equal (vl-rebuild-caselist x (vl-exprlist-fix new-exprs)
                                  new-stmts)
             (vl-rebuild-caselist x new-exprs new-stmts)))

    Theorem: vl-rebuild-caselist-vl-exprlist-equiv-congruence-on-new-exprs

    (defthm
          vl-rebuild-caselist-vl-exprlist-equiv-congruence-on-new-exprs
     (implies (vl-exprlist-equiv new-exprs new-exprs-equiv)
              (equal (vl-rebuild-caselist x new-exprs new-stmts)
                     (vl-rebuild-caselist x new-exprs-equiv new-stmts)))
     :rule-classes :congruence)

    Theorem: vl-rebuild-caselist-of-vl-stmtlist-fix-new-stmts

    (defthm vl-rebuild-caselist-of-vl-stmtlist-fix-new-stmts
      (equal
           (vl-rebuild-caselist x new-exprs (vl-stmtlist-fix new-stmts))
           (vl-rebuild-caselist x new-exprs new-stmts)))

    Theorem: vl-rebuild-caselist-vl-stmtlist-equiv-congruence-on-new-stmts

    (defthm
          vl-rebuild-caselist-vl-stmtlist-equiv-congruence-on-new-stmts
     (implies (vl-stmtlist-equiv new-stmts new-stmts-equiv)
              (equal (vl-rebuild-caselist x new-exprs new-stmts)
                     (vl-rebuild-caselist x new-exprs new-stmts-equiv)))
     :rule-classes :congruence)