		Search-engine friendly clone of the ACL2 documentation.

Vl-lucidstate-mark

Vl-luciddb-mark

Signature
(vl-luciddb-mark mtype key occ db ctx) → new-db
Arguments: mtype — Guard (member mtype '(:used :set)).; key — Guard (vl-lucidkey-p key).; occ — Guard (vl-lucidocc-p occ).; db — Guard (vl-luciddb-p db).; ctx — Guard (vl-context1-p ctx).
Returns: new-db — Type (vl-luciddb-p new-db).

Definitions and Theorems

Function: vl-luciddb-mark

(defun vl-luciddb-mark (mtype key occ db ctx)
  (declare (xargs :guard (and (member mtype '(:used :set))
                              (vl-lucidkey-p key)
                              (vl-lucidocc-p occ)
                              (vl-luciddb-p db)
                              (vl-context1-p ctx))))
  (let ((__function__ 'vl-luciddb-mark))
    (declare (ignorable __function__))
    (b* ((db (vl-luciddb-fix db))
         (occ (vl-lucidocc-fix occ))
         (key (vl-lucidkey-fix key))
         (ctx (vl-context1-fix ctx))
         (val (cdr (hons-get key db)))
         ((unless val)
          (let ((err (list __function__ ctx)))
            (hons-acons key
                        (change-vl-lucidval *vl-empty-lucidval*
                                            :used (list occ)
                                            :errors (list err))
                        db)))
         ((vl-lucidval val))
         (val (if (eq mtype :used)
                  (change-vl-lucidval val
                                      :used (cons occ val.used))
                (change-vl-lucidval val
                                    :set (cons occ val.set))))
         (db (hons-acons key val db)))
      db)))

Theorem: vl-luciddb-p-of-vl-luciddb-mark

(defthm vl-luciddb-p-of-vl-luciddb-mark
  (b* ((new-db (vl-luciddb-mark mtype key occ db ctx)))
    (vl-luciddb-p new-db))
  :rule-classes :rewrite)

Theorem: vl-luciddb-mark-of-vl-lucidkey-fix-key

(defthm vl-luciddb-mark-of-vl-lucidkey-fix-key
  (equal (vl-luciddb-mark mtype (vl-lucidkey-fix key)
                          occ db ctx)
         (vl-luciddb-mark mtype key occ db ctx)))

Theorem: vl-luciddb-mark-vl-lucidkey-equiv-congruence-on-key

(defthm vl-luciddb-mark-vl-lucidkey-equiv-congruence-on-key
  (implies (vl-lucidkey-equiv key key-equiv)
           (equal (vl-luciddb-mark mtype key occ db ctx)
                  (vl-luciddb-mark mtype key-equiv occ db ctx)))
  :rule-classes :congruence)

Theorem: vl-luciddb-mark-of-vl-lucidocc-fix-occ

(defthm vl-luciddb-mark-of-vl-lucidocc-fix-occ
  (equal (vl-luciddb-mark mtype key (vl-lucidocc-fix occ)
                          db ctx)
         (vl-luciddb-mark mtype key occ db ctx)))

Theorem: vl-luciddb-mark-vl-lucidocc-equiv-congruence-on-occ

(defthm vl-luciddb-mark-vl-lucidocc-equiv-congruence-on-occ
  (implies (vl-lucidocc-equiv occ occ-equiv)
           (equal (vl-luciddb-mark mtype key occ db ctx)
                  (vl-luciddb-mark mtype key occ-equiv db ctx)))
  :rule-classes :congruence)

Theorem: vl-luciddb-mark-of-vl-luciddb-fix-db

(defthm vl-luciddb-mark-of-vl-luciddb-fix-db
  (equal (vl-luciddb-mark mtype key occ (vl-luciddb-fix db)
                          ctx)
         (vl-luciddb-mark mtype key occ db ctx)))

Theorem: vl-luciddb-mark-vl-luciddb-equiv-congruence-on-db

(defthm vl-luciddb-mark-vl-luciddb-equiv-congruence-on-db
  (implies (vl-luciddb-equiv db db-equiv)
           (equal (vl-luciddb-mark mtype key occ db ctx)
                  (vl-luciddb-mark mtype key occ db-equiv ctx)))
  :rule-classes :congruence)

Theorem: vl-luciddb-mark-of-vl-context1-fix-ctx

(defthm vl-luciddb-mark-of-vl-context1-fix-ctx
  (equal (vl-luciddb-mark mtype key occ db (vl-context1-fix ctx))
         (vl-luciddb-mark mtype key occ db ctx)))

Theorem: vl-luciddb-mark-vl-context1-equiv-congruence-on-ctx

(defthm vl-luciddb-mark-vl-context1-equiv-congruence-on-ctx
  (implies (vl-context1-equiv ctx ctx-equiv)
           (equal (vl-luciddb-mark mtype key occ db ctx)
                  (vl-luciddb-mark mtype key occ db ctx-equiv)))
  :rule-classes :congruence)