		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-struct-read-scalar

Check if a term may represent a structure read of a scalar member.

Signature
(atc-check-struct-read-scalar term prec-tags) → (mv erp yes/no fn arg tag member mem-type)
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).; arg — Type (pseudo-termp arg).; tag — Type (identp tag).; member — Type (identp member).; mem-type — Type (typep mem-type).

If the term is a call of one of the ACL2 functions that represent C structure read operations for scalar members, we return the argument term, 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 member.

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

Definitions and Theorems

Function: atc-check-struct-read-scalar

(defun atc-check-struct-read-scalar (term prec-tags)
 (declare
      (xargs :guard (and (pseudo-termp term)
                         (atc-string-taginfo-alistp prec-tags))))
 (let ((__function__ 'atc-check-struct-read-scalar))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil nil (irr-ident)
     (irr-ident)
     (irr-type))
    ((acl2::fun (no))
     (retok nil nil nil (irr-ident)
            (irr-ident)
            (irr-type)))
    ((mv okp fn args)
     (fty-check-fn-call term))
    ((unless okp) (no))
    ((mv okp struct tag read member)
     (atc-check-symbol-4part fn))
    ((unless (and okp
                  (equal (symbol-name struct) "STRUCT")
                  (equal (symbol-name read) "READ")))
     (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-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-nonchar-integerp mem-type))
     (reterr
          (raise "Internal error: scalar member ~x0 has type ~x1."
                 member mem-type)))
    ((unless (list-lenp 1 args))
     (reterr (raise "Internal error: ~x0 not applied to 1 argument."
                    fn)))
    (arg (car args)))
   (retok t fn arg tag member mem-type))))

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

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

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

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

Theorem: pseudo-termp-of-atc-check-struct-read-scalar.arg

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

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

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

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

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

Theorem: typep-of-atc-check-struct-read-scalar.mem-type

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

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

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

Theorem: type-nonchar-integerp-of-atc-check-struct-read-scalar

(defthm type-nonchar-integerp-of-atc-check-struct-read-scalar
  (b* (((mv acl2::?erp ?yes/no
            ?fn ?arg acl2::?tag ?member ?mem-type)
        (atc-check-struct-read-scalar term prec-tags)))
    (implies yes/no
             (type-nonchar-integerp mem-type))))