		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. If the literal is a character string literal (i.e. it has no encoding prefix) or a UTF-8 string literal (i.e. it has the u8 prefix), it has an array type with element type char. If an encoding prefix is present, the literal may have type wchar_t or char16_t or char32_t. Since we do not yet model the values of these type definitions, we return an array type with an unknown element type in these cases.

Definitions and Theorems

Function: valid-stringlit

(defun valid-stringlit (strlit ienv)
  (declare (xargs :guard (and (stringlitp strlit) (ienvp ienv))))
  (b* (((reterr) (irr-type))
       ((stringlit strlit) strlit)
       ((erp &)
        (valid-s-char-list strlit.schars strlit.prefix? ienv)))
    (retok (make-type-array
                :of
                (if (or (not strlit.prefix?)
                        (eprefix-case strlit.prefix? :locase-u8))
                    (type-char)
                  (type-unknown))))))

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 (ienv-fix ienv))
         (valid-stringlit strlit ienv)))

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

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