		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-slicesize-resolve

Signature
(vl-slicesize-resolve x ss scopes) → (mv err size)
Arguments: x — Guard (vl-slicesize-p x).; ss — Guard (vl-scopestack-p ss).; scopes — Guard (vl-elabscopes-p scopes).
Returns: err — Type (iff (vl-msg-p err) err).; size — Type (implies (not err) (posp size)).

Definitions and Theorems

Function: vl-slicesize-resolve

(defun vl-slicesize-resolve (x ss scopes)
  (declare (xargs :guard (and (vl-slicesize-p x)
                              (vl-scopestack-p ss)
                              (vl-elabscopes-p scopes))))
  (let ((__function__ 'vl-slicesize-resolve))
    (declare (ignorable __function__))
    (b* ((x (vl-slicesize-fix x)))
      (vl-slicesize-case
           x :none (mv nil 1)
           :expr
           (b* (((unless (vl-expr-resolved-p x.expr))
                 (mv (vmsg "Slice size is unresolved expression")
                     nil))
                (val (vl-resolved->val x.expr))
                ((unless (posp val))
                 (mv (vmsg "Slice size must be positive")
                     nil)))
             (mv nil val))
           :type
           (b* (((mv err type)
                 (vl-datatype-usertype-resolve x.type ss
                                               :scopes scopes))
                ((when err) (mv err nil))
                ((mv err size) (vl-datatype-size type))
                ((when err) (mv err nil))
                ((unless (posp size))
                 (mv (vmsg "Slice size must be nonzero")
                     nil)))
             (mv nil size))))))

Theorem: return-type-of-vl-slicesize-resolve.err

(defthm return-type-of-vl-slicesize-resolve.err
  (b* (((mv ?err ?size)
        (vl-slicesize-resolve x ss scopes)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-slicesize-resolve.size

(defthm return-type-of-vl-slicesize-resolve.size
  (b* (((mv ?err ?size)
        (vl-slicesize-resolve x ss scopes)))
    (implies (not err) (posp size)))
  :rule-classes :type-prescription)

Theorem: vl-slicesize-resolve-of-vl-slicesize-fix-x

(defthm vl-slicesize-resolve-of-vl-slicesize-fix-x
  (equal (vl-slicesize-resolve (vl-slicesize-fix x)
                               ss scopes)
         (vl-slicesize-resolve x ss scopes)))

Theorem: vl-slicesize-resolve-vl-slicesize-equiv-congruence-on-x

(defthm vl-slicesize-resolve-vl-slicesize-equiv-congruence-on-x
  (implies (vl-slicesize-equiv x x-equiv)
           (equal (vl-slicesize-resolve x ss scopes)
                  (vl-slicesize-resolve x-equiv ss scopes)))
  :rule-classes :congruence)

Theorem: vl-slicesize-resolve-of-vl-scopestack-fix-ss

(defthm vl-slicesize-resolve-of-vl-scopestack-fix-ss
  (equal (vl-slicesize-resolve x (vl-scopestack-fix ss)
                               scopes)
         (vl-slicesize-resolve x ss scopes)))

Theorem: vl-slicesize-resolve-vl-scopestack-equiv-congruence-on-ss

(defthm vl-slicesize-resolve-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-slicesize-resolve x ss scopes)
                  (vl-slicesize-resolve x ss-equiv scopes)))
  :rule-classes :congruence)

Theorem: vl-slicesize-resolve-of-vl-elabscopes-fix-scopes

(defthm vl-slicesize-resolve-of-vl-elabscopes-fix-scopes
  (equal (vl-slicesize-resolve x ss (vl-elabscopes-fix scopes))
         (vl-slicesize-resolve x ss scopes)))

Theorem: vl-slicesize-resolve-vl-elabscopes-equiv-congruence-on-scopes

(defthm
      vl-slicesize-resolve-vl-elabscopes-equiv-congruence-on-scopes
  (implies (vl-elabscopes-equiv scopes scopes-equiv)
           (equal (vl-slicesize-resolve x ss scopes)
                  (vl-slicesize-resolve x ss scopes-equiv)))
  :rule-classes :congruence)