From e9ab375c9ac9c94b3f9d74d10b1f39077cb29de3 Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Mon, 8 Apr 2024 20:50:30 +0200 Subject: [PATCH] doc: `lean.h` --- src/include/lean/lean.h | 104 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 104 insertions(+) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 7bd035b57940..bb47874f0637 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -451,6 +451,19 @@ static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ /* Just free memory */ LEAN_EXPORT void lean_dealloc(lean_object * o); +/* +An object `o` satisfies `lean_is_ctor` if it is a member of an inductive type, barring the exceptions +listed at https://lean-lang.org/lean4/doc/dev/ffi.html?highlight=ffi#translating-types-from-lean-to-c. +A notable example of an exception are inductive types where all constructors have no parameters (enumeration types). +A notable example of types which *do* satisfy `lean_is_ctor` are structure types which are represented +as inductive types with a single constructor (whose parameters are the structure's fields). + +Accessing the fields of such an object `o` works differently depending on the type of the field. +For fields whose values are represented by `lean_object*` (for example, strings, arrays or other types +satisfying `lean_is_ctor`), use `lean_ctor_get`. For fields containing values represented by scalars +(for example, booleans, enumeration types, integer types or floating point types), use the family of +`lean_ctor_get_...` functions. +*/ static inline bool lean_is_ctor(lean_object * o) { return lean_ptr_tag(o) <= LeanMaxCtorTag; } static inline bool lean_is_closure(lean_object * o) { return lean_ptr_tag(o) == LeanClosure; } static inline bool lean_is_array(lean_object * o) { return lean_ptr_tag(o) == LeanArray; } @@ -521,6 +534,23 @@ static inline void lean_set_non_heap_header_for_big(lean_object * o, unsigned ta /* Constructor objects */ +/* +Returns the number of non-scalar parameters of a given ctor-object. + +For example, let `o` be a value of the following structure in Lean: + +``` +structure S where + a : String + b : String + c : Bool + d : UInt64 + e : Array Nat +``` + +Then `lean_ctor_num_objs(o) == 3`, as `a`, `b` and `e` are the non-scalar +parameters of the constructor (`S.mk`) used to construct `o`. +*/ static inline unsigned lean_ctor_num_objs(lean_object * o) { assert(lean_is_ctor(o)); return lean_ptr_other(o); @@ -543,6 +573,29 @@ static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, uns return o; } +/* +Returns the `i`th non-scalar parameter of a given ctor-object. Notably, +the index `i` does not index the entire list of parameters of a given +constructor, but rather only the non-scalar ones. + +For example, let `o` be a value of the following structure in Lean: + +``` +structure S where + a : String + b : String + c : Bool + d : UInt64 + e : Array Nat +``` + +Then +* `lean_ctor_get(o, 0)` returns the object representing `a` +* `lean_ctor_get(o, 1)` returns the object representing `b` +* `lean_ctor_get(o, 2)` returns the object representing `e` + +To get the number of non-scalar parameters use `lean_ctor_num_objs`. +*/ static inline b_lean_obj_res lean_ctor_get(b_lean_obj_arg o, unsigned i) { assert(i < lean_ctor_num_objs(o)); return lean_ctor_obj_cptr(o)[i]; @@ -570,26 +623,77 @@ static inline size_t lean_ctor_get_usize(b_lean_obj_arg o, unsigned i) { return *((size_t*)(lean_ctor_obj_cptr(o) + i)); } +/* +Given a ctor-object, returns a scalar parameter of type `uint8_t` at a given offset. + +The offset does *not* represent an index into the list of parameters of an inductive +type constructor, but is instead only a byte offset. To access a specific constructor +parameter, construct the correct byte offset as follows. + +All scalar parameters of a ctor-object are represented in a contiguous block following +the non-scalar parameters. Thus, the base offset required to access a scalar parameter +of a ctor-object `o` is `lean_ctor_num_objs(o) * sizeof(void*)` (cf. the documentation +for `lean_ctor_num_objs` for more details). Then, to locate the desired scalar parameter, +add the sizes of all scalar parameters preceeding the target parameter. For example, +let `o` be a value of the following structure in Lean: + +``` +structure S where + a : String + b : Bool + c : UInt64 + e : Array Nat + d : UInt8 +``` + +Then +* the base offset is `base_offset := 3 * sizeof(void*)`. +* as `b` is the first scalar parameter, its offset is exactly the `base_offset`. +* the offset for `c` is `base_offset + sizeof(uint8_t)`, where `sizeof(uint8_t)` + is the number of bytes used by the preceeding parameter `b`. +* the offset for `d` is `base_offset + sizeof(uint8_t) + sizeof(uint64_t)` where + `sizeof(uint8_t) + sizeof(uint64_t)` are the number of bytes used by the preceeding + parameters `b` and `c`. + +Thus, `lean_ctor_get_uint8(o, 3 * sizeof(void*) + sizeof(uint8_t) + sizeof(uint64_t))` +returns the value of `d`. +*/ static inline uint8_t lean_ctor_get_uint8(b_lean_obj_arg o, unsigned offset) { assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); return *((uint8_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); } +/* +Given a ctor-object, returns a scalar parameter of type `uint16_t` at a given offset. +For an explanation of the offset, cf. the documentation for `lean_ctor_get_uint8`. +*/ static inline uint16_t lean_ctor_get_uint16(b_lean_obj_arg o, unsigned offset) { assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); return *((uint16_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); } +/* +Given a ctor-object, returns a scalar parameter of type `uint32_t` at a given offset. +For an explanation of the offset, cf. the documentation for `lean_ctor_get_uint8`. +*/ static inline uint32_t lean_ctor_get_uint32(b_lean_obj_arg o, unsigned offset) { assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); return *((uint32_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); } +/* +Given a ctor-object, returns a scalar parameter of type `uint64_t` at a given offset. +For an explanation of the offset, cf. the documentation for `lean_ctor_get_uint8`. +*/ static inline uint64_t lean_ctor_get_uint64(b_lean_obj_arg o, unsigned offset) { assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); return *((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); } +/* +Given a ctor-object, returns a scalar parameter of type `float` at a given offset. +For an explanation of the offset, cf. the documentation for `lean_ctor_get_uint8`. +*/ static inline double lean_ctor_get_float(b_lean_obj_arg o, unsigned offset) { assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); return *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));