Init.System.IO

def EIO.bindTask {α : Type u_1} {ε : Type} {β : Type} (t : Task α) (f : α → EIO ε (Task (Except ε β))) (prio : optParam Task.Priority Task.Priority.default) :

BaseIO (Task (Except ε β))

Equations

EIO.bindTask t f prio = BaseIO.bindTask t (fun a => EIO.catchExceptions (f a) fun e => pure { get := Except.error e }) prio

source

@[inline]

def EIO.mapTasks {α : Type u_1} {ε : Type} {β : Type} (f : List α → EIO ε β) (tasks : List (Task α)) (prio : optParam Task.Priority Task.Priority.default) :

BaseIO (Task (Except ε β))

Equations

EIO.mapTasks f tasks prio = BaseIO.mapTasks (fun as => EIO.toBaseIO (f as)) tasks prio

source

def IO.ofExcept {ε : Type u_1} {α : Type} [inst : ToString ε] (e : Except ε α) :

IO α

Equations

IO.ofExcept e = match e with | Except.ok a => pure a | Except.error e => throw (IO.userError (toString e))

source

def IO.lazyPure {α : Type} (fn : Unit → α) :

IO α

Equations

IO.lazyPure fn = pure (fn ())

source

@[extern lean_io_mono_ms_now]

constant IO.monoMsNow :

BaseIO Nat

source

@[extern lean_io_get_random_bytes]

constant IO.getRandomBytes (nBytes : USize) :

IO ByteArray

source

def IO.sleep (ms : UInt32) :

IO Unit

Equations

IO.sleep ms s = dbgSleep ms fun x => EStateM.Result.ok () s

source

@[inline]

def IO.asTask {α : Type} (act : IO α) (prio : optParam Task.Priority Task.Priority.default) :

BaseIO (Task (Except IO.Error α))

Equations

IO.asTask act prio = EIO.asTask act prio

source

@[inline]

def IO.mapTask {α : Type u_1} {β : Type} (f : α → IO β) (t : Task α) (prio : optParam Task.Priority Task.Priority.default) :

BaseIO (Task (Except IO.Error β))

Equations

IO.mapTask f t prio = EIO.mapTask f t prio

source

@[inline]

def IO.bindTask {α : Type u_1} {β : Type} (t : Task α) (f : α → IO (Task (Except IO.Error β))) (prio : optParam Task.Priority Task.Priority.default) :

BaseIO (Task (Except IO.Error β))

Equations

IO.bindTask t f prio = EIO.bindTask t f prio

source

@[inline]

def IO.mapTasks {α : Type u_1} {β : Type} (f : List α → IO β) (tasks : List (Task α)) (prio : optParam Task.Priority Task.Priority.default) :

BaseIO (Task (Except IO.Error β))

Equations

IO.mapTasks f tasks prio = EIO.mapTasks f tasks prio

source

@[extern lean_io_check_canceled]

constant IO.checkCanceled :

BaseIO Bool

source

@[extern lean_io_cancel]

constant IO.cancel {α : Type u_1} :

Task α → BaseIO Unit

source

@[extern lean_io_has_finished]

constant IO.hasFinished {α : Type u_1} :

Task α → BaseIO Bool

source

@[extern lean_io_wait]

constant IO.wait {α : Type} (t : Task α) :

BaseIO α

source

@[extern lean_io_wait_any]

constant IO.waitAny {α : Type} :

List (Task α) → IO α

source

@[extern lean_io_get_num_heartbeats]

constant IO.getNumHeartbeats :

BaseIO Nat

source

inductive IO.FS.Mode :

Type

read: IO.FS.Mode
write: IO.FS.Mode
readWrite: IO.FS.Mode
append: IO.FS.Mode

source

constant IO.FS.Handle :

Type

source

structure IO.FS.Stream :

Type

isEof : IO Bool
flush : IO Unit
read : USize → IO ByteArray
write : ByteArray → IO Unit
getLine : IO String
putStr : String → IO Unit

source

instance IO.FS.instInhabitedStream :

Inhabited IO.FS.Stream

Equations

IO.FS.instInhabitedStream = { default := { isEof := default, flush := default, read := default, write := default, getLine := default, putStr := default } }

source

@[extern lean_get_stdin]

constant IO.getStdin :

BaseIO IO.FS.Stream

source

@[extern lean_get_stdout]

constant IO.getStdout :

BaseIO IO.FS.Stream

source

@[extern lean_get_stderr]

constant IO.getStderr :

BaseIO IO.FS.Stream

source

@[extern lean_get_set_stdin]

constant IO.setStdin :

IO.FS.Stream → BaseIO IO.FS.Stream

source

@[extern lean_get_set_stdout]

