charset-fns

(in-package "STR")

(include-book "charset")

(local (include-book "arithmetic"))

(local (set-default-parents charset-p))

(define count-leading-charset
  ((x character-listp) (set charset-p))
  :returns (num natp :rule-classes :type-prescription)
  :short "Count how many characters at the start of a list are members of a
particular character set."
  (cond ((atom x) 0)
    ((char-in-charset-p (car x) set) (+ 1 (count-leading-charset (cdr x) set)))
    (t 0))
  ///
  (defthm upper-bound-of-count-leading-charset
    (<= (count-leading-charset x set)
      (len x))
    :rule-classes ((:rewrite) (:linear)))
  (defthm count-leading-charset-len
    (equal (equal (len x)
        (count-leading-charset x set))
      (chars-in-charset-p x set))
    :rule-classes ((:rewrite) (:rewrite :corollary (equal (< (count-leading-charset x set)
            (len x))
          (not (chars-in-charset-p x set))))
      (:linear :corollary (implies (not (chars-in-charset-p x set))
          (< (count-leading-charset x set)
            (len x))))))
  (defthm count-leading-charset-zero
    (equal (equal 0 (count-leading-charset x set))
      (not (char-in-charset-p (car x) set)))
    :rule-classes ((:rewrite) (:rewrite :corollary (equal (< 0 (count-leading-charset x set))
          (char-in-charset-p (car x) set)))
      (:linear :corollary (implies (char-in-charset-p (car x) set)
          (< 0 (count-leading-charset x set))))))
  (defthm count-leading-charset-sound
    (let ((n (count-leading-charset x set)))
      (chars-in-charset-p (take n x) set)))
  (defthm count-leading-charset-complete
    (b* ((n (count-leading-charset x set)) (next-char (nth n x)))
      (not (char-in-charset-p next-char set)))
    :hints (("Goal" :induct (count-leading-charset x set)
       :in-theory (enable nth)))))

(define str-count-leading-charset
  ((n natp "Current position in the string.") (x stringp "String we're iterating through.")
    (xl (eql xl (length x))
      "Precomputed length of @('x').")
    (set charset-p "Set of characters we're counting."))
  :guard (<= n xl)
  :returns (n natp :rule-classes :type-prescription)
  :short "String version of @(see count-leading-charset)."
  :enabled t
  (declare (type (integer 0 *) xl n)
    (type string x))
  (mbe :logic (let ((chars (nthcdr n (coerce x 'list))))
      (count-leading-charset chars set))
    :exec (b* (((when (eql n xl)) 0) ((the character char1) (char x n))
        ((when (char-in-charset-p char1 set)) (+ 1
            (str-count-leading-charset (+ 1 n)
              x
              xl
              set))))
      0))
  :verify-guards nil
  ///
  (verify-guards str-count-leading-charset
    :hints (("Goal" :in-theory (enable count-leading-charset)))))

(define str-count-leading-charset-fast
  ((n natp "Current position in the string.") (x stringp "String we're iterating through.")
    (xl (eql xl (length x))
      "Precomputed length of @('x').")
    (set charset-p "Set of characters we're counting."))
  :guard (<= n xl)
  :returns (n natp :rule-classes :type-prescription)
  :short "Fixnum optimized version of @(see str-count-leading-charset)."
  :enabled t
  (declare (type (unsigned-byte 60) n xl)
    (type string x))
  (mbe :logic (let ((chars (nthcdr n (coerce x 'list))))
      (count-leading-charset chars set))
    :exec (b* (((when (eql n xl)) 0) ((the character char1) (char x n))
        ((the (unsigned-byte 60) n) (+ 1 n))
        ((when (char-in-charset-p char1 set)) (the (integer 0 *)
            (+ 1
              (str-count-leading-charset-fast n
                x
                xl
                set)))))
      0))
  :verify-guards nil
  ///
  (verify-guards str-count-leading-charset-fast
    :hints (("Goal" :in-theory (enable count-leading-charset)))))