		Search-engine friendly clone of the ACL2 documentation.

Defobject-info

Make-defobject-info

Basic constructor macro for defobject-info structures.

Syntax

(make-defobject-info [:name-ident <name-ident>] 
                     [:name-symbol <name-symbol>] 
                     [:type <type>] 
                     [:init <init>] 
                     [:recognizer <recognizer>] 
                     [:initializer <initializer>] 
                     [:call <call>])

This is the usual way to construct defobject-info structures. It simply conses together a structure with the specified fields.

This macro generates a new defobject-info structure from scratch. See also change-defobject-info, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-defobject-info

(defmacro make-defobject-info (&rest args)
  (std::make-aggregate 'defobject-info
                       args
                       '((:name-ident)
                         (:name-symbol)
                         (:type)
                         (:init)
                         (:recognizer)
                         (:initializer)
                         (:call))
                       'make-defobject-info
                       nil))

Function: defobject-info

(defun defobject-info
       (name-ident name-symbol
                   type init recognizer initializer call)
  (declare (xargs :guard (and (identp name-ident)
                              (symbolp name-symbol)
                              (typep type)
                              (initer-optionp init)
                              (symbolp recognizer)
                              (symbolp initializer)
                              (pseudo-event-formp call))))
  (declare (xargs :guard t))
  (let ((__function__ 'defobject-info))
    (declare (ignorable __function__))
    (b* ((name-ident (mbe :logic (ident-fix name-ident)
                          :exec name-ident))
         (name-symbol (mbe :logic (symbol-fix name-symbol)
                           :exec name-symbol))
         (type (mbe :logic (type-fix type) :exec type))
         (init (mbe :logic (initer-option-fix init)
                    :exec init))
         (recognizer (mbe :logic (symbol-fix recognizer)
                          :exec recognizer))
         (initializer (mbe :logic (symbol-fix initializer)
                           :exec initializer))
         (call (mbe :logic (acl2::pseudo-event-form-fix call)
                    :exec call)))
      (list (cons 'name-ident name-ident)
            (cons 'name-symbol name-symbol)
            (cons 'type type)
            (cons 'init init)
            (cons 'recognizer recognizer)
            (cons 'initializer initializer)
            (cons 'call call)))))