1
; OSLIB -- Operating System Utilities
2
; Copyright (C) 2013-2014 Centaur Technology
5
; Centaur Technology Formal Verification Group
6
; 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
7
; http://www.centtech.com/
9
; License: (An MIT/X11-style license)
11
; Permission is hereby granted, free of charge, to any person obtaining a
12
; copy of this software and associated documentation files (the "Software"),
13
; to deal in the Software without restriction, including without limitation
14
; the rights to use, copy, modify, merge, publish, distribute, sublicense,
15
; and/or sell copies of the Software, and to permit persons to whom the
16
; Software is furnished to do so, subject to the following conditions:
18
; The above copyright notice and this permission notice shall be included in
19
; all copies or substantial portions of the Software.
21
; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
22
; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
23
; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
24
; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
25
; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
26
; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
27
; DEALINGS IN THE SOFTWARE.
29
; Original author: Jared Davis <jared@centtech.com>
32
(include-book "../ls")
33
(include-book "std/util/defconsts" :dir :system)
34
(include-book "misc/assert" :dir :system)
36
(defconsts (*files* state)
39
(assert! (member-equal ".fileforls" *files*))
40
(assert! (member-equal "ls.lisp" *files*))
41
(assert! (member-equal "top.lisp" *files*))
42
(assert! (not (member-equal "." *files*)))
43
(assert! (not (member-equal ".." *files*)))
45
(defconsts (*acl2-all* state)
46
(b* ((acl2-src-dir (f-get-global 'acl2::acl2-sources-dir state)))
47
(oslib::ls! acl2-src-dir)))
49
(assert! (member-equal "axioms.lisp" *acl2-all*)) ;; Regular file with extension
50
(assert! (member-equal "Makefile" *acl2-all*)) ;; Regular file without extension
51
(assert! (member-equal "emacs" *acl2-all*)) ;; Directory
53
(defconsts (*acl2reg* state)
54
(b* ((acl2-src-dir (f-get-global 'acl2::acl2-sources-dir state)))
55
(oslib::ls-files! acl2-src-dir)))
57
(assert! (member-equal "axioms.lisp" *acl2reg*))
58
(assert! (subsetp-equal *acl2reg* *acl2-all*))
60
(defconsts (*acl2dirs* state)
61
(b* ((acl2-src-dir (f-get-global 'acl2::acl2-sources-dir state)))
62
(oslib::ls-subdirs! acl2-src-dir)))
64
(assert! (member-equal "emacs" *acl2dirs*))
65
(assert! (subsetp-equal *acl2dirs* *acl2-all*))
66
(assert! (or (subsetp-equal *acl2-all* (append *acl2dirs* *acl2reg*))
67
(cw "Oops, somehow acl2-all has files that aren't dirs or regular? ~x0~%"
68
(set-difference-equal *acl2-all*
69
(append *acl2dirs* *acl2reg*)))))
71
(assert! (or (not (intersection-equal *acl2dirs* *acl2reg*))
72
(cw "Oops, intersecting files and dirs? ~x0~%"
73
(intersection-equal *acl2dirs* *acl2reg*))))