		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Init-value-to-value

Turn an initialization value into a value of a given type.

Signature
(init-value-to-value type ival) → val
Arguments: type — Guard (typep type).; ival — Guard (init-valuep ival).
Returns: val — Type (value-resultp val).

Executing an initializer yields an initialization value, which determines a value for the object being initialized, as formalized by this ACL2 function.

If the initialization value consists of a single value, we require the value's type to match the given type, and we just return the underlying value. In our current C subset, it is always the case that the value is scalar, never aggregate. So, if the check on the type succeeds, it means that the given type is scalar too.

If the initialization value consists of a list of values, we require the given type to be an array type with either no size or size equal to the length of the list of values. We require all the values to have the array element type. We require that there is at least one value, since arrays cannot be empty in C. We create an array value from the values and return it.

Definitions and Theorems

Function: init-value-to-value

(defun init-value-to-value (type ival)
  (declare (xargs :guard (and (typep type) (init-valuep ival))))
  (let ((__function__ 'init-value-to-value))
    (declare (ignorable __function__))
    (init-value-case
         ival :single
         (if (type-equiv (type-of-value ival.get)
                         type)
             ival.get
           (error (list :init-value-mismatch
                        :required (type-fix type)
                        :supplied (init-value-fix ival))))
         :list
         (b* (((unless (type-case type :array))
               (error (list :init-value-type-mismatch
                            :required :array-type
                            :supplied (init-value-fix ival))))
              (elemtype (type-array->of type))
              ((unless (equal (type-list-of-value-list ival.get)
                              (repeat (len ival.get) elemtype)))
               (error (list :init-value-element-type-mismatch
                            :required elemtype
                            :supplied ival.get)))
              (size (type-array->size type))
              ((when (and size (not (equal size (len ival.get)))))
               (error (list :init-value-size-mismatch
                            :required size
                            :supplied (len ival.get))))
              ((unless (consp ival.get))
               (error (list :init-value-empty-mismatch))))
           (make-value-array :elemtype elemtype
                             :elements ival.get)))))

Theorem: value-resultp-of-init-value-to-value

(defthm value-resultp-of-init-value-to-value
  (b* ((val (init-value-to-value type ival)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: init-value-to-value-of-type-fix-type

(defthm init-value-to-value-of-type-fix-type
  (equal (init-value-to-value (type-fix type)
                              ival)
         (init-value-to-value type ival)))

Theorem: init-value-to-value-type-equiv-congruence-on-type

(defthm init-value-to-value-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (init-value-to-value type ival)
                  (init-value-to-value type-equiv ival)))
  :rule-classes :congruence)

Theorem: init-value-to-value-of-init-value-fix-ival

(defthm init-value-to-value-of-init-value-fix-ival
  (equal (init-value-to-value type (init-value-fix ival))
         (init-value-to-value type ival)))

Theorem: init-value-to-value-init-value-equiv-congruence-on-ival

(defthm init-value-to-value-init-value-equiv-congruence-on-ival
  (implies (init-value-equiv ival ival-equiv)
           (equal (init-value-to-value type ival)
                  (init-value-to-value type ival-equiv)))
  :rule-classes :congruence)