		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-stringlit-list

Validate a list of string literals.

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

Our abstract syntax preserves information about adjacent string literals [C17:5.1.1.2/6], by using lists of string literals, instead of single string literals, in various places. So the validator also operates on such lists of string literals.

One basic requirement is that the list is not empty, because there must be at least one string literal; in the future we could built that constraint into the abstract syntax, but for now we put that as a check in the validator.

Another requirement is that there cannot be both UTF-8 and wide prefixes [C17:6.4.5/2], where these kinds of prefixes are defined in [C17:6.4.5/3]. We check that by projecting the optional prefixes and checking for incompatible occurrences.

Whether string literals with different prefixes (satisfying the requirement just mentioned) can be concatenated, and what their combined type is, is implementation-defined [C17:6.4.5/5]. We plan to extend our implementation environments with information about how to treat those cases, but for now we allow all concatenations.

If all literals in the concatenation are character string literals or UTF-8 string literals, the result is an array type with the element type char. Otherwise, it is an array type with an unknown element type. This covers both the case of well-defined wide string literals (whose types we do not yet model), and the implementation-defined mixed string encoding.

Definitions and Theorems

Function: valid-stringlit-list-loop

(defun valid-stringlit-list-loop (strlits ienv)
  (declare (xargs :guard (and (stringlit-listp strlits)
                              (ienvp ienv))))
  (b*
   (((reterr) nil nil)
    ((when (endp strlits)) (retok nil nil))
    ((erp &)
     (valid-stringlit (car strlits) ienv))
    (first-prefix? (stringlit->prefix? (car strlits)))
    ((erp rest-prefix? conflictp)
     (valid-stringlit-list-loop (cdr strlits)
                                ienv))
    (prefix? (or first-prefix? rest-prefix?))
    (conflictp (or conflictp
                   (and first-prefix? rest-prefix?
                        (not (equal first-prefix? rest-prefix?))))))
   (retok prefix? conflictp)))

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

(defthm maybe-msgp-of-valid-stringlit-list-loop.erp
  (b* (((mv acl2::?erp ?prefix? ?conflictp)
        (valid-stringlit-list-loop strlits ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: eprefix-optionp-of-valid-stringlit-list-loop.prefix?

(defthm eprefix-optionp-of-valid-stringlit-list-loop.prefix?
  (b* (((mv acl2::?erp ?prefix? ?conflictp)
        (valid-stringlit-list-loop strlits ienv)))
    (eprefix-optionp prefix?))
  :rule-classes :rewrite)

Theorem: booleanp-of-valid-stringlit-list-loop.conflictp

(defthm booleanp-of-valid-stringlit-list-loop.conflictp
  (b* (((mv acl2::?erp ?prefix? ?conflictp)
        (valid-stringlit-list-loop strlits ienv)))
    (booleanp conflictp))
  :rule-classes :type-prescription)

Theorem: valid-stringlit-list-loop-of-stringlit-list-fix-strlits

(defthm valid-stringlit-list-loop-of-stringlit-list-fix-strlits
  (equal (valid-stringlit-list-loop (stringlit-list-fix strlits)
                                    ienv)
         (valid-stringlit-list-loop strlits ienv)))

Theorem: valid-stringlit-list-loop-stringlit-list-equiv-congruence-on-strlits

(defthm
 valid-stringlit-list-loop-stringlit-list-equiv-congruence-on-strlits
 (implies (stringlit-list-equiv strlits strlits-equiv)
          (equal (valid-stringlit-list-loop strlits ienv)
                 (valid-stringlit-list-loop strlits-equiv ienv)))
 :rule-classes :congruence)

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

(defthm valid-stringlit-list-loop-of-ienv-fix-ienv
  (equal (valid-stringlit-list-loop strlits (ienv-fix ienv))
         (valid-stringlit-list-loop strlits ienv)))

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

(defthm valid-stringlit-list-loop-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-stringlit-list-loop strlits ienv)
                  (valid-stringlit-list-loop strlits ienv-equiv)))
  :rule-classes :congruence)

Function: valid-stringlit-list

(defun valid-stringlit-list (strlits ienv)
 (declare (xargs :guard (and (stringlit-listp strlits)
                             (ienvp ienv))))
 (b*
  (((reterr) (irr-type))
   ((unless (consp strlits))
    (retmsg$ "There must be at least one string literal."))
   ((erp prefix? conflictp)
    (valid-stringlit-list-loop strlits ienv))
   (prefixes (stringlit-list->prefix?-list strlits))
   ((when (and (member-equal (eprefix-locase-u8)
                             prefixes)
               (or (member-equal (eprefix-locase-u)
                                 prefixes)
                   (member-equal (eprefix-upcase-u)
                                 prefixes)
                   (member-equal (eprefix-upcase-l)
                                 prefixes))))
    (retmsg$
         "Incompatible prefixes ~x0 in the list of string literals."
         prefixes)))
  (retok (make-type-array
              :of
              (if (or conflictp
                      (and prefix?
                           (not (eprefix-case prefix? :locase-u8))))
                  (type-unknown)
                (type-char))))))

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

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

Theorem: typep-of-valid-stringlit-list.type

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

Theorem: valid-stringlit-list-of-stringlit-list-fix-strlits

(defthm valid-stringlit-list-of-stringlit-list-fix-strlits
  (equal (valid-stringlit-list (stringlit-list-fix strlits)
                               ienv)
         (valid-stringlit-list strlits ienv)))

Theorem: valid-stringlit-list-stringlit-list-equiv-congruence-on-strlits

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

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

(defthm valid-stringlit-list-of-ienv-fix-ienv
  (equal (valid-stringlit-list strlits (ienv-fix ienv))
         (valid-stringlit-list strlits ienv)))

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

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