		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-expr-to-svex-lhs

Signature
(vl-expr-to-svex-lhs x ss scopes) → (mv vttree svex type)
Arguments: x — Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).; scopes — Guard (vl-elabscopes-p scopes).
Returns: vttree — Type (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree)))) .; svex — Type (and (sv::lhs-p svex) (sv::svarlist-addr-p (sv::lhs-vars svex))).; type — Type (and (vl-maybe-datatype-p type) (implies type (vl-datatype-resolved-p type))) .

Definitions and Theorems

Function: vl-expr-to-svex-lhs

(defun vl-expr-to-svex-lhs (x ss scopes)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-expr-to-svex-lhs))
  (declare (ignorable __function__))
  (b*
   ((vttree nil)
    ((mv vttree svex type)
     (vl-expr-case
        x :vl-index
        (vl-index-expr-to-svex x ss scopes)
        :vl-concat
        (b* (((vmv vttree svex size)
              (vl-expr-to-svex-selfdet x nil ss scopes))
             ((unless (posp size))
              (mv vttree svex nil)))
          (mv vttree
              svex (vl-size-to-unsigned-logic size)))
        :vl-stream
        (b* (((vmv vttree svex size)
              (vl-streaming-concat-to-svex x ss scopes))
             ((unless (posp size))
              (mv (vfatal :type :vl-expr-to-svex-fail
                          :msg "Bad LHS: zero-size streaming concat"
                          :args (list (vl-expr-fix x)))
                  (svex-x)
                  nil)))
          (mv vttree
              svex (vl-size-to-unsigned-logic size)))
        :otherwise (mv (vfatal :type :vl-expr-to-svex-fail
                               :msg "Bad LHS expression: ~a0"
                               :args (list (vl-expr-fix x)))
                       (svex-x)
                       nil)))
    ((unless type) (mv vttree nil type))
    ((mv err size) (vl-datatype-size type))
    ((when (or err (not size)))
     (mv
      (vfatal
       :type :vl-expr-to-svex-fail
       :msg
       "Couldn't size the datatype ~a0 of ~
                                    LHS expression ~a1: ~@2"
       :args (list type (vl-expr-fix x)
                   (or err (vmsg "unsizeable"))))
      nil nil))
    (lhssvex (sv::svex-lhsrewrite svex size))
    ((unless (sv::lhssvex-bounded-p size lhssvex))
     (mv (vfatal :type :vl-expr->svex-lhs-fail
                 :msg "Not a supported LHS expression: ~a0"
                 :args (list (vl-expr-fix x)))
         nil nil)))
   (mv vttree
       (sv::svex->lhs-bound size lhssvex)
       type))))

Theorem: return-type-of-vl-expr-to-svex-lhs.vttree

(defthm return-type-of-vl-expr-to-svex-lhs.vttree
 (b* (((mv ?vttree ?svex common-lisp::?type)
       (vl-expr-to-svex-lhs x ss scopes)))
  (and
      (vttree-p vttree)
      (sv::svarlist-addr-p
           (sv::constraintlist-vars (vttree->constraints vttree)))))
 :rule-classes :rewrite)

Theorem: return-type-of-vl-expr-to-svex-lhs.svex

(defthm return-type-of-vl-expr-to-svex-lhs.svex
  (b* (((mv ?vttree ?svex common-lisp::?type)
        (vl-expr-to-svex-lhs x ss scopes)))
    (and (sv::lhs-p svex)
         (sv::svarlist-addr-p (sv::lhs-vars svex))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-expr-to-svex-lhs.type

(defthm return-type-of-vl-expr-to-svex-lhs.type
  (b* (((mv ?vttree ?svex common-lisp::?type)
        (vl-expr-to-svex-lhs x ss scopes)))
    (and (vl-maybe-datatype-p type)
         (implies type (vl-datatype-resolved-p type))))
  :rule-classes :rewrite)

Theorem: vl-expr-to-svex-lhs-type-size-ok

(defthm vl-expr-to-svex-lhs-type-size-ok
  (b* (((mv ?vttree ?svex common-lisp::?type)
        (vl-expr-to-svex-lhs x ss scopes)))
    (implies type
             (not (mv-nth 0 (vl-datatype-size type))))))

Theorem: vl-expr-to-svex-lhs-of-vl-expr-fix-x

(defthm vl-expr-to-svex-lhs-of-vl-expr-fix-x
  (equal (vl-expr-to-svex-lhs (vl-expr-fix x)
                              ss scopes)
         (vl-expr-to-svex-lhs x ss scopes)))

Theorem: vl-expr-to-svex-lhs-vl-expr-equiv-congruence-on-x

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

Theorem: vl-expr-to-svex-lhs-of-vl-scopestack-fix-ss

(defthm vl-expr-to-svex-lhs-of-vl-scopestack-fix-ss
  (equal (vl-expr-to-svex-lhs x (vl-scopestack-fix ss)
                              scopes)
         (vl-expr-to-svex-lhs x ss scopes)))

Theorem: vl-expr-to-svex-lhs-vl-scopestack-equiv-congruence-on-ss

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

Theorem: vl-expr-to-svex-lhs-of-vl-elabscopes-fix-scopes

(defthm vl-expr-to-svex-lhs-of-vl-elabscopes-fix-scopes
  (equal (vl-expr-to-svex-lhs x ss (vl-elabscopes-fix scopes))
         (vl-expr-to-svex-lhs x ss scopes)))

Theorem: vl-expr-to-svex-lhs-vl-elabscopes-equiv-congruence-on-scopes

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