		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-hidslice-mark

Signature
(vl-hidslice-mark mtype hid left right ss st ctx) → new-st
Arguments: mtype — Guard (member mtype '(:used :set)).; hid — Guard (vl-scopeexpr-p hid).; left — Guard (vl-expr-p left).; right — Guard (vl-expr-p right).; 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-hidslice-mark

(defun vl-hidslice-mark (mtype hid left right ss st ctx)
  (declare (xargs :guard (and (member mtype '(:used :set))
                              (vl-scopeexpr-p hid)
                              (vl-expr-p left)
                              (vl-expr-p right)
                              (vl-scopestack-p ss)
                              (vl-lucidstate-p st)
                              (vl-lucidctx-p ctx))))
  (let ((__function__ 'vl-hidslice-mark))
    (declare (ignorable __function__))
    (b* (((mv err trace ?scopectx tail)
          (vl-follow-scopeexpr hid 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 (vl-hidexpr-case tail :end)
                  (make-vl-lucidocc-slice :left left
                                          :right right
                                          :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-hidslice-mark

(defthm vl-lucidstate-p-of-vl-hidslice-mark
  (b* ((new-st (vl-hidslice-mark mtype hid left right ss st ctx)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-hidslice-mark-of-vl-scopeexpr-fix-hid

(defthm vl-hidslice-mark-of-vl-scopeexpr-fix-hid
  (equal (vl-hidslice-mark mtype (vl-scopeexpr-fix hid)
                           left right ss st ctx)
         (vl-hidslice-mark mtype hid left right ss st ctx)))

Theorem: vl-hidslice-mark-vl-scopeexpr-equiv-congruence-on-hid

(defthm vl-hidslice-mark-vl-scopeexpr-equiv-congruence-on-hid
 (implies
    (vl-scopeexpr-equiv hid hid-equiv)
    (equal (vl-hidslice-mark mtype hid left right ss st ctx)
           (vl-hidslice-mark mtype hid-equiv left right ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-hidslice-mark-of-vl-expr-fix-left

(defthm vl-hidslice-mark-of-vl-expr-fix-left
  (equal (vl-hidslice-mark mtype hid (vl-expr-fix left)
                           right ss st ctx)
         (vl-hidslice-mark mtype hid left right ss st ctx)))

Theorem: vl-hidslice-mark-vl-expr-equiv-congruence-on-left

(defthm vl-hidslice-mark-vl-expr-equiv-congruence-on-left
 (implies
    (vl-expr-equiv left left-equiv)
    (equal (vl-hidslice-mark mtype hid left right ss st ctx)
           (vl-hidslice-mark mtype hid left-equiv right ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-hidslice-mark-of-vl-expr-fix-right

(defthm vl-hidslice-mark-of-vl-expr-fix-right
  (equal (vl-hidslice-mark mtype hid left (vl-expr-fix right)
                           ss st ctx)
         (vl-hidslice-mark mtype hid left right ss st ctx)))

Theorem: vl-hidslice-mark-vl-expr-equiv-congruence-on-right

(defthm vl-hidslice-mark-vl-expr-equiv-congruence-on-right
 (implies
    (vl-expr-equiv right right-equiv)
    (equal (vl-hidslice-mark mtype hid left right ss st ctx)
           (vl-hidslice-mark mtype hid left right-equiv ss st ctx)))
 :rule-classes :congruence)

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

(defthm vl-hidslice-mark-of-vl-scopestack-fix-ss
  (equal (vl-hidslice-mark mtype
                           hid left right (vl-scopestack-fix ss)
                           st ctx)
         (vl-hidslice-mark mtype hid left right ss st ctx)))

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

(defthm vl-hidslice-mark-vl-scopestack-equiv-congruence-on-ss
 (implies
    (vl-scopestack-equiv ss ss-equiv)
    (equal (vl-hidslice-mark mtype hid left right ss st ctx)
           (vl-hidslice-mark mtype hid left right ss-equiv st ctx)))
 :rule-classes :congruence)

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

(defthm vl-hidslice-mark-of-vl-lucidstate-fix-st
  (equal (vl-hidslice-mark mtype
                           hid left right ss (vl-lucidstate-fix st)
                           ctx)
         (vl-hidslice-mark mtype hid left right ss st ctx)))

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

(defthm vl-hidslice-mark-vl-lucidstate-equiv-congruence-on-st
 (implies
    (vl-lucidstate-equiv st st-equiv)
    (equal (vl-hidslice-mark mtype hid left right ss st ctx)
           (vl-hidslice-mark mtype hid left right ss st-equiv ctx)))
 :rule-classes :congruence)

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

(defthm vl-hidslice-mark-of-vl-lucidctx-fix-ctx
  (equal (vl-hidslice-mark mtype hid
                           left right ss st (vl-lucidctx-fix ctx))
         (vl-hidslice-mark mtype hid left right ss st ctx)))

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

(defthm vl-hidslice-mark-vl-lucidctx-equiv-congruence-on-ctx
 (implies
    (vl-lucidctx-equiv ctx ctx-equiv)
    (equal (vl-hidslice-mark mtype hid left right ss st ctx)
           (vl-hidslice-mark mtype hid left right ss st ctx-equiv)))
 :rule-classes :congruence)