		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-mark-simple

Signature
(vl-lucid-mark-simple mtype name ss st ctx) → new-st
Arguments: mtype — Guard (member mtype '(:used :set)).; name — Guard (stringp name).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).; ctx — Guard (vl-lucidctx-p ctx).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-lucid-mark-simple

(defun vl-lucid-mark-simple (mtype name ss st ctx)
  (declare (xargs :guard (and (member mtype '(:used :set))
                              (stringp name)
                              (vl-scopestack-p ss)
                              (vl-lucidstate-p st)
                              (vl-lucidctx-p ctx))))
  (let ((__function__ 'vl-lucid-mark-simple))
    (declare (ignorable __function__))
    (b* ((st (vl-lucidstate-fix st))
         ((mv item item-ss)
          (vl-scopestack-find-item/ss name ss))
         ((unless item)
          (cw "Warning: missing item ~s0 in ~x1.~%"
              name (vl-scopestack->path ss))
          st)
         (key (make-vl-lucidkey :item item
                                :scopestack item-ss))
         (occ (make-vl-lucidocc-solo :ctx ctx)))
      (vl-lucidstate-mark mtype key occ st ctx))))

Theorem: vl-lucidstate-p-of-vl-lucid-mark-simple

(defthm vl-lucidstate-p-of-vl-lucid-mark-simple
  (b* ((new-st (vl-lucid-mark-simple mtype name ss st ctx)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-lucid-mark-simple-of-str-fix-name

(defthm vl-lucid-mark-simple-of-str-fix-name
  (equal (vl-lucid-mark-simple mtype (str-fix name)
                               ss st ctx)
         (vl-lucid-mark-simple mtype name ss st ctx)))

Theorem: vl-lucid-mark-simple-streqv-congruence-on-name

(defthm vl-lucid-mark-simple-streqv-congruence-on-name
 (implies (streqv name name-equiv)
          (equal (vl-lucid-mark-simple mtype name ss st ctx)
                 (vl-lucid-mark-simple mtype name-equiv ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-lucid-mark-simple-of-vl-scopestack-fix-ss

(defthm vl-lucid-mark-simple-of-vl-scopestack-fix-ss
  (equal (vl-lucid-mark-simple mtype name (vl-scopestack-fix ss)
                               st ctx)
         (vl-lucid-mark-simple mtype name ss st ctx)))

Theorem: vl-lucid-mark-simple-vl-scopestack-equiv-congruence-on-ss

(defthm vl-lucid-mark-simple-vl-scopestack-equiv-congruence-on-ss
 (implies (vl-scopestack-equiv ss ss-equiv)
          (equal (vl-lucid-mark-simple mtype name ss st ctx)
                 (vl-lucid-mark-simple mtype name ss-equiv st ctx)))
 :rule-classes :congruence)

Theorem: vl-lucid-mark-simple-of-vl-lucidstate-fix-st

(defthm vl-lucid-mark-simple-of-vl-lucidstate-fix-st
  (equal (vl-lucid-mark-simple mtype name ss (vl-lucidstate-fix st)
                               ctx)
         (vl-lucid-mark-simple mtype name ss st ctx)))

Theorem: vl-lucid-mark-simple-vl-lucidstate-equiv-congruence-on-st

(defthm vl-lucid-mark-simple-vl-lucidstate-equiv-congruence-on-st
 (implies (vl-lucidstate-equiv st st-equiv)
          (equal (vl-lucid-mark-simple mtype name ss st ctx)
                 (vl-lucid-mark-simple mtype name ss st-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-lucid-mark-simple-of-vl-lucidctx-fix-ctx

(defthm vl-lucid-mark-simple-of-vl-lucidctx-fix-ctx
  (equal
       (vl-lucid-mark-simple mtype name ss st (vl-lucidctx-fix ctx))
       (vl-lucid-mark-simple mtype name ss st ctx)))

Theorem: vl-lucid-mark-simple-vl-lucidctx-equiv-congruence-on-ctx

(defthm vl-lucid-mark-simple-vl-lucidctx-equiv-congruence-on-ctx
 (implies (vl-lucidctx-equiv ctx ctx-equiv)
          (equal (vl-lucid-mark-simple mtype name ss st ctx)
                 (vl-lucid-mark-simple mtype name ss st ctx-equiv)))
 :rule-classes :congruence)