/usr/share/acl2-6.3/books/str/fast-cat.lisp is in acl2-books-source 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 | ; 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 "cat")
; In CCL, the performance of str::cat is boosted by a factor of 6.6-9.5x by
; including this file, according to the stupid benchmarks at the end of this
; file.
;
; Perhaps Gary will write a compiler-macro to speed up concatenate in CCL, at
; which point this file will no longer be needed.
;
; I haven't tested performance in other Lisps. If misc/fast-coerce is any
; indication, it may be that some other Lisps will also benefit.
(defttag fast-cat)
(acl2::progn!
(set-raw-mode t)
(defun fast-string-append (x y)
(declare (type string x)
(type string y))
(let* ((xl (length x))
(yl (length y))
(rl (the fixnum (+ (the fixnum xl) (the fixnum yl))))
(ret (make-array rl :element-type 'character))
(i 0)
(j 0))
(declare (type fixnum xl)
(type fixnum yl)
(type fixnum rl)
(type fixnum i)
(type fixnum j)
(type string ret))
(loop until (= i xl)
do
(setf (schar ret i) (schar x i))
(incf i))
(loop until (= i rl)
do
(setf (schar ret i) (schar y j))
(incf i)
(incf j))
ret))
(defun fast-string-append-lst (x)
(when (atom x)
(return-from fast-string-append-lst ""))
(when (atom (cdr x))
(return-from fast-string-append-lst (car x)))
(let ((result-length 0))
(declare (type fixnum result-length))
(loop for str in x do
(incf result-length (length (the string str))))
(let ((ret (make-array result-length :element-type 'character))
(i 0)
(j 0))
(declare (type string ret)
(type fixnum i)
(type fixnum j))
(loop for str in x do
(let ((strlen (length str)))
(declare (type fixnum strlen))
(setq j 0)
(loop until (= j strlen)
do
(setf (schar ret i) (schar str j))
(incf i)
(incf j))))
ret)))
(defun rchars-to-string (rchars)
(the string
(nreverse
(the string (coerce (the list rchars) 'string))))))
#|
(include-book
"fast-cat" :ttags :all)
:q
(ccl::egc nil)
; STR::CAT is about 9.5x faster for this test:
(progn
(ccl::gc)
;; 1.413 seconds, 1.12 GB allocated
(time (loop for i fixnum from 1 to 10000000
do
(str::cat "sillyNameOneMightSee" "[33]"))))
(progn
(ccl::gc)
;; 13.375 seconds, 1.12 GB allocated
(time (loop for i fixnum from 1 to 10000000
do
(concatenate 'string "sillyNameOneMightSee" "[33]"))))
; STR::CAT is about 6.6x faster in this loop.
; BOZO weird -- why does CCL's concatenate function take so much less memory
; than ours?
(progn
(ccl::gc)
;; 2.112 seconds, 1.760 gb
(time (loop for i fixnum from 1 to 10000000
do
(str::cat "sillyNameOneMightSee" "[33]" "more"))))
(progn
(ccl::gc)
;; 14.101 seconds, 1.28 gb
(time (loop for i fixnum from 1 to 10000000
do
(concatenate 'string "sillyNameOneMightSee" "[33]" "more"))))
; Hrmn, this takes 480 MB:
(defun f (x) (list x x x))
(time
(loop for i fixnum from 1 to 10000000
do
(f i)))
; And indeed (- 1760 1280) is 480. So it looks like CCL's concatenate is
; somehow able to avoid consing its arguments into a list like our
; fast-concatenate macro is doing.
; Well, go figure. I'm not sure how to avoid this.
(defparameter *test* (coerce "blah blah blah this is some text" 'list))
(progn
(ccl::gc)
;; 6.782 seconds, 1.6 GB allocated
(let ((test *test*))
(time (loop for i fixnum from 1 to 10000000
collect
(str::rchars-to-string test))))
nil)
(progn
(ccl::gc)
;; 11.629 seconds, 3.04 GB allocated
(let ((test *test*))
(time (loop for i fixnum from 1 to 10000000
collect
(reverse (coerce test 'string)))))
nil)
(progn
(ccl::gc)
;; 10.314 seconds, 6.72 GB allocated
(let ((test *test*))
(time (loop for i fixnum from 1 to 10000000
collect
(coerce (reverse test) 'string))))
nil)
|#
|