		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-gensel

Validate a generic selection expression, given the types for the components.

Signature
(valid-gensel expr type type-alist) → (mv erp type)
Arguments: expr — Guard (exprp expr).; type — Guard (typep type).; type-alist — Guard (type-option-type-alistp type-alist).
Returns: erp — Type (maybe-msgp erp).; type — Type (typep type).

For now we do not perform any of the checks prescribed in [C17:6.5.1.1/2]. We will perform them later, when we refine our validator. We return the unknown type.

Definitions and Theorems

Function: valid-gensel

(defun valid-gensel (expr type type-alist)
 (declare (xargs :guard (and (exprp expr)
                             (typep type)
                             (type-option-type-alistp type-alist))))
 (declare (ignore expr type type-alist))
 (declare (xargs :guard (expr-case expr :gensel)))
 (retok (type-unknown)))

Theorem: maybe-msgp-of-valid-gensel.erp

(defthm maybe-msgp-of-valid-gensel.erp
  (b* (((mv acl2::?erp ?type)
        (valid-gensel expr type type-alist)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: typep-of-valid-gensel.type

(defthm typep-of-valid-gensel.type
  (b* (((mv acl2::?erp ?type)
        (valid-gensel expr type type-alist)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-gensel-of-expr-fix-expr

(defthm valid-gensel-of-expr-fix-expr
  (equal (valid-gensel (expr-fix expr)
                       type type-alist)
         (valid-gensel expr type type-alist)))

Theorem: valid-gensel-expr-equiv-congruence-on-expr

(defthm valid-gensel-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (valid-gensel expr type type-alist)
                  (valid-gensel expr-equiv type type-alist)))
  :rule-classes :congruence)

Theorem: valid-gensel-of-type-fix-type

(defthm valid-gensel-of-type-fix-type
  (equal (valid-gensel expr (type-fix type)
                       type-alist)
         (valid-gensel expr type type-alist)))

Theorem: valid-gensel-type-equiv-congruence-on-type

(defthm valid-gensel-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (valid-gensel expr type type-alist)
                  (valid-gensel expr type-equiv type-alist)))
  :rule-classes :congruence)

Theorem: valid-gensel-of-type-option-type-alist-fix-type-alist

(defthm valid-gensel-of-type-option-type-alist-fix-type-alist
  (equal (valid-gensel expr type
                       (type-option-type-alist-fix type-alist))
         (valid-gensel expr type type-alist)))

Theorem: valid-gensel-type-option-type-alist-equiv-congruence-on-type-alist

(defthm
 valid-gensel-type-option-type-alist-equiv-congruence-on-type-alist
 (implies (type-option-type-alist-equiv type-alist type-alist-equiv)
          (equal (valid-gensel expr type type-alist)
                 (valid-gensel expr type type-alist-equiv)))
 :rule-classes :congruence)