		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-target

Process a target among t1, ..., tp.

Signature
(atc-process-target target previous-structs previous-objs previous-fns uncalled-fns wrld) → (mv erp target$ new-previous-structs new-previous-objs new-previous-fns new-uncalled-fns)
Arguments: previous-structs — Guard (symbol-listp previous-structs).; previous-objs — Guard (symbol-listp previous-objs).; previous-fns — Guard (symbol-listp previous-fns).; uncalled-fns — Guard (symbol-listp uncalled-fns).; wrld — Guard (plist-worldp wrld).
Returns: target$ — Type (symbolp target$).; new-previous-structs — Type (symbol-listp new-previous-structs), given (symbol-listp previous-structs).; new-previous-objs — Type (symbol-listp new-previous-objs), given (symbol-listp previous-objs).; new-previous-fns — Type (symbol-listp new-previous-fns), given (symbol-listp previous-fns).; new-uncalled-fns — Type (symbol-listp new-uncalled-fns), given (symbol-listp uncalled-fns).

The parameters previous-fns and uncalled-fns are explained in atc-process-function. The parameters previous-structs and previous-objs are analogous to previous-fns, but for the defstruct and defobject targets instead of the function targets: it lists all the defstruct and defobject targets that precede target in the list of targets (t1 ... tp). This is used to detect duplicate symbol names.

If the target is a function name, its processing is delegated to atc-process-function, except for ensuring that its symbol name is distinct from the symbol names of the preceding targets. Otherwise, the target must be a defstruct or defobject name, and it is processed here: we check that it is in the defstruct or defobject table; furthermore, if it is a defobject target, we ensure that it differs from the preceding function targets.

If all the checks are successful, we also return the target itself, with a guaranteed symbolp type, so that calling code has that fact readily available.

Definitions and Theorems

Function: atc-process-target

(defun atc-process-target (target previous-structs previous-objs
                                  previous-fns uncalled-fns wrld)
 (declare (xargs :guard (and (symbol-listp previous-structs)
                             (symbol-listp previous-objs)
                             (symbol-listp previous-fns)
                             (symbol-listp uncalled-fns)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-process-target))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil nil nil nil)
    ((unless (symbolp target))
     (reterr (msg "The target ~x0 is not a symbol."
                  target)))
    (functionp (function-symbolp target wrld))
    (struct-info (defstruct-table-lookup (symbol-name target)
                                         wrld))
    (obj-info (defobject-table-lookup (symbol-name target)
                                      wrld))
    ((when (and functionp struct-info obj-info))
     (reterr
      (msg
       "The target ~x0 ambiguously denotes ~
                      a function, a DEFSTRUCT, and a DEFOBJECT."
       target)))
    ((when (and functionp struct-info))
     (reterr
      (msg
       "The target ~x0 ambiguously denotes ~
                      a function and a DEFSTRUCT."
       target)))
    ((when (and functionp obj-info))
     (reterr
      (msg
       "The target ~x0 ambiguously denotes ~
                      a function and a DEFOBJECT"
       target)))
    ((when (and struct-info obj-info))
     (reterr
      (msg
       "The target ~x0 ambiguously denotes ~
                      a DEFSTRUCT and a DEFOBJECT."
       target)))
    ((when functionp)
     (b*
      ((found (member-equal (symbol-name target)
                            (symbol-name-lst previous-fns)))
       ((when found)
        (reterr
         (msg
          "The target function ~x0 has the same name as ~
                            the target function ~x1 that precedes it."
          target (car previous-fns))))
       (found (member-equal (symbol-name target)
                            (symbol-name-lst previous-structs)))
       ((when found)
        (reterr
         (msg
          "The target function ~x0 has the same name as ~
                            the target DEFSTRUCT ~x1 that precedes it."
          target (car previous-structs))))
       (found (member-equal (symbol-name target)
                            (symbol-name-lst previous-objs)))
       ((when found)
        (reterr
         (msg
          "The target function ~x0 has the same name as ~
                            the target DEFOBJECT ~x1 that precedes it."
          target (car previous-objs))))
       ((erp previous-fns uncalled-fns)
        (atc-process-function
             target previous-fns uncalled-fns wrld)))
      (retok target previous-structs previous-objs
             previous-fns uncalled-fns)))
    ((when struct-info)
     (b*
      ((found (member-equal (symbol-name target)
                            (symbol-name-lst previous-fns)))
       ((when found)
        (reterr
         (msg
          "The target DEFSTRUCT ~x0 has the same name as ~
                            the target function ~x1 that precedes it."
          target (car previous-fns))))
       (found (member-equal (symbol-name target)
                            (symbol-name-lst previous-structs)))
       ((when found)
        (reterr
         (msg
          "The target DEFSTRUCT ~x0 has the same name as ~
                            the target DEFSTRUCT ~x1 that precedes it."
          target (car previous-structs))))
       (found (member-equal (symbol-name target)
                            (symbol-name-lst previous-objs)))
       ((when found)
        (reterr
         (msg
          "The target DEFSTRUCT ~x0 has the same name as ~
                            the target DEFOBJECT ~x1 that precedes it."
          target (car previous-objs))))
       (previous-structs (cons target previous-structs)))
      (retok target previous-structs previous-objs
             previous-fns uncalled-fns)))
    ((when obj-info)
     (b*
      ((found (member-equal (symbol-name target)
                            (symbol-name-lst previous-fns)))
       ((when found)
        (reterr
         (msg
          "The target DEFOBJECT ~x0 has the same name as ~
                            the target function ~x1 that precedes it."
          target (car previous-fns))))
       (found (member-equal (symbol-name target)
                            (symbol-name-lst previous-structs)))
       ((when found)
        (reterr
         (msg
          "The target DEFOBJECT ~x0 has the same name as ~
                            the target DEFSTRUCT ~x1 that precedes it."
          target (car previous-structs))))
       (found (member-equal (symbol-name target)
                            (symbol-name-lst previous-objs)))
       ((when found)
        (reterr
         (msg
          "The target DEFOBJECT ~x0 has the same name as ~
                            the target DEFOBJECT ~x1 that precedes it."
          target (car previous-objs))))
       (previous-objs (cons target previous-objs)))
      (retok target previous-structs previous-objs
             previous-fns uncalled-fns))))
   (reterr
    (msg
     "The target ~x0 is a symbol that does not identify ~
                  any function or DEFSTRUCT or DEFOBJECT."
     target)))))

