aniva
/
RustCallLean
1
0
Fork 0
Code Issues Pull Requests 1 Packages Projects Releases Wiki Activity

Add IO monad example

This commit is contained in:
Leni Aniva 2024-03-10 08:47:25 -07:00
parent 66dbf9ba3e
commit 86dc7f289e
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 22 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Callee/Callee.lean
View File

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

18
src/main.rs
View File

@ -23,6 +23,7 @@ mod callee {
pub fn my_function(s: 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 stylize(s: lean_obj_arg) -> lean_obj_res;
pub fn think(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;
} }
} }
@ -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() { fn main() {
initialize(); initialize();
println!("Lean initialization complete!"); println!("Lean initialization complete!");
@ -127,4 +144,5 @@ fn main() {
assert_eq!(call_think("Stanford"), Ok("tanford".to_string())); assert_eq!(call_think("Stanford"), Ok("tanford".to_string()));
assert_eq!(call_think("Else"), Err(4)); assert_eq!(call_think("Else"), Err(4));
call_print_in_upper();
} }