		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-namedarg-lucidcheck

Signature
(vl-namedarg-lucidcheck x ss st ctx inst-ss) → new-st
Arguments: x — Guard (vl-namedarg-p x).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).; ctx — Guard (vl-lucidctx-p ctx).; inst-ss — Scopestack of the instantiated module/interface.
Guard (vl-scopestack-p inst-ss).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-namedarg-lucidcheck

(defun vl-namedarg-lucidcheck (x ss st ctx inst-ss)
 (declare (xargs :guard (and (vl-namedarg-p x)
                             (vl-scopestack-p ss)
                             (vl-lucidstate-p st)
                             (vl-lucidctx-p ctx)
                             (vl-scopestack-p inst-ss))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-namedarg-lucidcheck))
  (declare (ignorable __function__))
  (b* ((x (vl-namedarg-fix x))
       (ss (vl-scopestack-fix ss))
       (st (vl-lucidstate-fix st)))
   (b* (((vl-namedarg x))
        (ctx (change-vl-lucidctx ctx
                                 :portname x.name))
        (dir (vl-lucid-instmod-find-port-dir x.name inst-ss))
        ((unless x.expr) st))
    (case
      dir
      (:vl-input (vl-rhsexpr-lucidcheck x.expr ss st ctx))
      (:vl-output (vl-lhsexpr-lucidcheck x.expr ss st ctx))
      (otherwise (b* ((st (vl-rhsexpr-lucidcheck x.expr ss st ctx))
                      (st (vl-lhsexpr-lucidcheck x.expr ss st ctx)))
                   st)))))))

Theorem: vl-lucidstate-p-of-vl-namedarg-lucidcheck

(defthm vl-lucidstate-p-of-vl-namedarg-lucidcheck
  (b* ((new-st (vl-namedarg-lucidcheck x ss st ctx inst-ss)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-namedarg-lucidcheck-of-vl-namedarg-fix-x

(defthm vl-namedarg-lucidcheck-of-vl-namedarg-fix-x
  (equal (vl-namedarg-lucidcheck (vl-namedarg-fix x)
                                 ss st ctx inst-ss)
         (vl-namedarg-lucidcheck x ss st ctx inst-ss)))

Theorem: vl-namedarg-lucidcheck-vl-namedarg-equiv-congruence-on-x

(defthm vl-namedarg-lucidcheck-vl-namedarg-equiv-congruence-on-x
  (implies
       (vl-namedarg-equiv x x-equiv)
       (equal (vl-namedarg-lucidcheck x ss st ctx inst-ss)
              (vl-namedarg-lucidcheck x-equiv ss st ctx inst-ss)))
  :rule-classes :congruence)

Theorem: vl-namedarg-lucidcheck-of-vl-scopestack-fix-ss

(defthm vl-namedarg-lucidcheck-of-vl-scopestack-fix-ss
  (equal (vl-namedarg-lucidcheck x (vl-scopestack-fix ss)
                                 st ctx inst-ss)
         (vl-namedarg-lucidcheck x ss st ctx inst-ss)))

Theorem: vl-namedarg-lucidcheck-vl-scopestack-equiv-congruence-on-ss

(defthm vl-namedarg-lucidcheck-vl-scopestack-equiv-congruence-on-ss
  (implies
       (vl-scopestack-equiv ss ss-equiv)
       (equal (vl-namedarg-lucidcheck x ss st ctx inst-ss)
              (vl-namedarg-lucidcheck x ss-equiv st ctx inst-ss)))
  :rule-classes :congruence)

Theorem: vl-namedarg-lucidcheck-of-vl-lucidstate-fix-st

(defthm vl-namedarg-lucidcheck-of-vl-lucidstate-fix-st
  (equal (vl-namedarg-lucidcheck x ss (vl-lucidstate-fix st)
                                 ctx inst-ss)
         (vl-namedarg-lucidcheck x ss st ctx inst-ss)))

Theorem: vl-namedarg-lucidcheck-vl-lucidstate-equiv-congruence-on-st

(defthm vl-namedarg-lucidcheck-vl-lucidstate-equiv-congruence-on-st
  (implies
       (vl-lucidstate-equiv st st-equiv)
       (equal (vl-namedarg-lucidcheck x ss st ctx inst-ss)
              (vl-namedarg-lucidcheck x ss st-equiv ctx inst-ss)))
  :rule-classes :congruence)

Theorem: vl-namedarg-lucidcheck-of-vl-lucidctx-fix-ctx

(defthm vl-namedarg-lucidcheck-of-vl-lucidctx-fix-ctx
  (equal (vl-namedarg-lucidcheck x ss st (vl-lucidctx-fix ctx)
                                 inst-ss)
         (vl-namedarg-lucidcheck x ss st ctx inst-ss)))

Theorem: vl-namedarg-lucidcheck-vl-lucidctx-equiv-congruence-on-ctx

(defthm vl-namedarg-lucidcheck-vl-lucidctx-equiv-congruence-on-ctx
  (implies
       (vl-lucidctx-equiv ctx ctx-equiv)
       (equal (vl-namedarg-lucidcheck x ss st ctx inst-ss)
              (vl-namedarg-lucidcheck x ss st ctx-equiv inst-ss)))
  :rule-classes :congruence)

Theorem: vl-namedarg-lucidcheck-of-vl-scopestack-fix-inst-ss

(defthm vl-namedarg-lucidcheck-of-vl-scopestack-fix-inst-ss
 (equal
    (vl-namedarg-lucidcheck x ss st ctx (vl-scopestack-fix inst-ss))
    (vl-namedarg-lucidcheck x ss st ctx inst-ss)))

Theorem: vl-namedarg-lucidcheck-vl-scopestack-equiv-congruence-on-inst-ss

(defthm
   vl-namedarg-lucidcheck-vl-scopestack-equiv-congruence-on-inst-ss
  (implies
       (vl-scopestack-equiv inst-ss inst-ss-equiv)
       (equal (vl-namedarg-lucidcheck x ss st ctx inst-ss)
              (vl-namedarg-lucidcheck x ss st ctx inst-ss-equiv)))
  :rule-classes :congruence)