← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/oslib/tempfile.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/oslib/tempfile.lisp
1
1
; OSLIB -- Operating System Utilities
2
 
; Copyright (C) 2013 Centaur Technology
 
2
; Copyright (C) 2013-2014 Centaur Technology
3
3
;
4
4
; Contact:
5
5
;   Centaur Technology Formal Verification Group
31
31
 
32
32
(in-package "OSLIB")
33
33
(include-book "getpid")
34
 
(include-book "catpath")
35
 
(include-book "std/strings/decimal" :dir :system)
36
 
(include-book "std/strings/cat" :dir :system)
37
 
 
38
 
(defsection tempfile
39
 
  :parents (oslib)
40
 
  :short "Generate a suitable name for a temporary file."
41
 
 
42
 
  :long "<p>Signature: @(call tempfile) &rarr; @('(mv filename/nil
43
 
state)').</p>
44
 
 
45
 
<p>Example:</p>
46
 
 
47
 
@({
48
 
 (tempfile \"foo\") --> (\"/tmp/jared-31721-foo\" <state>)
49
 
})
50
 
 
51
 
<p>Note: this function is attachable.  If you need to generate temporary file
52
 
names using some other scheme, you can define your own strategy and attach it
53
 
to @('tempfile-fn'); see @(see defattach).</p>
54
 
 
55
 
<p>The intent is that this function should produce a good @('filename') to use
56
 
for the name of a temporary file.  To allow @('tempfile') implementations to
57
 
fail for whatever reason, @('filename') may be @('nil').</p>
58
 
 
59
 
@(def tempfile)
60
 
@(def tempfile-fn)"
61
 
 
62
 
  (defmacro tempfile (basename &optional (state 'state))
63
 
    `(tempfile-fn ,basename ,state))
64
 
 
65
 
  (encapsulate
66
 
    (((tempfile-fn * state) => (mv * state)
67
 
      :formals (basename state)
68
 
      :guard (stringp basename)))
69
 
 
70
 
    (local (defun tempfile-fn (basename state)
71
 
             (declare (xargs :stobjs state)
72
 
                      (ignore basename))
73
 
             (mv "" state)))
74
 
 
75
 
    (defthm type-of-tempfile-fn
76
 
      ;; Tempfile-fn can fail, for whatever reason, by producing NIL.
77
 
      (or (stringp (mv-nth 0 (tempfile-fn basename state)))
78
 
          (not (mv-nth 0 (tempfile-fn basename state))))
79
 
      :rule-classes :type-prescription)
80
 
 
81
 
    (defthm state-p1-of-tempfile-fn
82
 
      (implies (force (state-p1 state))
83
 
               (state-p1 (mv-nth 1 (tempfile-fn basename state)))))))
84
 
 
85
 
 
86
 
 
87
 
(define default-tempfile-aux
88
 
  ((tempdir stringp "Directory to generate the file in")
89
 
   (basename stringp "Base name to use for the new file")
90
 
   state)
91
 
  :returns (mv (tempfile "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')"
92
 
                         (or (stringp tempfile)
93
 
                             (not tempfile))
94
 
                         :rule-classes :type-prescription)
95
 
               (state state-p1 :hyp (force (state-p1 state))))
96
 
 
97
 
  :parents (tempfile)
98
 
  :short "Join together a temp directory, the user name, the PID, and the base
99
 
name to create a temporary filename."
100
 
 
101
 
  (b* (((mv pid state) (getpid state))
102
 
       ((unless (natp pid))
103
 
        (er hard? __function__ "getpid failed")
104
 
        (mv nil state))
105
 
       ((mv ?err user state) (getenv$ "USER" state))
106
 
       ((unless (stringp user))
107
 
        (er hard? __function__ "reading $USER failed")
108
 
        (mv nil state))
109
 
       (filename (str::cat user "-" (str::natstr pid) "-" basename))
110
 
       (path     (catpath tempdir filename)))
111
 
    (mv path state)))
112
 
 
113
 
 
114
 
 
115
 
(define default-tempdir (state)
116
 
  :returns (mv (tempdir "Directory to use for temporary files."
117
 
                        stringp :rule-classes :type-prescription)
118
 
               (state state-p1 :hyp (force (state-p1 state))))
119
 
 
120
 
  :parents (tempfile)
121
 
  :short "Figure out what directory to use for temporary files."
122
 
  :long "<p>We think it's conventional for Linux programs to look at the value
123
 
of the @('TMPDIR') environment variable.  On Windows, apparently programs
124
 
should use @('TEMP').  If either of these is set, we try to respect the choice.
125
 
Otherwise, we just default to @('/tmp').</p>"
126
 
 
127
 
  (b* (((mv ?err tempdir state) (getenv$ "TMPDIR" state))
128
 
       ((mv ?err temp state)   (getenv$ "TEMP" state)))
129
 
    (mv (or (and (stringp tempdir) tempdir)
130
 
            (and (stringp temp) temp)
131
 
            "/tmp")
132
 
        state)))
133
 
 
134
 
 
135
 
(define default-tempfile ((basename stringp)
136
 
                          state)
137
 
  :returns (mv (tempfile (or (stringp tempfile)
138
 
                             (not tempfile))
139
 
                         :rule-classes :type-prescription)
140
 
               (state state-p1 :hyp (force (state-p1 state))))
141
 
  :parents (tempfile)
142
 
  :short "Default way to generate temporary file names."
143
 
  (b* (((mv dir state) (default-tempdir state)))
144
 
    (default-tempfile-aux dir basename state)))
145
 
 
146
 
 
147
 
(defattach tempfile-fn default-tempfile)
148
 
 
149
 
 
 
34
(include-book "tempfile-logic")