/usr/share/acl2-6.3/books/str/strprefixp.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 | ; 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 "eqv")
(include-book "std/lists/prefixp" :dir :system)
(local (include-book "std/lists/nthcdr" :dir :system))
(local (include-book "arithmetic"))
(local (defthm prefixp-lemma-1
(implies (and (natp xn)
(natp yn)
(< xn (len x))
(< yn (len y))
(not (equal (nth xn x) (nth yn y))))
(not (prefixp (nthcdr xn x) (nthcdr yn y))))
:hints(("Goal" :in-theory (enable nthcdr nth prefixp)))))
(local (defthm prefixp-lemma-2
(implies (and (natp xn)
(natp yn)
(< xn (len x))
(< yn (len y))
(equal (nth xn x) (nth yn y)))
(equal (prefixp (nthcdr xn x) (nthcdr yn y))
(prefixp (cdr (nthcdr xn x)) (cdr (nthcdr yn y)))))
:hints(("Goal" :in-theory (enable prefixp nth nthcdr)))))
(defsection strprefixp-impl
:parents (strprefixp)
:short "Fast implementation of @(see strprefixp)."
(defund strprefixp-impl (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)
(natp xl)
(natp yl)
(= xl (length x))
(= yl (length y))
(<= xn (length x))
(<= yn (length y)))
:measure (min (nfix (- (nfix xl) (nfix xn)))
(nfix (- (nfix yl) (nfix yn))))))
(cond ((mbe :logic (zp (- (nfix xl) (nfix xn)))
:exec (int= xn xl))
t)
((mbe :logic (zp (- (nfix yl) (nfix yn)))
:exec (int= yn yl))
nil)
((eql (the character (char x xn))
(the character (char y yn)))
(mbe :logic (strprefixp-impl x y
(+ (nfix xn) 1)
(+ (nfix yn) 1)
xl yl)
:exec (strprefixp-impl (the string x)
(the string y)
(the integer (+ (the integer xn) 1))
(the integer (+ (the integer yn) 1))
(the integer xl)
(the integer yl))))
(t
nil)))
(local (in-theory (enable strprefixp-impl)))
(defthm strprefixp-impl-elim
(implies (and (force (stringp x))
(force (stringp y))
(force (natp xn))
(force (natp yn))
(force (= xl (length x)))
(force (= yl (length y)))
(force (<= xn xl))
(force (<= yn yl)))
(equal (strprefixp-impl x y xn yn xl yl)
(prefixp (nthcdr xn (explode x))
(nthcdr yn (explode y)))))))
(defsection strprefixp
:parents (substrings)
:short "Case-sensitive string prefix test."
:long "<p>@(call strprefixp) determines if the string @('x') is a prefix of
the string @('y'), in a case-sensitive manner.</p>
<p>Logically, this is identical to</p>
@({
(prefixp (explode x) (explode y))
})
<p>But we use a more efficient implementation which avoids coercing the strings
into character lists.</p>"
(definline strprefixp (x y)
(declare (type string x)
(type string y))
(mbe :logic (prefixp (explode x)
(explode y))
:exec (strprefixp-impl (the string x)
(the string y)
(the integer 0)
(the integer 0)
(the integer (length (the string x)))
(the integer (length (the string y))))))
(defcong streqv equal (strprefixp x y) 1)
(defcong streqv equal (strprefixp x y) 2))
|