		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-upscope-to-svex-upscope

Signature
(vl-upscope-to-svex-upscope vl-levels ss &key (strictp 't)) → (mv err svex-levels)
Arguments: vl-levels — number of levels up we're going.
Guard (natp vl-levels).; ss — scopestack we're traversing.
Guard (vl-scopestack-p ss).; strictp — Guard (booleanp strictp).
Returns: err — Type (implies err (vl-msg-p err)).; svex-levels — Type (implies (not err) (natp svex-levels)).

Definitions and Theorems

Function: vl-upscope-to-svex-upscope-fn

(defun vl-upscope-to-svex-upscope-fn (vl-levels ss strictp)
 (declare (xargs :guard (and (natp vl-levels)
                             (vl-scopestack-p ss)
                             (booleanp strictp))))
 (let ((__function__ 'vl-upscope-to-svex-upscope))
  (declare (ignorable __function__))
  (b* (((when (zp vl-levels)) (mv nil 0)))
   (vl-scopestack-case
    ss :null
    (mv (vmsg "Tried to go ~x0 level~s1 up from the empty scope"
              vl-levels (if (eql vl-levels 1) "" "s"))
        nil)
    :global
    (mv (vmsg "Tried to go ~x0 level~s1 up from the global scope"
              vl-levels (if (eql vl-levels 1) "" "s"))
        nil)
    :local
    (b*
     ((type (vl-scope->scopetype ss.top))
      ((mv err incr)
       (case
        type (:vl-genblock (mv nil 1))
        (:vl-genarrayblock (mv nil 1))
        (:vl-genarray (mv nil 1))
        (:vl-blockstmt (mv nil 0))
        (:vl-forstmt (mv nil 0))
        (:vl-foreachstmt (mv nil 0))
        (:vl-fundecl (mv nil 0))
        (otherwise
         (if strictp
          (mv
           (vmsg
            "Tried to go ~x0 level~s1 up through a scope of type ~x2"
            vl-levels (if (eql vl-levels 1) "" "s")
            type)
           nil)
          (mv nil 0)))))
      ((when err) (mv err nil))
      ((mv err rest)
       (vl-upscope-to-svex-upscope (1- vl-levels)
                                   ss.super))
      ((when err) (mv err nil)))
     (mv nil (+ incr rest)))))))

Theorem: return-type-of-vl-upscope-to-svex-upscope.err

(defthm return-type-of-vl-upscope-to-svex-upscope.err
  (b* (((mv ?err ?svex-levels)
        (vl-upscope-to-svex-upscope-fn vl-levels ss strictp)))
    (implies err (vl-msg-p err)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-upscope-to-svex-upscope.svex-levels

(defthm return-type-of-vl-upscope-to-svex-upscope.svex-levels
  (b* (((mv ?err ?svex-levels)
        (vl-upscope-to-svex-upscope-fn vl-levels ss strictp)))
    (implies (not err) (natp svex-levels)))
  :rule-classes :type-prescription)

Theorem: vl-upscope-to-svex-upscope-fn-of-nfix-vl-levels

(defthm vl-upscope-to-svex-upscope-fn-of-nfix-vl-levels
  (equal (vl-upscope-to-svex-upscope-fn (nfix vl-levels)
                                        ss strictp)
         (vl-upscope-to-svex-upscope-fn vl-levels ss strictp)))

Theorem: vl-upscope-to-svex-upscope-fn-nat-equiv-congruence-on-vl-levels

(defthm
    vl-upscope-to-svex-upscope-fn-nat-equiv-congruence-on-vl-levels
 (implies
   (acl2::nat-equiv vl-levels vl-levels-equiv)
   (equal
        (vl-upscope-to-svex-upscope-fn vl-levels ss strictp)
        (vl-upscope-to-svex-upscope-fn vl-levels-equiv ss strictp)))
 :rule-classes :congruence)

Theorem: vl-upscope-to-svex-upscope-fn-of-vl-scopestack-fix-ss

(defthm vl-upscope-to-svex-upscope-fn-of-vl-scopestack-fix-ss
 (equal
     (vl-upscope-to-svex-upscope-fn vl-levels (vl-scopestack-fix ss)
                                    strictp)
     (vl-upscope-to-svex-upscope-fn vl-levels ss strictp)))

Theorem: vl-upscope-to-svex-upscope-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-upscope-to-svex-upscope-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal
        (vl-upscope-to-svex-upscope-fn vl-levels ss strictp)
        (vl-upscope-to-svex-upscope-fn vl-levels ss-equiv strictp)))
 :rule-classes :congruence)

Theorem: vl-upscope-to-svex-upscope-fn-of-bool-fix-strictp

(defthm vl-upscope-to-svex-upscope-fn-of-bool-fix-strictp
  (equal (vl-upscope-to-svex-upscope-fn
              vl-levels ss (acl2::bool-fix strictp))
         (vl-upscope-to-svex-upscope-fn vl-levels ss strictp)))

Theorem: vl-upscope-to-svex-upscope-fn-iff-congruence-on-strictp

(defthm vl-upscope-to-svex-upscope-fn-iff-congruence-on-strictp
 (implies
   (iff strictp strictp-equiv)
   (equal
        (vl-upscope-to-svex-upscope-fn vl-levels ss strictp)
        (vl-upscope-to-svex-upscope-fn vl-levels ss strictp-equiv)))
 :rule-classes :congruence)