@@ -84,6 +84,83 @@ impl LeanPutResponse<LeanOwned> {
8484}
8585```
8686
87+ ### External objects (` LeanExternal<T, R> ` )
88+
89+ External objects let you store arbitrary Rust data inside a Lean object. Lean
90+ sees an opaque type; Rust controls allocation, access, mutation, and cleanup.
91+
92+ ** Register** an external class exactly once, using ` OnceLock ` or ` LazyLock ` :
93+
94+ ``` rust
95+ use std :: sync :: LazyLock ;
96+ use lean_ffi :: object :: {ExternalClass , LeanExternal , LeanOwned , LeanBorrowed };
97+
98+ struct Hasher { state : Vec <u8 > }
99+
100+ // register_with_drop<T> generates a finalizer that calls drop(Box::from_raw(ptr))
101+ // and a no-op foreach (no Lean objects inside T to traverse).
102+ static HASHER_CLASS : LazyLock <ExternalClass > =
103+ LazyLock :: new (ExternalClass :: register_with_drop :: <Hasher >);
104+ ```
105+
106+ ** Create** — ` LeanExternal::alloc ` boxes the value and returns an owned
107+ external object:
108+
109+ ``` rust
110+ // Lean: @[extern "rs_hasher_new"] opaque Hasher.new : Unit → Hasher
111+ #[unsafe (no_mangle)]
112+ extern " C" fn rs_hasher_new (_unit : LeanOwned ) -> LeanExternal <Hasher , LeanOwned > {
113+ LeanExternal :: alloc (& HASHER_CLASS , Hasher { state : Vec :: new () })
114+ }
115+ ```
116+
117+ ** Read** — ` .get() ` borrows the stored ` &T ` . Works on both owned and borrowed
118+ references:
119+
120+ ``` rust
121+ // Lean: @[extern "rs_hasher_bytes"] opaque Hasher.bytes : @& Hasher → ByteArray
122+ #[unsafe (no_mangle)]
123+ extern " C" fn rs_hasher_bytes (
124+ h : LeanExternal <Hasher , LeanBorrowed <'_ >>, // @& → borrowed
125+ ) -> LeanByteArray <LeanOwned > {
126+ LeanByteArray :: from_bytes (& h . get (). state) // &Hasher — no clone, no refcount change
127+ }
128+ ```
129+
130+ ** Update** — ` .get_mut() ` returns ` Option<&mut T> ` , which is ` Some ` when the
131+ object is exclusively owned (` m_rc == 1 ` ). This enables
132+ in-place mutation without allocating a new external object. When shared ` .get_mut() `
133+ returns ` None ` and instead clones into a new object on write.
134+
135+ ``` rust
136+ // Lean: @[extern "rs_hasher_update"] opaque Hasher.update : Hasher → @& ByteArray → Hasher
137+ #[unsafe (no_mangle)]
138+ extern " C" fn rs_hasher_update (
139+ mut h : LeanExternal <Hasher , LeanOwned >,
140+ input : LeanByteArray <LeanBorrowed <'_ >>,
141+ ) -> LeanExternal <Hasher , LeanOwned > {
142+ if let Some (state ) = h . get_mut () {
143+ state . state. extend_from_slice (input . as_bytes ()); // mutate in place
144+ h
145+ } else {
146+ // shared — clone and allocate a new external object
147+ let mut new_state = h . get (). clone ();
148+ new_state . state. extend_from_slice (input . as_bytes ());
149+ LeanExternal :: alloc (& HASHER_CLASS , new_state )
150+ }
151+ }
152+ ```
153+
154+ ** Delete** — follows the same ownership rules as other domain types:
155+
156+ - ` LeanExternal<T, LeanOwned> ` — ` Drop ` calls ` lean_dec ` . When the refcount
157+ reaches zero, Lean calls the class finalizer, which (via ` register_with_drop ` )
158+ runs ` drop(Box::from_raw(ptr)) ` to free the Rust value.
159+ - ` LeanExternal<T, LeanBorrowed<'_>> ` — no refcount changes, no cleanup.
160+ Use for ` @& ` parameters.
161+ - Converting to ` LeanOwned ` (e.g. to store in a ctor field): call ` .into() ` .
162+
163+
87164### FFI function signatures
88165
89166Use domain types in ` extern "C" ` function signatures. The ownership type parameter
@@ -134,6 +211,44 @@ let size = ctor.get_u64(1, 0); // u64 at scalar offset 0 (past 1 non-scalar
134211let flag = ctor . get_bool (1 , 8 ); // bool at scalar offset 8
135212```
136213
214+ ## In-Place Mutation
215+
216+ Lean's runtime supports in-place mutation when an object is ** exclusively owned**
217+ (` m_rc == 1 ` , single-threaded mode). When shared, the object is copied first.
218+ ` LeanRef::is_exclusive() ` exposes this check.
219+
220+ These methods consume ` self ` and return a (possibly new) object, mutating in
221+ place when exclusive or copying first when shared:
222+
223+ ### ` LeanArray `
224+
225+ | Method | C equivalent | Description |
226+ | --------| --------------| -------------|
227+ | ` set(&self, i, val) ` | ` lean_array_set_core ` | Set element (asserts exclusive — use for freshly allocated arrays) |
228+ | ` uset(self, i, val) ` | ` lean_array_uset ` | Set element (copies if shared) |
229+ | ` push(self, val) ` | ` lean_array_push ` | Append an element |
230+ | ` pop(self) ` | ` lean_array_pop ` | Remove the last element |
231+ | ` uswap(self, i, j) ` | ` lean_array_uswap ` | Swap elements at ` i ` and ` j ` |
232+
233+ ### ` LeanByteArray `
234+
235+ | Method | C equivalent | Description |
236+ | --------| --------------| -------------|
237+ | ` set_data(&self, data) ` | ` lean_sarray_cptr ` + memcpy | Bulk write (asserts exclusive — use for freshly allocated arrays) |
238+ | ` uset(self, i, val) ` | ` lean_byte_array_uset ` | Set byte (copies if shared) |
239+ | ` push(self, val) ` | ` lean_byte_array_push ` | Append a byte |
240+ | ` copy(self) ` | ` lean_copy_byte_array ` | Deep copy into a new exclusive array |
241+
242+ ### ` LeanString `
243+
244+ | Method | C equivalent | Description |
245+ | --------| --------------| -------------|
246+ | ` push(self, c) ` | ` lean_string_push ` | Append a UTF-32 character |
247+ | ` append(self, other) ` | ` lean_string_append ` | Concatenate another string (borrowed) |
248+
249+ ` LeanExternal<T> ` also supports in-place mutation via ` get_mut() ` — see the
250+ ** Update** section under [ External objects] ( #external-objects-leanexternalt-r ) .
251+
137252## Notes
138253
139254### Rust panic behavior
@@ -162,10 +277,13 @@ without special handling.
162277### ` lean_string_size ` vs ` lean_string_byte_size `
163278
164279` lean_string_byte_size ` returns the ** total object memory size**
165- (` sizeof(lean_string_object) + m_size ` ), not the string data length.
280+ (` sizeof(lean_string_object) + capacity ` ), not the string data length.
166281Use ` lean_string_size ` instead, which returns ` m_size ` — the number of data
167- bytes including the NUL terminator. The ` LeanString::byte_len() ` wrapper handles
168- this correctly by returning ` lean_string_size(obj) - 1 ` .
282+ bytes including the NUL terminator. ` LeanString ` wraps these correctly:
283+
284+ - ` byte_len() ` — data bytes excluding NUL (` m_size - 1 ` )
285+ - ` length() ` — UTF-8 character count (` m_length ` )
286+ - ` as_str() ` — view as ` &str `
169287
170288## License
171289
0 commit comments