Like https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld.
Makes sure we never reorder IO
operations.
TODO: mark opaque
Equations
Instances For
Equations
- instMonadEIO = inferInstanceAs (Monad (EStateM ε IO.RealWorld))
Equations
- instMonadFinallyEIO = inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld))
Equations
- instMonadExceptOfEIO = inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld))
Equations
- instInhabitedEIO = inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
Equations
Equations
Equations
- BaseIO.toEIO act s = match act s with | EStateM.Result.ok a s => EStateM.Result.ok a s
Instances For
Equations
- EIO.toBaseIO act s = match act s with | EStateM.Result.ok a s => EStateM.Result.ok (Except.ok a) s | EStateM.Result.error ex s => EStateM.Result.ok (Except.error ex) s
Instances For
Equations
- EIO.catchExceptions act h s = match act s with | EStateM.Result.ok a s => EStateM.Result.ok a s | EStateM.Result.error ex s => h ex s
Instances For
Equations
- unsafeBaseIO fn = match EStateM.run fn () with | EStateM.Result.ok a a_1 => a
Instances For
Programs can execute IO actions during initialization that occurs before
the main
function is executed. The attribute [init
specifies
which IO action is executed to set the value of an opaque constant.
The action initializing
returns true
iff it is invoked during initialization.
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.
See BaseIO.asTask
.
See BaseIO.asTask
.
Equations
- BaseIO.mapTasks f tasks prio = BaseIO.mapTasks.go f prio tasks []
Instances For
Equations
- BaseIO.mapTasks.go f prio (t :: ts) x = BaseIO.bindTask t (fun a => BaseIO.mapTasks.go f prio ts (a :: x)) prio
- BaseIO.mapTasks.go f prio [] x = BaseIO.asTask (f (List.reverse x)) prio
Instances For
EIO
specialization of BaseIO.asTask
.
Equations
- EIO.asTask act prio = BaseIO.asTask (EIO.toBaseIO act) prio
Instances For
EIO
specialization of BaseIO.mapTask
.
Equations
- EIO.mapTask f t prio = BaseIO.mapTask (fun a => EIO.toBaseIO (f a)) t prio
Instances For
EIO
specialization of BaseIO.bindTask
.
Equations
- EIO.bindTask t f prio = BaseIO.bindTask t (fun a => EIO.catchExceptions (f a) fun e => pure { get := Except.error e }) prio
Instances For
EIO
specialization of BaseIO.mapTasks
.
Equations
- EIO.mapTasks f tasks prio = BaseIO.mapTasks (fun as => EIO.toBaseIO (f as)) tasks prio
Instances For
Equations
- IO.ofExcept e = match e with | Except.ok a => pure a | Except.error e => throw (IO.userError (toString e))
Instances For
Equations
- IO.lazyPure fn = pure (fn ())
Instances For
Monotonically increasing time since an unspecified past point in milliseconds. No relation to wall clock time.
Monotonically increasing time since an unspecified past point in nanoseconds. No relation to wall clock time.
Read bytes from a system entropy source. Not guaranteed to be cryptographically secure.
If nBytes = 0
, return immediately with an empty buffer.
IO
specialization of EIO.asTask
.
Equations
- IO.asTask act prio = EIO.asTask act prio
Instances For
IO
specialization of EIO.mapTask
.
Equations
- IO.mapTask f t prio = EIO.mapTask f t prio
Instances For
IO
specialization of EIO.bindTask
.
Equations
- IO.bindTask t f prio = EIO.bindTask t f prio
Instances For
IO
specialization of EIO.mapTasks
.
Equations
- IO.mapTasks f tasks prio = EIO.mapTasks f tasks prio
Instances For
Check if the task's cancellation flag has been set by calling IO.cancel
or dropping the last reference to the task.
Wait until any of the tasks in the given list has finished, then return its result.
Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread.
- read: IO.FS.Mode
- write: IO.FS.Mode
- readWrite: IO.FS.Mode
- append: IO.FS.Mode
Instances For
Read up to the given number of bytes from the stream. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.
Read text up to (including) the next line break from the stream. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.
A pure-Lean abstraction of POSIX streams. We use Stream
s for the standard streams stdin/stdout/stderr so we can
capture output of #eval
commands into memory.
Instances For
Equations
- IO.FS.instInhabitedStream = { default := { flush := default, read := default, write := default, getLine := default, putStr := default } }
Replaces the stdin stream of the current thread and returns its previous value.
Replaces the stdout stream of the current thread and returns its previous value.
Replaces the stderr stream of the current thread and returns its previous value.
Read up to the given number of bytes from the handle. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.
Read text up to (including) the next line break from the handle. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.
Remove given directory. Fails if not empty; see also IO.FS.removeDirAll
.
Equations
- IO.FS.withFile fn mode f = IO.FS.Handle.mk fn mode >>= f
Instances For
Equations
- IO.FS.Handle.putStrLn h s = IO.FS.Handle.putStr h (String.push s (Char.ofNat 10))
Instances For
Instances For
Equations
- IO.FS.Handle.readToEnd h = IO.FS.Handle.readToEnd.loop h ""
Instances For
Equations
- IO.FS.readBinFile fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read IO.FS.Handle.readBinToEnd h
Instances For
Equations
- IO.FS.readFile fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read IO.FS.Handle.readToEnd h
Instances For
Equations
- IO.FS.lines fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read IO.FS.lines.read h #[]
Instances For
Equations
- IO.FS.writeBinFile fname content = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.write IO.FS.Handle.write h content
Instances For
Equations
- IO.FS.writeFile fname content = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.write IO.FS.Handle.putStr h content
Instances For
Equations
- IO.FS.Stream.putStrLn strm s = IO.FS.Stream.putStr strm (String.push s (Char.ofNat 10))
Instances For
Equations
- IO.FS.instReprDirEntry = { reprPrec := IO.FS.reprDirEntry✝ }
Equations
- IO.FS.DirEntry.path entry = entry.root / { toString := entry.fileName }
Instances For
- dir: IO.FS.FileType
- file: IO.FS.FileType
- symlink: IO.FS.FileType
- other: IO.FS.FileType
Instances For
Equations
- IO.FS.instReprFileType = { reprPrec := IO.FS.reprFileType✝ }
Equations
- IO.FS.instBEqFileType = { beq := IO.FS.beqFileType✝ }
Equations
- IO.FS.instReprSystemTime = { reprPrec := IO.FS.reprSystemTime✝ }
Equations
- IO.FS.instBEqSystemTime = { beq := IO.FS.beqSystemTime✝ }
Equations
- IO.FS.instOrdSystemTime = { compare := IO.FS.ordSystemTime✝ }
Equations
- IO.FS.instInhabitedSystemTime = { default := { sec := default, nsec := default } }
- accessed : IO.FS.SystemTime
- modified : IO.FS.SystemTime
- byteSize : UInt64
- type : IO.FS.FileType
Instances For
Equations
- IO.FS.instReprMetadata = { reprPrec := IO.FS.reprMetadata✝ }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- System.FilePath.pathExists p = do let __do_lift ← EIO.toBaseIO (System.FilePath.metadata p) pure (Except.toBool __do_lift)
Instances For
Return all filesystem entries of a preorder traversal of all directories satisfying enter
, starting at p
.
Symbolic links are visited as well by default.
Equations
- System.FilePath.walkDir p enter = Prod.snd <$> StateT.run (System.FilePath.walkDir.go enter p) #[]
Instances For
Equations
- IO.withStdin h x = do let prev ← liftM (IO.setStdin h) tryFinally x (discard (liftM (IO.setStdin prev)))
Instances For
Equations
- IO.withStdout h x = do let prev ← liftM (IO.setStdout h) tryFinally x (discard (liftM (IO.setStdout prev)))
Instances For
Equations
- IO.withStderr h x = do let prev ← liftM (IO.setStderr h) tryFinally x (discard (liftM (IO.setStderr prev)))
Instances For
Equations
- IO.println s = IO.print (String.push (toString s) (Char.ofNat 10))
Instances For
Equations
- IO.eprintln s = IO.eprint (String.push (toString s) (Char.ofNat 10))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Create given path and all missing parents as directories.
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.
- piped: IO.Process.Stdio
- inherit: IO.Process.Stdio
- null: IO.Process.Stdio
Instances For
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
Instances For
Configuration for the process' stdin handle.
stdin : IO.Process.StdioConfiguration for the process' stdout handle.
stdout : IO.Process.StdioConfiguration for the process' stderr handle.
stderr : IO.Process.Stdio
Instances For
Command name.
cmd : StringArguments for the process
Working directory for the process. Inherit from current process if
none
.cwd : Option System.FilePathAdd or remove environment variables for the process.
Instances For
- stdin : IO.Process.Stdio.toHandleType cfg.stdin
- stdout : IO.Process.Stdio.toHandleType cfg.stdout
- stderr : IO.Process.Stdio.toHandleType cfg.stderr
Instances For
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.
Run process to completion and capture output.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Run process to completion and return stdout on success.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
- user : IO.AccessRight
- group : IO.AccessRight
- other : IO.AccessRight
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- IO.setAccessRights filename mode = IO.Prim.setAccessRights filename (IO.FileRight.flags mode)
Instances For
Equations
- IO.instMonadLiftSTRealWorldBaseIO = { monadLift := fun {α} => id }
Equations
- IO.FS.Stream.ofHandle 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 }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Run action with stdin
emptied and stdout+stderr
captured into a String
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.instEval = { eval := fun a x => IO.println (toString (a ())) }
Equations
- Lean.instEval_1 = { eval := fun a x => IO.println (repr (a ())) }
Equations
- Lean.instEvalUnit = { eval := fun u hideUnit => if hideUnit = true then pure () else IO.println (repr (u ())) }
Equations
- Lean.instEvalIO = { eval := fun x x_1 => do let a ← x () Lean.Eval.eval (fun x => a) true }
Equations
- One or more equations did not get rendered due to their size.