constant IO.setStdout :

IO.FS.Stream → BaseIO IO.FS.Stream

source

@[extern lean_get_set_stderr]

constant IO.setStderr :

IO.FS.Stream → BaseIO IO.FS.Stream

source

@[specialize]

partial def IO.iterate {α : Type} {β : Type} (a : α) (f : α → IO (α ⊕ β)) :

IO β

source

@[extern lean_io_prim_handle_mk]

constant IO.FS.Handle.mkPrim (fn : System.FilePath) (mode : String) :

IO IO.FS.Handle

source

def IO.FS.Handle.mk (fn : System.FilePath) (Mode : IO.FS.Mode) (bin : optParam Bool true) :

IO IO.FS.Handle

Equations

IO.FS.Handle.mk fn Mode bin = IO.FS.Handle.mkPrim fn (IO.FS.Handle.fopenFlags Mode bin)

source

@[extern lean_io_prim_handle_is_eof]

constant IO.FS.Handle.isEof (h : IO.FS.Handle) :

BaseIO Bool

source

@[extern lean_io_prim_handle_flush]

constant IO.FS.Handle.flush (h : IO.FS.Handle) :

IO Unit

source

@[extern lean_io_prim_handle_read]

constant IO.FS.Handle.read (h : IO.FS.Handle) (bytes : USize) :

IO ByteArray

source

@[extern lean_io_prim_handle_write]

constant IO.FS.Handle.write (h : IO.FS.Handle) (buffer : ByteArray) :

IO Unit

source

@[extern lean_io_prim_handle_get_line]

constant IO.FS.Handle.getLine (h : IO.FS.Handle) :

IO String

source

@[extern lean_io_prim_handle_put_str]

constant IO.FS.Handle.putStr (h : IO.FS.Handle) (s : String) :

IO Unit

source

@[extern lean_io_realpath]

constant IO.FS.realPath (fname : System.FilePath) :

IO System.FilePath

source

@[extern lean_io_remove_file]

constant IO.FS.removeFile (fname : System.FilePath) :

IO Unit

source

@[extern lean_io_remove_dir]

constant IO.FS.removeDir :

System.FilePath → IO Unit

source

@[extern lean_io_create_dir]

constant IO.FS.createDir :

System.FilePath → IO Unit

source

@[extern lean_io_getenv]

constant IO.getEnv (var : String) :

BaseIO (Option String)

source

@[extern lean_io_app_path]

constant IO.appPath :

IO System.FilePath

source

@[extern lean_io_current_dir]

constant IO.currentDir :

IO System.FilePath

source

@[inline]

def IO.FS.withFile {α : Type} (fn : System.FilePath) (mode : IO.FS.Mode) (f : IO.FS.Handle → IO α) :

IO α

Equations

IO.FS.withFile fn mode f = IO.FS.Handle.mk fn mode true >>= f

source

def IO.FS.Handle.putStrLn (h : IO.FS.Handle) (s : String) :

IO Unit

Equations

IO.FS.Handle.putStrLn h s = IO.FS.Handle.putStr h (String.push s (Char.ofNat 10))

source

def IO.FS.Handle.readBinToEnd (h : IO.FS.Handle) :

IO ByteArray

Equations

IO.FS.Handle.readBinToEnd h = (fun loop => loop ByteArray.empty) (IO.FS.Handle.readBinToEnd.loop h)

source

partial def IO.FS.Handle.readBinToEnd.loop (h : IO.FS.Handle) (acc : ByteArray) :

IO ByteArray

source

def IO.FS.Handle.readToEnd (h : IO.FS.Handle) :

IO String

Equations

IO.FS.Handle.readToEnd h = (fun loop => loop "") (IO.FS.Handle.readToEnd.loop h)

source

partial def IO.FS.Handle.readToEnd.loop (h : IO.FS.Handle) (s : String) :

IO String

source

def IO.FS.readBinFile (fname : System.FilePath) :

IO ByteArray

Equations

IO.FS.readBinFile fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read true IO.FS.Handle.readBinToEnd h

source

def IO.FS.readFile (fname : System.FilePath) :

IO String

Equations

IO.FS.readFile fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read false IO.FS.Handle.readToEnd h

source

def IO.FS.lines (fname : System.FilePath) :

IO (Array String)

Equations

