/usr/share/acl2-4.3/books/str/istrprefixp.lisp is in acl2-books-source 4.3-3.
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 | ; ACL2 String Library
; Copyright (C) 2009-2010 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 "iprefixp")
(include-book "unicode/nthcdr" :dir :system)
(local (include-book "arithmetic"))
(local (defthm iprefixp-lemma-1
(implies (and (natp xn)
(natp yn)
(< xn (len x))
(< yn (len y))
(not (ichareqv (nth xn x) (nth yn y))))
(not (iprefixp (nthcdr xn x) (nthcdr yn y))))
:hints(("Goal" :in-theory (enable nthcdr nth iprefixp)))))
(local (defthm iprefixp-lemma-2
(implies (and (natp xn)
(natp yn)
(< xn (len x))
(< yn (len y))
(ichareqv (nth xn x) (nth yn y)))
(equal (iprefixp (nthcdr xn x) (nthcdr yn y))
(iprefixp (cdr (nthcdr xn x)) (cdr (nthcdr yn y)))))
:hints(("Goal" :in-theory (enable iprefixp nth nthcdr)))))
(defund istrprefixp-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))))
:guard-hints (("Goal" :in-theory (enable ichareqv)))))
(cond ((mbe :logic (zp (- (nfix xl) (nfix xn)))
:exec (= (the integer xn)
(the integer xl)))
t)
((mbe :logic (zp (- (nfix yl) (nfix yn)))
:exec (= (the integer yn)
(the integer yl)))
nil)
((mbe :logic (ichareqv (char x xn)
(char y yn))
:exec (let ((cx (the character (char (the string x) (the integer xn))))
(cy (the character (char (the string y) (the integer yn)))))
(if (standard-char-p (the character cx))
(if (standard-char-p (the character cy))
(char-equal (the character cx) (the character cy))
nil)
(eql (the character cx) (the character cy)))))
(mbe :logic (istrprefixp-impl x y
(+ (nfix xn) 1)
(+ (nfix yn) 1)
xl yl)
:exec (istrprefixp-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)))
(defthm istrprefixp-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 (istrprefixp-impl x y xn yn xl yl)
(iprefixp (nthcdr xn (coerce x 'list))
(nthcdr yn (coerce y 'list)))))
:hints(("Goal" :in-theory (enable istrprefixp-impl))))
(defun istrprefixp (x y)
":Doc-Section Str
Case-insensitive string prefix test~/
~c[(istrprefixp x y)] determines if the string x is a prefix of the string y, in
a case-insensitive manner.
Logically, this is identical to ~c[(iprefixp (coerce x 'list) (coerce y 'list))],
but we use a more efficient implementation which avoids coercing the strings.~/
~l[str::strprefixp] and ~pl[str::iprefixp]"
(declare (type string x)
(type string y))
(mbe :logic (iprefixp (coerce x 'list)
(coerce y 'list))
:exec (istrprefixp-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))))))
|