File: stat-replicant.lisp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (117 lines) | stat: -rw-r--r-- 4,084 bytes parent folder | download | duplicates (3)
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))