		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-hidsolo-mark

Signature
(vl-hidsolo-mark mtype force-bogusp x ss st ctx) → new-st
Arguments: mtype — Guard (member mtype '(:used :set)).; force-bogusp — Guard (booleanp force-bogusp).; x — Guard (vl-scopeexpr-p x).; 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-hidsolo-mark

(defun vl-hidsolo-mark (mtype force-bogusp x ss st ctx)
  (declare (xargs :guard (and (member mtype '(:used :set))
                              (booleanp force-bogusp)
                              (vl-scopeexpr-p x)
                              (vl-scopestack-p ss)
                              (vl-lucidstate-p st)
                              (vl-lucidctx-p ctx))))
  (let ((__function__ 'vl-hidsolo-mark))
    (declare (ignorable __function__))
    (b* (((mv err trace ?scopectx tail)
          (vl-follow-scopeexpr x ss))
         ((when err)
          (b* (((vl-lucidstate st)))
            (change-vl-lucidstate st
                                  :warnings st.warnings)))
         ((cons (vl-hidstep step) rest) trace)
         (key (make-vl-lucidkey
                   :item step.item
                   :scopestack (vl-normalize-scopestack step.ss)))
         (occ (if (and (not force-bogusp)
                       (vl-hidexpr-case tail :end))
                  (make-vl-lucidocc-solo :ctx ctx)
                (make-vl-lucidocc-tail :ctx ctx)))
         (st (vl-hidtrace-mark-interfaces mtype rest st ctx))
         (st (vl-lucidstate-mark mtype key occ st ctx)))
      st)))

Theorem: vl-lucidstate-p-of-vl-hidsolo-mark

(defthm vl-lucidstate-p-of-vl-hidsolo-mark
  (b* ((new-st (vl-hidsolo-mark mtype force-bogusp x ss st ctx)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-hidsolo-mark-of-bool-fix-force-bogusp

(defthm vl-hidsolo-mark-of-bool-fix-force-bogusp
  (equal (vl-hidsolo-mark mtype (acl2::bool-fix force-bogusp)
                          x ss st ctx)
         (vl-hidsolo-mark mtype force-bogusp x ss st ctx)))

Theorem: vl-hidsolo-mark-iff-congruence-on-force-bogusp

(defthm vl-hidsolo-mark-iff-congruence-on-force-bogusp
 (implies
     (iff force-bogusp force-bogusp-equiv)
     (equal (vl-hidsolo-mark mtype force-bogusp x ss st ctx)
            (vl-hidsolo-mark mtype force-bogusp-equiv x ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-hidsolo-mark-of-vl-scopeexpr-fix-x

(defthm vl-hidsolo-mark-of-vl-scopeexpr-fix-x
  (equal (vl-hidsolo-mark mtype force-bogusp (vl-scopeexpr-fix x)
                          ss st ctx)
         (vl-hidsolo-mark mtype force-bogusp x ss st ctx)))

Theorem: vl-hidsolo-mark-vl-scopeexpr-equiv-congruence-on-x

(defthm vl-hidsolo-mark-vl-scopeexpr-equiv-congruence-on-x
 (implies
     (vl-scopeexpr-equiv x x-equiv)
     (equal (vl-hidsolo-mark mtype force-bogusp x ss st ctx)
            (vl-hidsolo-mark mtype force-bogusp x-equiv ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-hidsolo-mark-of-vl-scopestack-fix-ss

(defthm vl-hidsolo-mark-of-vl-scopestack-fix-ss
  (equal (vl-hidsolo-mark mtype
                          force-bogusp x (vl-scopestack-fix ss)
                          st ctx)
         (vl-hidsolo-mark mtype force-bogusp x ss st ctx)))

Theorem: vl-hidsolo-mark-vl-scopestack-equiv-congruence-on-ss

(defthm vl-hidsolo-mark-vl-scopestack-equiv-congruence-on-ss
 (implies
     (vl-scopestack-equiv ss ss-equiv)
     (equal (vl-hidsolo-mark mtype force-bogusp x ss st ctx)
            (vl-hidsolo-mark mtype force-bogusp x ss-equiv st ctx)))
 :rule-classes :congruence)

Theorem: vl-hidsolo-mark-of-vl-lucidstate-fix-st

(defthm vl-hidsolo-mark-of-vl-lucidstate-fix-st
  (equal (vl-hidsolo-mark mtype
                          force-bogusp x ss (vl-lucidstate-fix st)
                          ctx)
         (vl-hidsolo-mark mtype force-bogusp x ss st ctx)))

Theorem: vl-hidsolo-mark-vl-lucidstate-equiv-congruence-on-st

(defthm vl-hidsolo-mark-vl-lucidstate-equiv-congruence-on-st
 (implies
     (vl-lucidstate-equiv st st-equiv)
     (equal (vl-hidsolo-mark mtype force-bogusp x ss st ctx)
            (vl-hidsolo-mark mtype force-bogusp x ss st-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-hidsolo-mark-of-vl-lucidctx-fix-ctx

(defthm vl-hidsolo-mark-of-vl-lucidctx-fix-ctx
  (equal (vl-hidsolo-mark mtype force-bogusp
                          x ss st (vl-lucidctx-fix ctx))
         (vl-hidsolo-mark mtype force-bogusp x ss st ctx)))

Theorem: vl-hidsolo-mark-vl-lucidctx-equiv-congruence-on-ctx

(defthm vl-hidsolo-mark-vl-lucidctx-equiv-congruence-on-ctx
 (implies
     (vl-lucidctx-equiv ctx ctx-equiv)
     (equal (vl-hidsolo-mark mtype force-bogusp x ss st ctx)
            (vl-hidsolo-mark mtype force-bogusp x ss st ctx-equiv)))
 :rule-classes :congruence)