		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-paramdecl-lucidcheck

Signature
(vl-paramdecl-lucidcheck x ss st) → new-st
Arguments: x — Guard (vl-paramdecl-p x).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-paramdecl-lucidcheck

(defun vl-paramdecl-lucidcheck (x ss st)
 (declare (xargs :guard (and (vl-paramdecl-p x)
                             (vl-scopestack-p ss)
                             (vl-lucidstate-p st))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-paramdecl-lucidcheck))
  (declare (ignorable __function__))
  (b* ((x (vl-paramdecl-fix x))
       (ss (vl-scopestack-fix ss))
       (st (vl-lucidstate-fix st)))
   (b* (((vl-paramdecl x))
        (ctx (vl-lucid-ctx ss x)))
    (vl-paramtype-case
     x.type
     (:vl-implicitvalueparam
         (b* (((unless x.type.default) st)
              (st (vl-lucid-mark-simple :set x.name ss st ctx))
              (st (vl-rhsexpr-lucidcheck x.type.default ss st ctx)))
           st))
     (:vl-explicitvalueparam
         (b* ((st (vl-datatype-lucidcheck x.type.type ss st ctx))
              ((unless x.type.default) st)
              (st (vl-lucid-mark-simple :set x.name ss st ctx))
              (st (vl-rhsexpr-lucidcheck x.type.default ss st ctx)))
           st))
     (:vl-typeparam
        (b* (((unless x.type.default) st)
             (st (vl-lucid-mark-simple :set x.name ss st ctx))
             (st (vl-datatype-lucidcheck x.type.default ss st ctx)))
          st)))))))

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

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

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

(defthm vl-paramdecl-lucidcheck-of-vl-paramdecl-fix-x
  (equal (vl-paramdecl-lucidcheck (vl-paramdecl-fix x)
                                  ss st)
         (vl-paramdecl-lucidcheck x ss st)))

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

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

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

(defthm vl-paramdecl-lucidcheck-of-vl-scopestack-fix-ss
  (equal (vl-paramdecl-lucidcheck x (vl-scopestack-fix ss)
                                  st)
         (vl-paramdecl-lucidcheck x ss st)))

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

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

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

(defthm vl-paramdecl-lucidcheck-of-vl-lucidstate-fix-st
  (equal (vl-paramdecl-lucidcheck x ss (vl-lucidstate-fix st))
         (vl-paramdecl-lucidcheck x ss st)))

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

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