		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-sort-blockitems-aux

Signature
(vl-sort-blockitems-aux x vardecls-acc paramdecls-acc imports-acc) → (mv vardecls paramdecls imports)
Arguments: x — Guard (vl-blockitemlist-p x).; vardecls-acc — Guard (vl-vardecllist-p vardecls-acc).; paramdecls-acc — Guard (vl-paramdecllist-p paramdecls-acc).; imports-acc — Guard (vl-importlist-p imports-acc).
Returns: vardecls — Type (vl-vardecllist-p vardecls).; paramdecls — Type (vl-paramdecllist-p paramdecls).; imports — Type (vl-importlist-p imports).

Definitions and Theorems

Function: vl-sort-blockitems-aux

(defun vl-sort-blockitems-aux
       (x vardecls-acc paramdecls-acc imports-acc)
 (declare (xargs :guard (and (vl-blockitemlist-p x)
                             (vl-vardecllist-p vardecls-acc)
                             (vl-paramdecllist-p paramdecls-acc)
                             (vl-importlist-p imports-acc))))
 (let ((__function__ 'vl-sort-blockitems-aux))
   (declare (ignorable __function__))
   (b*
    (((when (atom x))
      (mv (rev (vl-vardecllist-fix vardecls-acc))
          (rev (vl-paramdecllist-fix paramdecls-acc))
          (rev (vl-importlist-fix imports-acc))))
     (x1 (vl-blockitem-fix (car x)))
     ((mv vardecls-acc paramdecls-acc imports-acc)
      (case (tag x1)
            (:vl-vardecl (mv (cons x1 vardecls-acc)
                             paramdecls-acc imports-acc))
            (:vl-paramdecl (mv vardecls-acc (cons x1 paramdecls-acc)
                               imports-acc))
            (otherwise (mv vardecls-acc paramdecls-acc
                           (cons x1 imports-acc))))))
    (vl-sort-blockitems-aux (cdr x)
                            vardecls-acc
                            paramdecls-acc imports-acc))))

Theorem: vl-vardecllist-p-of-vl-sort-blockitems-aux.vardecls

(defthm vl-vardecllist-p-of-vl-sort-blockitems-aux.vardecls
  (b* (((mv ?vardecls ?paramdecls ?imports)
        (vl-sort-blockitems-aux x vardecls-acc
                                paramdecls-acc imports-acc)))
    (vl-vardecllist-p vardecls))
  :rule-classes :rewrite)

Theorem: vl-paramdecllist-p-of-vl-sort-blockitems-aux.paramdecls

(defthm vl-paramdecllist-p-of-vl-sort-blockitems-aux.paramdecls
  (b* (((mv ?vardecls ?paramdecls ?imports)
        (vl-sort-blockitems-aux x vardecls-acc
                                paramdecls-acc imports-acc)))
    (vl-paramdecllist-p paramdecls))
  :rule-classes :rewrite)

Theorem: vl-importlist-p-of-vl-sort-blockitems-aux.imports

(defthm vl-importlist-p-of-vl-sort-blockitems-aux.imports
  (b* (((mv ?vardecls ?paramdecls ?imports)
        (vl-sort-blockitems-aux x vardecls-acc
                                paramdecls-acc imports-acc)))
    (vl-importlist-p imports))
  :rule-classes :rewrite)

Theorem: vl-sort-blockitems-aux-of-vl-blockitemlist-fix-x

(defthm vl-sort-blockitems-aux-of-vl-blockitemlist-fix-x
 (equal
    (vl-sort-blockitems-aux (vl-blockitemlist-fix x)
                            vardecls-acc paramdecls-acc imports-acc)
    (vl-sort-blockitems-aux x vardecls-acc
                            paramdecls-acc imports-acc)))

Theorem: vl-sort-blockitems-aux-vl-blockitemlist-equiv-congruence-on-x

(defthm
      vl-sort-blockitems-aux-vl-blockitemlist-equiv-congruence-on-x
 (implies
  (vl-blockitemlist-equiv x x-equiv)
  (equal
    (vl-sort-blockitems-aux x
                            vardecls-acc paramdecls-acc imports-acc)
    (vl-sort-blockitems-aux x-equiv vardecls-acc
                            paramdecls-acc imports-acc)))
 :rule-classes :congruence)

Theorem: vl-sort-blockitems-aux-of-vl-vardecllist-fix-vardecls-acc

(defthm vl-sort-blockitems-aux-of-vl-vardecllist-fix-vardecls-acc
  (equal (vl-sort-blockitems-aux x (vl-vardecllist-fix vardecls-acc)
                                 paramdecls-acc imports-acc)
         (vl-sort-blockitems-aux x vardecls-acc
                                 paramdecls-acc imports-acc)))

Theorem: vl-sort-blockitems-aux-vl-vardecllist-equiv-congruence-on-vardecls-acc

(defthm
 vl-sort-blockitems-aux-vl-vardecllist-equiv-congruence-on-vardecls-acc
 (implies
  (vl-vardecllist-equiv vardecls-acc vardecls-acc-equiv)
  (equal
    (vl-sort-blockitems-aux x
                            vardecls-acc paramdecls-acc imports-acc)
    (vl-sort-blockitems-aux x vardecls-acc-equiv
                            paramdecls-acc imports-acc)))
 :rule-classes :congruence)

Theorem: vl-sort-blockitems-aux-of-vl-paramdecllist-fix-paramdecls-acc

(defthm
      vl-sort-blockitems-aux-of-vl-paramdecllist-fix-paramdecls-acc
  (equal
       (vl-sort-blockitems-aux x vardecls-acc
                               (vl-paramdecllist-fix paramdecls-acc)
                               imports-acc)
       (vl-sort-blockitems-aux x vardecls-acc
                               paramdecls-acc imports-acc)))

Theorem: vl-sort-blockitems-aux-vl-paramdecllist-equiv-congruence-on-paramdecls-acc

(defthm
 vl-sort-blockitems-aux-vl-paramdecllist-equiv-congruence-on-paramdecls-acc
 (implies
  (vl-paramdecllist-equiv paramdecls-acc paramdecls-acc-equiv)
  (equal
    (vl-sort-blockitems-aux x
                            vardecls-acc paramdecls-acc imports-acc)
    (vl-sort-blockitems-aux x vardecls-acc
                            paramdecls-acc-equiv imports-acc)))
 :rule-classes :congruence)

Theorem: vl-sort-blockitems-aux-of-vl-importlist-fix-imports-acc

(defthm vl-sort-blockitems-aux-of-vl-importlist-fix-imports-acc
  (equal (vl-sort-blockitems-aux x vardecls-acc paramdecls-acc
                                 (vl-importlist-fix imports-acc))
         (vl-sort-blockitems-aux x vardecls-acc
                                 paramdecls-acc imports-acc)))

Theorem: vl-sort-blockitems-aux-vl-importlist-equiv-congruence-on-imports-acc

(defthm
 vl-sort-blockitems-aux-vl-importlist-equiv-congruence-on-imports-acc
 (implies
  (vl-importlist-equiv imports-acc imports-acc-equiv)
  (equal
    (vl-sort-blockitems-aux x
                            vardecls-acc paramdecls-acc imports-acc)
    (vl-sort-blockitems-aux x vardecls-acc
                            paramdecls-acc imports-acc-equiv)))
 :rule-classes :congruence)