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
|
(include-book "../lofat")
(include-book "centaur/getopt/top" :dir :system)
(include-book "oslib/argv" :dir :system)
(encapsulate
()
(local (include-book "arithmetic-3/top" :dir :system))
(defun
fixed-width-print-helper (x n)
(declare
(xargs :hints (("goal" :in-theory (disable floor mod)))))
(if
(or (zp n) (zp x))
nil
(append
(fixed-width-print-helper (floor x 10) (- n 1))
(list (code-char (+ (mod x 10) (char-code #\0))))))))
(defthm len-of-fixed-width-print-helper
(<= (len (fixed-width-print-helper x n))
(nfix n))
:rule-classes :linear
:hints (("goal" :in-theory (disable ceiling floor))))
(defun fixed-width-print (x n)
(coerce (if (zp x)
(cons #\0
(make-list (- n 1) :initial-element #\space))
(append (fixed-width-print-helper x n)
(make-list (- n (len (fixed-width-print-helper x n)))
:initial-element #\space)))
'string))
(defthm
length-of-fixed-width-print
(implies (not (zp n))
(equal (len (explode (fixed-width-print x n)))
n))
:hints (("goal" :in-theory (enable fixed-width-print))))
(defoptions stat-opts
:parents (demo2)
:tag :demo2
((file-system "Provide filesystem parameters"
booleanp
:rule-classes :type-prescription
:alias #\f)))
(b*
(((mv argv state) (oslib::argv))
((mv errmsg opts ?extra-args) (parse-stat-opts argv))
((when errmsg)
(mv fat32$c state))
((stat-opts opts) opts)
((unless opts.file-system)
(mv fat32$c state))
((mv & val state)
(getenv$ "DISK" state))
((mv fat32$c &)
(disk-image-to-lofat
fat32$c val state))
((mv & val state)
(getenv$ "STAT_OUTPUT" state))
((mv channel state)
(open-output-channel val :character state))
((mv & path state)
(getenv$ "STAT_INPUT" state))
(statfsbuf (lofat-statfs fat32$c))
(state
(pprogn
(princ$ " File: \"" channel state)
(princ$ path channel state)
(princ$"\"" channel state)
(newline channel state)
(princ$ " ID: " channel state)
;; Choosing to print 0 as a constant here - rather than take it from the
;; stat - becasue the coreutils version has some complicated rules for
;; printing the value in the f_fsid field
(princ$ (fixed-width-print 0 8) channel state)
(princ$ " Namelen: " channel state)
(princ$ (fixed-width-print
(struct-statfs->f_namelen statfsbuf)
7)
channel state)
(princ$ " Type: " channel state)
(if (equal (struct-statfs->f_type statfsbuf) *S_MAGIC_FUSEBLK*)
(princ$ "fuseblk" channel state)
(princ$ "UNKNOWN ()" channel state))
(newline channel state)
(princ$ "Block size: " channel state)
(princ$ (fixed-width-print
(struct-statfs->f_bsize statfsbuf) 10)
channel state)
(princ$ " Fundamental block size: " channel state)
(princ$ (struct-statfs->f_bsize statfsbuf) channel state)
(newline channel state)
(princ$ "Blocks: Total: " channel state)
(princ$ (fixed-width-print
(struct-statfs->f_blocks statfsbuf)
10) channel state)
(princ$ " Free: " channel state)
(princ$ (fixed-width-print
(struct-statfs->f_bavail statfsbuf)
10) channel state)
(princ$ " Available: " channel state)
(princ$ (struct-statfs->f_bavail statfsbuf) channel state)
(newline channel state)
(princ$ "Inodes: Total: " channel state)
(princ$ (fixed-width-print
(struct-statfs->f_files statfsbuf)
10) channel state)
(princ$ " Free: " channel state)
(princ$ (struct-statfs->f_ffree statfsbuf) channel state)
(newline channel state)
(close-output-channel channel state))))
(mv fat32$c state))
|
