acl2-books-source 6.3-5 / usr / share / acl2-6.3 / books / str / cat.lisp

; ACL2 String Library
; Copyright (C) 2009-2013 Centaur Technology
;
; Contact:
;   Centaur Technology Formal Verification Group
;   7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
;   http://www.centtech.com/
;
; This program is free software; you can redistribute it and/or modify it under
; the terms of the GNU General Public License as published by the Free Software
; Foundation; either version 2 of the License, or (at your option) any later
; version.  This program is distributed in the hope that it will be useful but
; WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
; FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for
; more details.  You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free Software
; Foundation, Inc., 51 Franklin Street, Suite 500, Boston, MA 02110-1335, USA.
;
; Original author: Jared Davis <jared@centtech.com>

(in-package "STR")
(include-book "ieqv")
(include-book "tools/bstar" :dir :system)
(include-book "std/lists/list-defuns" :dir :system)
(local (include-book "arithmetic"))
(local (include-book "std/lists/equiv" :dir :system))

(defsection cat
  :parents (concatenation)
  :short "Concatenate strings."

  :long "<p>@('(str::cat x y z ...)') is like @('(concatenate 'string x y z
...)'), but is less to type.</p>

<p>  If that's your goal, you might instead consider using the approach
outlined in @(see revappend-chars).</p>

