Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125/// Standard library: `ByteBuf` -- a flat byte buffer the C FFI can/// address (`SSL_read`/`SSL_write` in motes/tls take a `void*` plus a/// length; nothing else in `std/` exposes one).////// A `ByteBuf` records its length: `length` is the byte count it was/// created with (or later `truncate`d to), and `to_list`'s `len` is/// clamped to that, so an over-large `len` cannot read past the/// allocation. `truncate` a buffer to `SSL_read`'s return to keep only/// what actually came back. Values are opaque like `FdStream`/// (std/stream.mo): never pattern-match, compare or print one.////// Compiled, a `ByteBuf` is the heap kind `plans/bootstrapping//// mlir-codegen.md`'s `Buf E` generalises ("a fourth heap kind"): a/// block carrying its element kind (u8), its length, and a/// 64-byte-aligned atomic payload. `ByteBuf` is that kind's u8 case, so/// the buffer an FFI function sees is already the memory a kernel/// `memref` would. `free` is a deliberate no-op there -- Boehm reclaims a/// forgotten buffer, and a real free on a word another live value holds/// would be a use-after-free.////// The two backends hold different words and values never cross between/// them. Interpreted, it is a registry id (the `Fiber`/`Scope` handle/// convention, core_native.rs) whose length is its `Vec`'s, and `free`/// really drops it. `ptr` hands out the raw address and so exists only/// compiled -- under the interpreter forcing it fails `unknown native:/// bytebuf_ptr`.
pub type ByteBuf { bytebuf}
#[native "bytebuf_alloc"]priv def bytebuf_alloc_raw (n : I64) : RawIO ByteBuf
/// Allocate `n` zeroed bytes.pub def ByteBuf.alloc (n : I64) : IO ByteBuf := IO.mk (bytebuf_alloc_raw n)
/// The raw address of the payload, for FFI functions that write into or/// read out of it. Compiled backend only (see the module doc).#[native "bytebuf_ptr"]pub def ByteBuf.ptr (b : ByteBuf) : Ptr
/// Read the pointer-sized word at the start of the buffer, for a C/// function that returns a handle through an out-parameter. The buffer/// must hold at least 8 bytes; a shorter one yields the NULL word instead/// of reading past its payload. Compiled backend only, like `ptr`: the/// interpreter has no raw addresses.////// This is the typed alternative to a general `load(ptr)` helper. The/// argument is a `ByteBuf`, so no arbitrary address can be supplied, and/// the runtime checks the buffer's kind and length.#[native "bytebuf_take_ptr"]pub def ByteBuf.take_ptr (b : ByteBuf) : Ptr
/// How many bytes the buffer holds: its creation size, or what/// `truncate` cut it to.#[native "bytebuf_len"]pub def ByteBuf.length (b : ByteBuf) : I64
#[native "bytebuf_of_list"]priv def bytebuf_of_list_raw (xs : List U8) : RawIO ByteBuf
/// Copy `xs` into a fresh buffer.pub def ByteBuf.of_list (xs : List U8) : IO ByteBuf := IO.mk (bytebuf_of_list_raw xs)
#[native "bytebuf_to_list"]priv def bytebuf_to_list_raw (b : ByteBuf) (len : I64) : RawIO (List U8)
/// The first `len` bytes of the buffer as a list, clamped to the buffer's/// own length.pub def ByteBuf.to_list (b : ByteBuf) (len : I64) : IO (List U8) := IO.mk (bytebuf_to_list_raw b len)
#[native "bytebuf_free"]priv def bytebuf_free_raw (b : ByteBuf) : RawIO Unit
/// Release the buffer (a no-op under the compiled GC backend).pub def ByteBuf.free (b : ByteBuf) : IO Unit := IO.mk (bytebuf_free_raw b)
/// The first `len` bytes of the buffer as a `String`, clamped to the/// buffer's own length exactly as `to_list` is -- one copy, where/// `String.from_list (ByteBuf.to_list ...)` would build and walk a cons/// cell per byte. Bytes that are not valid UTF-8 come back lossily/// (U+FFFD) under the interpreter, whose `String` must be UTF-8; the/// compiled backend copies them verbatim.pub def ByteBuf.to_string (b : ByteBuf) (len : I64) : IO String := IO.mk (bytebuf_to_string b len)
/// Copy `s`'s bytes into a fresh buffer -- `of_list`'s shape, from text.pub def ByteBuf.of_string (s : String) : IO ByteBuf := IO.mk (bytebuf_of_string s)
/// Shrink the recorded length to `n`, keeping the first `n` bytes; `n`/// is clamped to `[0, length]`, so this never grows a buffer. The/// allocation itself is unchanged -- the bytes past `n` just stop/// being part of it.pub def ByteBuf.truncate (b : ByteBuf) (n : I64) : IO Unit := IO.mk (bytebuf_truncate b n)
/// Copy all of `src` into `dst` starting at byte `offset` -- one memmove./// Clamped to `dst`'s length, so this never grows `dst`; an offset/// outside `[0, length dst]` copies nothing. Gathering chunks into one/// buffer this way is how `IO.read_file` decodes a file ONCE rather than/// chunk by chunk (a character split across two chunks would otherwise/// decode as U+FFFD under the interpreter).////// Consumes and returns `dst` (view-types P2's shape, applied to the/// mutable buffer): the caller threads the returned handle on rather/// than mentioning the input twice.pub def ByteBuf.copy_into (dst : ByteBuf) (offset : I64) (src : ByteBuf) : IO ByteBuf := IO.mk (bytebuf_copy_into dst offset src)
#[native "bytebuf_to_string"]priv def bytebuf_to_string (b : ByteBuf) (len : I64) : RawIO String
#[native "bytebuf_of_string"]priv def bytebuf_of_string (s : String) : RawIO ByteBuf
#[native "bytebuf_truncate"]priv def bytebuf_truncate (b : ByteBuf) (n : I64) : RawIO Unit
#[native "bytebuf_copy_into"]priv def bytebuf_copy_into (dst : ByteBuf) (offset : I64) (src : ByteBuf) : RawIO ByteBuf