		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-dissect-pair

Signature
(vl-lucid-dissect-pair key val reportcard st) → reportcard
Arguments: key — Guard (vl-lucidkey-p key).; val — Guard (vl-lucidval-p val).; reportcard — Guard (vl-reportcard-p reportcard).; st — Guard (vl-lucidstate-p st).
Returns: reportcard — Type (vl-reportcard-p reportcard).

Definitions and Theorems

Function: vl-lucid-dissect-pair

(defun vl-lucid-dissect-pair (key val reportcard st)
 (declare (xargs :guard (and (vl-lucidkey-p key)
                             (vl-lucidval-p val)
                             (vl-reportcard-p reportcard)
                             (vl-lucidstate-p st))))
 (let ((__function__ 'vl-lucid-dissect-pair))
  (declare (ignorable __function__))
  (b*
   ((reportcard (vl-reportcard-fix reportcard))
    ((vl-lucidstate st))
    ((vl-lucidkey key))
    ((vl-lucidval val))
    (topname (or (vl-scopestack-top-level-name key.scopestack)
                 :design))
    ((when val.errors)
     (b*
      ((w
        (make-vl-warning
         :type :vl-lucid-error
         :msg
         "Error computing use/set information for ~s0.  Debugging details: ~x1."
         :args (list (with-local-ps (vl-pp-lucidkey key))
                     val.errors)
         :fatalp nil
         :fn __function__)))
      (vl-extend-reportcard topname w reportcard))))
   (case
    (tag key.item)
    (:vl-fundecl
     (b*
      (((when (vl-lucid-some-solo-occp val.used))
        reportcard)
       (w
        (make-vl-warning
         :type :vl-lucid-unused
         :msg "Function ~w0 is never used. (~s1)"
         :args
         (list
             (vl-fundecl->name key.item)
             (with-local-ps (vl-pp-scopestack-path key.scopestack)))
         :fn __function__
         :fatalp nil)))
      (vl-extend-reportcard topname w reportcard)))
    (:vl-taskdecl
     (b*
      (((when (vl-lucid-some-solo-occp val.used))
        reportcard)
       (w
        (make-vl-warning
         :type :vl-lucid-unused
         :msg "Task ~w0 is never used. (~s1)"
         :args
         (list
             (vl-taskdecl->name key.item)
             (with-local-ps (vl-pp-scopestack-path key.scopestack)))
         :fn __function__
         :fatalp nil)))
      (vl-extend-reportcard topname w reportcard)))
    (:vl-typedef
     (b*
      (((when (vl-lucid-some-solo-occp val.used))
        reportcard)
       (w
        (make-vl-warning
         :type :vl-lucid-unused
         :msg "Type ~w0 is never used. (~s1)"
         :args
         (list
             (vl-typedef->name key.item)
             (with-local-ps (vl-pp-scopestack-path key.scopestack)))
         :fn __function__
         :fatalp nil)))
      (vl-extend-reportcard topname w reportcard)))
    (:vl-vardecl
     (b*
      ((warnings
        (vl-lucid-dissect-var-main key.scopestack key.item
                                   val.used val.set st.generatesp)))
      (vl-extend-reportcard-list topname warnings reportcard)))
    (:vl-paramdecl
     (b*
      (((unless st.paramsp) reportcard)
       (warnings
        (vl-lucid-dissect-var-main key.scopestack key.item
                                   val.used val.set st.generatesp)))
      (vl-extend-reportcard-list topname warnings reportcard)))
    (:vl-interfaceport
     (b*
      (((when (or val.used val.set))
        reportcard)
       (w
        (make-vl-warning
         :type :vl-lucid-spurious
         :msg "Interface port ~w0 is never mentioned. (~s1)"
         :args
         (list
             (vl-interfaceport->name key.item)
             (with-local-ps (vl-pp-scopestack-path key.scopestack)))
         :fn __function__
         :fatalp nil)))
      (vl-extend-reportcard topname w reportcard)))
    (:vl-modinst
     (b*
      (((vl-modinst key.item))
       (mod (vl-scopestack-find-definition
                 key.item.modname key.scopestack))
       ((unless (eq (tag mod) :vl-interface))
        reportcard)
       ((when (or val.used val.set))
        reportcard)
       (w
        (make-vl-warning
         :type :vl-lucid-spurious
         :msg "Interface ~w0 is never mentioned. (~s1)"
         :args
         (list
             key.item.instname
             (with-local-ps (vl-pp-scopestack-path key.scopestack)))
         :fn __function__
         :fatalp nil)))
      (vl-extend-reportcard topname w reportcard)))
    (otherwise reportcard)))))

Theorem: vl-reportcard-p-of-vl-lucid-dissect-pair

(defthm vl-reportcard-p-of-vl-lucid-dissect-pair
  (b* ((reportcard (vl-lucid-dissect-pair key val reportcard st)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: vl-lucid-dissect-pair-of-vl-lucidkey-fix-key

(defthm vl-lucid-dissect-pair-of-vl-lucidkey-fix-key
  (equal (vl-lucid-dissect-pair (vl-lucidkey-fix key)
                                val reportcard st)
         (vl-lucid-dissect-pair key val reportcard st)))

Theorem: vl-lucid-dissect-pair-vl-lucidkey-equiv-congruence-on-key

(defthm vl-lucid-dissect-pair-vl-lucidkey-equiv-congruence-on-key
  (implies
       (vl-lucidkey-equiv key key-equiv)
       (equal (vl-lucid-dissect-pair key val reportcard st)
              (vl-lucid-dissect-pair key-equiv val reportcard st)))
  :rule-classes :congruence)

Theorem: vl-lucid-dissect-pair-of-vl-lucidval-fix-val

(defthm vl-lucid-dissect-pair-of-vl-lucidval-fix-val
  (equal (vl-lucid-dissect-pair key (vl-lucidval-fix val)
                                reportcard st)
         (vl-lucid-dissect-pair key val reportcard st)))

Theorem: vl-lucid-dissect-pair-vl-lucidval-equiv-congruence-on-val

(defthm vl-lucid-dissect-pair-vl-lucidval-equiv-congruence-on-val
  (implies
       (vl-lucidval-equiv val val-equiv)
       (equal (vl-lucid-dissect-pair key val reportcard st)
              (vl-lucid-dissect-pair key val-equiv reportcard st)))
  :rule-classes :congruence)

Theorem: vl-lucid-dissect-pair-of-vl-reportcard-fix-reportcard

(defthm vl-lucid-dissect-pair-of-vl-reportcard-fix-reportcard
  (equal
       (vl-lucid-dissect-pair key val (vl-reportcard-fix reportcard)
                              st)
       (vl-lucid-dissect-pair key val reportcard st)))

Theorem: vl-lucid-dissect-pair-vl-reportcard-equiv-congruence-on-reportcard

(defthm
 vl-lucid-dissect-pair-vl-reportcard-equiv-congruence-on-reportcard
 (implies
      (vl-reportcard-equiv reportcard reportcard-equiv)
      (equal (vl-lucid-dissect-pair key val reportcard st)
             (vl-lucid-dissect-pair key val reportcard-equiv st)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-pair-of-vl-lucidstate-fix-st

(defthm vl-lucid-dissect-pair-of-vl-lucidstate-fix-st
  (equal
       (vl-lucid-dissect-pair key
                              val reportcard (vl-lucidstate-fix st))
       (vl-lucid-dissect-pair key val reportcard st)))

Theorem: vl-lucid-dissect-pair-vl-lucidstate-equiv-congruence-on-st

(defthm vl-lucid-dissect-pair-vl-lucidstate-equiv-congruence-on-st
  (implies
       (vl-lucidstate-equiv st st-equiv)
       (equal (vl-lucid-dissect-pair key val reportcard st)
              (vl-lucid-dissect-pair key val reportcard st-equiv)))
  :rule-classes :congruence)