Extend the lexscopes with a local declaration.
(vl-lexscopes-declare-name name decl scopes warnings) → (mv scopes warnings)
Function:
(defun vl-lexscopes-declare-name (name decl scopes warnings) (declare (xargs :guard (and (stringp name) (acl2::any-p decl) (vl-lexscopes-p scopes) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-lexscopes-declare-name)) (declare (ignorable __function__)) (b* ((name (string-fix name)) (scopes (vl-lexscopes-fix scopes)) (warnings (vl-warninglist-fix warnings)) ((when (atom scopes)) (raise "Expected at least one scope.") (mv scopes warnings)) (scope1 (car scopes)) (entry (vl-lexscope-find name scope1)) ((unless entry) (mv (cons (hons-acons name (make-vl-lexscope-entry :decl decl :direct-pkg nil :wildpkgs nil) scope1) (cdr scopes)) warnings)) ((vl-lexscope-entry entry)) (warnings (if entry.direct-pkg (fatal :type :vl-name-clash :msg "~a0: can't declare ~s1 after importing it from ~s2." :args (list decl name entry.direct-pkg)) (ok))) (new-entry (change-vl-lexscope-entry entry :decl (or entry.decl decl))) (new-scope1 (hons-acons name new-entry scope1)) (new-scopes (cons new-scope1 (cdr scopes)))) (mv new-scopes warnings))))
Theorem:
(defthm vl-lexscopes-p-of-vl-lexscopes-declare-name.scopes (b* (((mv ?scopes ?warnings) (vl-lexscopes-declare-name name decl scopes warnings))) (vl-lexscopes-p scopes)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-lexscopes-declare-name.warnings (b* (((mv ?scopes ?warnings) (vl-lexscopes-declare-name name decl scopes warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-lexscopes-declare-name-of-str-fix-name (equal (vl-lexscopes-declare-name (str-fix name) decl scopes warnings) (vl-lexscopes-declare-name name decl scopes warnings)))
Theorem:
(defthm vl-lexscopes-declare-name-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-lexscopes-declare-name name decl scopes warnings) (vl-lexscopes-declare-name name-equiv decl scopes warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-lexscopes-declare-name-of-identity-decl (equal (vl-lexscopes-declare-name name (identity decl) scopes warnings) (vl-lexscopes-declare-name name decl scopes warnings)))
Theorem:
(defthm vl-lexscopes-declare-name-equal-congruence-on-decl (implies (equal decl decl-equiv) (equal (vl-lexscopes-declare-name name decl scopes warnings) (vl-lexscopes-declare-name name decl-equiv scopes warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-lexscopes-declare-name-of-vl-lexscopes-fix-scopes (equal (vl-lexscopes-declare-name name decl (vl-lexscopes-fix scopes) warnings) (vl-lexscopes-declare-name name decl scopes warnings)))
Theorem:
(defthm vl-lexscopes-declare-name-vl-lexscopes-equiv-congruence-on-scopes (implies (vl-lexscopes-equiv scopes scopes-equiv) (equal (vl-lexscopes-declare-name name decl scopes warnings) (vl-lexscopes-declare-name name decl scopes-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-lexscopes-declare-name-of-vl-warninglist-fix-warnings (equal (vl-lexscopes-declare-name name decl scopes (vl-warninglist-fix warnings)) (vl-lexscopes-declare-name name decl scopes warnings)))
Theorem:
(defthm vl-lexscopes-declare-name-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-lexscopes-declare-name name decl scopes warnings) (vl-lexscopes-declare-name name decl scopes warnings-equiv))) :rule-classes :congruence)