summaryrefslogtreecommitdiff
path: root/compiler/ExtractBuiltin.ml
diff options
context:
space:
mode:
authorSon HO2023-11-28 08:04:43 +0100
committerGitHub2023-11-28 08:04:43 +0100
commitb78850a81dfea78bc280f1b5b6d2fdcb421e386a (patch)
tree3a4807b26856c0c2e21f1a8a4cdf80da136c26ec /compiler/ExtractBuiltin.ml
parentbacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (diff)
parenta3a3ab9723348e24f83073a52145128f34022265 (diff)
Merge pull request #46 from AeneasVerif/son_improves
Minor improvements for the extraction
Diffstat (limited to '')
-rw-r--r--compiler/ExtractBuiltin.ml15
1 files changed, 12 insertions, 3 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 30ec7c19..24d16dca 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -127,9 +127,15 @@ let mk_struct_constructor (type_name : string) : string =
a type parameter for the allocator to use, which we want to filter.
*)
let builtin_types () : builtin_type_info list =
- let mk_type (rust_name : string) ?(keep_params : bool list option = None)
+ let mk_type (rust_name : string) ?(custom_name : string option = None)
+ ?(keep_params : bool list option = None)
?(kind : type_variant_kind = KOpaque) () : builtin_type_info =
- let extract_name = flatten_name (split_on_separator rust_name) in
+ let rust_name = parse_pattern rust_name in
+ let extract_name =
+ match custom_name with
+ | None -> flatten_name (pattern_to_type_extract_name rust_name)
+ | Some name -> flatten_name (split_on_separator name)
+ in
let body_info : builtin_type_body_info option =
match kind with
| KOpaque -> None
@@ -147,13 +153,16 @@ let builtin_types () : builtin_type_info list =
Some (Struct (constructor, fields))
| KEnum -> raise (Failure "TODO")
in
- let rust_name = parse_pattern rust_name in
{ rust_name; extract_name; keep_params; body_info }
in
[
(* Alloc *)
mk_type "alloc::alloc::Global" ();
+ (* String *)
+ mk_type "alloc::string::String"
+ ~custom_name:(Some (backend_choice "string" "String"))
+ ();
(* Vec *)
mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) ();
(* Range *)