		Search-engine friendly clone of the ACL2 documentation.

Immdeps-main

Vl-atomguts-immdeps

Gather immediate dependencies from an atom.

Signature
(vl-atomguts-immdeps guts ans &key (ss 'ss) (ctx 'ctx)) → ans
Arguments: guts — Guts of the atom we're dealing with.
Guard (vl-atomguts-p guts).; ans — Answer we are building.
Guard (vl-immdeps-p ans).; ss — Our current scope.
Guard (vl-scopestack-p ss).; ctx — Context for warnings.
Guard (acl2::any-p ctx).
Returns: ans — Type (vl-immdeps-p ans).

Definitions and Theorems

Function: vl-atomguts-immdeps-fn

(defun vl-atomguts-immdeps-fn (guts ans ss ctx)
 (declare (xargs :guard (and (vl-atomguts-p guts)
                             (vl-immdeps-p ans)
                             (vl-scopestack-p ss)
                             (acl2::any-p ctx))))
 (let ((__function__ 'vl-atomguts-immdeps))
  (declare (ignorable __function__))
  (b* ((ans (vl-immdeps-fix ans))
       (guts (vl-atomguts-fix guts)))
   (case
      (tag guts)
      (:vl-id (vl-immdeps-add-item (vl-id->name guts)
                                   ans))
      (:vl-funname (vl-immdeps-add-item (vl-funname->name guts)
                                        ans))
      (:vl-typename (vl-immdeps-add-item (vl-typename->name guts)
                                         ans))
      ((:vl-constint :vl-weirdint
                     :vl-extint :vl-string
                     :vl-real :vl-time
                     :vl-basictype :vl-sysfunname)
       ans)
      (:vl-keyguts ans)
      (:vl-tagname
           (vl-immdeps-add-error
                ans
                :type :vl-immdeps-fudging
                :msg "~a0: don't know how to handle tag name ~s1.~%"
                :args (list ctx (vl-tagname->name guts))
                :fatalp t))
      (:vl-hidpiece
           (vl-immdeps-add-error
                ans
                :type :vl-immdeps-fudging
                :msg "~a0: atomic hid piece???  skipping ~s1.~%"
                :args (list ctx (vl-hidpiece->name guts))
                :fatalp t))
      (otherwise (progn$ (impossible) ans))))))

Theorem: vl-immdeps-p-of-vl-atomguts-immdeps

(defthm vl-immdeps-p-of-vl-atomguts-immdeps
  (b* ((ans (vl-atomguts-immdeps-fn guts ans ss ctx)))
    (vl-immdeps-p ans))
  :rule-classes :rewrite)

Theorem: vl-atomguts-immdeps-fn-of-vl-atomguts-fix-guts

(defthm vl-atomguts-immdeps-fn-of-vl-atomguts-fix-guts
  (equal (vl-atomguts-immdeps-fn (vl-atomguts-fix guts)
                                 ans ss ctx)
         (vl-atomguts-immdeps-fn guts ans ss ctx)))

Theorem: vl-atomguts-immdeps-fn-vl-atomguts-equiv-congruence-on-guts

(defthm vl-atomguts-immdeps-fn-vl-atomguts-equiv-congruence-on-guts
  (implies (vl-atomguts-equiv guts guts-equiv)
           (equal (vl-atomguts-immdeps-fn guts ans ss ctx)
                  (vl-atomguts-immdeps-fn guts-equiv ans ss ctx)))
  :rule-classes :congruence)

Theorem: vl-atomguts-immdeps-fn-of-vl-immdeps-fix-ans

(defthm vl-atomguts-immdeps-fn-of-vl-immdeps-fix-ans
  (equal (vl-atomguts-immdeps-fn guts (vl-immdeps-fix ans)
                                 ss ctx)
         (vl-atomguts-immdeps-fn guts ans ss ctx)))

Theorem: vl-atomguts-immdeps-fn-vl-immdeps-equiv-congruence-on-ans

(defthm vl-atomguts-immdeps-fn-vl-immdeps-equiv-congruence-on-ans
  (implies (vl-immdeps-equiv ans ans-equiv)
           (equal (vl-atomguts-immdeps-fn guts ans ss ctx)
                  (vl-atomguts-immdeps-fn guts ans-equiv ss ctx)))
  :rule-classes :congruence)

Theorem: vl-atomguts-immdeps-fn-of-vl-scopestack-fix-ss

(defthm vl-atomguts-immdeps-fn-of-vl-scopestack-fix-ss
  (equal (vl-atomguts-immdeps-fn guts ans (vl-scopestack-fix ss)
                                 ctx)
         (vl-atomguts-immdeps-fn guts ans ss ctx)))

Theorem: vl-atomguts-immdeps-fn-vl-scopestack-equiv-congruence-on-ss

(defthm vl-atomguts-immdeps-fn-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-atomguts-immdeps-fn guts ans ss ctx)
                  (vl-atomguts-immdeps-fn guts ans ss-equiv ctx)))
  :rule-classes :congruence)

Theorem: vl-atomguts-immdeps-fn-of-identity-ctx

(defthm vl-atomguts-immdeps-fn-of-identity-ctx
  (equal (vl-atomguts-immdeps-fn guts ans ss (identity ctx))
         (vl-atomguts-immdeps-fn guts ans ss ctx)))

Theorem: vl-atomguts-immdeps-fn-equal-congruence-on-ctx

(defthm vl-atomguts-immdeps-fn-equal-congruence-on-ctx
  (implies (equal ctx ctx-equiv)
           (equal (vl-atomguts-immdeps-fn guts ans ss ctx)
                  (vl-atomguts-immdeps-fn guts ans ss ctx-equiv)))
  :rule-classes :congruence)