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))
|