Work with a lean structure type in rust

LeanFfiExperiment/Basic.lean

@@ -35,6 +35,9 @@ instance : ToString AST where
   toString (input: AST) : String :=
   s!"\{ name: {input.name}, count: {input.count} }"
 
+@[export myastfunction]
+def myAST (input: UInt32) : AST :=
+  { name := "Test AST", count := input.toNat }
 
 def parseCFile (input: String): AST :=
   {

lean-ffi-experiment-rust/src/main.rs

@@ -140,6 +140,50 @@ unsafe fn lean_string_to_str<'a>(obj: *mut LeanObject) -> &'a str {
     std::str::from_utf8(bytes).expect("Lean strings are valid UTF-8")
 }
 
+// A Lean `structure` with more than one field (and not itself wrapped in
+// `class`/single-field newtype optimizations) compiles down to a
+// `lean_ctor_object`: a `lean_object` header followed by one `lean_object *`
+// per field, in declaration order. `m_other` (see `LeanObjectHeader`) holds
+// the field count. This layout is documented directly in lean.h:
+//   lean_object   m_header;
+//   lean_object * m_objs[];
+#[repr(C)]
+struct LeanCtorObject {
+    header: LeanObjectHeader,
+}
+
+/// Mirrors `lean_ctor_get` from lean.h (`static inline`, not linkable):
+/// reads field `i` out of a constructor object as a borrowed `lean_object *`.
+unsafe fn lean_ctor_get(obj: *mut LeanObject, i: usize) -> *mut LeanObject {
+    let objs = unsafe { (obj as *const u8).add(std::mem::size_of::<LeanCtorObject>()) }
+        as *const *mut LeanObject;
+    unsafe { *objs.add(i) }
+}
+
+/// Reads the two fields (`name : String`, `count : Nat`) out of an owned
+/// `lean_object *` known to represent Lean's `AST` structure and prints them
+/// individually, having decomposed the constructor object ourselves rather
+/// than asking Lean for its `ToString` rendering.
+unsafe fn describe_lean_ast(obj: *mut LeanObject) {
+    let tag = unsafe { (*(obj as *const LeanObjectHeader)).m_tag };
+    let num_fields = unsafe { (*(obj as *const LeanObjectHeader)).m_other };
+    assert_eq!(
+        tag, 0,
+        "AST has a single constructor, expected tag 0, got {tag}"
+    );
+    assert_eq!(
+        num_fields, 2,
+        "expected AST's 2 fields (name, count), got {num_fields}"
+    );
+
+    let name_obj = unsafe { lean_ctor_get(obj, 0) };
+    let count_obj = unsafe { lean_ctor_get(obj, 1) };
+
+    let name = unsafe { lean_string_to_str(name_obj) };
+    println!(".name: {name:?}");
+    unsafe { describe_lean_nat(".count", count_obj) };
+}
+
 #[allow(dead_code)]
 unsafe extern "C" {
     fn mycustomintfunction(x: u32) -> u32;
@@ -162,6 +206,10 @@ unsafe extern "C" {
     // `lean_string_to_str`.
     fn mycustomstringfunction(x: u32) -> *mut LeanObject;
 
+    // Returns an owned `lean_object *` representing an `AST` (a 2-field
+    // `structure`) - see `describe_lean_ast`.
+    fn myastfunction(x: u32) -> *mut LeanObject;
+
     // Initializers - names from objdump
     #[link_name = "initialize_lean_x2dffi_x2dexperiment_LeanFfiExperiment"]
     fn initialize_LeanFfiExperiment(builtin: u8) -> *mut LeanObject;
@@ -221,6 +269,11 @@ fn main() {
     println!("\nCalling `myCustomStringFunction : UInt32 -> String` with input {string_input}:");
     println!("  result: {text:?}");
 
+    let ast_input: u32 = 7;
+    let ast = unsafe { myastfunction(ast_input) };
+    println!("\nCalling `myAST : UInt32 -> AST` with input {ast_input}:");
+    unsafe { describe_lean_ast(ast) };
+
     /* this segfaults because mycustomint is a zero-argument Lean function
      * that gets placed into the .bss section of the shared library
      */