		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-gen-everything

Generate all the events.

Signature
(defobject-gen-everything name name-string name-ident type init initer? call) → event
Arguments: name — Guard (symbolp name).; name-string — Guard (stringp name-string).; name-ident — Guard (identp name-ident).; type — Guard (typep type).; initer? — Guard (initer-optionp initer?).; call — Guard (pseudo-event-formp call).
Returns: event — Type (pseudo-event-formp event).

These are the recognizer, initializer, and table event. They are put into one progn event. We conclude with a deflabel event that facilitates history manipulation.

Definitions and Theorems

Function: defobject-gen-everything

(defun defobject-gen-everything
       (name name-string
             name-ident type init initer? call)
 (declare (xargs :guard (and (symbolp name)
                             (stringp name-string)
                             (identp name-ident)
                             (typep type)
                             (initer-optionp initer?)
                             (pseudo-event-formp call))))
 (let ((__function__ 'defobject-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((recognizer-name (packn-pos (list 'object- name '-p)
                                name))
    (initializer-name (packn-pos (list 'object- name '-init)
                                 name))
    ((mv recognizer-event initializer-event)
     (cond
      ((type-integerp type)
       (b*
        (((unless (type-nonchar-integerp type))
          (raise "Internal error: not integer type ~x0."
                 type)
          (mv '(_) '(_)))
         (fixtype (integer-type-to-fixtype type))
         (fixtype-pred (pack fixtype 'p))
         (fixtype-from-integer (pack fixtype '-from-integer))
         (recognizer-event
          (cons
              'define
              (cons recognizer-name
                    (cons '(x)
                          (cons ':returns
                                (cons '(yes/no booleanp)
                                      (cons (cons fixtype-pred '(x))
                                            'nil)))))))
         (initializer-event
          (cons
           'define
           (cons
            initializer-name
            (cons
             'nil
             (cons
              ':returns
              (cons (cons 'object
                          (cons recognizer-name 'nil))
                    (cons (or init (cons fixtype-from-integer '(0)))
                          'nil))))))))
        (mv recognizer-event initializer-event)))
      ((type-case type :array)
       (b*
        (((unless (type-nonchar-integerp (type-array->of type)))
          (raise "Internal error: not integer array type ~x0."
                 type)
          (mv '(_) '(_)))
         (fixtype (integer-type-to-fixtype (type-array->of type)))
         (fixtype-from-integer (pack fixtype '-from-integer))
         (size (type-array->size type))
         (type-arrayp (pack fixtype '-arrayp))
         (type-array-length (pack fixtype '-array-length))
         (type-array-of (pack fixtype '-array-of))
         (recognizer-event
          (cons
           'define
           (cons
            recognizer-name
            (cons
             '(x)
             (cons
              ':returns
              (cons
               '(yes/no booleanp)
               (cons
                (cons
                 'and
                 (cons
                     (cons type-arrayp '(x))
                     (cons (cons 'equal
                                 (cons (cons type-array-length '(x))
                                       (cons size 'nil)))
                           'nil)))
                'nil)))))))
         (initializer-event
          (cons
           'define
           (cons
            initializer-name
            (cons
             'nil
             (cons
              ':returns
              (cons
               (cons 'object
                     (cons recognizer-name 'nil))
               (cons
                (cons
                 type-array-of
                 (cons
                  (if (consp init)
                      (cons 'list init)
                   (cons
                        'repeat
                        (cons size
                              (cons (cons fixtype-from-integer '(0))
                                    'nil))))
                  'nil))
                'nil))))))))
        (mv recognizer-event initializer-event)))
      (t (prog2$ (raise "Internal error: type ~x0." type)
                 (mv '(_) '(_))))))
    (info (make-defobject-info :name-ident name-ident
                               :name-symbol name
                               :type type
                               :init initer?
                               :recognizer recognizer-name
                               :initializer initializer-name
                               :call call))
    (table-event (defobject-table-record-event name-string info))
    (label-event (cons 'deflabel (cons name 'nil))))
   (cons 'progn
         (cons recognizer-event
               (cons initializer-event
                     (cons table-event
                           (cons label-event 'nil))))))))

Theorem: pseudo-event-formp-of-defobject-gen-everything

(defthm pseudo-event-formp-of-defobject-gen-everything
 (b*
  ((event
      (defobject-gen-everything name name-string
                                name-ident type init initer? call)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)