		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-process-init

Process the :init input.

Signature
(defobject-process-init init type wrld) → (mv erp initer?)
Arguments: type — Guard (typep type).; wrld — Guard (plist-worldp wrld).
Returns: initer? — An initer-optionp.

We ensure that it is either nil, or a single term that appropriately represents an expression if the type is an integer type, or a non-empty list of terms that appropriately represent expressions if the type is an integer array type; in the last case, the length of the list must match the (positive) size of the array type.

Definitions and Theorems

Function: defobject-process-init

(defun defobject-process-init (init type wrld)
 (declare (xargs :guard (and (typep type) (plist-worldp wrld))))
 (let ((__function__ 'defobject-process-init))
  (declare (ignorable __function__))
  (b* (((reterr) (irr-initer))
       ((when (null init)) (retok nil)))
   (cond
    ((type-integerp type)
     (b* (((erp expr)
           (defobject-process-init-term init type wrld)))
       (retok (initer-single expr))))
    ((type-case type :array)
     (b*
      (((unless (true-listp init))
        (reterr
         (msg
          "Since the object's type is ~x0, ~
                               the :INIT input must be a list, ~
                               but it is ~x0 instead."
          type init)))
       (elemtype (type-array->of type))
       (size (type-array->size type))
       ((unless (equal (len init) size))
        (reterr
         (msg
          "The number ~x0 of elements of the :INIT input ~
                        must match the size ~x1 of the array ~
                        specified by the :TYPE input."
          (len init)
          size)))
       ((erp exprs)
        (defobject-process-init-terms init elemtype wrld)))
      (retok (initer-list exprs))))
    (t (reterr (raise "Internal error: type ~x0." type)))))))