diff options
| author | Son HO | 2024-04-12 08:59:55 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-12 08:59:55 +0200 |
| commit | 03a175b423c9ccff2160300c4d349978f9b1aeb9 (patch) | |
| tree | c85831d9d4bae5116cda6261befafdc229303205 /compiler | |
| parent | 77d74452489f85f558efe07d72d0200c80b16444 (diff) | |
| parent | 502f25a653a0afe7787b92a3004374e7670ea69b (diff) | |
Merge pull request #110 from zhassan-aws/checked-ops
Add builtins for some checked ops for the Lean backend
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 401d0137..3ba8d11d 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -240,6 +240,26 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = let f = { extract_name = basename } in (rust_name, filter, f) in + let mk_scalar_fun (rust_name : string -> string) + (extract_name : string -> string) : + (pattern * bool list option * builtin_fun_info) list = + List.map + (fun ty -> mk_fun (rust_name ty) (Some (extract_name ty)) None) + [ + "usize"; + "u8"; + "u16"; + "u32"; + "u64"; + "u128"; + "isize"; + "i8"; + "i16"; + "i32"; + "i64"; + "i128"; + ] + in [ mk_fun "core::mem::replace" None None; mk_fun "core::slice::{[@T]}::len" @@ -325,6 +345,14 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = [@T]>}::index_mut" (Some "core_slice_index_Slice_index_mut") None; ] + @ List.flatten + (List.map + (fun op -> + mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op) + (fun ty -> + StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op)) + [ "add"; "sub"; "mul"; "div"; "rem" ]) let mk_builtin_funs_map () = let m = |