Theorem: symbolp-of-atc-process-target.target$

(defthm symbolp-of-atc-process-target.target$
  (b* (((mv acl2::?erp ?target$
            ?new-previous-structs ?new-previous-objs
            ?new-previous-fns ?new-uncalled-fns)
        (atc-process-target target previous-structs previous-objs
                            previous-fns uncalled-fns wrld)))
    (symbolp target$))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-process-target.new-previous-structs

(defthm symbol-listp-of-atc-process-target.new-previous-structs
 (implies
     (symbol-listp previous-structs)
     (b* (((mv acl2::?erp ?target$
               ?new-previous-structs ?new-previous-objs
               ?new-previous-fns ?new-uncalled-fns)
           (atc-process-target target previous-structs previous-objs
                               previous-fns uncalled-fns wrld)))
       (symbol-listp new-previous-structs)))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-process-target.new-previous-objs

(defthm symbol-listp-of-atc-process-target.new-previous-objs
 (implies
     (symbol-listp previous-objs)
     (b* (((mv acl2::?erp ?target$
               ?new-previous-structs ?new-previous-objs
               ?new-previous-fns ?new-uncalled-fns)
           (atc-process-target target previous-structs previous-objs
                               previous-fns uncalled-fns wrld)))
       (symbol-listp new-previous-objs)))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-process-target.new-previous-fns

(defthm symbol-listp-of-atc-process-target.new-previous-fns
 (implies
     (symbol-listp previous-fns)
     (b* (((mv acl2::?erp ?target$
               ?new-previous-structs ?new-previous-objs
               ?new-previous-fns ?new-uncalled-fns)
           (atc-process-target target previous-structs previous-objs
                               previous-fns uncalled-fns wrld)))
       (symbol-listp new-previous-fns)))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-process-target.new-uncalled-fns

(defthm symbol-listp-of-atc-process-target.new-uncalled-fns
 (implies
     (symbol-listp uncalled-fns)
     (b* (((mv acl2::?erp ?target$
               ?new-previous-structs ?new-previous-objs
               ?new-previous-fns ?new-uncalled-fns)
           (atc-process-target target previous-structs previous-objs
                               previous-fns uncalled-fns wrld)))
       (symbol-listp new-uncalled-fns)))
 :rule-classes :rewrite)

Theorem: true-listp-of-atc-process-target.new-previous-structs

(defthm true-listp-of-atc-process-target.new-previous-structs
 (implies
     (true-listp previous-structs)
     (b* (((mv acl2::?erp ?target$
               ?new-previous-structs ?new-previous-objs
               ?new-previous-fns ?new-uncalled-fns)
           (atc-process-target target previous-structs previous-objs
                               previous-fns uncalled-fns wrld)))
       (true-listp new-previous-structs)))
 :rule-classes :type-prescription)

Theorem: true-listp-of-atc-process-target.new-previous-objs

(defthm true-listp-of-atc-process-target.new-previous-objs
 (implies
     (true-listp previous-objs)
     (b* (((mv acl2::?erp ?target$
               ?new-previous-structs ?new-previous-objs
               ?new-previous-fns ?new-uncalled-fns)
           (atc-process-target target previous-structs previous-objs
                               previous-fns uncalled-fns wrld)))
       (true-listp new-previous-objs)))
 :rule-classes :type-prescription)

Theorem: true-listp-of-atc-process-target.new-previous-fns

(defthm true-listp-of-atc-process-target.new-previous-fns
 (implies
     (true-listp previous-fns)
     (b* (((mv acl2::?erp ?target$
               ?new-previous-structs ?new-previous-objs
               ?new-previous-fns ?new-uncalled-fns)
           (atc-process-target target previous-structs previous-objs
                               previous-fns uncalled-fns wrld)))
       (true-listp new-previous-fns)))
 :rule-classes :type-prescription)

Theorem: true-listp-of-atc-process-target.new-uncalled-fns

(defthm true-listp-of-atc-process-target.new-uncalled-fns
 (implies
     (true-listp uncalled-fns)
     (b* (((mv acl2::?erp ?target$
               ?new-previous-structs ?new-previous-objs
               ?new-previous-fns ?new-uncalled-fns)
           (atc-process-target target previous-structs previous-objs
                               previous-fns uncalled-fns wrld)))
       (true-listp new-uncalled-fns)))
 :rule-classes :type-prescription)