		Search-engine friendly clone of the ACL2 documentation.

Message-utilities

Msg-downcase-first

Convert the first character of a structured message to lower case.

Signature
(msg-downcase-first msg) → new-msg
Arguments: msg — Guard (msgp msg).
Returns: new-msg — Type (msgp new-msg), given the guard.

If the message is a string, we use str::downcase-first on the string.

Otherwise, if the format string of the message does not start with a tilde-directive (see fmt), we use str::downcase-first on the format string.

Otherwise, we need to look at the tilde-directive that starts the format string of the message, and possibly modify the tilde-directive and the corresponding value in the alist, in order to suitably convert the first character of the resulting formatted string to lower case. This is done as follows:

If the command character of the tilde-directive is x, y, X, Y, f, or F, we leave the message unchanged because these directives prints all the ACL2 values in a way that capitalization does not really apply: numbers are not words, symbols are in all caps or start with |, characters start with #, strings start with ", and cons pairs start with (.
If the command character of the tilde-directive is t, c, space, _, newline, %, |, ~, or -, we leave the message unchanged because these directives do not print words.
If the command character of the tilde-directive is n, we leave the message unchanged because that directive already prints words that start with lower case characters.
If the command character of the tilde-directive is N, we replace it with n.
If the command character of the tilde-directive is @, we find the corresponding message in the alist and we recursively process it with this function.
If the command character of the tilde-directive is s or S, we find the corresponding string or symbol in the alist, and if it is a string we use str::downcase-first on it. If instead it is a symbol, we leave the message unchanged because symbols are in all caps or start with | (as in the case of the x and other command characters above).
If the command character of the tilde-directive is #, *, &, or v, we stop with an error: these directives are currently not supported by the implementation.

Since msgp is a weak recognizer for messages, there is no guarantee that the format string is followed by an alist, and that the values in the alist have the appropriate types. This function leaves the message unchanged if some of these properties do not hold.

Definitions and Theorems

Function: msg-downcase-first

(defun msg-downcase-first (msg)
 (declare (xargs :guard (msgp msg)))
 (let ((__function__ 'msg-downcase-first))
  (declare (ignorable __function__))
  (b*
   (((when (stringp msg))
     (str::downcase-first msg))
    ((cons string alist) msg)
    ((unless (and (> (length string) 0)
                  (eql (char string 0) #\~)))
     (cons (str::downcase-first string)
           alist))
    ((unless (and (>= (length string) 3)
                  (member (char string 1)
                          (list #\@ #\# #\* #\& #\v #\N #\s #\S))))
     msg))
   (case (char string 1)
    (#\@ (b* (((unless (alistp alist)) msg)
              (value (cdr (assoc (char string 2) alist)))
              ((unless (msgp value)) msg)
              (new-alist (acons (char string 2)
                                (msg-downcase-first value)
                                alist)))
           (cons string new-alist)))
    (#\N (b* ((new-string (concatenate 'string
                                       "~n" (subseq string 2 nil))))
           (cons new-string alist)))
    ((#\s #\S)
     (b* (((unless (alistp alist)) msg)
          (value (cdr (assoc (char string 2) alist)))
          ((unless (stringp value)) msg)
          (new-alist (acons (char string 2)
                            (str::downcase-first value)
                            alist)))
       (cons string new-alist)))
    (otherwise (prog2$ (raise "Message not supported: ~x0" msg)
                       msg))))))

Theorem: msgp-of-msg-downcase-first

(defthm msgp-of-msg-downcase-first
  (implies (and (msgp msg))
           (b* ((new-msg (msg-downcase-first msg)))
             (msgp new-msg)))
  :rule-classes :rewrite)