char-case

(in-package "STR")

(include-book "eqv")

(local (include-book "arithmetic"))

(defmacro little-a nil (char-code #\a))

(defmacro little-z nil (char-code #\z))

(defmacro big-a nil (char-code #\A))

(defmacro big-z nil (char-code #\Z))

(defmacro case-delta
  nil
  (- (little-a) (big-a)))

(define up-alpha-p
  ((x :type character))
  :returns bool
  :parents (cases upper-case-p)
  :short "Determine if a character is an upper-case letter (A-Z)."
  :long "<p>ACL2 has a built-in alternative to this function, @(see
 acl2::upper-case-p), which however can also recognize characters that are not
 standard characters.  (Historical note: Before May 2024, the guard for
 acl2::upper-case-p required standard-char-p yet also converted only standard
 characters; this provided motivation for the development of
 up-alpha-p.)</p>"
  :inline t
  (b* (((the (unsigned-byte 8) code) (char-code x)))
    (and (<= (big-a) code)
      (<= code (big-z))))
  ///
  (defcong chareqv equal (up-alpha-p x) 1)
  (local (defund exhaustive-test
      (n)
      (and (let ((x (code-char n)))
          (equal (upper-case-p x)
            (and (<= (big-a) (char-code x))
              (<= (char-code x) (big-z)))))
        (or (zp n) (exhaustive-test (- n 1))))))
  (local (defthm lemma1
      (implies (and (natp n) (<= n 255))
        (equal (char-code (code-char n)) n))))
  (local (defthm lemma2
      (implies (and (natp n)
          (natp m)
          (exhaustive-test n)
          (= x (code-char m))
          (<= m n)
          (<= n 255))
        (equal (upper-case-p x)
          (and (<= (big-a) (char-code x))
            (<= (char-code x) (big-z)))))
      :hints (("Goal" :induct (exhaustive-test n)
         :in-theory (enable exhaustive-test)))))
  (local (in-theory (enable standard-char-p)))
  (local (defthm lemma3
      (implies (standard-char-p x)
        (equal (upper-case-p x)
          (and (<= (big-a) (char-code x))
            (<= (char-code x) (big-z)))))
      :hints (("Goal" :in-theory (disable lemma2)
         :use ((:instance lemma2
            (n 255)
            (m (char-code x))))))))
  (local (defthm lemma4
      (implies (not (characterp x))
        (not (upper-case-p x)))
      :hints (("Goal" :in-theory (enable upper-case-p)))))
  (local (defthm lemma5
      (implies (standard-char-p x)
        (equal (upper-case-p x)
          (and (<= (big-a) (char-code x))
            (<= (char-code x) (big-z)))))
      :hints (("Goal" :cases ((characterp x))))))
  (defthm upper-case-p-is-up-alpha-p
    (implies (standard-char-p x)
      (equal (upper-case-p x)
        (up-alpha-p (double-rewrite x)))))
  (in-theory (disable upper-case-p-char-upcase)))

(define down-alpha-p
  ((x :type character))
  :returns bool
  :parents (cases lower-case-p)
  :short "Determine if a character is a lower-case letter (a-z)."
  :long "<p>ACL2 has a built-in alternative to this function, @(see
 acl2::lower-case-p), which however can also recognize characters that are not
 standard characters.  (Historical note: Before May 2024, the guard for
 acl2::lower-case-p required standard-char-p yet also converted only standard
 characters; this provided motivation for the development of
 down-alpha-p.)</p>"
  :inline t
  (b* (((the (unsigned-byte 8) code) (char-code x)))
    (and (<= (little-a) code)
      (<= code (little-z))))
  ///
  (defcong chareqv
    equal
    (down-alpha-p x)
    1)
  (local (defund exhaustive-test
      (n)
      (and (let ((x (code-char n)))
          (equal (lower-case-p x)
            (and (<= (little-a) (char-code x))
              (<= (char-code x) (little-z)))))
        (or (zp n) (exhaustive-test (- n 1))))))
  (local (defthm lemma1
      (implies (and (natp n) (<= n 255))
        (equal (char-code (code-char n)) n))))
  (local (defthm lemma2
      (implies (and (natp n)
          (natp m)
          (exhaustive-test n)
          (= x (code-char m))
          (<= m n)
          (<= n 255))
        (equal (lower-case-p x)
          (and (<= (little-a) (char-code x))
            (<= (char-code x) (little-z)))))
      :hints (("Goal" :induct (exhaustive-test n)
         :in-theory (enable exhaustive-test)))))
  (local (in-theory (enable standard-char-p)))
  (local (defthm lemma3
      (implies (standard-char-p x)
        (equal (lower-case-p x)
          (and (<= (little-a) (char-code x))
            (<= (char-code x) (little-z)))))
      :hints (("Goal" :in-theory (disable lemma2)
         :use ((:instance lemma2
            (n 255)
            (m (char-code x))))))))
  (local (defthm lemma4
      (implies (not (characterp x))
        (not (lower-case-p x)))
      :hints (("Goal" :in-theory (enable lower-case-p)))))
  (local (defthm lemma5
      (implies (standard-char-p x)
        (equal (lower-case-p x)
          (and (<= (little-a) (char-code x))
            (<= (char-code x) (little-z)))))
      :hints (("Goal" :cases ((characterp x))))))
  (defthm lower-case-p-is-down-alpha-p
    (implies (standard-char-p x)
      (equal (lower-case-p x)
        (down-alpha-p (double-rewrite x)))))
  (in-theory (disable lower-case-p-char-downcase))
  (defthm down-alpha-p-when-up-alpha-p
    (implies (up-alpha-p x)
      (not (down-alpha-p x)))
    :hints (("Goal" :in-theory (enable up-alpha-p down-alpha-p)))))

(define upcase-char
  ((x :type character))
  :returns (char characterp :rule-classes :type-prescription)
  :parents (cases char-upcase)
  :short "Convert a character to upper-case."
  :long "<p>@(call upcase-char) converts lower-case standard characters into
 their upper-case equivalents, and returns other characters unchanged.</p>

 <p>ACL2 has a built-in alternative to this function, @(see acl2::char-upcase),
 which however can also convert characters that are not standard characters.
 (Historical note: Before May 2024, the guard for acl2::char-upcase required
 standard-char-p yet also converted only standard characters; this provided
 motivation for the development of upcase-char.)</p>"
  :inline t
  (b* (((the (unsigned-byte 8) code) (char-code x)))
    (if (and (<= (little-a) code)
        (<= code (little-z)))
      (code-char (the (unsigned-byte 8) (- code (case-delta))))
      (mbe :logic (char-fix x) :exec x)))
  ///
  (defcong chareqv
    equal
    (upcase-char x)
    1)
  (defthm upcase-char-does-nothing-unless-down-alpha-p
    (implies (not (down-alpha-p x))
      (equal (upcase-char x) (char-fix x)))
    :hints (("Goal" :in-theory (enable down-alpha-p))))
  (defthm upcase-char-of-upcase-char
    (equal (upcase-char (upcase-char x))
      (upcase-char x)))
  (local (defund exhaustive-test
      (n)
      (and (let ((x (code-char n)))
          (implies (standard-char-p x)
            (equal (char-upcase x)
              (if (and (<= (little-a) (char-code x))
                  (<= (char-code x) (little-z)))
                (code-char (- (char-code x) (case-delta)))
                x))))
        (or (zp n) (exhaustive-test (- n 1))))))
  (local (defthm lemma1
      (implies (and (natp n) (<= n 255))
        (equal (char-code (code-char n)) n))))
  (local (defthm lemma2
      (implies (and (natp n)
          (natp m)
          (exhaustive-test n)
          (= x (code-char m))
          (<= m n)
          (<= n 255)
          (standard-char-p x))
        (equal (char-upcase x)
          (if (and (<= (little-a) (char-code x))
              (<= (char-code x) (little-z)))
            (code-char (- (char-code x) (case-delta)))
            x)))
      :hints (("Goal" :induct (exhaustive-test n)
         :in-theory (enable exhaustive-test)))))
  (local (defthm lemma3
      (implies (standard-char-p x)
        (equal (char-upcase x)
          (if (and (<= (little-a) (char-code x))
              (<= (char-code x) (little-z)))
            (code-char (- (char-code x) (case-delta)))
            x)))
      :hints (("Goal" :in-theory (disable lemma2)
         :use ((:instance lemma2
            (n 255)
            (m (char-code x))))))))
  (local (defthm lemma4
      (implies (standard-char-p x)
        (equal (char-upcase x)
          (if (and (<= (little-a) (char-code x))
              (<= (char-code x) (little-z)))
            (code-char (- (char-code x) (case-delta)))
            x)))))
  (defthm char-upcase-is-upcase-char
    (implies (standard-char-p x)
      (equal (char-upcase x)
        (upcase-char (double-rewrite x)))))
  (defthm not-down-alpha-p-of-upcase-char
    (not (down-alpha-p (upcase-char x)))
    :hints (("goal" :in-theory (enable down-alpha-p)))))

(define downcase-char
  ((x :type character))
  :returns (char characterp :rule-classes :type-prescription)
  :parents (cases char-downcase)
  :short "Convert a character to lower-case."
  :long "<p>@(call downcase-char) converts upper-case characters into their
 lower-case equivalents, and returns other characters unchanged.</p>

 <p>ACL2 has a built-in alternative to this function, @(see
 acl2::char-downcase), which however can also convert characters that are not
 standard characters.  (Historical note: Before May 2024, the guard for
 acl2::char-downcase required standard-char-p yet also converted only standard
 characters; this provided motivation for the development of
 downcase-char.)</p>"
  :inline t
  (b* (((the (unsigned-byte 8) code) (char-code x)))
    (if (and (<= (big-a) code)
        (<= code (big-z)))
      (code-char (the (unsigned-byte 8) (+ code (case-delta))))
      (mbe :logic (char-fix x) :exec x)))
  ///
  (defcong chareqv
    equal
    (downcase-char x)
    1)
  (defthm downcase-char-does-nothing-unless-up-alpha-p
    (implies (not (up-alpha-p x))
      (equal (downcase-char x) (char-fix x)))
    :hints (("Goal" :in-theory (enable up-alpha-p))))
  (defthm downcase-char-of-downcase-char
    (equal (downcase-char (downcase-char x))
      (downcase-char x)))
  (defthm downcase-char-of-upcase-char
    (equal (downcase-char (upcase-char x))
      (downcase-char x))
    :hints (("Goal" :in-theory (enable upcase-char char-fix))))
  (defthm upcase-char-of-downcase-char
    (equal (upcase-char (downcase-char x))
      (upcase-char x))
    :hints (("Goal" :in-theory (enable upcase-char char-fix))))
  (local (defund exhaustive-test
      (n)
      (and (let ((x (code-char n)))
          (implies (standard-char-p x)
            (equal (char-downcase x)
              (if (and (<= (big-a) (char-code x))
                  (<= (char-code x) (big-z)))
                (code-char (+ (char-code x) (case-delta)))
                x))))
        (or (zp n) (exhaustive-test (- n 1))))))
  (local (defthm lemma1
      (implies (and (natp n) (<= n 255))
        (equal (char-code (code-char n)) n))))
  (local (defthm lemma2
      (implies (and (natp n)
          (natp m)
          (exhaustive-test n)
          (= x (code-char m))
          (<= m n)
          (<= n 255)
          (standard-char-p x))
        (equal (char-downcase x)
          (if (and (<= (big-a) (char-code x))
              (<= (char-code x) (big-z)))
            (code-char (+ (char-code x) (case-delta)))
            x)))
      :hints (("Goal" :induct (exhaustive-test n)
         :in-theory (enable exhaustive-test)))))
  (local (defthm lemma3
      (implies (standard-char-p x)
        (equal (char-downcase x)
          (if (and (<= (big-a) (char-code x))
              (<= (char-code x) (big-z)))
            (code-char (+ (char-code x) (case-delta)))
            x)))
      :hints (("Goal" :in-theory (disable lemma2)
         :use ((:instance lemma2
            (n 255)
            (m (char-code x))))))))
  (local (defthm lemma4
      (implies (standard-char-p x)
        (equal (char-downcase x)
          (if (characterp x)
            (if (and (<= (big-a) (char-code x))
                (<= (char-code x) (big-z)))
              (code-char (+ (char-code x) (case-delta)))
              x)
            (code-char 0))))))
  (defthm char-downcase-is-downcase-char
    (implies (standard-char-p x)
      (equal (char-downcase x)
        (downcase-char (double-rewrite x))))))

(define upcase-char-str
  ((c characterp))
  :returns (str stringp :rule-classes :type-prescription)
  :parents (cases)
  :short "Convert a character into an upper-case one-element string."
  :long "<p>@(call upcase-char-str) is logically equal to:</p>

@({
 (implode (list (upcase-char c)))
})

<p>But we store these strings in a table so that they don't have to be
recomputed.  This is mainly useful to reduce the creation of temporary strings
during @(see upcase-first).</p>"
  :enabled t
  :inline t
  (mbe :logic (implode (list (upcase-char c)))
    :exec (aref1 '*upcase-first-strtbl*
      *upcase-first-strtbl*
      (char-code c)))
  :prepwork ((defun make-upcase-first-strtbl
     (n)
     (declare (xargs :guard (and (natp n) (<= n 255))
         :ruler-extenders :all))
     (cons (cons n
         (implode (list (upcase-char (code-char n)))))
       (if (zp n)
         nil
         (make-upcase-first-strtbl (- n 1))))) (defconst *upcase-first-strtbl*
      (compress1 '*upcase-first-strtbl*
        (cons '(:header :dimensions (256) :maximum-length 257)
          (make-upcase-first-strtbl 255))))
    (local (in-theory (disable aref1)))
    (local (defun test
        (n)
        (declare (xargs :ruler-extenders :all))
        (and (equal (aref1 '*upcase-first-strtbl*
              *upcase-first-strtbl*
              n)
            (implode (list (upcase-char (code-char n)))))
          (if (zp n)
            t
            (test (- n 1))))))
    (local (defthm l0
        (implies (and (natp i)
            (natp n)
            (<= i n)
            (<= n 255)
            (test n))
          (equal (aref1 '*upcase-first-strtbl*
              *upcase-first-strtbl*
              i)
            (implode (list (upcase-char (code-char i))))))
        :hints (("Goal" :induct (test n)))))
    (local (defthm l1
        (implies (and (natp i) (<= i 255))
          (equal (aref1 '*upcase-first-strtbl*
              *upcase-first-strtbl*
              i)
            (implode (list (upcase-char (code-char i))))))
        :hints (("Goal" :use ((:instance l0 (n 255)))))))))

(define downcase-char-str
  ((c :type character))
  :returns (str stringp :rule-classes :type-prescription)
  :parents (cases)
  :short "Convert a character into a lower-case one-element string."
  :long "<p>@(call downcase-char-str) is logically equal to:</p>

@({
 (implode (downcase-char c))
})

<p>But we store these strings in a table so that they don't have to be
recomputed.  This is mainly useful to reduce the creation of temporary strings
during @(see downcase-first).</p>"
  :enabled t
  :inline t
  (mbe :logic (implode (list (downcase-char c)))
    :exec (aref1 '*downcase-first-strtbl*
      *downcase-first-strtbl*
      (char-code c)))
  :prepwork ((defun make-downcase-first-strtbl
     (n)
     (declare (xargs :guard (and (natp n) (<= n 255))
         :ruler-extenders :all))
     (cons (cons n
         (implode (list (downcase-char (code-char n)))))
       (if (zp n)
         nil
         (make-downcase-first-strtbl (- n 1))))) (defconst *downcase-first-strtbl*
      (compress1 '*downcase-first-strtbl*
        (cons '(:header :dimensions (256) :maximum-length 257)
          (make-downcase-first-strtbl 255))))
    (local (in-theory (disable aref1)))
    (local (defun test
        (n)
        (declare (xargs :ruler-extenders :all))
        (and (equal (aref1 '*downcase-first-strtbl*
              *downcase-first-strtbl*
              n)
            (implode (list (downcase-char (code-char n)))))
          (if (zp n)
            t
            (test (- n 1))))))
    (local (defthm l0
        (implies (and (natp i)
            (natp n)
            (<= i n)
            (<= n 255)
            (test n))
          (equal (aref1 '*downcase-first-strtbl*
              *downcase-first-strtbl*
              i)
            (implode (list (downcase-char (code-char i))))))
        :hints (("Goal" :induct (test n)))))
    (local (defthm l1
        (implies (and (natp i) (<= i 255))
          (equal (aref1 '*downcase-first-strtbl*
              *downcase-first-strtbl*
              i)
            (implode (list (downcase-char (code-char i))))))
        :hints (("Goal" :use ((:instance l0 (n 255)))))))))