		Search-engine friendly clone of the ACL2 documentation.

Static-environments

Get-struct-sinfo

Retrieve information about a struct type from a static environment.

Signature
(get-struct-sinfo circ env) → info
Arguments: circ — Guard (identifierp circ).; env — Guard (senvp env).
Returns: info — Type (struct-sinfo-optionp info).

We return nil if the function is not found. This includes the case that the identifier is in the environment but it does not refer to a struct type

Definitions and Theorems

Function: get-struct-sinfo

(defun get-struct-sinfo (circ env)
  (declare (xargs :guard (and (identifierp circ) (senvp env))))
  (let ((__function__ 'get-struct-sinfo))
    (declare (ignorable __function__))
    (b* ((info (get-ident-sinfo circ env))
         ((unless info) nil))
      (ident-sinfo-case info
                        :var/const nil
                        :function nil
                        :struct info.get))))

Theorem: struct-sinfo-optionp-of-get-struct-sinfo

(defthm struct-sinfo-optionp-of-get-struct-sinfo
  (b* ((info (get-struct-sinfo circ env)))
    (struct-sinfo-optionp info))
  :rule-classes :rewrite)

Theorem: get-struct-sinfo-of-identifier-fix-circ

(defthm get-struct-sinfo-of-identifier-fix-circ
  (equal (get-struct-sinfo (identifier-fix circ)
                           env)
         (get-struct-sinfo circ env)))

Theorem: get-struct-sinfo-identifier-equiv-congruence-on-circ

(defthm get-struct-sinfo-identifier-equiv-congruence-on-circ
  (implies (identifier-equiv circ circ-equiv)
           (equal (get-struct-sinfo circ env)
                  (get-struct-sinfo circ-equiv env)))
  :rule-classes :congruence)

Theorem: get-struct-sinfo-of-senv-fix-env

(defthm get-struct-sinfo-of-senv-fix-env
  (equal (get-struct-sinfo circ (senv-fix env))
         (get-struct-sinfo circ env)))

Theorem: get-struct-sinfo-senv-equiv-congruence-on-env

(defthm get-struct-sinfo-senv-equiv-congruence-on-env
  (implies (senv-equiv env env-equiv)
           (equal (get-struct-sinfo circ env)
                  (get-struct-sinfo circ env-equiv)))
  :rule-classes :congruence)