		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-stringlit

Validate a string literal.

Signature
(valid-stringlit strlit ienv) → (mv erp type)
Arguments: strlit — Guard (stringlitp strlit).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; type — Type (typep type).

We check the characters that form the string literal, with respect to the prefix (if any). If validation is successful, we return the type of the string literal, which according to [C17:6.4.5/6], is an array type of char or wchar_t or char16_t or char32_t. In our current approximate type system, we just have a single type for arrays, so we return that.

Definitions and Theorems

Function: valid-stringlit

(defun valid-stringlit (strlit ienv)
  (declare (xargs :guard (and (stringlitp strlit) (ienvp ienv))))
  (let ((__function__ 'valid-stringlit))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-type))
         ((stringlit strlit) strlit)
         ((erp &)
          (valid-s-char-list strlit.schars strlit.prefix? ienv)))
      (retok (type-array)))))

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

(defthm maybe-msgp-of-valid-stringlit.erp
  (b* (((mv acl2::?erp ?type)
        (valid-stringlit strlit ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: typep-of-valid-stringlit.type

(defthm typep-of-valid-stringlit.type
  (b* (((mv acl2::?erp ?type)
        (valid-stringlit strlit ienv)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-stringlit-of-stringlit-fix-strlit

(defthm valid-stringlit-of-stringlit-fix-strlit
  (equal (valid-stringlit (stringlit-fix strlit)
                          ienv)
         (valid-stringlit strlit ienv)))

Theorem: valid-stringlit-stringlit-equiv-congruence-on-strlit

(defthm valid-stringlit-stringlit-equiv-congruence-on-strlit
  (implies (stringlit-equiv strlit strlit-equiv)
           (equal (valid-stringlit strlit ienv)
                  (valid-stringlit strlit-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-stringlit-of-ienv-fix-ienv

(defthm valid-stringlit-of-ienv-fix-ienv
  (equal (valid-stringlit strlit (c::ienv-fix ienv))
         (valid-stringlit strlit ienv)))

Theorem: valid-stringlit-ienv-equiv-congruence-on-ienv

(defthm valid-stringlit-ienv-equiv-congruence-on-ienv
  (implies (c::ienv-equiv ienv ienv-equiv)
           (equal (valid-stringlit strlit ienv)
                  (valid-stringlit strlit ienv-equiv)))
  :rule-classes :congruence)