		Search-engine friendly clone of the ACL2 documentation.

Vl-scope-luciddb-init

Vl-scope-luciddb-init-aux

Signature
(vl-scope-luciddb-init-aux locals ss db) → new-db
Arguments: locals — The local variables declared in some scope.
Guard (vl-scopeitem-alist-p locals).; 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 the variables in locals.
Type (vl-luciddb-p new-db).

Definitions and Theorems

Function: vl-scope-luciddb-init-aux

(defun vl-scope-luciddb-init-aux (locals ss db)
  (declare (xargs :guard (and (vl-scopeitem-alist-p locals)
                              (vl-scopestack-p ss)
                              (vl-luciddb-p db))))
  (let ((__function__ 'vl-scope-luciddb-init-aux))
    (declare (ignorable __function__))
    (b* ((locals (vl-scopeitem-alist-fix locals))
         ((when (atom locals))
          (vl-luciddb-fix db))
         ((cons ?name item) (car locals))
         (key (make-vl-lucidkey :item item
                                :scopestack ss))
         (db (hons-acons key *vl-empty-lucidval* db)))
      (vl-scope-luciddb-init-aux (cdr locals)
                                 ss db))))

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

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

Theorem: vl-scope-luciddb-init-aux-of-vl-scopeitem-alist-fix-locals

(defthm vl-scope-luciddb-init-aux-of-vl-scopeitem-alist-fix-locals
  (equal (vl-scope-luciddb-init-aux (vl-scopeitem-alist-fix locals)
                                    ss db)
         (vl-scope-luciddb-init-aux locals ss db)))

Theorem: vl-scope-luciddb-init-aux-vl-scopeitem-alist-equiv-congruence-on-locals

(defthm
 vl-scope-luciddb-init-aux-vl-scopeitem-alist-equiv-congruence-on-locals
 (implies (vl-scopeitem-alist-equiv locals locals-equiv)
          (equal (vl-scope-luciddb-init-aux locals ss db)
                 (vl-scope-luciddb-init-aux locals-equiv ss db)))
 :rule-classes :congruence)

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

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

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

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

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

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

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

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