<p>In some Lisps, using @('(concatenate 'string ...)') to join strings can be
even worse than just the cost of creating and initializing a new array.  The
@(see concatenate) function is quite flexible and can handle many types of
input, and this flexibility can cause some overhead if the Lisp does not
optimize for the @(''string') case.</p>

<p>So, if you are willing to accept a trust tag, then you may <b>optionally</b>
load the book:</p>

@({
  (include-book \"str/fast-cat\" :dir :system)
})

<p>which may improve the performance of @('str::cat').  How does this work?
Basically @('str::cat') calls one of @('fast-string-append') or
@('fast-string-append-lst'), depending on how many arguments it is given.  By
default, these functions are aliases for ACL2's @(see string-append) and
@('string-append-lst') functions.  But if you load the @('fast-cat') book,
these functions will be redefined to use raw Lisp array operations, and the
result may be faster.</p>"

  (defun fast-string-append (str1 str2)
    "May be redefined under-the-hood in str/fast-cat.lisp"
    ;; We don't inline this because you might want to develop books without
    ;; fast-cat (for fewer ttags), but then include fast-cat later for more
    ;; performance.
    (declare (type string str1 str2))
    (string-append str1 str2))

  (defun fast-string-append-lst (x)
    "May be redefined under-the-hood in str/fast-cat.lisp"
    ;; We don't inline this because you might want to develop books without
    ;; fast-cat (for fewer ttags), but then include fast-cat later for more
    ;; performance.
    (declare (xargs :guard (string-listp x)))
    (string-append-lst x))

  (defmacro fast-concatenate (result-type &rest sequences)
    (declare (xargs :guard (member-equal result-type '('string 'list))))
    (cond ((equal result-type ''string)
           (cond ((and sequences
                       (cdr sequences)
                       (null (cddr sequences)))
                  (list 'fast-string-append
                        (car sequences)
                        (cadr sequences)))
                 (t
                  (list 'fast-string-append-lst
                        (cons 'list sequences)))))
          (t
           `(append (list . ,sequences)))))

  (defmacro cat (&rest args)
    `(fast-concatenate 'string . ,args)))


(defsection append-chars
  :parents (concatenation)
  :short "Append a string's characters onto a list."

  :long "<p>@(call append-chars) takes the characters from the string @('x')
and appends them onto @('y').</p>

<p>Its logical definition is nothing more than @('(append (explode x) y)').</p>

<p>In the execution, we traverse the string @('x') using @(see char) to avoid
the overhead of @(see coerce)-ing it into a character list before performing
the @(see append).  This reduces the overhead from @('2n') conses to @('n')
conses, where @('n') is the length of @('x').</p>"

  (defund append-chars-aux (x n y)
    "Appends the characters from x[0:n] onto y"
    (declare (type string x)
             (type (integer 0 *) n)
             (xargs :guard (< n (length x))))
    (if (zp n)
        (cons (char x 0) y)
      (append-chars-aux x
                        (the (integer 0 *) (- n 1))
                        (cons (char x n) y))))

  (local (defthm lemma
           (implies (and (not (zp n))
                         (<= n (len x)))
                    (equal (append (take (- n 1) x) (cons (nth (- n 1) x) y))
                           (append (take n x) y)))
           :hints(("goal"
                   :in-theory (enable acl2::take-redefinition)
                   :induct (take n x)))))

  (defthm append-chars-aux-correct
    (implies (and (stringp x)
                  (natp n)
                  (< n (length x)))
             (equal (append-chars-aux x n y)
                    (append (take (+ 1 n) (explode x)) y)))
    :hints(("Goal"
            :in-theory (enable append-chars-aux)
            :induct (append-chars-aux x n y))))

  (local (in-theory (disable append-chars-aux-correct)))

  (local (defthm append-chars-aux-correct-better
           (implies (and (stringp x)
                         (natp n)
                         (< n (length x)))
                    (equal (append-chars-aux x n y)
                           (append (take (+ 1 n) (explode x)) y)))
           :hints(("Goal" :use ((:instance append-chars-aux-correct))))))

  (definlined append-chars (x y)
    (declare (type string x))
    (mbe :logic (append (explode x) y)
         :exec (b* (((the (integer 0 *) xl) (length x))
                    ((when (eql xl 0))
                     y)
                    ((the (integer 0 *) n) (- xl 1)))
                 (append-chars-aux x n y))))

  (local (in-theory (enable append-chars)))

  (defthm character-listp-of-append-chars
    (equal (character-listp (append-chars x y))
           (character-listp y)))

  (defcong streqv equal (append-chars x y) 1)
  (defcong istreqv icharlisteqv (append-chars x y) 1)
  (defcong list-equiv list-equiv (append-chars x y) 2)
  (defcong charlisteqv charlisteqv (append-chars x y) 2)
  (defcong icharlisteqv icharlisteqv (append-chars x y) 2))




(defsection revappend-chars
  :parents (concatenation)
  :short "Append a string's characters onto a list, in reverse order."

  :long "<p>@(call revappend-chars) takes the characters from the string
@('x'), reverses them, and appends the result onto @('y').</p>

<p>Its logical definition is nothing more than @('(revappend (explode x) y)').</p>

<p>In the execution, we traverse the string @('x') using @(see char) to avoid
the overhead of @(see coerce)-ing it into a character list before performing
the @(see revappend).  This reduces the overhead from @('2n') conses to @('n')
conses, where @('n') is the length of @('x').</p>

<p>This function may seem strange at first glance, but it provides a convenient
way to efficiently, incrementally build a string out of small parts.  For
instance, a sequence such as:</p>

@({
 (let* ((acc nil)
        (acc (str::revappend-chars \"Hello, \" acc))
        (acc (str::revappend-chars \"World!\" acc))
        (acc ...))
    (reverse (implode acc)))
})

<p>Is essentially the same as:</p>

@({
 (let* ((acc \"\")
        (acc (str::cat acc \"Hello, \"))
        (acc (str::cat acc \"World!\"))
        (acc ...))
   acc)
})

<p>But it is comparably much more efficient because it avoids the creation of
the intermediate strings.  See the performance discussion in @(see str::cat)
for more details.  Also see @(see rchars-to-string), which is a potentially
more efficient way to do the final @(see reverse)/@(see coerce) steps.</p>"

  (defund revappend-chars-aux (x n xl y)
    (declare (type string x)
             (type (integer 0 *) n xl)
             (xargs :guard (and (<= n xl)
                                (equal xl (length x)))
                    :measure (nfix (- (nfix xl) (nfix n)))))
    (if (mbe :logic (zp (- (nfix xl) (nfix n)))
             :exec (eql n xl))
        y
      (revappend-chars-aux x
                           (the (integer 0 *)
                             (+ 1 (the (integer 0 *) (lnfix n))))
                           xl
                           (cons (char x n) y))))

  (defthm revappend-chars-aux-correct
    (implies (and (stringp x)
                  (natp n)
                  (natp xl)
                  (<= n xl)
                  (equal xl (length x)))
             (equal (revappend-chars-aux x n xl y)
                    (revappend (nthcdr n (explode x)) y)))
    :hints(("Goal"
            :in-theory (e/d (revappend-chars-aux)
                            (acl2::revappend-removal))
            :induct (revappend-chars-aux x n xl y))))

  (definlined revappend-chars (x y)
    (declare (xargs :guard (stringp x))
             (type string x))
    (mbe :logic (revappend (explode x) y)
         :exec (revappend-chars-aux x 0 (length x) y)))

  (local (in-theory (enable revappend-chars)))

  (defthm character-listp-of-revappend-chars
    (equal (character-listp (revappend-chars x y))
           (character-listp y)))

  (defcong streqv equal (revappend-chars x y) 1)
  (defcong istreqv icharlisteqv (revappend-chars x y) 1)
  (defcong list-equiv list-equiv (revappend-chars x y) 2)
  (defcong charlisteqv charlisteqv (revappend-chars x y) 2)
  (defcong icharlisteqv icharlisteqv (revappend-chars x y) 2))



#||

(include-book ;; newline to fool dependency scanner
 "cat")

;; Simple experiments on fv-1:

(defparameter *str* "Hello, world!")

;; 3.84 seconds, 2.08 GB allocated
(progn
  (gc$)
  (time (loop for i fixnum from 1 to 5000000
              do
              (revappend (coerce *str* 'list) nil))))

;; 2.88 seconds, 1.04 GB allocated
(progn
  (gc$)
  (time (loop for i fixnum from 1 to 5000000
              do
              (STR::revappend-chars *str* nil))))


;; 4.38 seconds, 2.08 GB allocated
(progn
  (gc$)
  (time (loop for i fixnum from 1 to 5000000
              do
              (append (coerce *str* 'list) nil))))

;; 3.00 seconds, 1.04 GB allocated
(progn
  (gc$)
  (time (loop for i fixnum from 1 to 5000000
              do
              (STR::append-chars *str* nil))))

||#


(defsection prefix-strings
  :parents (concatenation)
  :short "Concatenates a prefix onto every string in a list of strings."

  :long "<p>@(call prefix-strings) produces a new string list by concatenating
@('prefix') onto every member of @('x').</p>"

  (defund prefix-strings (prefix x)
    (declare (type string prefix)
             (xargs :guard (string-listp x)))
    (if (atom x)
        nil
      (cons (cat prefix (car x))
            (prefix-strings prefix (cdr x)))))

  (local (in-theory (enable prefix-strings)))

  (defthm prefix-strings-when-atom
    (implies (atom x)
             (equal (prefix-strings prefix x)
                    nil)))

  (defthm prefix-strings-of-cons
    (equal (prefix-strings prefix (cons a x))
           (cons (cat prefix a)
                 (prefix-strings prefix x))))

  (defthm string-listp-of-prefix-strings
    (string-listp (prefix-strings prefix x)))

  (defthm len-of-prefix-strings
    (equal (len (prefix-strings prefix x))
           (len x)))

  (defcong streqv equal (prefix-strings prefix x) 1)

  (local (defthmd l0
           (equal (prefix-strings prefix (list-fix x))
                  (prefix-strings prefix x))))

  (defcong list-equiv equal (prefix-strings prefix x) 2
    :hints(("Goal" :in-theory (enable list-equiv)
            :use ((:instance l0 (x x))
                  (:instance l0 (x acl2::x-equiv)))))))


(defsection rchars-to-string
  :parents (concatenation)
  :short "Possibly optimized way to reverse a character list and coerce it to a
string."

  :long "<p>@(call rchars-to-string) is logically equal to</p>

@({
   (reverse (coerce rchars 'string))
})

<p>We leave it enabled and would not expect to ever reason about it.  This
operation is useful as the final step in a string-building strategy where
characters are accumulated onto a list in reverse order; see for instance @(see
revappend-chars).</p>

<p>When you just load books like @('str/top') or @('str/cat'), this logical
definition is exactly what gets executed.  This definition is not too bad, and
doing the @(see coerce) first means that the @(see reverse) is done on a
string (i.e., an array) instead of a list, which is generally efficient.</p>

<p>But if you are willing to accept a trust tag, then you may <b>optionally</b>
load the book:</p>

@({
  (include-book \"str/fast-cat\" :dir :system)
})

<p>This may improve the performance of @('rchars-to-string') by replacing the
@(see reverse) call with a call of @('nreverse').  We can \"obviously\" see
that this is safe since the string produced by the @('coerce') is not visible
to any other part of the program.</p>"

  (defun rchars-to-string (rchars)
    "May be redefined under-the-hood in str/fast-cat.lisp"
    ;; We don't inline this because you might want to develop books without
    ;; fast-cat (for fewer ttags), but then include fast-cat later for more
    ;; performance.
    (declare (xargs :guard (character-listp rchars)))
    (the string
      (reverse
       (the string (coerce (the list rchars) 'string))))))


(defsection join
  :parents (concatenation)
  :short "Concatenate a list of strings with some separator between."

  :long "<p>@(call join) joins together the list of strings @('x'), inserting
the string @('separator') between the members.  For example:</p>

@({
 (join '(\"a\" \"b\" \"c\") \".\") = \"a.b.c\"
 (join '(\"a\" \"b\" \"c\") \"->\") = \"a->b->c\"
})

<p>We always return a string; an empty @('x') results in the empty string, and
any empty strings within @('x') just implicitly don't contribute to the
result.</p>

<p>Any sort of string concatenation is slow, but @('join') is reasonably
efficient: it creates a single character list for the result (in reverse order)
without any use of @(see coerce), then uses @(see rchars-to-string) to build
and reverse the result string.</p>"

  (defund join-aux (x separator acc)
    (declare (xargs :guard (string-listp x))
             (type string separator))
    (cond ((atom x)
           acc)
          ((atom (cdr x))
           (revappend-chars (car x) acc))
          (t
           (let* ((acc (revappend-chars (car x) acc))
                  (acc (revappend-chars separator acc)))
             (join-aux (cdr x) separator acc)))))

  (defund join (x separator)
    (declare (type string separator))
    (declare (xargs :guard (string-listp x)
                    :verify-guards nil))
    (mbe :logic
         (cond ((atom x)
                "")
               ((atom (cdr x))
                (if (stringp (car x))
                    (car x)
                  ""))
               (t
                (cat (car x) separator (join (cdr x) separator))))
         :exec
         (rchars-to-string (join-aux x separator nil))))

  (local (in-theory (enable join join-aux)))

  (defthm join-aux-removal
    (implies (and (string-listp x)
                  (stringp separator))
             (equal (join-aux x separator acc)
                    (revappend (coerce (join x separator) 'list)
                               acc)))
    :hints(("Goal"
            :induct (join-aux x separator acc)
            :in-theory (enable revappend-chars))))

  (verify-guards join)

  (defthm stringp-of-join
    (stringp (join x separator))
    :rule-classes :type-prescription)

  (local (defthmd l0
           (equal (join (list-fix x) separator)
                  (join x separator))))

  (defcong list-equiv equal (join x separator) 1
    :hints(("Goal" :in-theory (enable list-equiv)
            :use ((:instance l0 (x x))
                  (:instance l0 (x acl2::x-equiv))))))

  (defcong streqv equal (join x separator) 2)
  (defcong istreqv istreqv (join x separator) 2))