• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
        • Charlistnat<
        • Ichar<
        • Istr<
        • Icharlist<
        • Strnat<
          • Strnat<-aux
        • Istrsort
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Strnat<

Strnat<-aux

Implementation of strnat<.

(strnat<-aux x y xn yn xl yl) is basically the adaptation of charlistnat< for strings. Here, X and Y are the strings being compared, and XL and YL are their pre-computed lengths. XN and YN are the indices into the two strings that are our current positions.

BOZO why do we have XN and YN separately? It seems like we should only need one index.

Definitions and Theorems

Function: strnat<-aux

(defun strnat<-aux (x y xn yn xl yl)
 (declare (type string x)
          (type string y)
          (type integer xn)
          (type integer yn)
          (type integer xl)
          (type integer yl)
          (xargs :guard (and (stringp x)
                             (stringp y)
                             (natp xn)
                             (natp yn)
                             (equal xl (length x))
                             (equal yl (length y))
                             (<= xn xl)
                             (<= yn yl)))
          (ignorable xl yl))
 (mbe
  :logic
  (let* ((x (if (stringp x) x ""))
         (y (if (stringp y) y ""))
         (xn (nfix xn))
         (yn (nfix yn))
         (xl (length x))
         (yl (length y)))
    (cond ((zp (- yl yn)) nil)
          ((zp (- xl xn)) t)
          ((and (dec-digit-char-p (char x xn))
                (dec-digit-char-p (char y yn)))
           (b* (((mv v1 l1)
                 (parse-nat-from-string x 0 0 xn xl))
                ((mv v2 l2)
                 (parse-nat-from-string y 0 0 yn yl)))
             (cond ((or (< v1 v2)
                        (and (int= v1 v2) (< l1 l2)))
                    t)
                   ((or (< v2 v1)
                        (and (int= v1 v2) (< l2 l1)))
                    nil)
                   (t (strnat<-aux x y (+ xn l1)
                                   (+ yn l2)
                                   xl yl)))))
          ((char< (char x xn) (char y yn)) t)
          ((char< (char y yn) (char x xn)) nil)
          (t (strnat<-aux x y (+ 1 xn)
                          (+ 1 yn)
                          xl yl))))
  :exec
  (cond
   ((int= yn yl) nil)
   ((int= xn xl) t)
   (t
    (let* ((char-x (the character
                        (char (the string x) (the integer xn))))
           (char-y (the character
                        (char (the string y) (the integer yn))))
           (code-x (the (unsigned-byte 8)
                        (char-code (the character char-x))))
           (code-y (the (unsigned-byte 8)
                        (char-code (the character char-y)))))
     (declare (type character char-x)
              (type character char-y)
              (type (unsigned-byte 8) code-x)
              (type (unsigned-byte 8) code-y))
     (cond
      ((and (<= (the (unsigned-byte 8) 48)
                (the (unsigned-byte 8) code-x))
            (<= (the (unsigned-byte 8) code-x)
                (the (unsigned-byte 8) 57))
            (<= (the (unsigned-byte 8) 48)
                (the (unsigned-byte 8) code-y))
            (<= (the (unsigned-byte 8) code-y)
                (the (unsigned-byte 8) 57)))
       (b* (((mv v1 l1)
             (parse-nat-from-string (the string x)
                                    (the integer 0)
                                    (the integer 0)
                                    (the integer xn)
                                    (the integer xl)))
            ((mv v2 l2)
             (parse-nat-from-string (the string y)
                                    (the integer 0)
                                    (the integer 0)
                                    (the integer yn)
                                    (the integer yl))))
        (cond
         ((or (< (the integer v1) (the integer v2))
              (and (int= v1 v2)
                   (< (the integer l1) (the integer l2))))
          t)
         ((or (< (the integer v2) (the integer v1))
              (and (int= v1 v2)
                   (< (the integer l2) (the integer l1))))
          nil)
         (t (strnat<-aux (the string x)
                         (the string y)
                         (the integer
                              (+ (the integer xn) (the integer l1)))
                         (the integer
                              (+ (the integer yn) (the integer l2)))
                         (the integer xl)
                         (the integer yl))))))
      ((< (the (unsigned-byte 8) code-x)
          (the (unsigned-byte 8) code-y))
       t)
      ((< (the (unsigned-byte 8) code-y)
          (the (unsigned-byte 8) code-x))
       nil)
      (t (strnat<-aux (the string x)
                      (the string y)
                      (the integer
                           (+ (the integer 1) (the integer xn)))
                      (the integer
                           (+ (the integer 1) (the integer yn)))
                      (the integer xl)
                      (the integer yl)))))))))

Theorem: strnat<-aux-correct

(defthm strnat<-aux-correct
  (implies (and (stringp x)
                (stringp y)
                (natp xn)
                (natp yn)
                (equal xl (length x))
                (equal yl (length y))
                (<= xn xl)
                (<= yn yl))
           (equal (strnat<-aux x y xn yn xl yl)
                  (charlistnat< (nthcdr xn (explode x))
                                (nthcdr yn (explode y))))))