core / system.io - mathlib docs

io.finally a cleanup = io.catch (sum.inr <$> a) (return ∘ sum.inl) >>= λ (res : e ⊕ α), cleanup >>= λ (_x : unit), io.finally._match_1 res
io.finally._match_1 (sum.inr res) = return res
io.finally._match_1 (sum.inl error) = monad_io.fail e α error

source

@[protected]

def io.fail {α : Type} (s : string) :

io α

Equations

io.fail s = monad_io.fail io.error α (io.error.other s)

source

def io.put_str :

string → io unit

Equations

io.put_str = monad_io_terminal.put_str

source

def io.put_str_ln (s : string) :

io unit

Equations

io.put_str_ln s = io.put_str s >> io.put_str "\n"

source

def io.get_line :

io string

Equations

io.get_line = monad_io_terminal.get_line

source

def io.cmdline_args :

io (list string)

Equations

io.cmdline_args = return (monad_io_terminal.cmdline_args io_core)

source

def io.print {α : Type u_1} [has_to_string α] (s : α) :

io unit

Equations

io.print s = (io.put_str ∘ to_string) s

source

def io.print_ln {α : Type u_1} [has_to_string α] (s : α) :

io unit

Equations

io.print_ln s = io.print s >> io.put_str "\n"

source

def io.handle :

Type

Equations

io.handle = monad_io.handle io_core

source

def io.mk_file_handle (s : string) (m : io.mode) (bin : bool := ff) :

io io.handle

Equations

io.mk_file_handle s m bin = monad_io_file_system.mk_file_handle s m bin

source

def io.stdin :

io io.handle

Equations

io.stdin = monad_io_file_system.stdin

source

def io.stderr :

io io.handle

Equations

io.stderr = monad_io_file_system.stderr

source

def io.stdout :

io io.handle

Equations

io.stdout = monad_io_file_system.stdout

source

meta def io.serialize :

io.handle → expr → io unit

source

meta def io.deserialize :

io.handle → io expr

source

def io.env.get (env_var : string) :

io (option string)

Equations

io.env.get env_var = monad_io_environment.get_env env_var

source

def io.env.get_cwd :

io string

get the current working directory

Equations

io.env.get_cwd = monad_io_environment.get_cwd

source

def io.env.set_cwd (cwd : string) :

io unit

set the current working directory

Equations

io.env.set_cwd cwd = monad_io_environment.set_cwd cwd

source

def io.net.socket :

Type

Equations

io.net.socket = monad_io_net_system.socket io_core

source

def io.net.listen :

string → ℕ → io io.net.socket

Equations

io.net.listen = monad_io_net_system.listen

source

def io.net.accept :

io.net.socket → io io.net.socket

Equations

io.net.accept = monad_io_net_system.accept

source

def io.net.connect :

string → io io.net.socket

Equations

io.net.connect = monad_io_net_system.connect

source

def io.net.recv :

io.net.socket → ℕ → io char_buffer

Equations

io.net.recv = monad_io_net_system.recv

source

def io.net.send :

io.net.socket → char_buffer → io unit

Equations

io.net.send = monad_io_net_system.send

source

def io.net.close :

io.net.socket → io unit

Equations

io.net.close = monad_io_net_system.close

source

def io.fs.is_eof :

io.handle → io bool

Equations

io.fs.is_eof = monad_io_file_system.is_eof

source

def io.fs.flush :

io.handle → io unit

Equations

io.fs.flush = monad_io_file_system.flush

source

def io.fs.close :

io.handle → io unit

Equations

io.fs.close = monad_io_file_system.close

source

def io.fs.read :

io.handle → ℕ → io char_buffer

Equations

io.fs.read = monad_io_file_system.read

source

def io.fs.write :

io.handle → char_buffer → io unit

Equations

io.fs.write = monad_io_file_system.write

source

def io.fs.get_char (h : io.handle) :

io char

Equations

io.fs.get_char h = io.fs.read h 1 >>= λ (b : char_buffer), dite (buffer.size b = 1) (λ (h : buffer.size b = 1), return (buffer.read b ⟨0, _⟩)) (λ (h : ¬buffer.size b = 1), io.fail "get_char failed")

source

def io.fs.get_line :

io.handle → io char_buffer

Equations

