Callee/Callee.lean

@@ -1,19 +1,3 @@
 @[export my_function]
 def my_function (s: String): String :=
-  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
+  s ++ s!"abc"

src/main.rs

@@ -21,12 +21,9 @@ 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 initialize() {
+fn main() {
 	unsafe {
 		lean::lean_initialize_runtime_module();
 		lean::lean_initialize();
@@ -41,9 +38,8 @@ fn initialize() {
 		}
 		lean::lean_io_mark_end_initialization();
 	}
-}
+	println!("Lean initialization complete!");
 
-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());
@@ -54,77 +50,6 @@ fn call_my_function() {
 		lean::lean_dec(result_obj);
 		str
 	};
-	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));
+	println!("result: {result}");
 }