Init.System.IO

Run act in a separate Task. This is similar to Haskell's unsafeInterleaveIO, except that the Task is started eagerly as usual. Thus pure accesses to the Task do not influence the impure act computation. Unlike with pure tasks created by Task.spawn, tasks created by this function will be run even if the last reference to the task is dropped. The act should manually check for cancellation via IO.checkCanceled if it wants to react to that.

source

@[extern lean_io_map_task]

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

BaseIO (Task β)

See BaseIO.asTask.

source

@[extern lean_io_bind_task]

constant BaseIO.bindTask {α : Type u_1} {β : Type} (t : Task α) (f : α → BaseIO (Task β)) (prio : optParam Task.Priority Task.Priority.default) :

BaseIO (Task β)

See BaseIO.asTask.

source

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

BaseIO (Task β)

Equations

BaseIO.mapTasks f tasks prio = BaseIO.mapTasks.go f prio tasks []

source

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

List (Task α) → List α → BaseIO (Task β)

Equations

BaseIO.mapTasks.go f prio (t :: ts) _fun_discr = BaseIO.bindTask t (fun a => BaseIO.mapTasks.go f prio ts (a :: _fun_discr)) prio
BaseIO.mapTasks.go f prio [] _fun_discr = BaseIO.asTask (f (List.reverse _fun_discr)) prio

source

@[inline]

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

BaseIO (Task (Except ε α))

Equations

EIO.asTask act prio = BaseIO.asTask (EIO.toBaseIO act) prio

EIO specialization of BaseIO.asTask.

source

@[inline]

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

BaseIO (Task (Except ε β))

Equations

EIO.mapTask f t prio = BaseIO.mapTask (fun a => EIO.toBaseIO (f a)) t prio

EIO specialization of BaseIO.mapTask.

source

@[inline]

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

EIO specialization of BaseIO.bindTask.

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

EIO specialization of BaseIO.mapTasks.

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

Monotonically increasing time since an unspecified past point in milliseconds. No relation to wall clock time.

source

@[extern lean_io_mono_nanos_now]

constant IO.monoNanosNow :

BaseIO Nat

Monotonically increasing time since an unspecified past point in nanoseconds. No relation to wall clock time.

source

@[extern lean_io_get_random_bytes]

constant IO.getRandomBytes (nBytes : USize) :

IO ByteArray

Read bytes from a system entropy source. Not guaranteed to be cryptographically secure. If nBytes=0, return immediately with an empty buffer.

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

IO specialization of EIO.asTask.

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

IO specialization of EIO.mapTask.

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

IO specialization of EIO.bindTask.

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

IO specialization of EIO.mapTasks.

source

@[extern lean_io_check_canceled]

constant IO.checkCanceled :

BaseIO Bool

Check if the task's cancellation flag has been set by calling IO.cancel or dropping the last reference to the task.

source

@[extern lean_io_cancel]

constant IO.cancel {α : Type u_1} :

Task α → BaseIO Unit

Request cooperative cancellation of the task. The task must explicitly call IO.checkCanceled to react to the cancellation.

source

@[extern lean_io_has_finished]

constant IO.hasFinished {α : Type u_1} :

Task α → BaseIO Bool

Check if the task has finished execution, at which point calling Task.get will return immediately.

source

@[extern lean_io_wait]

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

BaseIO α

Wait for the task to finish, then return its result.

source

@[extern lean_io_wait_any]

constant IO.waitAny {α : Type} :

List (Task α) → IO α

Wait until any of the tasks in the given list has finished, then return its result.

source

@[extern lean_io_get_num_heartbeats]

constant IO.getNumHeartbeats :

BaseIO Nat

Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread.

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

A pure-Lean abstraction of POSIX streams. We use Streams for the standard streams stdin/stdout/stderr so we can capture output of #eval commands into memory.

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

Replaces the stdin stream of the current thread and returns its previous value.

source

@[extern lean_get_set_stdout]

constant IO.setStdout :

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

Replaces the stdout stream of the current thread and returns its previous value.

source

@[extern lean_get_set_stderr]

constant IO.setStderr :

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

Replaces the stderr stream of the current thread and returns its previous value.

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

Returns whether the end of the file has been reached while reading a file. h.isEof returns true /after/ the first attempt at reading past the end of h. Once h.isEof is true, reading h will always return an empty array.

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

Remove given directory. Fails if not empty; see also IO.FS.removeDirAll.

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 = IO.FS.Handle.readBinToEnd.loop h ByteArray.empty

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 = 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 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.instReprSystemTime :

Repr IO.FS.SystemTime

Equations

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

source

instance IO.FS.instBEqSystemTime :

BEq IO.FS.SystemTime

Equations

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

source

