diff options
| author | Son Ho | 2023-10-24 15:49:54 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-24 15:49:54 +0200 |
| commit | 9ddd174959970f87658191034b70d0cfa02ff451 (patch) | |
| tree | ba746d7a01a7603730b8dd9613010b3dc0476f12 /compiler/ExtractBuiltin.ml | |
| parent | b631875f8166b3db81187a179eef2f21f52db2bd (diff) | |
Filter some type arguments for the builtin types/functions
Diffstat (limited to 'compiler/ExtractBuiltin.ml')
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index d3cea54e..65c18efd 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -203,9 +203,8 @@ type builtin_fun_info = { let builtin_funs () : (string list * bool list option * builtin_fun_info list) list = let rg0 = Some Types.RegionGroupId.zero in - (* TODO: fix the names below *) [ - ( [ "core::mem::replace" ], + ( [ "core"; "mem"; "replace" ], None, [ { @@ -223,7 +222,7 @@ let builtin_funs () : | Lean -> "mem.replace_back"); }; ] ); - ( [ "alloc::vec::Vec::new" ], + ( [ "alloc"; "vec"; "Vec"; "new" ], Some [ true; false ], [ { @@ -241,7 +240,7 @@ let builtin_funs () : | Lean -> "Vec.new_back"); }; ] ); - ( [ "alloc::vec::Vec::push" ], + ( [ "alloc"; "vec"; "Vec"; "push" ], Some [ true; false ], [ (* The forward function shouldn't be used *) @@ -260,7 +259,7 @@ let builtin_funs () : | Lean -> "Vec.push"); }; ] ); - ( [ "alloc::vec::Vec::insert" ], + ( [ "alloc"; "vec"; "Vec"; "insert" ], Some [ true; false ], [ (* The forward function shouldn't be used *) @@ -279,7 +278,7 @@ let builtin_funs () : | Lean -> "Vec.insert"); }; ] ); - ( [ "alloc::vec::Vec::len" ], + ( [ "alloc"; "vec"; "Vec"; "len" ], Some [ true; false ], [ { @@ -290,7 +289,7 @@ let builtin_funs () : | Lean -> "Vec.len"); }; ] ); - ( [ "alloc::vec::Vec::index" ], + ( [ "alloc"; "vec"; "Vec"; "index" ], Some [ true; false ], [ { @@ -309,7 +308,7 @@ let builtin_funs () : | Lean -> "Vec.index_shared_back"); }; ] ); - ( [ "alloc::vec::Vec::index_mut" ], + ( [ "alloc"; "vec"; "Vec"; "index_mut" ], Some [ true; false ], [ { |