io.fs.get_line = monad_io_file_system.get_line

source

def io.fs.put_char (h : io.handle) (c : char) :

io unit

Equations

io.fs.put_char h c = io.fs.write h (mk_buffer.push_back c)

source

def io.fs.put_str (h : io.handle) (s : string) :

io unit

Equations

io.fs.put_str h s = io.fs.write h (mk_buffer.append_string s)

source

def io.fs.put_str_ln (h : io.handle) (s : string) :

io unit

Equations

io.fs.put_str_ln h s = io.fs.put_str h s >> io.fs.put_str h "\n"

source

def io.fs.read_to_end (h : io.handle) :

io char_buffer

Equations

io.fs.read_to_end h = io.iterate mk_buffer (λ (r : char_buffer), io.fs.is_eof h >>= λ (done : bool), ite ↥done (return none) (io.fs.read h 1024 >>= λ (c : char_buffer), return (some (r ++ c))))

source

def io.fs.read_file (s : string) (bin : bool := ff) :

io char_buffer

Equations

io.fs.read_file s bin = io.mk_file_handle s io.mode.read bin >>= λ (h : io.handle), io.fs.read_to_end h

source

def io.fs.file_exists :

string → io bool

Equations

io.fs.file_exists = monad_io_file_system.file_exists

source

def io.fs.dir_exists :

string → io bool

Equations

io.fs.dir_exists = monad_io_file_system.dir_exists

source

def io.fs.remove :

string → io unit

Equations

io.fs.remove = monad_io_file_system.remove

source

def io.fs.rename :

string → string → io unit

Equations

io.fs.rename = monad_io_file_system.rename

source

def io.fs.mkdir (path : string) (recursive : bool := ff) :

io bool

Equations

io.fs.mkdir path recursive = monad_io_file_system.mkdir path recursive

source

def io.fs.rmdir :

string → io bool

Equations

io.fs.rmdir = monad_io_file_system.rmdir

source

def io.proc.child :

Type

Equations

io.proc.child = monad_io_process.child io_core

source

def io.proc.child.stdin :

io.proc.child → io.handle

Equations

io.proc.child.stdin = monad_io_process.stdin

source

def io.proc.child.stdout :

io.proc.child → io.handle

Equations

io.proc.child.stdout = monad_io_process.stdout

source

def io.proc.child.stderr :

io.proc.child → io.handle

Equations

io.proc.child.stderr = monad_io_process.stderr

source

def io.proc.spawn (p : io.process.spawn_args) :

io io.proc.child

Equations

io.proc.spawn p = monad_io_process.spawn p

source

def io.proc.wait (c : io.proc.child) :

io ℕ

Equations

io.proc.wait c = monad_io_process.wait c

source

def io.proc.sleep (n : ℕ) :

io unit

Equations

io.proc.sleep n = monad_io_process.sleep n

source

def io.set_rand_gen :

std_gen → io unit

Equations

io.set_rand_gen = monad_io_random.set_rand_gen

source

def io.rand (lo : ℕ := std_range.fst) (hi : ℕ := std_range.snd) :

io ℕ

Equations

io.rand lo hi = monad_io_random.rand lo hi

source

meta constant format.print_using :

format → options → io unit

source

meta def format.print (fmt : format) :

io unit

source

meta def pp_using {α : Type} [has_to_format α] (a : α) (o : options) :

io unit

source

meta def pp {α : Type} [has_to_format α] (a : α) :

io unit

source

def io.cmd (args : io.process.spawn_args) :

io string

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.

Equations

io.cmd args = io.proc.spawn {cmd := args.cmd, args := args.args, stdin := args.stdin, stdout := io.process.stdio.piped, stderr := args.stderr, cwd := args.cwd, env := args.env} >>= λ (child : io.proc.child), io.fs.read_to_end child.stdout >>= λ (buf : char_buffer), io.fs.close child.stdout >>= λ (_x : unit), io.proc.wait child >>= λ (exitv : ℕ), when (exitv ≠ 0) (io.fail ("process exited with status " ++ repr exitv)) >>= λ (_x : unit), return (buffer.to_string buf)

source

meta constant tactic.unsafe_run_io {α : Type} :

io α → tactic α

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.

source

meta constant io.run_tactic {α : Type} (a : tactic α) :

io α

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.