IO.FS.lines fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read false (fun read => read #[]) (IO.FS.lines.read h)

source

partial def IO.FS.lines.read (h : IO.FS.Handle) (lines : Array String) :

IO (Array String)

source

def IO.FS.writeBinFile (fname : System.FilePath) (content : ByteArray) :

IO Unit

Equations

IO.FS.writeBinFile fname content = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.write true IO.FS.Handle.write h content

source

def IO.FS.writeFile (fname : System.FilePath) (content : String) :

IO Unit

Equations

IO.FS.writeFile fname content = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.write false IO.FS.Handle.putStr h content

source

def IO.FS.Stream.putStrLn (strm : IO.FS.Stream) (s : String) :

IO Unit

Equations

IO.FS.Stream.putStrLn strm s = IO.FS.Stream.putStr strm (String.push s (Char.ofNat 10))

source

structure IO.FS.DirEntry :

Type

root : System.FilePath
fileName : String

source

instance IO.FS.instReprDirEntry :

Repr IO.FS.DirEntry

Equations

IO.FS.instReprDirEntry = { reprPrec := [anonymous] }

source

def IO.FS.DirEntry.path (entry : IO.FS.DirEntry) :

System.FilePath

Equations

IO.FS.DirEntry.path entry = entry.root / { toString := entry.fileName }

source

inductive IO.FS.FileType :

Type

source

instance IO.FS.instReprFileType :

Repr IO.FS.FileType

Equations

IO.FS.instReprFileType = { reprPrec := [anonymous] }

source

instance IO.FS.instBEqFileType :

BEq IO.FS.FileType

Equations

IO.FS.instBEqFileType = { beq := [anonymous] }

source

structure IO.FS.SystemTime :

Type

sec : Int
nsec : UInt32

source

instance IO.FS.instBEqSystemTime :

BEq IO.FS.SystemTime

Equations

IO.FS.instBEqSystemTime = { beq := [anonymous] }

source

instance IO.FS.instReprSystemTime :

Repr IO.FS.SystemTime

Equations

IO.FS.instReprSystemTime = { reprPrec := [anonymous] }

source

instance IO.FS.instInhabitedSystemTime :

Inhabited IO.FS.SystemTime

Equations

IO.FS.instInhabitedSystemTime = { default := { sec := default, nsec := default } }

source

instance IO.FS.instOrdSystemTime :

Ord IO.FS.SystemTime

Equations

IO.FS.instOrdSystemTime = { compare := [anonymous] }

source

instance IO.FS.instLTSystemTime :

LT IO.FS.SystemTime

Equations

IO.FS.instLTSystemTime = ltOfOrd

source

instance IO.FS.instLESystemTime :

LE IO.FS.SystemTime

Equations

IO.FS.instLESystemTime = leOfOrd

source

structure IO.FS.Metadata :

Type

accessed : IO.FS.SystemTime
modified : IO.FS.SystemTime
byteSize : UInt64
type : IO.FS.FileType

source

instance IO.FS.instReprMetadata :

Repr IO.FS.Metadata

Equations

IO.FS.instReprMetadata = { reprPrec := [anonymous] }

source

@[extern lean_io_read_dir]

constant System.FilePath.readDir :

System.FilePath → IO (Array IO.FS.DirEntry)

source

@[extern lean_io_metadata]

constant System.FilePath.metadata :

System.FilePath → IO IO.FS.Metadata

source

def System.FilePath.isDir (p : System.FilePath) :

BaseIO Bool

Equations

System.FilePath.isDir p = do let a ← EIO.toBaseIO (System.FilePath.metadata p) match a with | Except.ok m => pure (m.type == IO.FS.FileType.dir) | Except.error x => pure false

source

def System.FilePath.pathExists (p : System.FilePath) :

BaseIO Bool

Equations

System.FilePath.pathExists p = do let a ← EIO.toBaseIO (System.FilePath.metadata p) pure (Except.toBool a)

source

def System.FilePath.walkDir (p : System.FilePath) (enter : optParam (System.FilePath → IO Bool) fun x => pure true) :

IO (Array System.FilePath)

Equations

System.FilePath.walkDir p enter = (fun go => Prod.snd <$> StateT.run (go p) #[]) (System.FilePath.walkDir.go enter)

source

partial def System.FilePath.walkDir.go (enter : optParam (System.FilePath → IO Bool) fun x => pure true) (p : System.FilePath) :

StateT (Array System.FilePath) IO Unit

source

def IO.withStdin {m : Type → Type u_1} {α : Type} [inst : Monad m] [inst : MonadFinally m] [inst : MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :

m α

Equations

IO.withStdin h x = do let prev ← liftM (IO.setStdin h) tryFinally x (discard (liftM (IO.setStdin prev)))

source

def IO.withStdout {m : Type → Type u_1} {α : Type} [inst : Monad m] [inst : MonadFinally m] [inst : MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :

m α

Equations

IO.withStdout h x = do let prev ← liftM (IO.setStdout h) tryFinally x (discard (liftM (IO.setStdout prev)))

source

def IO.withStderr {m : Type → Type u_1} {α : Type} [inst : Monad m] [inst : MonadFinally m] [inst : MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :

m α

Equations

IO.withStderr h x = do let prev ← liftM (IO.setStderr h) tryFinally x (discard (liftM (IO.setStderr prev)))

source

def IO.print {α : Type u_1} [inst : ToString α] (s : α) :

IO Unit

Equations

IO.print s = do let out ← liftM IO.getStdout IO.FS.Stream.putStr out (toString s)

source

def IO.println {α : Type u_1} [inst : ToString α] (s : α) :

IO Unit

Equations

IO.println s = IO.print (String.push (toString s) (Char.ofNat 10))

source

def IO.eprint {α : Type u_1} [inst : ToString α] (s : α) :

IO Unit

Equations

IO.eprint s = do let out ← liftM IO.getStderr IO.FS.Stream.putStr out (toString s)

source

def IO.eprintln {α : Type u_1} [inst : ToString α] (s : α) :

IO Unit

Equations

IO.eprintln s = IO.eprint (String.push (toString s) (Char.ofNat 10))

source

def IO.appDir :

IO System.FilePath

Equations

IO.appDir = do let p ← IO.appPath let discr ← pure (System.FilePath.parent p) match discr with | some p => IO.FS.realPath p | x => throw (IO.userError (toString "System.IO.appDir: unexpected filename '" ++ toString p ++ toString "'"))

source

partial def IO.FS.createDirAll (p : System.FilePath) :

IO Unit

source

partial def IO.FS.removeDirAll (p : System.FilePath) :

IO Unit

source

inductive IO.Process.Stdio :

Type

source

noncomputable def IO.Process.Stdio.toHandleType :

IO.Process.Stdio → Type

Equations

IO.Process.Stdio.toHandleType x = match x with | IO.Process.Stdio.piped => IO.FS.Handle | IO.Process.Stdio.inherit => Unit | IO.Process.Stdio.null => Unit

source

structure IO.Process.StdioConfig :

Type

source

structure IO.Process.SpawnArgs extends IO.Process.StdioConfig :

Type

source

structure IO.Process.Child (cfg : IO.Process.StdioConfig) :

Type

stdin : IO.Process.Stdio.toHandleType cfg.stdin
stdout : IO.Process.Stdio.toHandleType cfg.stdout
stderr : IO.Process.Stdio.toHandleType cfg.stderr

source

@[extern lean_io_process_spawn]

constant IO.Process.spawn (args : IO.Process.SpawnArgs) :

IO (IO.Process.Child args.toStdioConfig)

source

@[extern lean_io_process_child_wait]

constant IO.Process.Child.wait {cfg : IO.Process.StdioConfig} :

IO.Process.Child cfg → IO UInt32

source

@[extern lean_io_process_child_take_stdin]

constant IO.Process.Child.takeStdin {cfg : IO.Process.StdioConfig} :

IO.Process.Child cfg → IO (IO.Process.Stdio.toHandleType cfg.stdin × IO.Process.Child { stdin := IO.Process.Stdio.null, stdout := cfg.stdout, stderr := cfg.stderr })

source

structure IO.Process.Output :

Type

exitCode : UInt32
stdout : String
stderr : String

source

def IO.Process.output (args : IO.Process.SpawnArgs) :

IO IO.Process.Output

Equations

IO.Process.output args = do let child ← IO.Process.spawn { toStdioConfig := { stdin := args.toStdioConfig.stdin, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }, cmd := args.cmd, args := args.args, cwd := args.cwd, env := args.env } let stdout ← liftM (IO.asTask (IO.FS.Handle.readToEnd child.stdout) Task.Priority.dedicated) let stderr ← IO.FS.Handle.readToEnd child.stderr let exitCode ← IO.Process.Child.wait child let stdout ← IO.ofExcept stdout.get pure { exitCode := exitCode, stdout := stdout, stderr := stderr }

source

def IO.Process.run (args : IO.Process.SpawnArgs) :

IO String

Equations

IO.Process.run args = do let out ← IO.Process.output args let _do_jp : PUnit → IO String := fun y => pure out.stdout if (out.exitCode != 0) = true then do let y ← throw (IO.userError ("process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode)) _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

@[extern lean_io_exit]

constant IO.Process.exit {α : Type} :

UInt8 → IO α

source

structure IO.AccessRight :

Type

read : Bool
write : Bool
execution : Bool

source

def IO.AccessRight.flags (acc : IO.AccessRight) :

UInt32

Equations

IO.AccessRight.flags acc = let r := if acc.read = true then 4 else 0; let w := if acc.write = true then 2 else 0; let x := if acc.execution = true then 1 else 0; UInt32.lor r (UInt32.lor w x)