Add IO monad example

Callee/Callee.lean

@@ -17,3 +17,7 @@ def think (s: String): Think :=
     Think.Success (s.drop 1)
   else
     Think.Failure s.length
+
+@[export print_in_upper]
+def print_in_upper (s: String): IO Unit := do
+  IO.println s.toUpper

build.rs

@@ -9,6 +9,9 @@ fn main() {
 	println!("cargo:rustc-link-search={callee_root}");
 	println!("cargo:rustc-link-search={lean_root}/lib/lean");
 
+	let bindgen_dir = env::temp_dir().join("bindgen");
+	let extern_src_path = bindgen_dir.join("leanextern.c");
+
 	let bindings = bindgen::Builder::default()
 		.header(&input)
 		// Tell cargo to invalidate the built crate whenever any of the
@@ -17,6 +20,8 @@ fn main() {
 		// The following is specific to `lean.h`: There are a lot of static
 		// function
 		.wrap_static_fns(true)
+		.wrap_static_fns_suffix("__leanextern")
+		.wrap_static_fns_path(&extern_src_path)
 		// but some functions use `_Atomic(int)` types that bindgen cannot handle,
 		// so they are blocklisted. The types which use `_Atomic` are treated as
 		// opaque.
@@ -30,11 +35,7 @@ fn main() {
 		.write_to_file(output_path.join("lean.rs"))
 		.expect("Couldn't write bindings!");
 
-	let extern_src_path = env::temp_dir().join("bindgen").join("extern.c");
+	let extern_obj_path = bindgen_dir.join("leanextern.o");
-	let extern_obj_path = env::temp_dir().join("bindgen").join("extern.o");
-
-	// This is the path to the static library file.
-	let lib_path = output_path.join("libextern.a");
 
 	// Compile the generated wrappers into an object file.
 	let clang_output = std::process::Command::new("clang")
@@ -56,23 +57,20 @@ fn main() {
 		);
 	}
 
-	// Turn the object file into a static library
 	#[cfg(not(target_os = "windows"))]
 	let lib_output = std::process::Command::new("ar")
 		.arg("rcs")
-		.arg(output_path.join(&lib_path))
+		.arg(bindgen_dir.join("libleanextern.a"))
 		.arg(&extern_obj_path)
-		.output()
+		.output().unwrap();
-		.unwrap();
 	#[cfg(target_os = "windows")]
 	let lib_output = std::process::Command::new("LIB")
-		.arg(obj_path)
+		.arg(&extern_obj_path)
 		.arg(format!(
 			"/OUT:{}",
-			output_path.join("libextern.lib").display()
+			bindgen_dir.join("libleanextern.lib").display()
 		))
-		.output()
+		.output().unwrap();
-		.unwrap();
 	if !lib_output.status.success() {
 		panic!(
 			"Could not emit library file:\n{}",
@@ -81,6 +79,6 @@ fn main() {
 	}
 
 	// Statically link against the generated lib
-	println!("cargo:rustc-link-search={}", output_path.display());
+	println!("cargo:rustc-link-search={}", bindgen_dir.display());
-	println!("cargo:rustc-link-lib=static=extern");
+	println!("cargo:rustc-link-lib=static=leanextern");
 }

src/main.rs

@@ -18,11 +18,12 @@ mod callee {
 
 	#[link(name = "Callee")]
 	extern "C" {
-		#[allow(non_snake_case)]
+		#[link_name = "initialize_Callee"]
-		pub fn initialize_Callee(builtin: u8, world: lean_obj_arg) -> lean_obj_res;
+		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;
+		pub fn print_in_upper(s: lean_obj_arg, world: lean_obj_arg) -> lean_obj_res;
 	}
 }
 
@@ -31,7 +32,7 @@ fn initialize() {
 		lean::lean_initialize_runtime_module();
 		lean::lean_initialize();
 		let builtin: u8 = 1;
-		let res = callee::initialize_Callee(builtin, lean::lean_io_mk_world());
+		let res = callee::initialize(builtin, lean::lean_io_mk_world());
 		if lean::lean_io_result_is_ok(res) {
 			lean::lean_dec_ref(res);
 		} else {
@@ -118,6 +119,22 @@ fn call_think(s: &str) -> Result<String, usize> {
 	}
 }
 
+fn call_print_in_upper()
+{
+	let c_str = std::ffi::CString::new("caller").unwrap();
+	unsafe {
+		let native_str = lean::lean_mk_string(c_str.as_ptr());
+		let res = callee::print_in_upper(native_str, lean::lean_io_mk_world());
+		if lean::lean_io_result_is_ok(res) {
+			lean::lean_dec_ref(res);
+		} else {
+			lean::lean_io_result_show_error(res);
+			lean::lean_dec(res);
+			panic!("IO Monad execution failed");
+		}
+	};
+}
+
 fn main() {
 	initialize();
 	println!("Lean initialization complete!");
@@ -127,4 +144,5 @@ fn main() {
 
 	assert_eq!(call_think("Stanford"), Ok("tanford".to_string()));
 	assert_eq!(call_think("Else"), Err(4));
+	call_print_in_upper();
 }