		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-operandinfo-to-svex

Signature
(vl-operandinfo-to-svex x indices ss scopes) → (mv err svex)
Arguments: x — Guard (vl-operandinfo-p x).; indices — Guard (sv::svexlist-p indices).; ss — Guard (vl-scopestack-p ss).; scopes — Guard (vl-elabscopes-p scopes).
Returns: err — Type (iff (vl-msg-p err) err).; svex — Type (sv::svex-p svex).

Definitions and Theorems

Function: vl-operandinfo-to-svex

(defun vl-operandinfo-to-svex (x indices ss scopes)
 (declare (xargs :guard (and (vl-operandinfo-p x)
                             (sv::svexlist-p indices)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (declare
      (xargs :guard (and (vl-operandinfo-usertypes-ok x)
                         (equal (len indices)
                                (vl-operandinfo-index-count x)))))
 (let ((__function__ 'vl-operandinfo-to-svex))
  (declare (ignorable __function__))
  (b*
   (((vl-operandinfo x))
    ((mv err size)
     (vl-datatype-size x.type))
    ((when err) (mv err (svex-x)))
    ((unless size)
     (mv (vmsg "Unsizable datatype ~a0" x.type)
         (svex-x)))
    ((mv ?caveat class)
     (vl-datatype-arithclass x.type))
    ((mv err select paramval)
     (vl-operandinfo-to-svex-select x indices ss scopes))
    ((when err) (mv err (svex-x)))
    (svex-select (sv::svex-select-to-svex select))
    (svex-ext
         (if (vl-integer-arithclass-p class)
             (svex-extend (vl-integer-arithclass->exprsign class)
                          size svex-select)
           svex-select))
    ((unless paramval)
     (mv nil (sv::svex-reduce-consts svex-ext)))
    (param-svex
       (sv::svex-reduce-consts
            (sv::svex-replace-var svex-ext
                                  (sv::svex-select-inner-var select)
                                  (sv::svex-quote paramval)))))
   (mv nil param-svex))))

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

(defthm return-type-of-vl-operandinfo-to-svex.err
  (b* (((mv ?err ?svex)
        (vl-operandinfo-to-svex x indices ss scopes)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: svex-p-of-vl-operandinfo-to-svex.svex

(defthm svex-p-of-vl-operandinfo-to-svex.svex
  (b* (((mv ?err ?svex)
        (vl-operandinfo-to-svex x indices ss scopes)))
    (sv::svex-p svex))
  :rule-classes :rewrite)

Theorem: vars-of-vl-operandinfo-to-svex

(defthm vars-of-vl-operandinfo-to-svex
  (b* (((mv ?err ?svex)
        (vl-operandinfo-to-svex x indices ss scopes)))
    (implies (sv::svarlist-addr-p (sv::svexlist-vars indices))
             (sv::svarlist-addr-p (sv::svex-vars svex)))))

Theorem: vl-operandinfo-to-svex-of-vl-operandinfo-fix-x

(defthm vl-operandinfo-to-svex-of-vl-operandinfo-fix-x
  (equal (vl-operandinfo-to-svex (vl-operandinfo-fix x)
                                 indices ss scopes)
         (vl-operandinfo-to-svex x indices ss scopes)))

Theorem: vl-operandinfo-to-svex-vl-operandinfo-equiv-congruence-on-x

(defthm vl-operandinfo-to-svex-vl-operandinfo-equiv-congruence-on-x
  (implies
       (vl-operandinfo-equiv x x-equiv)
       (equal (vl-operandinfo-to-svex x indices ss scopes)
              (vl-operandinfo-to-svex x-equiv indices ss scopes)))
  :rule-classes :congruence)

Theorem: vl-operandinfo-to-svex-of-svexlist-fix-indices

(defthm vl-operandinfo-to-svex-of-svexlist-fix-indices
  (equal (vl-operandinfo-to-svex x (sv::svexlist-fix indices)
                                 ss scopes)
         (vl-operandinfo-to-svex x indices ss scopes)))

Theorem: vl-operandinfo-to-svex-svexlist-equiv-congruence-on-indices

(defthm vl-operandinfo-to-svex-svexlist-equiv-congruence-on-indices
  (implies
       (sv::svexlist-equiv indices indices-equiv)
       (equal (vl-operandinfo-to-svex x indices ss scopes)
              (vl-operandinfo-to-svex x indices-equiv ss scopes)))
  :rule-classes :congruence)

Theorem: vl-operandinfo-to-svex-of-vl-scopestack-fix-ss

(defthm vl-operandinfo-to-svex-of-vl-scopestack-fix-ss
  (equal (vl-operandinfo-to-svex x indices (vl-scopestack-fix ss)
                                 scopes)
         (vl-operandinfo-to-svex x indices ss scopes)))

Theorem: vl-operandinfo-to-svex-vl-scopestack-equiv-congruence-on-ss

(defthm vl-operandinfo-to-svex-vl-scopestack-equiv-congruence-on-ss
  (implies
       (vl-scopestack-equiv ss ss-equiv)
       (equal (vl-operandinfo-to-svex x indices ss scopes)
              (vl-operandinfo-to-svex x indices ss-equiv scopes)))
  :rule-classes :congruence)

Theorem: vl-operandinfo-to-svex-of-vl-elabscopes-fix-scopes

(defthm vl-operandinfo-to-svex-of-vl-elabscopes-fix-scopes
 (equal
    (vl-operandinfo-to-svex x indices ss (vl-elabscopes-fix scopes))
    (vl-operandinfo-to-svex x indices ss scopes)))

Theorem: vl-operandinfo-to-svex-vl-elabscopes-equiv-congruence-on-scopes

(defthm
    vl-operandinfo-to-svex-vl-elabscopes-equiv-congruence-on-scopes
  (implies
       (vl-elabscopes-equiv scopes scopes-equiv)
       (equal (vl-operandinfo-to-svex x indices ss scopes)
              (vl-operandinfo-to-svex x indices ss scopes-equiv)))
  :rule-classes :congruence)