		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-scopecontext-to-addr

Create an svex address from a path, based on which scope the scopecontext object indicates.

Signature
(vl-scopecontext-to-addr x ss path &key (strictp 't)) → (mv err addr)
Arguments: x — Guard (vl-scopecontext-p x).; ss — Guard (vl-scopestack-p ss).; path — Guard (sv::path-p path).; strictp — Guard (booleanp strictp).
Returns: err — Type (iff (vl-msg-p err) err).; addr — Type (and (implies (not err) (sv::address-p addr)) (implies addr (sv::address-p addr))) .

Svex supports three kinds of addresses -- see sv::address for more. This function tries to determine the right kind of address to make from a VL hid expression by looking up the basename of the path in the scopestack to see where it was found.

The scopecontext tells us almost what we need to know to make a proper svex address. Either:

It's at root scope. We make a root address.
It's in a package or class scope. We support this when not strictp, meaning we're looking up a parameter value rather than a variable name.
It's at local scope, N levels up. We make a local address, but we have to translate the number of levels by examining the scopestack. -- see below.

There is a subtle disconnect between svex's concept of scopes and VL's. In VL, if you're inside a generate block in a module, you probably have three scope levels: the block, the module, and the global scope. In svex, if you're inside the same block, you might be inside several more levels of scope if the module is instantiated deep in the hierarchy, or if the module is the top module, you might just be inside the block within the module (so only two levels deep). In translating between these we assume that VL scopes basically consist of a single global scope, the single module scope, and some number of nested block scopes. In translating to svex, we require that the number of levels up only includes these nested block scopes. We also need to be careful to be consistent with our scoping conventions -- most particularly, a generate array (the elaborated result of a generate loop) has a level of scoping for the array itself, and an additional one for each of the blocks in the array (the replicated loop bodies). On the other hand, statement scopes are handled by the vl-svstmt transform which eliminates local variables, so subscopes within statements are not related to svex scopes. Vl-upscope-to-svex-upscope accounts for these issues.

For package and module contexts, we produce an error because variables in those scopes aren't yet supported. We also return an address, however, because we use this for resolving function names, in which case the error can be ignored.

Definitions and Theorems

Function: vl-scopecontext-to-addr-fn

(defun vl-scopecontext-to-addr-fn (x ss path strictp)
 (declare (xargs :guard (and (vl-scopecontext-p x)
                             (vl-scopestack-p ss)
                             (sv::path-p path)
                             (booleanp strictp))))
 (let ((__function__ 'vl-scopecontext-to-addr))
  (declare (ignorable __function__))
  (vl-scopecontext-case
   x :local
   (b* (((mv err levels)
         (vl-upscope-to-svex-upscope x.levels ss
                                     :strictp strictp))
        ((when err) (mv err nil)))
     (mv nil
         (sv::make-address :path path
                           :scope levels)))
   :root (mv nil
             (sv::make-address :path path
                               :scope :root))
   :package
   (mv
    (and strictp
         (vmsg "Package-scoped variables aren't yet supported"))
    (sv::make-address
      :scope :root
      :path (sv::make-path-scope :namespace (vl-package->name x.pkg)
                                 :subpath path)))
   :class
   (mv
    (and strictp
         (vmsg "Class-scoped variables aren't yet supported"))
    (sv::make-address
      :scope :root
      :path (sv::make-path-scope :namespace (vl-class->name x.class)
                                 :subpath path)))
   :module
   (mv
    (and strictp
         (vmsg "Module-scoped variables aren't yet supported"))
    (sv::make-address
       :scope :root
       :path (sv::make-path-scope :namespace (vl-module->name x.mod)
                                  :subpath path)))
   :interface
   (mv
    (and strictp
         (vmsg "Module-scoped variables aren't yet supported"))
    (sv::make-address
        :scope :root
        :path
        (sv::make-path-scope :namespace (vl-interface->name x.iface)
                             :subpath path))))))

Theorem: return-type-of-vl-scopecontext-to-addr.err

(defthm return-type-of-vl-scopecontext-to-addr.err
  (b* (((mv ?err ?addr)
        (vl-scopecontext-to-addr-fn x ss path strictp)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-scopecontext-to-addr.addr

(defthm return-type-of-vl-scopecontext-to-addr.addr
  (b* (((mv ?err ?addr)
        (vl-scopecontext-to-addr-fn x ss path strictp)))
    (and (implies (not err) (sv::address-p addr))
         (implies addr (sv::address-p addr))))
  :rule-classes :rewrite)

Theorem: vl-scopecontext-to-addr-fn-of-vl-scopecontext-fix-x

(defthm vl-scopecontext-to-addr-fn-of-vl-scopecontext-fix-x
  (equal (vl-scopecontext-to-addr-fn (vl-scopecontext-fix x)
                                     ss path strictp)
         (vl-scopecontext-to-addr-fn x ss path strictp)))

Theorem: vl-scopecontext-to-addr-fn-vl-scopecontext-equiv-congruence-on-x

(defthm
   vl-scopecontext-to-addr-fn-vl-scopecontext-equiv-congruence-on-x
  (implies
       (vl-scopecontext-equiv x x-equiv)
       (equal (vl-scopecontext-to-addr-fn x ss path strictp)
              (vl-scopecontext-to-addr-fn x-equiv ss path strictp)))
  :rule-classes :congruence)

Theorem: vl-scopecontext-to-addr-fn-of-vl-scopestack-fix-ss

(defthm vl-scopecontext-to-addr-fn-of-vl-scopestack-fix-ss
  (equal (vl-scopecontext-to-addr-fn x (vl-scopestack-fix ss)
                                     path strictp)
         (vl-scopecontext-to-addr-fn x ss path strictp)))

Theorem: vl-scopecontext-to-addr-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
    vl-scopecontext-to-addr-fn-vl-scopestack-equiv-congruence-on-ss
  (implies
       (vl-scopestack-equiv ss ss-equiv)
       (equal (vl-scopecontext-to-addr-fn x ss path strictp)
              (vl-scopecontext-to-addr-fn x ss-equiv path strictp)))
  :rule-classes :congruence)

Theorem: vl-scopecontext-to-addr-fn-of-path-fix-path

(defthm vl-scopecontext-to-addr-fn-of-path-fix-path
  (equal (vl-scopecontext-to-addr-fn x ss (sv::path-fix path)
                                     strictp)
         (vl-scopecontext-to-addr-fn x ss path strictp)))

Theorem: vl-scopecontext-to-addr-fn-path-equiv-congruence-on-path

(defthm vl-scopecontext-to-addr-fn-path-equiv-congruence-on-path
  (implies
       (sv::path-equiv path path-equiv)
       (equal (vl-scopecontext-to-addr-fn x ss path strictp)
              (vl-scopecontext-to-addr-fn x ss path-equiv strictp)))
  :rule-classes :congruence)

Theorem: vl-scopecontext-to-addr-fn-of-bool-fix-strictp

(defthm vl-scopecontext-to-addr-fn-of-bool-fix-strictp
 (equal
     (vl-scopecontext-to-addr-fn x ss path (acl2::bool-fix strictp))
     (vl-scopecontext-to-addr-fn x ss path strictp)))

Theorem: vl-scopecontext-to-addr-fn-iff-congruence-on-strictp

(defthm vl-scopecontext-to-addr-fn-iff-congruence-on-strictp
  (implies
       (iff strictp strictp-equiv)
       (equal (vl-scopecontext-to-addr-fn x ss path strictp)
              (vl-scopecontext-to-addr-fn x ss path strictp-equiv)))
  :rule-classes :congruence)