instance IO.FS.instOrdSystemTime :

Ord IO.FS.SystemTime

Equations

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

source

instance IO.FS.instInhabitedSystemTime :

Inhabited IO.FS.SystemTime

Equations

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

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 a => 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 = Prod.snd <$> StateT.run (System.FilePath.walkDir.go enter p) #[]

Return all filesystem entries of a preorder traversal of all directories satisfying enter, starting at p. Symbolic links are visited as well by default.

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

Create given path and all missing parents as directories.

source

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

IO Unit

Fully remove given directory by deleting all contained files and directories in an unspecified order. Fails if any contained entry cannot be deleted or was newly created during execution.

source

inductive IO.Process.Stdio :

Type

source

noncomputable def IO.Process.Stdio.toHandleType :

IO.Process.Stdio → Type

Equations

IO.Process.Stdio.toHandleType _fun_discr = match _fun_discr 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 })

Extract the stdin field from a Child object, allowing them to be freed independently. This operation is necessary for closing the child process' stdin while still holding on to a process handle, e.g. for Child.wait. A file handle is closed when all references to it are dropped, which without this operation includes the Child object.

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 }

Run process to completion and capture output.

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

Run process to completion and return stdout on success.

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)

source

structure IO.FileRight :

Type

source

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

UInt32

Equations

IO.FileRight.flags acc = let u := UInt32.shiftLeft (IO.AccessRight.flags acc.user) 6; let g := UInt32.shiftLeft (IO.AccessRight.flags acc.group) 3; let o := IO.AccessRight.flags acc.other; UInt32.lor u (UInt32.lor g o)

source

@[extern lean_chmod]

constant IO.Prim.setAccessRights (filename : System.FilePath) (mode : UInt32) :

IO Unit

source

def IO.setAccessRights (filename : System.FilePath) (mode : IO.FileRight) :

IO Unit

Equations

IO.setAccessRights filename mode = IO.Prim.setAccessRights filename (IO.FileRight.flags mode)

source

@[inline]

abbrev IO.Ref (α : Type) :

Type

Equations

IO.Ref α = ST.Ref IO.RealWorld α

source

instance IO.instMonadLiftSTRealWorldBaseIO :

MonadLift (ST IO.RealWorld) BaseIO

Equations

IO.instMonadLiftSTRealWorldBaseIO = { monadLift := fun {α} => id }

source

def IO.mkRef {α : Type} (a : α) :

BaseIO (IO.Ref α)

Equations

IO.mkRef a = ST.mkRef a

source

def IO.FS.Stream.ofHandle (h : IO.FS.Handle) :

IO.FS.Stream

Equations

IO.FS.Stream.ofHandle h = { isEof := liftM (IO.FS.Handle.isEof h), flush := IO.FS.Handle.flush h, read := IO.FS.Handle.read h, write := IO.FS.Handle.write h, getLine := IO.FS.Handle.getLine h, putStr := IO.FS.Handle.putStr h }

source

structure IO.FS.Stream.Buffer :

Type

data : ByteArray
pos : Nat

source

def IO.FS.Stream.ofBuffer (r : IO.Ref IO.FS.Stream.Buffer) :

IO.FS.Stream

Equations

IO.FS.Stream.ofBuffer r = { isEof := do let b ← ST.Ref.get r pure (decide (b.pos ≥ ByteArray.size b.data)), flush := pure (), read := fun n => ST.Ref.modifyGet r fun b => let data := ByteArray.extract b.data b.pos (b.pos + USize.toNat n); (data, { data := b.data, pos := b.pos + ByteArray.size data }), write := fun data => ST.Ref.modify r fun b => { data := ByteArray.copySlice data 0 b.data b.pos (ByteArray.size data) false, pos := b.pos + ByteArray.size data }, getLine := ST.Ref.modifyGet r fun b => let pos := match ByteArray.findIdx? b.data (fun u => u == 0 || decide (u = Nat.toUInt8 (Char.toNat (Char.ofNat 10)))) b.pos with | some pos => if (ByteArray.get! b.data pos == 0) = true then pos else pos + 1 | none => ByteArray.size b.data; (String.fromUTF8Unchecked (ByteArray.extract b.data b.pos pos), { data := b.data, pos := pos }), putStr := fun s => ST.Ref.modify r fun b => let data := String.toUTF8 s; { data := ByteArray.copySlice data 0 b.data b.pos (ByteArray.size data) false, pos := b.pos + ByteArray.size data } }

source

def IO.FS.withIsolatedStreams {m : Type → Type u_1} {α : Type} [inst : Monad m] [inst : MonadFinally m] [inst : MonadLiftT BaseIO m] (x : m α) (isolateStderr : optParam Bool true) :

m (String × α)

Equations