		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-valid-bits-for-datatype

Signature
(vl-lucid-valid-bits-for-datatype x ss ctx) → (mv simple-p bits)
Arguments: x — Guard (vl-datatype-p x).; ss — Guard (vl-scopestack-p ss).; ctx — Guard (any-p ctx).
Returns: simple-p — Type (booleanp simple-p).; bits — Type (and (integer-listp bits) (setp bits)).

Definitions and Theorems

Function: vl-lucid-valid-bits-for-datatype

(defun vl-lucid-valid-bits-for-datatype (x ss ctx)
 (declare (xargs :guard (and (vl-datatype-p x)
                             (vl-scopestack-p ss)
                             (any-p ctx))))
 (let ((__function__ 'vl-lucid-valid-bits-for-datatype))
  (declare (ignorable __function__))
  (b* (((mv err x)
        (vl-datatype-usertype-resolve
             x ss
             :rec-limit 1000
             :scopes (vl-elabscopes-init-ss ss)))
       ((when err) (mv nil nil)))
   (vl-datatype-case
    x
    (:vl-coretype
     (case
      x.name
      ((:vl-logic :vl-reg :vl-bit)
       (b*
        (((when (consp x.udims)) (mv nil nil))
         ((when (atom x.pdims)) (mv t '(0)))
         ((unless (and (atom (cdr x.pdims))
                       (b* ((dim (first x.pdims)))
                         (vl-dimension-case dim :range))
                       (vl-range-resolved-p
                            (vl-dimension->range (first x.pdims)))))
          (mv nil nil)))
        (mv
         t
         (vl-lucid-range->bits (vl-dimension->range (first x.pdims))
                               ctx))))
      ((:vl-byte :vl-shortint
                 :vl-int :vl-longint
                 :vl-integer :vl-time)
       (if (or (consp x.pdims) (consp x.udims))
           (mv nil nil)
         (case x.name (:vl-byte (mv t (nats-from 0 8)))
               (:vl-shortint (mv t (nats-from 0 16)))
               (:vl-int (mv t (nats-from 0 32)))
               (:vl-longint (mv t (nats-from 0 64)))
               (:vl-integer (mv t (nats-from 0 32)))
               (:vl-time (mv t (nats-from 0 64)))
               (otherwise (mv (impossible) nil)))))
      (otherwise (mv nil nil))))
    (:vl-struct (mv nil nil))
    (:vl-union (mv nil nil))
    (:vl-enum (mv nil nil))
    (:vl-usertype (mv nil nil))))))

Theorem: booleanp-of-vl-lucid-valid-bits-for-datatype.simple-p

(defthm booleanp-of-vl-lucid-valid-bits-for-datatype.simple-p
  (b* (((mv ?simple-p ?bits)
        (vl-lucid-valid-bits-for-datatype x ss ctx)))
    (booleanp simple-p))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-lucid-valid-bits-for-datatype.bits

(defthm return-type-of-vl-lucid-valid-bits-for-datatype.bits
  (b* (((mv ?simple-p ?bits)
        (vl-lucid-valid-bits-for-datatype x ss ctx)))
    (and (integer-listp bits) (setp bits)))
  :rule-classes :rewrite)

Theorem: vl-lucid-valid-bits-for-datatype-of-vl-datatype-fix-x

(defthm vl-lucid-valid-bits-for-datatype-of-vl-datatype-fix-x
  (equal (vl-lucid-valid-bits-for-datatype (vl-datatype-fix x)
                                           ss ctx)
         (vl-lucid-valid-bits-for-datatype x ss ctx)))

Theorem: vl-lucid-valid-bits-for-datatype-vl-datatype-equiv-congruence-on-x

(defthm
 vl-lucid-valid-bits-for-datatype-vl-datatype-equiv-congruence-on-x
 (implies (vl-datatype-equiv x x-equiv)
          (equal (vl-lucid-valid-bits-for-datatype x ss ctx)
                 (vl-lucid-valid-bits-for-datatype x-equiv ss ctx)))
 :rule-classes :congruence)

Theorem: vl-lucid-valid-bits-for-datatype-of-vl-scopestack-fix-ss

(defthm vl-lucid-valid-bits-for-datatype-of-vl-scopestack-fix-ss
  (equal (vl-lucid-valid-bits-for-datatype x (vl-scopestack-fix ss)
                                           ctx)
         (vl-lucid-valid-bits-for-datatype x ss ctx)))

Theorem: vl-lucid-valid-bits-for-datatype-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-lucid-valid-bits-for-datatype-vl-scopestack-equiv-congruence-on-ss
 (implies (vl-scopestack-equiv ss ss-equiv)
          (equal (vl-lucid-valid-bits-for-datatype x ss ctx)
                 (vl-lucid-valid-bits-for-datatype x ss-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-lucid-valid-bits-for-datatype-of-identity-ctx

(defthm vl-lucid-valid-bits-for-datatype-of-identity-ctx
  (equal (vl-lucid-valid-bits-for-datatype x ss (identity ctx))
         (vl-lucid-valid-bits-for-datatype x ss ctx)))

Theorem: vl-lucid-valid-bits-for-datatype-equal-congruence-on-ctx

(defthm vl-lucid-valid-bits-for-datatype-equal-congruence-on-ctx
 (implies (equal ctx ctx-equiv)
          (equal (vl-lucid-valid-bits-for-datatype x ss ctx)
                 (vl-lucid-valid-bits-for-datatype x ss ctx-equiv)))
 :rule-classes :congruence)