		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-stringlit

Validate a string literal.

Signature
(valid-stringlit strlit) → (mv erp type)
Arguments: strlit — Guard (stringlitp strlit).
Returns: 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 [C: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)
  (declare (xargs :guard (stringlitp strlit)))
  (let ((__function__ 'valid-stringlit))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-type))
         ((stringlit strlit) strlit)
         ((erp &)
          (valid-s-char-list strlit.schars strlit.prefix?)))
      (retok (type-array)))))

Theorem: typep-of-valid-stringlit.type

(defthm typep-of-valid-stringlit.type
  (b* (((mv acl2::?erp ?type)
        (valid-stringlit strlit)))
    (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))
         (valid-stringlit strlit)))

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)
                  (valid-stringlit strlit-equiv)))
  :rule-classes :congruence)