messages

(in-package "ACL2")

(set-induction-depth-limit 0)

(make-define-config :no-function t)

(defxdoc message-utilities
  :parents (kestrel-utilities)
  :short "Utilities for <see topic='@(url msgp)'>messages</see>.")

(defxdoc msg$
  :parents (msg message-utilities)
  :short "A variant of @('msg') which is easier to reason about."
  :long (topstring (p "@('msg$') is a macro which will rewrite to a call of @('msg$-logic').
       @('msg$-logic') is kept disabled and is known to produce a
       @('msgp'). For execution, @('msg$') expands to something which is
       inlined for efficiency.")))

(define maybe-msgp
  (x)
  :returns (yes/no booleanp)
  :parents (message-utilities)
  :short "Recognize @('nil') and messages."
  (or (msgp x) (null x))
  ///
  (defrule maybe-msgp-compound-recognizer
    (if (maybe-msgp x)
      (or (equal x nil)
        (stringp x)
        (and (consp x) (true-listp x)))
      (and (not (equal x nil)) (not (stringp x))))
    :rule-classes :compound-recognizer)
  (defrule maybe-msgp-when-msgp
    (implies (msgp x) (maybe-msgp x))))

(deflist msg-listp
  (x)
  (msgp x)
  :parents (message-utilities)
  :short "Recognize true lists of messages."
  :true-listp t
  :elementp-of-nil nil)

(define msg-fix
  ((msg msgp))
  :returns (msg$ msgp)
  (mbe :logic (if (msgp msg)
      msg
      "")
    :exec (the (or string cons) msg))
  :inline t)

(defruled msg-fix-when-not-msgp
  (implies (not (msgp msg)) (equal (msg-fix msg) ""))
  :enable msg-fix)

(define msg$0
  ((str stringp))
  (mbe :logic (if (stringp str)
      str
      "")
    :exec str)
  :inline t)

(define msg$1
  ((str stringp) arg0)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0)
  :inline t)

(define msg$2
  ((str stringp) arg0 arg1)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1)
  :inline t)

(define msg$3
  ((str stringp) arg0 arg1 arg2)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1
    arg2)
  :inline t)

(define msg$4
  ((str stringp) arg0 arg1 arg2 arg3)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1
    arg2
    arg3)
  :inline t)

(define msg$5
  ((str stringp) arg0 arg1 arg2 arg3 arg4)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1
    arg2
    arg3
    arg4)
  :inline t)

(define msg$6
  ((str stringp) arg0 arg1 arg2 arg3 arg4 arg5)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1
    arg2
    arg3
    arg4
    arg5)
  :inline t)

(define msg$7
  ((str stringp) arg0 arg1 arg2 arg3 arg4 arg5 arg6)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1
    arg2
    arg3
    arg4
    arg5
    arg6)
  :inline t)

(define msg$8
  ((str stringp) arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1
    arg2
    arg3
    arg4
    arg5
    arg6
    arg7)
  :inline t)

(define msg$9
  ((str stringp) arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1
    arg2
    arg3
    arg4
    arg5
    arg6
    arg7
    arg8)
  :inline t)

(define msg$10
  ((str stringp) arg0
    arg1
    arg2
    arg3
    arg4
    arg5
    arg6
    arg7
    arg8
    arg9)
  (msg (mbe :logic (if (stringp str)
        str
        "")
      :exec str)
    arg0
    arg1
    arg2
    arg3
    arg4
    arg5
    arg6
    arg7
    arg8
    arg9)
  :inline t)

(define msg$-logic
  (str args)
  (declare (xargs :type-prescription (or (stringp (msg$-logic str args))
        (and (consp (msg$-logic str args))
          (true-listp (msg$-logic str args))))
      :guard (hide (comment "msg$-logic is not intended to be used in code. Use msg$ instead."
          (true-listp args)))
      :guard-hints (("Goal" :expand ((:free (x) (hide x)))))))
  :returns (msg msgp :hints (("Goal" :in-theory (enable msgp))))
  (if (consp args)
    (cons (if (stringp str)
        str
        "")
      (if (<= (len args) 10)
        (pairlis$ (take (len args) *base-10-chars*) args)
        nil))
    (if (stringp str)
      str
      ""))
  :prepwork ((defrulel character-alistp-of-pairlis$
     (implies (and (character-listp x) (equal (len x) (len y)))
       (character-alistp (pairlis$ x y)))
     :induct t
     :enable (pairlis$ character-alistp character-listp len))))

(define msg-downcase-first
  ((msg msgp))
  :returns (new-msg msgp
    :hints (("Goal" :induct t :in-theory (enable character-alistp))))
  :parents (message-utilities)
  :short "Convert the first character
          of a <see topic='@(url msg)'>structured message</see>
          to lower case."
  :long "<p>
   If the message is a string,
   we use @(tsee str::downcase-first) on the string.
   </p>
   <p>
   Otherwise, if the format string of the message
   does not start with a tilde-directive (see @(tsee fmt)),
   we use @(tsee str::downcase-first) on the format string.
   </p>
   <p>
   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:
   </p>
   <ul>
     <li>
     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 @(tsee cons) pairs start with @('(').
     </li>
     <li>
     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.
     </li>
     <li>
     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.
     </li>
     <li>
     If the command character of the tilde-directive is @('N'),
     we replace it with @('n').
     </li>
     <li>
     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.
     </li>
     <li>
     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 @(tsee 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).
     </li>
     <li>
     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.
     </li>
   </ul>
   <p>
   Since @(tsee 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.
   </p>"
  (b* ((msg (msg-fix msg)) ((when (stringp msg)) (downcase-first msg))
      ((cons string alist) msg)
      ((unless (and (> (length string) 0) (eql (char string 0) #\~))) (cons (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) (downcase-first value) alist)))
          (cons string new-alist)))
      (otherwise (prog2$ (raise "Message not supported: ~x0" msg) msg))))
  :no-function nil
  :measure (acl2-count (msg-fix msg)))

(define msg-upcase-first
  ((msg msgp))
  :returns (new-msg msgp
    :hints (("Goal" :induct t :in-theory (enable character-alistp))))
  :parents (message-utilities)
  :short "Convert the first character
          of a <see topic='@(url msg)'>structured message</see>
          to upper case."
  :long "<p>
   This is analogous to @(tsee msg-downcase-first),
   but we use @(tsee str::upcase-first) instead of @(tsee 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 @(tsee msg-downcase-first).
   </p>"
  (b* ((msg (msg-fix msg)) ((when (stringp msg)) (upcase-first msg))
      ((cons string alist) msg)
      ((unless (and (> (length string) 0) (eql (char string 0) #\~))) (cons (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) (upcase-first value) alist)))
          (cons string new-alist)))
      (otherwise (prog2$ (raise "Message not supported: ~x0" msg) msg))))
  :no-function nil
  :measure (acl2-count (msg-fix msg)))