/usr/share/acl2-6.5/books/regex/regex-chartrans.lisp is in acl2-books-source 6.5-2.
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 | (in-package "ACL2")
(defun is-uppercase (c)
(declare (xargs :guard (characterp c)))
(and (standard-char-p c)
(upper-case-p c)))
(defun is-lowercase (c)
(declare (xargs :guard (characterp c)))
(and (standard-char-p c)
(lower-case-p c)))
(defun make-case-insens-translation (i)
(declare (xargs :measure (nfix (- 256 i))
:guard (and (natp i)
(<= i 256))))
(if (zp (- 256 i))
nil
(let ((char (code-char i)))
(if (is-lowercase char)
(cons (cons char (char-upcase char))
(make-case-insens-translation (1+ i)))
(make-case-insens-translation (1+ i))))))
(defconst *case-insens-translation*
(make-case-insens-translation 0))
(in-theory (disable is-uppercase is-lowercase))
(defun translation-table-p (x)
(declare (xargs :guard t))
(if (atom x)
(equal x nil)
(and (consp (car x))
(characterp (caar x))
(characterp (cdar x))
(translation-table-p (cdr x)))))
(defthm translation-table-p-case-insens-trans
(translation-table-p *case-insens-translation*))
(defthm assoc-translation-table
(implies (and (translation-table-p trans)
(assoc ch trans))
(and (characterp (car (assoc ch trans)))
(characterp (cdr (assoc ch trans))))))
(defun apply-translation1 (clist trans)
(declare (xargs :guard (and (character-listp clist)
(translation-table-p trans))))
(if (atom clist)
nil
(let* ((ch (car clist))
(pair (assoc ch trans)))
(cons (if pair (cdr pair) ch)
(apply-translation1 (cdr clist) trans)))))
(defthm character-listp-apply-translation1
(implies (and (character-listp clist)
(translation-table-p trans))
(character-listp (apply-translation1 clist trans))))
(defthm apply-translation1-length
(equal (len (apply-translation1 clist trans))
(len clist)))
(defun apply-translation (str trans)
(declare (xargs :guard (and (stringp str)
(translation-table-p trans))))
(coerce (apply-translation1 (coerce str 'list) trans) 'string))
(defthm stringp-apply-translation
(implies (and (stringp str)
(translation-table-p trans))
(stringp (apply-translation str trans))))
(defthm apply-translation-length
(implies (and (stringp str)
(translation-table-p trans))
(equal (length (apply-translation str trans))
(length str))))
(in-theory (disable apply-translation))
(defun case-insens-trans (str)
(declare (xargs :guard (stringp str)))
(apply-translation str *case-insens-translation*))
(defthm stringp-case-insens-trans
(implies (stringp str)
(stringp (case-insens-trans str))))
(defthm case-insens-trans-length
(implies (stringp str)
(equal (length (case-insens-trans str))
(length str))))
(in-theory (disable case-insens-trans))
|