Fixing function for vl-ansi-portdecl structures.
(vl-ansi-portdecl-fix x) → new-x
Function:
(defun vl-ansi-portdecl-fix$inline (x) (declare (xargs :guard (vl-ansi-portdecl-p x))) (let ((__function__ 'vl-ansi-portdecl-fix)) (declare (ignorable __function__)) (mbe :logic (b* ((name (str-fix (cdr (std::da-nth 0 (cdr x))))) (loc (vl-location-fix (cdr (std::da-nth 1 (cdr x))))) (dir (vl-maybe-direction-fix (cdr (std::da-nth 2 (cdr x))))) (typename (maybe-string-fix (cdr (std::da-nth 3 (cdr x))))) (type (vl-maybe-datatype-fix (cdr (std::da-nth 4 (cdr x))))) (pdims (vl-dimensionlist-fix (cdr (std::da-nth 5 (cdr x))))) (udims (vl-dimensionlist-fix (cdr (std::da-nth 6 (cdr x))))) (nettype (vl-maybe-nettypename-fix (cdr (std::da-nth 7 (cdr x))))) (varp (acl2::bool-fix (cdr (std::da-nth 8 (cdr x))))) (modport (maybe-string-fix (cdr (std::da-nth 9 (cdr x))))) (signedness (vl-maybe-exprsign-fix (cdr (std::da-nth 10 (cdr x))))) (atts (vl-atts-fix (cdr (std::da-nth 11 (cdr x)))))) (cons :vl-ansi-portdecl (list (cons 'name name) (cons 'loc loc) (cons 'dir dir) (cons 'typename typename) (cons 'type type) (cons 'pdims pdims) (cons 'udims udims) (cons 'nettype nettype) (cons 'varp varp) (cons 'modport modport) (cons 'signedness signedness) (cons 'atts atts)))) :exec x)))
Theorem:
(defthm vl-ansi-portdecl-p-of-vl-ansi-portdecl-fix (b* ((new-x (vl-ansi-portdecl-fix$inline x))) (vl-ansi-portdecl-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-ansi-portdecl-fix-when-vl-ansi-portdecl-p (implies (vl-ansi-portdecl-p x) (equal (vl-ansi-portdecl-fix x) x)))
Function:
(defun vl-ansi-portdecl-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (vl-ansi-portdecl-p acl2::x) (vl-ansi-portdecl-p acl2::y)))) (equal (vl-ansi-portdecl-fix acl2::x) (vl-ansi-portdecl-fix acl2::y)))
Theorem:
(defthm vl-ansi-portdecl-equiv-is-an-equivalence (and (booleanp (vl-ansi-portdecl-equiv x y)) (vl-ansi-portdecl-equiv x x) (implies (vl-ansi-portdecl-equiv x y) (vl-ansi-portdecl-equiv y x)) (implies (and (vl-ansi-portdecl-equiv x y) (vl-ansi-portdecl-equiv y z)) (vl-ansi-portdecl-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm vl-ansi-portdecl-equiv-implies-equal-vl-ansi-portdecl-fix-1 (implies (vl-ansi-portdecl-equiv acl2::x x-equiv) (equal (vl-ansi-portdecl-fix acl2::x) (vl-ansi-portdecl-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm vl-ansi-portdecl-fix-under-vl-ansi-portdecl-equiv (vl-ansi-portdecl-equiv (vl-ansi-portdecl-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-vl-ansi-portdecl-fix-1-forward-to-vl-ansi-portdecl-equiv (implies (equal (vl-ansi-portdecl-fix acl2::x) acl2::y) (vl-ansi-portdecl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-vl-ansi-portdecl-fix-2-forward-to-vl-ansi-portdecl-equiv (implies (equal acl2::x (vl-ansi-portdecl-fix acl2::y)) (vl-ansi-portdecl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm vl-ansi-portdecl-equiv-of-vl-ansi-portdecl-fix-1-forward (implies (vl-ansi-portdecl-equiv (vl-ansi-portdecl-fix acl2::x) acl2::y) (vl-ansi-portdecl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm vl-ansi-portdecl-equiv-of-vl-ansi-portdecl-fix-2-forward (implies (vl-ansi-portdecl-equiv acl2::x (vl-ansi-portdecl-fix acl2::y)) (vl-ansi-portdecl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)