		Search-engine friendly clone of the ACL2 documentation.

Immdeps-main

Vl-expr-immdeps

Gather immediate dependencies for an expression.

Signature
(vl-expr-immdeps x ans &key (ss 'ss) (ctx 'ctx)) → ans
Arguments: x — Expression we're processing.
Guard (vl-expr-p x).; 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).

Theorem: return-type-of-vl-expr-immdeps.ans

(defthm return-type-of-vl-expr-immdeps.ans
  (b* ((?ans (vl-expr-immdeps-fn x ans ss ctx)))
    (vl-immdeps-p ans))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-immdeps.new-ans

(defthm return-type-of-vl-exprlist-immdeps.new-ans
  (b* ((?new-ans (vl-exprlist-immdeps-fn x ans ss ctx)))
    (vl-immdeps-p new-ans))
  :rule-classes :rewrite)

Theorem: vl-expr-immdeps-fn-of-vl-expr-fix-x

(defthm vl-expr-immdeps-fn-of-vl-expr-fix-x
  (equal (vl-expr-immdeps-fn (vl-expr-fix x)
                             ans ss ctx)
         (vl-expr-immdeps-fn x ans ss ctx)))

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

(defthm vl-expr-immdeps-fn-of-vl-immdeps-fix-ans
  (equal (vl-expr-immdeps-fn x (vl-immdeps-fix ans)
                             ss ctx)
         (vl-expr-immdeps-fn x ans ss ctx)))

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

(defthm vl-expr-immdeps-fn-of-vl-scopestack-fix-ss
  (equal (vl-expr-immdeps-fn x ans (vl-scopestack-fix ss)
                             ctx)
         (vl-expr-immdeps-fn x ans ss ctx)))

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

(defthm vl-expr-immdeps-fn-of-identity-ctx
  (equal (vl-expr-immdeps-fn x ans ss (identity ctx))
         (vl-expr-immdeps-fn x ans ss ctx)))

Theorem: vl-exprlist-immdeps-fn-of-vl-exprlist-fix-x

(defthm vl-exprlist-immdeps-fn-of-vl-exprlist-fix-x
  (equal (vl-exprlist-immdeps-fn (vl-exprlist-fix x)
                                 ans ss ctx)
         (vl-exprlist-immdeps-fn x ans ss ctx)))

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

(defthm vl-exprlist-immdeps-fn-of-vl-immdeps-fix-ans
  (equal (vl-exprlist-immdeps-fn x (vl-immdeps-fix ans)
                                 ss ctx)
         (vl-exprlist-immdeps-fn x ans ss ctx)))

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

(defthm vl-exprlist-immdeps-fn-of-vl-scopestack-fix-ss
  (equal (vl-exprlist-immdeps-fn x ans (vl-scopestack-fix ss)
                                 ctx)
         (vl-exprlist-immdeps-fn x ans ss ctx)))

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

(defthm vl-exprlist-immdeps-fn-of-identity-ctx
  (equal (vl-exprlist-immdeps-fn x ans ss (identity ctx))
         (vl-exprlist-immdeps-fn x ans ss ctx)))

Theorem: vl-expr-immdeps-fn-vl-expr-equiv-congruence-on-x

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

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

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

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

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

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

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

Theorem: vl-exprlist-immdeps-fn-vl-exprlist-equiv-congruence-on-x

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

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

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

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

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

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

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

Subtopics

Vl-exprlist-immdeps