		Search-engine friendly clone of the ACL2 documentation.

Message-utilities

Msg-upcase-first

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

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

This is analogous to msg-downcase-first, but we use str::upcase-first instead of str::downcase-first on the strings, and the roles of the n and N command characters of the tilde-directives are swapped. See the documentation of msg-downcase-first.

Definitions and Theorems

Function: msg-upcase-first

(defun msg-upcase-first (msg)
 (declare (xargs :guard (msgp msg)))
 (let ((__function__ 'msg-upcase-first))
  (declare (ignorable __function__))
  (b*
   (((when (stringp msg))
     (str::upcase-first msg))
    ((cons string alist) msg)
    ((unless (and (> (length string) 0)
                  (eql (char string 0) #\~)))
     (cons (str::upcase-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-upcase-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::upcase-first value)
                            alist)))
       (cons string new-alist)))
    (otherwise (prog2$ (raise "Message not supported: ~x0" msg)
                       msg))))))

Theorem: msgp-of-msg-upcase-first

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