-
Notifications
You must be signed in to change notification settings - Fork 80
/
io.lean
291 lines (211 loc) · 8.9 KB
/
io.lean
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
-/
import system.io_interface
/- The following constants have a builtin implementation -/
constant io_core : Type → Type → Type
/- Auxiliary definition used in the builtin implementation of monad_io_random_impl -/
def io_rand_nat : std_gen → nat → nat → nat × std_gen :=
rand_nat
@[instance] constant monad_io_impl : monad_io io_core
@[instance] constant monad_io_terminal_impl : monad_io_terminal io_core
@[instance] constant monad_io_net_system_impl : monad_io_net_system io_core
@[instance] constant monad_io_file_system_impl : monad_io_file_system io_core
@[instance] meta constant monad_io_serial_impl : monad_io_serial io_core
@[instance] constant monad_io_environment_impl : monad_io_environment io_core
@[instance] constant monad_io_process_impl : monad_io_process io_core
@[instance] constant monad_io_random_impl : monad_io_random io_core
instance io_core_is_monad (e : Type) : monad (io_core e) :=
monad_io_is_monad io_core e
instance io_core_is_monad_fail : monad_fail (io_core io.error) :=
monad_io_is_monad_fail io_core
instance io_core_is_alternative : alternative (io_core io.error) :=
monad_io_is_alternative io_core
@[reducible] def io (α : Type) :=
io_core io.error α
namespace io
/- Remark: the following definitions can be generalized and defined for any (m : Type -> Type -> Type)
that implements the required type classes. However, the generalized versions are very inconvenient to use,
(example: `#eval io.put_str "hello world"` does not work because we don't have enough information to infer `m`.).
-/
def iterate {e α} (a : α) (f : α → io_core e (option α)) : io_core e α :=
monad_io.iterate e α a f
def forever {e} (a : io_core e unit) : io_core e unit :=
iterate () $ λ _, a >> return (some ())
-- TODO(Leo): delete after we merge #1881
def catch {e₁ e₂ α} (a : io_core e₁ α) (b : e₁ → io_core e₂ α) : io_core e₂ α :=
monad_io.catch e₁ e₂ α a b
def finally {α e} (a : io_core e α) (cleanup : io_core e unit) : io_core e α := do
res ← catch (sum.inr <$> a) (return ∘ sum.inl),
cleanup,
match res with
| sum.inr res := return res
| sum.inl error := monad_io.fail _ _ error
end
protected def fail {α : Type} (s : string) : io α :=
monad_io.fail _ _ (io.error.other s)
def put_str : string → io unit :=
monad_io_terminal.put_str
def put_str_ln (s : string) : io unit :=
put_str s >> put_str "\n"
def get_line : io string :=
monad_io_terminal.get_line
def cmdline_args : io (list string) :=
return (monad_io_terminal.cmdline_args io_core)
def print {α} [has_to_string α] (s : α) : io unit :=
put_str ∘ to_string $ s
def print_ln {α} [has_to_string α] (s : α) : io unit :=
print s >> put_str "\n"
def handle : Type :=
monad_io.handle io_core
def mk_file_handle (s : string) (m : mode) (bin : bool := ff) : io handle :=
monad_io_file_system.mk_file_handle s m bin
def stdin : io handle :=
monad_io_file_system.stdin
def stderr : io handle :=
monad_io_file_system.stderr
def stdout : io handle :=
monad_io_file_system.stdout
meta def serialize : handle → expr → io unit :=
monad_io_serial.serialize
meta def deserialize : handle → io expr :=
monad_io_serial.deserialize
namespace env
def get (env_var : string) : io (option string) :=
monad_io_environment.get_env env_var
/-- get the current working directory -/
def get_cwd : io string :=
monad_io_environment.get_cwd
/-- set the current working directory -/
def set_cwd (cwd : string) : io unit :=
monad_io_environment.set_cwd cwd
end env
namespace net
def socket : Type :=
monad_io_net_system.socket io_core
def listen : string → nat → io socket :=
monad_io_net_system.listen
def accept : socket → io socket :=
monad_io_net_system.accept
def connect : string → io socket :=
monad_io_net_system.connect
def recv : socket → nat → io char_buffer :=
monad_io_net_system.recv
def send : socket → char_buffer → io unit :=
monad_io_net_system.send
def close : socket → io unit :=
monad_io_net_system.close
end net
namespace fs
def is_eof : handle → io bool :=
monad_io_file_system.is_eof
def flush : handle → io unit :=
monad_io_file_system.flush
def close : handle → io unit :=
monad_io_file_system.close
def read : handle → nat → io char_buffer :=
monad_io_file_system.read
def write : handle → char_buffer → io unit :=
monad_io_file_system.write
def get_char (h : handle) : io char :=
do b ← read h 1,
if h : b.size = 1 then return $ b.read ⟨0, h.symm ▸ nat.zero_lt_one⟩
else io.fail "get_char failed"
def get_line : handle → io char_buffer :=
monad_io_file_system.get_line
def put_char (h : handle) (c : char) : io unit :=
write h (mk_buffer.push_back c)
def put_str (h : handle) (s : string) : io unit :=
write h (mk_buffer.append_string s)
def put_str_ln (h : handle) (s : string) : io unit :=
put_str h s >> put_str h "\n"
def read_to_end (h : handle) : io char_buffer :=
iterate mk_buffer $ λ r,
do done ← is_eof h,
if done
then return none
else do
c ← read h 1024,
return $ some (r ++ c)
def read_file (s : string) (bin := ff) : io char_buffer :=
do h ← mk_file_handle s io.mode.read bin,
read_to_end h
def file_exists : string → io bool :=
monad_io_file_system.file_exists
def dir_exists : string → io bool :=
monad_io_file_system.dir_exists
def remove : string → io unit :=
monad_io_file_system.remove
def rename : string → string → io unit :=
monad_io_file_system.rename
def mkdir (path : string) (recursive : bool := ff) : io bool :=
monad_io_file_system.mkdir path recursive
def rmdir : string → io bool :=
monad_io_file_system.rmdir
end fs
namespace proc
def child : Type :=
monad_io_process.child io_core
def child.stdin : child → handle :=
monad_io_process.stdin
def child.stdout : child → handle :=
monad_io_process.stdout
def child.stderr : child → handle :=
monad_io_process.stderr
def spawn (p : io.process.spawn_args) : io child :=
monad_io_process.spawn p
def wait (c : child) : io nat :=
monad_io_process.wait c
def sleep (n : nat) : io unit :=
monad_io_process.sleep n
end proc
def set_rand_gen : std_gen → io unit :=
monad_io_random.set_rand_gen
def rand (lo : nat := std_range.1) (hi : nat := std_range.2) : io nat :=
monad_io_random.rand lo hi
end io
meta constant format.print_using : format → options → io unit
meta definition format.print (fmt : format) : io unit :=
format.print_using fmt options.mk
meta definition pp_using {α : Type} [has_to_format α] (a : α) (o : options) : io unit :=
format.print_using (to_fmt a) o
meta definition pp {α : Type} [has_to_format α] (a : α) : io unit :=
format.print (to_fmt a)
/-- Run the external process specified by `args`.
The process will run to completion with its output captured by a pipe, and
read into `string` which is then returned. -/
def io.cmd (args : io.process.spawn_args) : io string :=
do child ← io.proc.spawn { stdout := io.process.stdio.piped, ..args },
buf ← io.fs.read_to_end child.stdout,
io.fs.close child.stdout,
exitv ← io.proc.wait child,
when (exitv ≠ 0) $ io.fail $ "process exited with status " ++ repr exitv,
return buf.to_string
/--
This is the "back door" into the `io` monad, allowing IO computation to be performed during tactic execution.
For this to be safe, the IO computation should be ideally free of side effects and independent of its environment.
This primitive is used to invoke external tools (e.g., SAT and SMT solvers) from a tactic.
IMPORTANT: this primitive can be used to implement `unsafe_perform_io {α : Type} : io α → option α`
or `unsafe_perform_io {α : Type} [inhabited α] : io α → α`. This can be accomplished by executing
the resulting tactic using an empty `tactic_state` (we have `tactic_state.mk_empty`).
If `unsafe_perform_io` is defined, and used to perform side-effects, users need to take the following
precautions:
- Use `@[noinline]` attribute in any function to invokes `tactic.unsafe_perform_io`.
Reason: if the call is inlined, the IO may be performed more than once.
- Set `set_option compiler.cse false` before any function that invokes `tactic.unsafe_perform_io`.
This option disables common subexpression elimination. Common subexpression elimination
might combine two side effects that were meant to be separate.
TODO[Leo]: add `[noinline]` attribute and option `compiler.cse`.
-/
meta constant tactic.unsafe_run_io {α : Type} : io α → tactic α
/--
Execute the given tactic with a tactic_state object that contains:
- The current environment in the virtual machine.
- The current set of options in the virtual machine.
- Empty metavariable and local contexts.
- One single goal of the form `⊢ true`.
This action is mainly useful for writing tactics that inspect
the environment. -/
meta constant io.run_tactic {α : Type} (a : tactic α) : io α