mathlib docs: core.system.io

source

inductive io.error :

Type

other : string → io.error
sys : ℕ → io.error

source

inductive io.mode :

Type

read : io.mode
write : io.mode
read_write : io.mode
append : io.mode

source

inductive io.process.stdio :

Type

source

structure io.process.spawn_args :

Type

cmd : string
args : list string
stdin : io.process.stdio
stdout : io.process.stdio
stderr : io.process.stdio
cwd : option string
env : list (string × option string)

source

@[class]

structure monad_io (m : Type → Type → Type) :

Type 1

monad : Π (e : Type), monad (m e)
catch : Π (e₁ e₂ α : Type), m e₁ α → (e₁ → m e₂ α) → m e₂ α
fail : Π (e α : Type), e → m e α
iterate : Π (e α : Type), α → (α → m e (option α)) → m e α
handle : Type

Instances

monad_io_impl

source

@[class]

structure monad_io_terminal (m : Type → Type → Type) :

Type

put_str : string → m io.error unit
get_line : m io.error string
cmdline_args : list string

Instances

monad_io_terminal_impl

source

@[class]

structure monad_io_net_system (m : Type → Type → Type) [monad_io m] :

Type 1

socket : Type
listen : string → ℕ → m io.error (monad_io_net_system.socket m)
accept : monad_io_net_system.socket m → m io.error (monad_io_net_system.socket m)
connect : string → m io.error (monad_io_net_system.socket m)
recv : monad_io_net_system.socket m → ℕ → m io.error char_buffer
send : monad_io_net_system.socket m → char_buffer → m io.error unit
close : monad_io_net_system.socket m → m io.error unit

Instances

monad_io_net_system_impl

source

@[class]

structure monad_io_file_system (m : Type → Type → Type) [monad_io m] :

Type

mk_file_handle : string → io.mode → bool → m io.error (monad_io.handle m)
is_eof : monad_io.handle m → m io.error bool
flush : monad_io.handle m → m io.error unit
close : monad_io.handle m → m io.error unit
read : monad_io.handle m → ℕ → m io.error char_buffer
write : monad_io.handle m → char_buffer → m io.error unit
get_line : monad_io.handle m → m io.error char_buffer
stdin : m io.error (monad_io.handle m)
stdout : m io.error (monad_io.handle m)
stderr : m io.error (monad_io.handle m)
file_exists : string → m io.error bool
dir_exists : string → m io.error bool
remove : string → m io.error unit
rename : string → string → m io.error unit
mkdir : string → bool → m io.error bool
rmdir : string → m io.error bool

Instances

monad_io_file_system_impl

source

@[class]

meta structure monad_io_serial (m : Type → Type → Type) [monad_io m] :

Type

serialize : monad_io.handle m → expr → m io.error unit
deserialize : monad_io.handle m → m io.error expr

Instances

monad_io_serial_impl

source

@[class]

structure monad_io_environment (m : Type → Type → Type) :

Type

get_env : string → m io.error (option string)
get_cwd : m io.error string
set_cwd : string → m io.error unit

Instances

monad_io_environment_impl

source

@[class]

structure monad_io_process (m : Type → Type → Type) [monad_io m] :

Type 1

child : Type
stdin : monad_io_process.child m → monad_io.handle m
stdout : monad_io_process.child m → monad_io.handle m
stderr : monad_io_process.child m → monad_io.handle m
spawn : io.process.spawn_args → m io.error (monad_io_process.child m)
wait : monad_io_process.child m → m io.error ℕ
sleep : ℕ → m io.error unit

Instances

monad_io_process_impl

source

@[class]

structure monad_io_random (m : Type → Type → Type) :

Type

set_rand_gen : std_gen → m io.error unit
rand : ℕ → ℕ → m io.error ℕ

Instances

monad_io_random_impl

source

@[instance]

def monad_io_is_monad (m : Type → Type → Type) (e : Type) [monad_io m] :

monad (m e)

Equations

monad_io_is_monad m e = monad_io.monad e

source

@[instance]

def monad_io_is_monad_fail (m : Type → Type → Type) [monad_io m] :

monad_fail (m io.error)

Equations

monad_io_is_monad_fail m = {fail := λ (α : Type) (s : string), monad_io.fail io.error α (io.error.other s)}

source

@[instance]

def monad_io_is_alternative (m : Type → Type → Type) [monad_io m] :

alternative (m io.error)

Equations

monad_io_is_alternative m = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type) (x : _x → _x_1) (y : m io.error _x), pure x <*> y, map_const := λ (α β : Type), (λ (x : β → α) (y : m io.error β), pure x <*> y) ∘ function.const β}, to_has_pure := applicative.to_has_pure monad.to_applicative, to_has_seq := applicative.to_has_seq monad.to_applicative, to_has_seq_left := {seq_left := λ (α β : Type) (a : m io.error α) (b : m io.error β), (λ (_x _x_1 : Type) (x : _x → _x_1) (y : m io.error _x), pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type) (a : m io.error α) (b : m io.error β), (λ (_x _x_1 : Type) (x : _x → _x_1) (y : m io.error _x), pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := λ (α : Type) (a b : m io.error α), monad_io.catch io.error io.error α a (λ (_x : io.error), b)}, failure := λ (α : Type), monad_io.fail io.error α (io.error.other "failure")}