		Search-engine friendly clone of the ACL2 documentation.

Defobject-implementation

Defobject-process-name

Process the name input.

Signature
(defobject-process-name name call wrld) → (mv erp name-string name-ident redundantp)
Arguments: call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: name-string — Type (stringp name-string).; name-ident — Type (identp name-ident).; redundantp — Type (booleanp redundantp).

We check that it is a symbol whose name is a portable ASCII identifier. If its name is not a key of the defobject table, we return the name as a string and as an identifier, along with an indication that the call is not redundant. If its name is already in the defobject table, we ensure that the current call is identical to the one stored there, in which case we return an indication that the call is redundant.

Definitions and Theorems

Function: defobject-process-name

(defun defobject-process-name (name call wrld)
 (declare (xargs :guard (and (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__ 'defobject-process-name))
  (declare (ignorable __function__))
  (b*
   (((reterr) "" (irr-ident) nil)
    ((unless (symbolp name))
     (reterr (msg "The first input ~x0 must be a symbol."
                  name)))
    (name-string (symbol-name name))
    ((unless (paident-stringp name-string))
     (reterr
      (msg
       "The SYMBOL-NAME ~x0 of the first input ~x1 ~
                      must be a portable ASCII C identifier."
       name-string name)))
    (name-ident (ident name-string))
    (info (defobject-table-lookup name-string wrld))
    ((when info)
     (if (equal call (defobject-info->call info))
         (retok name-string name-ident t)
      (reterr
       (msg
        "There is already an external object with name ~x0, ~
                        recorded in the table of shallowly embedded ~
                        C external objects, ~
                        but its call ~x1 differs from the current call ~x2, ~
                        and so the call is not redundant."
        name-string (defobject-info->call info)
        call)))))
   (retok name-string name-ident nil))))

Theorem: stringp-of-defobject-process-name.name-string

(defthm stringp-of-defobject-process-name.name-string
  (b* (((mv acl2::?erp
            ?name-string ?name-ident ?redundantp)
        (defobject-process-name name call wrld)))
    (stringp name-string))
  :rule-classes :rewrite)

Theorem: identp-of-defobject-process-name.name-ident

(defthm identp-of-defobject-process-name.name-ident
  (b* (((mv acl2::?erp
            ?name-string ?name-ident ?redundantp)
        (defobject-process-name name call wrld)))
    (identp name-ident))
  :rule-classes :rewrite)

Theorem: booleanp-of-defobject-process-name.redundantp

(defthm booleanp-of-defobject-process-name.redundantp
  (b* (((mv acl2::?erp
            ?name-string ?name-ident ?redundantp)
        (defobject-process-name name call wrld)))
    (booleanp redundantp))
  :rule-classes :rewrite)