		Search-engine friendly clone of the ACL2 documentation.

Vl-lucidstate-init

Vl-scope-luciddb-init

Initialize variables for a scope.

Signature
(vl-scope-luciddb-init x ss db) → new-db
Arguments: x — Current scope we're processing, already added to the scopestack.
Guard (vl-scope-p x).; ss — Scopestack for our current location.
Guard (vl-scopestack-p ss).; db — Database we're initializing.
Guard (vl-luciddb-p db).
Returns: new-db — Database extended with all variables from this scope.
Type (vl-luciddb-p new-db).

The scopeinfo for x has locals, imports, and star-packages, but we only want the locals: any imports or star-packages are of course relevant for looking up variables, but those variables will have their own keys created when we process their packages, etc.

Definitions and Theorems

Function: vl-scope-luciddb-init

(defun vl-scope-luciddb-init (x ss db)
  (declare (xargs :guard (and (vl-scope-p x)
                              (vl-scopestack-p ss)
                              (vl-luciddb-p db))))
  (let ((__function__ 'vl-scope-luciddb-init))
    (declare (ignorable __function__))
    (b* ((x (vl-scope-fix x))
         (info (vl-scope->scopeinfo x (vl-scopestack->design ss)))
         (locals (vl-scopeinfo->locals info)))
      (vl-scope-luciddb-init-aux locals ss db))))

Theorem: vl-luciddb-p-of-vl-scope-luciddb-init

(defthm vl-luciddb-p-of-vl-scope-luciddb-init
  (b* ((new-db (vl-scope-luciddb-init x ss db)))
    (vl-luciddb-p new-db))
  :rule-classes :rewrite)

Theorem: vl-scope-luciddb-init-of-vl-scope-fix-x

(defthm vl-scope-luciddb-init-of-vl-scope-fix-x
  (equal (vl-scope-luciddb-init (vl-scope-fix x)
                                ss db)
         (vl-scope-luciddb-init x ss db)))

Theorem: vl-scope-luciddb-init-vl-scope-equiv-congruence-on-x

(defthm vl-scope-luciddb-init-vl-scope-equiv-congruence-on-x
  (implies (vl-scope-equiv x x-equiv)
           (equal (vl-scope-luciddb-init x ss db)
                  (vl-scope-luciddb-init x-equiv ss db)))
  :rule-classes :congruence)

Theorem: vl-scope-luciddb-init-of-vl-scopestack-fix-ss

(defthm vl-scope-luciddb-init-of-vl-scopestack-fix-ss
  (equal (vl-scope-luciddb-init x (vl-scopestack-fix ss)
                                db)
         (vl-scope-luciddb-init x ss db)))

Theorem: vl-scope-luciddb-init-vl-scopestack-equiv-congruence-on-ss

(defthm vl-scope-luciddb-init-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-scope-luciddb-init x ss db)
                  (vl-scope-luciddb-init x ss-equiv db)))
  :rule-classes :congruence)

Theorem: vl-scope-luciddb-init-of-vl-luciddb-fix-db

(defthm vl-scope-luciddb-init-of-vl-luciddb-fix-db
  (equal (vl-scope-luciddb-init x ss (vl-luciddb-fix db))
         (vl-scope-luciddb-init x ss db)))

Theorem: vl-scope-luciddb-init-vl-luciddb-equiv-congruence-on-db

(defthm vl-scope-luciddb-init-vl-luciddb-equiv-congruence-on-db
  (implies (vl-luciddb-equiv db db-equiv)
           (equal (vl-scope-luciddb-init x ss db)
                  (vl-scope-luciddb-init x ss db-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-scope-luciddb-init-aux