		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-hidsolo-mark

Signature
(vl-hidsolo-mark mtype force-bogusp hid ss st ctx) → new-st
Arguments: mtype — Guard (member mtype '(:used :set)).; force-bogusp — Guard (booleanp force-bogusp).; hid — Guard (vl-expr-p hid).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).; ctx — Guard (vl-context1-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 hid ss st ctx)
  (declare (xargs :guard (and (member mtype '(:used :set))
                              (booleanp force-bogusp)
                              (vl-expr-p hid)
                              (vl-scopestack-p ss)
                              (vl-lucidstate-p st)
                              (vl-context1-p ctx))))
  (declare (xargs :guard (vl-hidexpr-p hid)))
  (let ((__function__ 'vl-hidsolo-mark))
    (declare (ignorable __function__))
    (b* (((mv err trace tail)
          (vl-follow-hidexpr hid ss ctx))
         ((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 (or force-bogusp
                      (not (vl-hidexpr->endp tail)))
                  (make-vl-lucidocc-tail :ctx ctx :ss ss)
                (make-vl-lucidocc-solo :ctx ctx
                                       :ss ss)))
         (st (vl-hidtrace-mark-interfaces mtype rest ss 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 hid 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)
                          hid ss st ctx)
         (vl-hidsolo-mark mtype force-bogusp hid 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 hid ss st ctx)
              (vl-hidsolo-mark mtype
                               force-bogusp-equiv hid ss st ctx)))
  :rule-classes :congruence)

Theorem: vl-hidsolo-mark-of-vl-expr-fix-hid

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

Theorem: vl-hidsolo-mark-vl-expr-equiv-congruence-on-hid

(defthm vl-hidsolo-mark-vl-expr-equiv-congruence-on-hid
  (implies
       (vl-expr-equiv hid hid-equiv)
       (equal (vl-hidsolo-mark mtype force-bogusp hid ss st ctx)
              (vl-hidsolo-mark mtype
                               force-bogusp hid-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 hid (vl-scopestack-fix ss)
                          st ctx)
         (vl-hidsolo-mark mtype force-bogusp hid 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 hid ss st ctx)
              (vl-hidsolo-mark mtype
                               force-bogusp hid 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
                          hid ss (vl-lucidstate-fix st)
                          ctx)
         (vl-hidsolo-mark mtype force-bogusp hid 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 hid ss st ctx)
              (vl-hidsolo-mark mtype
                               force-bogusp hid ss st-equiv ctx)))
  :rule-classes :congruence)

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

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

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

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