		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-struct-read-array

Check if a term may represent a structure read of an element of an array member.

Signature
(atc-check-struct-read-array term prec-tags) → (mv erp yes/no fn index struct tag member elem-type flexiblep)
Arguments: term — Guard (pseudo-termp term).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; index — Type (pseudo-termp index).; struct — Type (pseudo-termp struct).; tag — Type (identp tag).; member — Type (identp member).; elem-type — Type (typep elem-type).; flexiblep — Type (booleanp flexiblep).

If the term is a call of the ACL2 function that represent the C structure read operation for elements of array members, we return the reader, the argument terms (index and structure), the tag name, and the name of the member. The C structure type of the reader must be in the preceding tags; we consult the alist to retrieve the relevant information.

We also return the type of the array element.

If the term does not have the right form, we return an indication of failure.

Definitions and Theorems

Function: atc-check-struct-read-array

(defun atc-check-struct-read-array (term prec-tags)
 (declare
      (xargs :guard (and (pseudo-termp term)
                         (atc-string-taginfo-alistp prec-tags))))
 (let ((__function__ 'atc-check-struct-read-array))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil nil nil (irr-ident)
     (irr-ident)
     (irr-type)
     nil)
    ((acl2::fun (no))
     (retok nil nil nil nil (irr-ident)
            (irr-ident)
            (irr-type)
            nil))
    ((mv okp fn args)
     (fty-check-fn-call term))
    ((unless okp) (no))
    ((mv okp struct tag read member element)
     (atc-check-symbol-5part fn))
    ((unless (and okp
                  (equal (symbol-name struct) "STRUCT")
                  (equal (symbol-name read) "READ")
                  (equal (symbol-name element)
                         "ELEMENT")))
     (no))
    (tag (symbol-name tag))
    (info (cdr (assoc-equal tag prec-tags)))
    ((unless info) (no))
    (info (atc-tag-info->defstruct info))
    ((unless (member-eq fn
                        (defstruct-info->reader-element-list info)))
     (reterr
      (msg
       "Invalid function ~x0 encountered: ~
                      it has the form of a structure read ~
                      for the structure type ~x1, ~
                      but it is not among the readers ~
                      associated to that structure type."
       fn tag)))
    (tag (defstruct-info->tag info))
    (members (defstruct-member-info-list->memtype-list
                  (defstruct-info->members info)))
    (member (symbol-name member))
    ((unless (paident-stringp member))
     (reterr
      (raise
           "Internal error: ~x0 is not a portable ASCII identifier."
           member)))
    (member (ident member))
    (mem-type (member-type-lookup member members))
    ((unless mem-type)
     (reterr (raise "Internal error: type of ~x0 not found."
                    member)))
    ((unless (type-case mem-type :array))
     (reterr (raise "Internal error: type of ~x0 is not array."
                    member)))
    (elem-type (type-array->of mem-type))
    (flexiblep (not (type-array->size mem-type)))
    ((unless (list-lenp 2 args))
     (reterr
          (raise "Internal error: ~x0 not applied to 2 arguments."
                 fn)))
    (index (first args))
    (struct (second args)))
   (retok t fn index struct
          tag member elem-type flexiblep))))

Theorem: booleanp-of-atc-check-struct-read-array.yes/no

(defthm booleanp-of-atc-check-struct-read-array.yes/no
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-struct-read-array.fn

(defthm symbolp-of-atc-check-struct-read-array.fn
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-struct-read-array.index

(defthm pseudo-termp-of-atc-check-struct-read-array.index
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (pseudo-termp index))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-struct-read-array.struct

(defthm pseudo-termp-of-atc-check-struct-read-array.struct
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (pseudo-termp struct))
  :rule-classes :rewrite)

Theorem: identp-of-atc-check-struct-read-array.tag

(defthm identp-of-atc-check-struct-read-array.tag
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (identp tag))
  :rule-classes :rewrite)

Theorem: identp-of-atc-check-struct-read-array.member

(defthm identp-of-atc-check-struct-read-array.member
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (identp member))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-struct-read-array.elem-type

(defthm typep-of-atc-check-struct-read-array.elem-type
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (typep elem-type))
  :rule-classes :rewrite)

Theorem: booleanp-of-atc-check-struct-read-array.flexiblep

(defthm booleanp-of-atc-check-struct-read-array.flexiblep
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (booleanp flexiblep))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-struct-read-array-index

(defthm pseudo-term-count-of-atc-check-struct-read-array-index
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (implies yes/no
             (< (pseudo-term-count index)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-atc-check-struct-read-array-struct

(defthm pseudo-term-count-of-atc-check-struct-read-array-struct
  (b* (((mv acl2::?erp
            ?yes/no ?fn ?index ?struct acl2::?tag
            ?member ?elem-type ?flexiblep)
        (atc-check-struct-read-array term prec-tags)))
    (implies yes/no
             (< (pseudo-term-count struct)
                (pseudo-term-count term))))
  :rule-classes :linear)