		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-process-init-term

Process a term that is the :init input or an element of :init input.

Signature
(defobject-process-init-term term required-type wrld) → (mv erp expr)
Arguments: required-type — Guard (typep required-type).; wrld — Guard (plist-worldp wrld).
Returns: expr — An exprp.

We translate the term. We check whether it has the form required in the user documentation, and whether it has the right type, which is passed as argument. We return the expression represented by the term, if all the checks succeed.

Definitions and Theorems

Function: defobject-process-init-term

(defun defobject-process-init-term (term required-type wrld)
 (declare (xargs :guard (and (typep required-type)
                             (plist-worldp wrld))))
 (let ((__function__ 'defobject-process-init-term))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-expr))
    ((mv term/msg stobjs-out)
     (acl2::check-user-term term wrld))
    ((unless (pseudo-termp term/msg))
     (reterr
      (msg
       "The initializer term ~x0 must be an untranslated term.  ~
                      ~@1"
       term term/msg)))
    ((unless (equal stobjs-out (list nil)))
     (reterr
      (msg
       "The initializer term ~x0 must return ~
                      a single non-stobj value, ~
                      but it returns ~x1 instead."
       term stobjs-out)))
    ((erp expr type)
     (defobject-term-to-expr term/msg))
    ((unless (equal type required-type))
     (reterr
      (msg
       "The initializer term ~x0 has type ~x1, ~
                      which does not match the required type ~x2."
       term type required-type))))
   (retok expr))))