From 01a51b4e080bb6b94c26b58d8e65bca204cb0f00 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 7 Mar 2024 21:37:37 -0800
Subject: [PATCH] Add structure and inductive examples

---
 Callee/Callee.lean | 18 +++++++++-
 src/main.rs        | 89 ++++++++++++++++++++++++++++++++++++++++++----
 2 files changed, 99 insertions(+), 8 deletions(-)

diff --git a/Callee/Callee.lean b/Callee/Callee.lean
index 46723c3..6aac9ab 100644
--- a/Callee/Callee.lean
+++ b/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
diff --git a/src/main.rs b/src/main.rs
index 5beb1d1..3c0b4b2 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -19,11 +19,14 @@ mod callee {
 	#[link(name = "Callee")]
 	extern "C" {
 		#[allow(non_snake_case)]
-		pub fn initialize_Callee(builtin: u8, world: *mut lean_object) -> *mut lean_object;
-		pub fn my_function(s: lean_obj_arg) -> lean_obj_arg;
+		pub fn initialize_Callee(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!("Object tag > constructor")
+		};
+		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));
 }