Merge branch 'data-structures'

Callee/Callee.lean

@@ -1,3 +1,19 @@
 @[export my_function]
 def my_function (s: String): String :=
-  s ++ s!"abc"
+  s ++ s!" at callee"
+
+  -- Formats a string in 3 different forms
+@[export stylize]
+def stylize (s: String): (String × String × String) :=
+  (s.capitalize, s.decapitalize, s.toUpper)
+
+inductive Think where
+  | Success (s: String)
+  | Failure (i: Nat)
+
+@[export think]
+def think (s: String): Think :=
+  if s.front == 'S' then
+    Think.Success (s.drop 1)
+  else
+    Think.Failure s.length

src/main.rs

@@ -21,9 +21,12 @@ mod callee {
 		#[link_name = "initialize_Callee"]
 		pub fn initialize(builtin: u8, world: lean_obj_arg) -> lean_obj_res;
 		pub fn my_function(s: lean_obj_arg) -> lean_obj_res;
+		pub fn stylize(s: lean_obj_arg) -> lean_obj_res;
+		pub fn think(s: lean_obj_arg) -> lean_obj_res;
 	}
 }
-fn main() {
+
+fn initialize() {
 	unsafe {
 		lean::lean_initialize_runtime_module();
 		lean::lean_initialize();
@@ -38,9 +41,10 @@ fn main() {
 		}
 		lean::lean_io_mark_end_initialization();
 	}
-	println!("Lean initialization complete!");
+}
 
-	let c_str = std::ffi::CString::new("hello ").unwrap();
+fn call_my_function() {
+	let c_str = std::ffi::CString::new("hello").unwrap();
 	let result = unsafe {
 		let native_str = lean::lean_mk_string(c_str.as_ptr());
 		let result_obj = callee::my_function(native_str);
@@ -50,6 +54,77 @@ fn main() {
 		lean::lean_dec(result_obj);
 		str
 	};
-
-	println!("result: {result}");
+	assert_eq!(result, "hello at callee");
+}
+
+fn unbox_lean_string(str: lean::b_lean_obj_arg) -> String {
+	unsafe { std::ffi::CStr::from_ptr(lean::lean_string_cstr(str)) }
+		.to_str()
+		.expect("Failed to convert C-string to string")
+		.to_string()
+}
+
+fn call_stylize() {
+	let input = std::ffi::CString::new("aBcDe").unwrap();
+	let (s1, s2, s3) = unsafe {
+		let result_obj = callee::stylize(lean::lean_mk_string(input.as_ptr()));
+		assert!(lean::lean_is_ctor(result_obj), "Tuple must be a ctor");
+		// Remember Lean tuples are nested!
+		assert_eq!(
+			lean::lean_ctor_num_objs(result_obj),
+			2,
+			"Tuple ctor has 3 elements"
+		);
+		let s1 = unbox_lean_string(lean::lean_ctor_get(result_obj, 0));
+		let result_obj2 = lean::lean_ctor_get(result_obj, 1);
+		let s2 = unbox_lean_string(lean::lean_ctor_get(result_obj2, 0));
+		let s3 = unbox_lean_string(lean::lean_ctor_get(result_obj2, 1));
+		lean::lean_dec(result_obj);
+		(s1, s2, s3)
+	};
+	assert_eq!(s1, "ABcDe");
+	assert_eq!(s2, "aBcDe");
+	assert_eq!(s3, "ABCDE");
+}
+
+fn call_think(s: &str) -> Result<String, usize> {
+	let input = std::ffi::CString::new(s).expect("Failed to convert to C-string");
+	unsafe {
+		let result_obj = callee::think(lean::lean_mk_string(input.as_ptr()));
+		let tag = lean::lean_ptr_tag(result_obj);
+		let result = if tag == 0 {
+			assert!(lean::lean_is_ctor(result_obj), "Think must be a ctor");
+			assert_eq!(
+				lean::lean_ctor_num_objs(result_obj),
+				1,
+				"Ctor must have 1 field"
+			);
+			let s = unbox_lean_string(lean::lean_ctor_get(result_obj, 0));
+			Ok(s)
+		} else if tag == 1 {
+			assert_eq!(
+				lean::lean_ctor_num_objs(result_obj),
+				1,
+				"Ctor must have 1 field"
+			);
+			let field = lean::lean_ctor_get(result_obj, 0);
+			let n = lean::lean_uint64_of_nat(field) as usize;
+			Err(n)
+		} else {
+			unreachable!("Invalid constructor id")
+		};
+		lean::lean_dec(result_obj);
+		result
+	}
+}
+
+fn main() {
+	initialize();
+	println!("Lean initialization complete!");
+
+	call_my_function();
+	call_stylize();
+
+	assert_eq!(call_think("Stanford"), Ok("tanford".to_string()));
+	assert_eq!(call_think("Else"), Err(4));
 }