summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Assumed.ml2
-rw-r--r--compiler/Extract.ml18
-rw-r--r--compiler/ExtractBase.ml3
-rw-r--r--compiler/ExtractBuiltin.ml394
-rw-r--r--compiler/ExtractName.ml177
-rw-r--r--compiler/ExtractTypes.ml106
-rw-r--r--compiler/FunsAnalysis.ml10
-rw-r--r--compiler/Interpreter.ml2
-rw-r--r--compiler/InterpreterExpressions.ml2
-rw-r--r--compiler/LlbcAstUtils.ml15
-rw-r--r--compiler/PrintPure.ml6
-rw-r--r--compiler/PureUtils.ml2
-rw-r--r--compiler/StringUtils.ml112
-rw-r--r--compiler/Substitute.ml4
-rw-r--r--compiler/SymbolicAst.ml2
-rw-r--r--compiler/SymbolicToPure.ml4
-rw-r--r--compiler/Translate.ml25
-rw-r--r--compiler/TranslateCore.ml48
-rw-r--r--compiler/dune3
19 files changed, 440 insertions, 495 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 6aec626a..48b7ee2b 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -42,7 +42,7 @@ module Sig = struct
let tvar_id_0 = TypeVarId.of_int 0
let tvar_0 : ty = TVar tvar_id_0
let cgvar_id_0 = ConstGenericVarId.of_int 0
- let cgvar_0 : const_generic = CGVar cgvar_id_0
+ let cgvar_0 : const_generic = CgVar cgvar_id_0
(** Region 'a of id 0 *)
let region_param_0 : region_var = { index = rvar_id_0; name = Some "'a" }
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index cd62c15c..fb3364f4 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -27,8 +27,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
let builtin =
let open ExtractBuiltin in
let funs_map = builtin_funs_map () in
- let sname = name_to_simple_name def.fwd.f.llbc_name in
- SimpleNameMap.find_opt sname funs_map
+ match_name_find_opt ctx.trans_ctx def.fwd.f.llbc_name funs_map
in
(* Use the builtin names if necessary *)
match builtin with
@@ -2024,9 +2023,9 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
(trait_decl : trait_decl) : extraction_ctx =
(* Lookup the information if this is a builtin trait *)
let open ExtractBuiltin in
- let sname = name_to_simple_name trait_decl.llbc_name in
let builtin_info =
- SimpleNameMap.find_opt sname (builtin_trait_decls_map ())
+ match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+ (builtin_trait_decls_map ())
in
let ctx =
let trait_name, trait_constructor =
@@ -2061,9 +2060,14 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
(* Check if the trait implementation is builtin *)
let builtin_info =
let open ExtractBuiltin in
- let type_sname = name_to_simple_name trait_impl.llbc_name in
- let trait_sname = name_to_simple_name trait_decl.llbc_name in
- SimpleNamePairMap.find_opt (type_sname, trait_sname)
+ (* Lookup the original Rust impl to retrieve the original trait ref (we
+ use it to derive the name)*)
+ let trait_impl =
+ TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
+ in
+ let decl_ref = trait_impl.impl_trait in
+ match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+ decl_ref.decl_generics
(builtin_trait_impls_map ())
in
(* Register some builtin information (if necessary) *)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index ae5a9a22..f1ba35a2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1085,8 +1085,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
(* Check if the global corresponds to an assumed global that we should map
to a custom definition in our standard library (for instance, happens
with "core::num::usize::MAX") *)
- let sname = name_to_simple_name def.name in
- match SimpleNameMap.find_opt sname builtin_globals_map with
+ match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with
| Some name ->
(* Yes: register the custom binding *)
ctx_add decl name ctx
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index db942ff0..d15905a2 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -5,38 +5,8 @@
*)
open Config
-open Types
-
-type simple_name = string list [@@deriving show, ord]
-
-(* TODO: update *)
-let name_to_simple_name (s : name) : simple_name =
- (* We simply ignore the disambiguators - TODO: update *)
- List.map
- (function
- | PeIdent (id, _) -> id
- | PeImpl i ->
- (* TODO *)
- show_impl_elem i)
- s
-
-(** Small helper which cuts a string at the occurrences of "::" *)
-let string_to_simple_name (s : string) : simple_name =
- (* No function to split by using string separator?? *)
- let name = String.split_on_char ':' s in
- List.filter (fun s -> s <> "") name
-
-module SimpleNameOrd = struct
- type t = simple_name
-
- let compare = compare_simple_name
- let to_string = show_simple_name
- let pp_t = pp_simple_name
- let show_t = show_simple_name
-end
-
-module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
-module SimpleNameSet = Collections.MakeSet (SimpleNameOrd)
+open Charon.NameMatcher (* TODO: include? *)
+include ExtractName (* TODO: only open? *)
(** Small utility to memoize some computations *)
let mk_memoized (f : unit -> 'a) : unit -> 'a =
@@ -51,6 +21,9 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a =
in
g
+let split_on_separator (s : string) : string list =
+ Str.split (Str.regexp "::") s
+
(** Switch between two values depending on the target backend.
We often compute the same value (typically: a name) if the target
@@ -62,36 +35,36 @@ let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a =
let builtin_globals : (string * string) list =
[
(* Min *)
- ("core::num::usize::MIN", "core_usize_min");
- ("core::num::u8::MIN", "core_u8_min");
- ("core::num::u16::MIN", "core_u16_min");
- ("core::num::u32::MIN", "core_u32_min");
- ("core::num::u64::MIN", "core_u64_min");
- ("core::num::u128::MIN", "core_u128_min");
- ("core::num::isize::MIN", "core_isize_min");
- ("core::num::i8::MIN", "core_i8_min");
- ("core::num::i16::MIN", "core_i16_min");
- ("core::num::i32::MIN", "core_i32_min");
- ("core::num::i64::MIN", "core_i64_min");
- ("core::num::i128::MIN", "core_i128_min");
+ ("core::num::{usize}::MIN", "core_usize_min");
+ ("core::num::{u8}::MIN", "core_u8_min");
+ ("core::num::{u16}::MIN", "core_u16_min");
+ ("core::num::{u32}::MIN", "core_u32_min");
+ ("core::num::{u64}::MIN", "core_u64_min");
+ ("core::num::{u128}::MIN", "core_u128_min");
+ ("core::num::{isize}::MIN", "core_isize_min");
+ ("core::num::{i8}::MIN", "core_i8_min");
+ ("core::num::{i16}::MIN", "core_i16_min");
+ ("core::num::{i32}::MIN", "core_i32_min");
+ ("core::num::{i64}::MIN", "core_i64_min");
+ ("core::num::{i128}::MIN", "core_i128_min");
(* Max *)
- ("core::num::usize::MAX", "core_usize_max");
- ("core::num::u8::MAX", "core_u8_max");
- ("core::num::u16::MAX", "core_u16_max");
- ("core::num::u32::MAX", "core_u32_max");
- ("core::num::u64::MAX", "core_u64_max");
- ("core::num::u128::MAX", "core_u128_max");
- ("core::num::isize::MAX", "core_isize_max");
- ("core::num::i8::MAX", "core_i8_max");
- ("core::num::i16::MAX", "core_i16_max");
- ("core::num::i32::MAX", "core_i32_max");
- ("core::num::i64::MAX", "core_i64_max");
- ("core::num::i128::MAX", "core_i128_max");
+ ("core::num::{usize}::MAX", "core_usize_max");
+ ("core::num::{u8}::MAX", "core_u8_max");
+ ("core::num::{u16}::MAX", "core_u16_max");
+ ("core::num::{u32}::MAX", "core_u32_max");
+ ("core::num::{u64}::MAX", "core_u64_max");
+ ("core::num::{u128}::MAX", "core_u128_max");
+ ("core::num::{isize}::MAX", "core_isize_max");
+ ("core::num::{i8}::MAX", "core_i8_max");
+ ("core::num::{i16}::MAX", "core_i16_max");
+ ("core::num::{i32}::MAX", "core_i32_max");
+ ("core::num::{i64}::MAX", "core_i64_max");
+ ("core::num::{i128}::MAX", "core_i128_max");
]
-let builtin_globals_map : string SimpleNameMap.t =
- SimpleNameMap.of_list
- (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals)
+let builtin_globals_map : string NameMatcherMap.t =
+ NameMatcherMap.of_list
+ (List.map (fun (x, y) -> (parse_pattern x, y)) builtin_globals)
type builtin_variant_info = { fields : (string * string) list }
[@@deriving show]
@@ -111,7 +84,7 @@ type builtin_type_body_info =
[@@deriving show]
type builtin_type_info = {
- rust_name : string list;
+ rust_name : pattern;
extract_name : string;
keep_params : bool list option;
(** We might want to filter some of the type parameters.
@@ -143,11 +116,11 @@ 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 list) ?(keep_params : bool list option = None)
+ let mk_type (rust_name : string) ?(keep_params : bool list option = None)
?(kind : type_variant_kind = KOpaque) () : builtin_type_info =
let extract_name =
let sep = backend_choice "_" "." in
- String.concat sep rust_name
+ String.concat sep (split_on_separator rust_name)
in
let body_info : builtin_type_body_info option =
match kind with
@@ -166,17 +139,17 @@ 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" ] ();
+ mk_type "alloc::alloc::Global" ();
(* Vec *)
- mk_type [ "alloc"; "vec"; "Vec" ] ~keep_params:(Some [ true; false ]) ();
+ mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) ();
(* Range *)
- mk_type
- [ "core"; "ops"; "range"; "Range" ]
+ mk_type "core::ops::range::Range"
~kind:(KStruct [ ("start", "start"); ("end", "end_") ])
();
(* Option
@@ -185,7 +158,7 @@ let builtin_types () : builtin_type_info list =
the target backend.
*)
{
- rust_name = [ "core"; "option"; "Option" ];
+ rust_name = parse_pattern "core::option::Option";
extract_name =
(match !backend with
| Lean -> "Option"
@@ -218,7 +191,7 @@ let builtin_types () : builtin_type_info list =
]
let mk_builtin_types_map () =
- SimpleNameMap.of_list
+ NameMatcherMap.of_list
(List.map (fun info -> (info.rust_name, info)) (builtin_types ()))
let builtin_types_map = mk_memoized mk_builtin_types_map
@@ -235,15 +208,22 @@ type builtin_fun_info = {
parameters. For instance, in the case of the `Vec` functions, there is
a type parameter for the allocator to use, which we want to filter.
*)
-let builtin_funs () :
- (string list * bool list option * builtin_fun_info list) list =
+let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
+ =
let rg0 = Some Types.RegionGroupId.zero in
(* Small utility *)
- let mk_fun (name : string list) (extract_name : string list option)
+ let mk_fun (rust_name : string) (extract_name : string option)
(filter : bool list option) (with_back : bool) (back_no_suffix : bool) :
- string list * bool list option * builtin_fun_info list =
+ pattern * bool list option * builtin_fun_info list =
+ let rust_name =
+ try parse_pattern rust_name
+ with Failure _ ->
+ raise (Failure ("Could not parse pattern: " ^ rust_name))
+ in
let extract_name =
- match extract_name with None -> name | Some name -> name
+ match extract_name with
+ | None -> pattern_to_fun_extract_name rust_name
+ | Some name -> split_on_separator name
in
let basename =
match !backend with
@@ -257,103 +237,55 @@ let builtin_funs () :
if with_back then [ { rg = rg0; extract_name = basename ^ back_suffix } ]
else []
in
- (name, filter, fwd @ back)
+ (rust_name, filter, fwd @ back)
in
[
- mk_fun [ "core"; "mem"; "replace" ] None None true false;
- mk_fun [ "alloc"; "vec"; "Vec"; "new" ] None None false false;
- mk_fun
- [ "alloc"; "vec"; "Vec"; "push" ]
- None
+ mk_fun "core::mem::replace" None None true false;
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::new" None None false false;
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::push" None
(Some [ true; false ])
true true;
- mk_fun
- [ "alloc"; "vec"; "Vec"; "insert" ]
- None
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::insert" None
(Some [ true; false ])
true true;
- mk_fun
- [ "alloc"; "vec"; "Vec"; "len" ]
- None
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::len" None
(Some [ true; false ])
true false;
- mk_fun
- [ "alloc"; "vec"; "Vec"; "index" ]
- None
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index" None
(Some [ true; true; false ])
true false;
- mk_fun
- [ "alloc"; "vec"; "Vec"; "index_mut" ]
- None
+ mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index_mut" None
(Some [ true; true; false ])
true false;
- mk_fun
- [ "alloc"; "boxed"; "Box"; "deref" ]
- None
+ mk_fun "alloc::boxed::{Box<@T>}::deref" None
(Some [ true; false ])
true false;
- mk_fun
- [ "alloc"; "boxed"; "Box"; "deref_mut" ]
- None
+ mk_fun "alloc::boxed::{Box<@T>}::deref_mut" None
(Some [ true; false ])
true false;
- (* TODO: fix the same like "[T]" below *)
- mk_fun
- [ "core"; "slice"; "index"; "[T]"; "index" ]
- (Some [ "core"; "slice"; "index"; "Slice"; "index" ])
- None true false;
- mk_fun
- [ "core"; "slice"; "index"; "[T]"; "index_mut" ]
- (Some [ "core"; "slice"; "index"; "Slice"; "index_mut" ])
- None true false;
- mk_fun
- [ "core"; "array"; "[T; N]"; "index" ]
- (Some [ "core"; "array"; "Array"; "index" ])
- None true false;
- mk_fun
- [ "core"; "array"; "[T; N]"; "index_mut" ]
- (Some [ "core"; "array"; "Array"; "index_mut" ])
- None true false;
- mk_fun [ "core"; "slice"; "index"; "Range"; "get" ] None None true false;
- mk_fun [ "core"; "slice"; "index"; "Range"; "get_mut" ] None None true false;
- mk_fun [ "core"; "slice"; "index"; "Range"; "index" ] None None true false;
- mk_fun
- [ "core"; "slice"; "index"; "Range"; "index_mut" ]
- None None true false;
- mk_fun
- [ "core"; "slice"; "index"; "Range"; "get_unchecked" ]
- None None false false;
- mk_fun
- [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ]
- None None false false;
- mk_fun
- [ "core"; "slice"; "index"; "usize"; "get" ]
- (Some [ "core"; "slice"; "index"; "Usize"; "get" ])
- None true false;
- mk_fun
- [ "core"; "slice"; "index"; "usize"; "get_mut" ]
- (Some [ "core"; "slice"; "index"; "Usize"; "get_mut" ])
- None true false;
- mk_fun
- [ "core"; "slice"; "index"; "usize"; "get_unchecked" ]
- (Some [ "core"; "slice"; "index"; "Usize"; "get_unchecked" ])
- None false false;
- mk_fun
- [ "core"; "slice"; "index"; "usize"; "get_unchecked_mut" ]
- (Some [ "core"; "slice"; "index"; "Usize"; "get_unchecked_mut" ])
- None false false;
- mk_fun
- [ "core"; "slice"; "index"; "usize"; "index" ]
- (Some [ "core"; "slice"; "index"; "Usize"; "index" ])
- None true false;
- mk_fun
- [ "core"; "slice"; "index"; "usize"; "index_mut" ]
- (Some [ "core"; "slice"; "index"; "Usize"; "index_mut" ])
- None true false;
+ mk_fun "core::slice::index::{[@T]}::index" None None true false;
+ mk_fun "core::slice::index::{[@T]}::index_mut" None None true false;
+ mk_fun "core::array::{[@T; @C]}::index" None None true false;
+ mk_fun "core::array::{[@T; @C]}::index_mut" None None true false;
+ mk_fun "core::slice::index::{Range<@T>}::get" None None true false;
+ mk_fun "core::slice::index::{Range<@T>}::get_mut" None None true false;
+ mk_fun "core::slice::index::{Range<@T>}::index" None None true false;
+ mk_fun "core::slice::index::{Range<@T>}::index_mut" None None true false;
+ mk_fun "core::slice::index::{Range<@T>}::get_unchecked" None None false
+ false;
+ mk_fun "core::slice::index::{Range<@T>}::get_unchecked_mut" None None false
+ false;
+ mk_fun "core::slice::index::{usize}::get" None None true false;
+ mk_fun "core::slice::index::{usize}::get_mut" None None true false;
+ mk_fun "core::slice::index::{usize}::get_unchecked" None None false false;
+ mk_fun "core::slice::index::{usize}::get_unchecked_mut" None None false
+ false;
+ mk_fun "core::slice::index::{usize}::index" None None true false;
+ mk_fun "core::slice::index::{usize}::index_mut" None None true false;
]
let mk_builtin_funs_map () =
- SimpleNameMap.of_list
+ NameMatcherMap.of_list
(List.map
(fun (name, filter, info) -> (name, (filter, info)))
(builtin_funs ()))
@@ -385,17 +317,22 @@ let builtin_fun_effects =
let int_funs =
List.map
(fun int_name ->
- List.map (fun op -> "core::num::" ^ int_name ^ "::" ^ op) int_ops)
+ List.map
+ (fun op ->
+ "core::num::" ^ "{"
+ ^ StringUtils.capitalize_first_letter int_name
+ ^ "}::" ^ op)
+ int_ops)
int_names
in
let int_funs = List.concat int_funs in
let no_fail_no_state_funs =
[
(* TODO: redundancy with the funs information below *)
- "alloc::vec::Vec::new";
- "alloc::vec::Vec::len";
- "alloc::boxed::Box::deref";
- "alloc::boxed::Box::deref_mut";
+ "alloc::vec::{alloc::vec::Vec<@T>}::new";
+ "alloc::vec::{alloc::vec::Vec<@T>}::len";
+ "alloc::boxed::{Box<@T>}::deref";
+ "alloc::boxed::{Box<@T>}::deref_mut";
"core::mem::replace";
"core::mem::take";
]
@@ -409,10 +346,10 @@ let builtin_fun_effects =
let no_state_funs =
[
(* TODO: redundancy with the funs information below *)
- "alloc::vec::Vec::push";
- "alloc::vec::Vec::index";
- "alloc::vec::Vec::index_mut";
- "alloc::vec::Vec::index_mut_back";
+ "alloc::vec::{alloc::vec::Vec<@T>}::push";
+ "alloc::vec::{alloc::vec::Vec<@T>}::index";
+ "alloc::vec::{alloc::vec::Vec<@T>}::index_mut";
+ "alloc::vec::{alloc::vec::Vec<@T>}::index_mut_back";
]
in
let no_state_funs =
@@ -421,11 +358,11 @@ let builtin_fun_effects =
no_fail_no_state_funs @ no_state_funs
let builtin_fun_effects_map =
- SimpleNameMap.of_list
- (List.map (fun (n, x) -> (string_to_simple_name n, x)) builtin_fun_effects)
+ NameMatcherMap.of_list
+ (List.map (fun (n, x) -> (parse_pattern n, x)) builtin_fun_effects)
type builtin_trait_decl_info = {
- rust_name : string;
+ rust_name : pattern;
extract_name : string;
constructor : string;
parent_clauses : string list;
@@ -441,13 +378,15 @@ type builtin_trait_decl_info = {
let builtin_trait_decls_info () =
let rg0 = Some Types.RegionGroupId.zero in
- let mk_trait (rust_name : string list) ?(extract_name : string option = None)
+ let mk_trait (rust_name : string) ?(extract_name : string option = None)
?(parent_clauses : string list = []) ?(types : string list = [])
?(methods : (string * bool) list = []) () : builtin_trait_decl_info =
+ let rust_name = parse_pattern rust_name in
let extract_name =
match extract_name with
| Some n -> n
| None -> (
+ let rust_name = pattern_to_fun_extract_name rust_name in
match !backend with
| Coq | FStar | HOL4 -> String.concat "_" rust_name
| Lean -> String.concat "." rust_name)
@@ -487,7 +426,6 @@ let builtin_trait_decls_info () =
in
List.map mk_method methods
in
- let rust_name = String.concat "::" rust_name in
{
rust_name;
extract_name;
@@ -500,34 +438,27 @@ let builtin_trait_decls_info () =
in
[
(* Deref *)
- mk_trait
- [ "core"; "ops"; "deref"; "Deref" ]
- ~types:[ "Target" ]
+ mk_trait "core::ops::deref::Deref" ~types:[ "Target" ]
~methods:[ ("deref", true) ]
();
(* DerefMut *)
- mk_trait
- [ "core"; "ops"; "deref"; "DerefMut" ]
+ mk_trait "core::ops::deref::DerefMut"
~parent_clauses:[ backend_choice "deref_inst" "derefInst" ]
~methods:[ ("deref_mut", true) ]
();
(* Index *)
- mk_trait
- [ "core"; "ops"; "index"; "Index" ]
- ~types:[ "Output" ]
+ mk_trait "core::ops::index::Index" ~types:[ "Output" ]
~methods:[ ("index", true) ]
();
(* IndexMut *)
- mk_trait
- [ "core"; "ops"; "index"; "IndexMut" ]
+ mk_trait "core::ops::index::IndexMut"
~parent_clauses:[ backend_choice "index_inst" "indexInst" ]
~methods:[ ("index_mut", true) ]
();
(* Sealed *)
- mk_trait [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ();
+ mk_trait "core::slice::index::private_slice_index::Sealed" ();
(* SliceIndex *)
- mk_trait
- [ "core"; "slice"; "index"; "SliceIndex" ]
+ mk_trait "core::slice::index::SliceIndex"
~parent_clauses:[ backend_choice "sealed_inst" "sealedInst" ]
~types:[ "Output" ]
~methods:
@@ -543,113 +474,56 @@ let builtin_trait_decls_info () =
]
let mk_builtin_trait_decls_map () =
- SimpleNameMap.of_list
+ NameMatcherMap.of_list
(List.map
- (fun info -> (string_to_simple_name info.rust_name, info))
+ (fun info -> (info.rust_name, info))
(builtin_trait_decls_info ()))
let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map
-(* TODO: generalize this.
-
- For now, the key is:
- - name of the impl (ex.: "alloc.boxed.Boxed")
- - name of the implemented trait (ex.: "core.ops.deref.Deref"
-*)
-type simple_name_pair = simple_name * simple_name [@@deriving show, ord]
-
-module SimpleNamePairOrd = struct
- type t = simple_name_pair
-
- let compare = compare_simple_name_pair
- let to_string = show_simple_name_pair
- let pp_t = pp_simple_name_pair
- let show_t = show_simple_name_pair
-end
-
-module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
-
-let builtin_trait_impls_info () :
- ((string list * string list) * (bool list option * string)) list =
- let fmt (type_name : string list)
- ?(extract_type_name : string list option = None)
- (trait_name : string list) ?(filter : bool list option = None) () :
- (string list * string list) * (bool list option * string) =
+let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
+ let fmt (rust_name : string) ?(filter : bool list option = None) () :
+ pattern * (bool list option * string) =
+ let rust_name = parse_pattern rust_name in
let name =
- let trait_name = String.concat "" trait_name ^ "Inst" in
+ let name = pattern_to_trait_impl_extract_name rust_name in
let sep = backend_choice "_" "." in
- let type_name =
- match extract_type_name with
- | Some type_name -> type_name
- | None -> type_name
- in
- String.concat sep type_name ^ sep ^ trait_name
+ String.concat sep name
in
- ((type_name, trait_name), (filter, name))
+ (rust_name, (filter, name))
in
- (* TODO: fix the names like "[T]" below *)
[
(* core::ops::Deref<alloc::boxed::Box<T>> *)
- fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "Deref" ] ();
- (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
- fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "DerefMut" ] ();
+ fmt "core::ops::Deref<Box<@T>>" ();
+ (* core::ops::Deref<alloc::boxed::Box<T>> *)
+ fmt "core::ops::Deref<Box<@T>>" ();
(* core::ops::index::Index<[T], I> *)
- fmt
- [ "core"; "slice"; "index"; "[T]" ]
- ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ])
- [ "core"; "ops"; "index"; "Index" ]
- ();
+ fmt "core::ops::index::Index<[@T], @I>" ();
(* core::ops::index::IndexMut<[T], I> *)
- fmt
- [ "core"; "slice"; "index"; "[T]" ]
- ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ])
- [ "core"; "ops"; "index"; "IndexMut" ]
- ();
+ fmt "core::ops::index::IndexMut<[@T], @I>" ();
(* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
- fmt
- [ "core"; "slice"; "index"; "private_slice_index"; "Range" ]
- [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ]
- ();
+ fmt "core::slice::index::private_slice_index::Sealed<Range<usize>>" ();
(* core::slice::index::SliceIndex<Range<usize>, [T]> *)
- fmt
- [ "core"; "slice"; "index"; "Range" ]
- [ "core"; "slice"; "index"; "SliceIndex" ]
- ();
+ fmt "core::slice::index::SliceIndex<Range<usize>, [@T]>" ();
(* core::ops::index::Index<[T; N], I> *)
- fmt
- [ "core"; "array"; "[T; N]" ]
- ~extract_type_name:(Some [ "core"; "array"; "Array" ])
- [ "core"; "ops"; "index"; "Index" ]
- ();
+ fmt "core::ops::index::Index<[@T; @N], @I>" ();
(* core::ops::index::IndexMut<[T; N], I> *)
- fmt
- [ "core"; "array"; "[T; N]" ]
- ~extract_type_name:(Some [ "core"; "array"; "Array" ])
- [ "core"; "ops"; "index"; "IndexMut" ]
- ();
+ fmt "core::ops::index::IndexMut<[@T; @N], @I>" ();
(* core::slice::index::private_slice_index::Sealed<usize> *)
- fmt
- [ "core"; "slice"; "index"; "private_slice_index"; "usize" ]
- [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ]
- ();
+ fmt "core::slice::index::private_slice_index::Sealed<usize>" ();
(* core::slice::index::SliceIndex<usize, [T]> *)
- fmt
- [ "core"; "slice"; "index"; "usize" ]
- [ "core"; "slice"; "index"; "SliceIndex" ]
- ();
- (* core::ops::index::Index<Vec<T>, T> *)
- fmt [ "alloc"; "vec"; "Vec" ]
- [ "core"; "ops"; "index"; "Index" ]
+ fmt "core::slice::index::SliceIndex<usize, [@T]>" ();
+ (* core::ops::index::Index<alloc::vec::Vec<T>, T> *)
+ fmt "core::ops::index::Index<alloc::vec::Vec<@T>, @T>"
~filter:(Some [ true; true; false ])
();
- (* core::ops::index::IndexMut<Vec<T>, T> *)
- fmt [ "alloc"; "vec"; "Vec" ]
- [ "core"; "ops"; "index"; "IndexMut" ]
+ (* core::ops::index::IndexMut<alloc::vec::Vec<T>, T> *)
+ fmt "core::ops::index::IndexMut<alloc::vec::Vec<@T>, @T>"
~filter:(Some [ true; true; false ])
();
]
let mk_builtin_trait_impls_map () =
- SimpleNamePairMap.of_list (builtin_trait_impls_info ())
+ NameMatcherMap.of_list (builtin_trait_impls_info ())
let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
new file mode 100644
index 00000000..4f5ca0d1
--- /dev/null
+++ b/compiler/ExtractName.ml
@@ -0,0 +1,177 @@
+(** Utilities for extracting names *)
+
+open Charon.NameMatcher
+
+module NameMatcherMap = struct
+ type 'a t = (pattern * 'a) list
+
+ let config = { map_vars_to_vars = true }
+
+ let find_opt (ctx : ctx) (name : Types.name) (m : 'a t) : 'a option =
+ match List.find_opt (fun (pat, _) -> match_name ctx config pat name) m with
+ | None -> None
+ | Some (_, v) -> Some v
+
+ let find_with_generics_opt (ctx : ctx) (name : Types.name)
+ (g : Types.generic_args) (m : 'a t) : 'a option =
+ match
+ List.find_opt
+ (fun (pat, _) -> match_name_with_generics ctx config pat name g)
+ m
+ with
+ | None -> None
+ | Some (_, v) -> Some v
+
+ let mem (ctx : ctx) (name : Types.name) (m : 'a t) : bool =
+ find_opt ctx name m <> None
+
+ let of_list (ls : (pattern * 'a) list) : 'a t = ls
+end
+
+(** Helper to convert name patterns to names for extraction.
+
+ For impl blocks, we simply use the name of the type (without its arguments)
+ if all the arguments are variables.
+ *)
+let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
+ string list =
+ let c = { tgt_kind = TkName } in
+ let is_var (g : generic_arg) : bool =
+ match g with
+ | GExpr (EVar _) -> true
+ | GRegion (RVar _) -> true
+ | _ -> false
+ in
+ let all_vars = List.for_all is_var in
+ let elem_to_string (e : pattern_elem) : string =
+ match e with
+ | PIdent _ -> pattern_elem_to_string c e
+ | PImpl ty -> (
+ match ty with
+ | EComp id -> (
+ (* Retrieve the last ident *)
+ let id = Collections.List.last id in
+ match id with
+ | PIdent (s, g) ->
+ if all_vars g then s else pattern_elem_to_string c id
+ | PImpl _ -> raise (Failure "Unreachable"))
+ | EPrimAdt (adt, g) ->
+ if all_vars g then
+ match adt with
+ | TTuple ->
+ let l = List.length g in
+ if l = 2 then "Pair" else expr_to_string c ty
+ | TArray -> "Array"
+ | TSlice -> "Slice"
+ else expr_to_string c ty
+ | ERef _ | EVar _ -> raise (Failure ""))
+ in
+ let rec pattern_to_string (n : pattern) : string list =
+ match n with
+ | [] -> raise (Failure "Unreachable")
+ | [ e ] ->
+ let e = elem_to_string e in
+ if is_trait_impl then [ e ^ "Inst" ] else [ e ]
+ | e :: n -> elem_to_string e :: pattern_to_string n
+ in
+ pattern_to_string name
+
+let pattern_to_fun_extract_name = pattern_to_extract_name false
+let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
+
+(* TODO: this is provisional. We just want to make sure that the extraction
+ names we derive from the patterns (for the builtin definitions) are
+ consistent with the extraction names we derive from the Rust names *)
+let name_to_simple_name (ctx : ctx) (n : Types.name) : string list =
+ pattern_to_extract_name false (name_to_pattern ctx n)
+
+let name_with_generics_to_simple_name (ctx : ctx) (n : Types.name)
+ (p : Types.generic_params) (g : Types.generic_args) : string list =
+ pattern_to_extract_name true (name_with_generics_to_pattern ctx n p g)
+
+(*
+ (* Prepare a name.
+ The first id elem is always the crate: if it is the local crate,
+ we remove it. We ignore disambiguators (there may be collisions, but we
+ check if there are).
+ *)
+ let rec name_to_simple_name (name : llbc_name) : string list =
+ (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
+ match name with
+ | (PeIdent (crate, _) as id) :: name ->
+ let name = if crate = crate_name then name else id :: name in
+ let open Types in
+ let name =
+ List.map
+ (function
+ | PeIdent (s, _) -> s
+ | PeImpl impl -> impl_elem_to_simple_name impl)
+ name
+ in
+ name
+ | _ ->
+ raise
+ (Failure
+ ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
+ and impl_elem_to_simple_name (impl : Types.impl_elem) : string =
+ (* We do something simple for now.
+ TODO: we might want to do something different for impl elements which are
+ actually trait implementations, in order to prevent name collisions (it
+ is possible to define several times the same trait for the same type,
+ but with different instantiations of the type, or different trait
+ requirements *)
+ ty_to_simple_name impl.generics impl.ty
+ and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) :
+ string =
+ (* We do something simple for now.
+ TODO: find a more principled way of converting types to names.
+ In particular, we might want to do something different for impl elements which are
+ actually trait implementations, in order to prevent name collisions (it
+ is possible to define several times the same trait for the same type,
+ but with different instantiations of the type, or different trait
+ requirements *)
+ match ty with
+ | TAdt (id, args) -> (
+ match id with
+ | TAdtId id ->
+ let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in
+ name_last_elem_as_ident def.name
+ | TTuple ->
+ (* TODO *)
+ "Tuple"
+ ^ String.concat ""
+ (List.map (ty_to_simple_name generics) args.types)
+ | TAssumed id -> (
+ match id with
+ | Types.TBox -> "Box"
+ | Types.TArray -> "Array"
+ | Types.TSlice -> "Slice"
+ | Types.TStr -> "Str"))
+ | TVar vid ->
+ (* Use the variable name *)
+ (List.find (fun (v : type_var) -> v.index = vid) generics.types).name
+ | TLiteral lty ->
+ StringUtils.capitalize_first_letter
+ (Print.Types.literal_type_to_string lty)
+ | TNever -> raise (Failure "Unreachable")
+ | TRef (_, rty, rk) -> (
+ let rty = ty_to_simple_name generics rty in
+ match rk with
+ | RMut -> "MutBorrow" ^ rty
+ | RShared -> "SharedBorrow" ^ rty)
+ | TRawPtr (rty, rk) -> (
+ let rty = ty_to_simple_name generics rty in
+ match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty)
+ | TTraitType (tr, _, name) ->
+ (* TODO: this is way too simple *)
+ let trait_decl =
+ TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id
+ ctx.trait_decls_ctx.trait_decls
+ in
+ name_last_elem_as_ident trait_decl.name ^ name
+ | TArrow (inputs, output) ->
+ "Arrow"
+ ^ String.concat ""
+ (List.map (ty_to_simple_name generics) (inputs @ [ output ]))
+ in
+*)
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index de4ec735..a74bd532 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -586,84 +586,16 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
we remove it. We ignore disambiguators (there may be collisions, but we
check if there are).
*)
- let rec name_to_simple_name (name : llbc_name) : string list =
+ let name_to_simple_name (name : llbc_name) : string list =
(* Rmk.: initially we only filtered the disambiguators equal to 0 *)
match name with
| (PeIdent (crate, _) as id) :: name ->
let name = if crate = crate_name then name else id :: name in
- let open Types in
- let name =
- List.map
- (function
- | PeIdent (s, _) -> s
- | PeImpl impl -> impl_elem_to_simple_name impl)
- name
- in
- name
+ name_to_simple_name ctx name
| _ ->
raise
(Failure
("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
- and impl_elem_to_simple_name (impl : Types.impl_elem) : string =
- (* We do something simple for now.
- TODO: we might want to do something different for impl elements which are
- actually trait implementations, in order to prevent name collisions (it
- is possible to define several times the same trait for the same type,
- but with different instantiations of the type, or different trait
- requirements *)
- ty_to_simple_name impl.generics impl.ty
- and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) :
- string =
- (* We do something simple for now.
- TODO: find a more principled way of converting types to names.
- In particular, we might want to do something different for impl elements which are
- actually trait implementations, in order to prevent name collisions (it
- is possible to define several times the same trait for the same type,
- but with different instantiations of the type, or different trait
- requirements *)
- match ty with
- | TAdt (id, args) -> (
- match id with
- | TAdtId id ->
- let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in
- name_last_elem_as_ident def.name
- | TTuple ->
- (* TODO *)
- "Tuple"
- ^ String.concat ""
- (List.map (ty_to_simple_name generics) args.types)
- | TAssumed id -> (
- match id with
- | Types.TBox -> "Box"
- | Types.TArray -> "Array"
- | Types.TSlice -> "Slice"
- | Types.TStr -> "Str"))
- | TVar vid ->
- (* Use the variable name *)
- (List.find (fun (v : type_var) -> v.index = vid) generics.types).name
- | TLiteral lty ->
- StringUtils.capitalize_first_letter
- (Print.Types.literal_type_to_string lty)
- | TNever -> raise (Failure "Unreachable")
- | TRef (_, rty, rk) -> (
- let rty = ty_to_simple_name generics rty in
- match rk with
- | RMut -> "MutBorrow" ^ rty
- | RShared -> "SharedBorrow" ^ rty)
- | TRawPtr (rty, rk) -> (
- let rty = ty_to_simple_name generics rty in
- match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty)
- | TTraitType (tr, _, name) ->
- (* TODO: this is way too simple *)
- let trait_decl =
- TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id
- ctx.trait_decls_ctx.trait_decls
- in
- name_last_elem_as_ident trait_decl.name ^ name
- | TArrow (inputs, output) ->
- "Arrow"
- ^ String.concat ""
- (List.map (ty_to_simple_name generics) (inputs @ [ output ]))
in
let flatten_name (name : string list) : string =
match !backend with
@@ -747,17 +679,22 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) :
string =
- (* TODO: provisional: we concatenate the trait impl name (which is its type)
- with the trait decl name *)
- let trait_decl =
- let name = trait_decl.llbc_name in
- let name = get_type_name_no_suffix name ^ "Inst" in
- (* Remove the occurrences of '.' *)
- String.concat "" (String.split_on_char '.' name)
- in
+ (* We derive the trait impl name from the implemented trait.
+ For instance, if this implementation is an instance of `trait::Trait`
+ for `<foo::Foo, u32>`, we generate the name: "trait.TraitFooFooU32Inst".
+ Importantly, it is to be noted that the name is independent of the place
+ where the instance has been defined (it is indepedent of the file, etc.).
+ *)
let name =
- flatten_name (get_type_name trait_impl.llbc_name @ [ trait_decl ])
+ (* We need to lookup the LLBC definitions, to have the original instantiation *)
+ let trait_impl =
+ TraitImplId.Map.find trait_impl.def_id ctx.trait_impls_ctx.trait_impls
+ in
+ let params = trait_impl.generics in
+ let args = trait_impl.impl_trait.decl_generics in
+ name_with_generics_to_simple_name ctx trait_decl.llbc_name params args
in
+ let name = flatten_name name in
match !backend with
| FStar -> StringUtils.lowercase_first_letter name
| Coq | HOL4 | Lean -> name
@@ -1185,11 +1122,11 @@ let extract_arrow (fmt : F.formatter) () : unit =
let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
(inside : bool) (cg : const_generic) : unit =
match cg with
- | CGGlobal id ->
+ | CgGlobal id ->
let s = ctx_get_global id ctx in
F.pp_print_string fmt s
- | CGValue v -> ctx.fmt.extract_literal fmt inside v
- | CGVar id ->
+ | CgValue v -> ctx.fmt.extract_literal fmt inside v
+ | CgVar id ->
let s = ctx_get_const_generic_var id ctx in
F.pp_print_string fmt s
@@ -1492,8 +1429,9 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
extraction_ctx =
(* Lookup the builtin information, if there is *)
let open ExtractBuiltin in
- let sname = name_to_simple_name def.llbc_name in
- let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in
+ let info =
+ match_name_find_opt ctx.trans_ctx def.llbc_name (builtin_types_map ())
+ in
(* Register the filtering information, if there is *)
let ctx =
match info with
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index a07ad35a..9ae6ce86 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -58,6 +58,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
let can_diverge = ref false in
let is_rec = ref false in
let group_has_builtin_info = ref false in
+ let name_matcher_ctx : Charon.NameMatcher.ctx =
+ {
+ type_decls = m.type_decls;
+ global_decls = m.global_decls;
+ trait_decls = m.trait_decls;
+ }
+ in
(* We have some specialized knowledge of some library functions; we don't
have any more custom treatment than this, and these functions can be modeled
@@ -65,8 +72,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
way. *)
let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option =
let open ExtractBuiltin in
- let name = name_to_simple_name f.name in
- SimpleNameMap.find_opt name builtin_fun_effects_map
+ NameMatcherMap.find_opt name_matcher_ctx f.name builtin_fun_effects_map
in
(* JP: Why not use a reduce visitor here with a tuple of the values to be
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 5b2db90d..c2e47da9 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -80,7 +80,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
let regions = List.map (fun _ -> RErased) regions in
let types = List.map (fun (v : type_var) -> TVar v.index) types in
let const_generics =
- List.map (fun (v : const_generic_var) -> CGVar v.index) const_generics
+ List.map (fun (v : const_generic_var) -> CgVar v.index) const_generics
in
(* Annoying that we have to generate this substitution here *)
let r_subst _ = raise (Failure "Unexpected region") in
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 1e28fd4b..38620be0 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -321,7 +321,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
( ctx0,
None,
value_as_symbolic v.value,
- SymbolicAst.VaCGValue vid,
+ SymbolicAst.VaCgValue vid,
e )))
| CFnPtr _ -> raise (Failure "TODO"))
| Copy p ->
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 01216157..ffdce481 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -31,21 +31,26 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
type_decl list * fun_decl list =
let open ExtractBuiltin in
+ let ctx : Charon.NameMatcher.ctx =
+ {
+ type_decls = k.type_decls;
+ global_decls = k.global_decls;
+ trait_decls = k.trait_decls;
+ }
+ in
let is_opaque_fun (d : fun_decl) : bool =
- let sname = name_to_simple_name d.name in
d.body = None
(* Something to pay attention to: we must ignore trait method *declarations*
(which don't have a body but must not be considered as opaque) *)
&& (match d.kind with TraitMethodDecl _ -> false | _ -> true)
&& ((not filter_assumed)
- || (not (SimpleNameMap.mem sname builtin_globals_map))
- && not (SimpleNameMap.mem sname (builtin_funs_map ())))
+ || (not (NameMatcherMap.mem ctx d.name builtin_globals_map))
+ && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ())))
in
let is_opaque_type (d : type_decl) : bool =
- let sname = name_to_simple_name d.name in
d.kind = Opaque
&& ((not filter_assumed)
- || not (SimpleNameMap.mem sname (builtin_types_map ())))
+ || not (NameMatcherMap.mem ctx d.name (builtin_types_map ())))
in
(* Note that by checking the function bodies we also the globals *)
( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls),
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index e6686951..a7ec9336 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -128,9 +128,9 @@ let type_id_to_string (env : fmt_env) (id : type_id) : string =
(* TODO: duplicates Charon.PrintTypes.const_generic_to_string *)
let const_generic_to_string (env : fmt_env) (cg : const_generic) : string =
match cg with
- | CGGlobal id -> global_decl_id_to_string env id
- | CGVar id -> const_generic_var_id_to_string env id
- | CGValue lit -> literal_to_string lit
+ | CgGlobal id -> global_decl_id_to_string env id
+ | CgVar id -> const_generic_var_id_to_string env id
+ | CgValue lit -> literal_to_string lit
let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
match ty with
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 5f92d18a..06270621 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -111,7 +111,7 @@ let ty_substitute (subst : subst) (ty : ty) : ty =
object
inherit [_] map_ty
method! visit_TVar _ var_id = subst.ty_subst var_id
- method! visit_CGVar _ var_id = subst.cg_subst var_id
+ method! visit_CgVar _ var_id = subst.cg_subst var_id
method! visit_Clause _ id = subst.tr_subst id
method! visit_Self _ = subst.tr_self
end
diff --git a/compiler/StringUtils.ml b/compiler/StringUtils.ml
index 161df27b..3ab4e808 100644
--- a/compiler/StringUtils.ml
+++ b/compiler/StringUtils.ml
@@ -1,111 +1 @@
-(** Utilities to work on strings, character per character.
-
- They operate on ASCII strings, and are used by the project to convert
- Rust names: Rust names are not fancy, so it shouldn't be a problem.
-
- Rk.: the poor support of OCaml for char manipulation is really annoying...
- *)
-
-let code_0 = 48
-let code_9 = 57
-let code_A = 65
-let code_Z = 90
-let code_a = 97
-let code_z = 122
-
-let is_lowercase_ascii (c : char) : bool =
- let c = Char.code c in
- code_a <= c && c <= code_z
-
-let is_uppercase_ascii (c : char) : bool =
- let c = Char.code c in
- code_A <= c && c <= code_Z
-
-let is_letter_ascii (c : char) : bool =
- is_lowercase_ascii c || is_uppercase_ascii c
-
-let is_digit_ascii (c : char) : bool =
- let c = Char.code c in
- code_0 <= c && c <= code_9
-
-let lowercase_ascii = Char.lowercase_ascii
-let uppercase_ascii = Char.uppercase_ascii
-
-(** Using buffers as per:
- {{: https://stackoverflow.com/questions/29957418/how-to-convert-char-list-to-string-in-ocaml} stackoverflow}
- *)
-let string_of_chars (chars : char list) : string =
- let buf = Buffer.create (List.length chars) in
- List.iter (Buffer.add_char buf) chars;
- Buffer.contents buf
-
-let string_to_chars (s : string) : char list =
- let length = String.length s in
- let rec apply i =
- if i = length then [] else String.get s i :: apply (i + 1)
- in
- apply 0
-
-(** This operates on ASCII *)
-let to_camel_case (s : string) : string =
- (* Note that we rebuild the string in reverse order *)
- let apply ((prev_is_under, acc) : bool * char list) (c : char) :
- bool * char list =
- if c = '_' then (true, acc)
- else
- let c = if prev_is_under then uppercase_ascii c else c in
- (false, c :: acc)
- in
- let _, chars = List.fold_left apply (true, []) (string_to_chars s) in
- string_of_chars (List.rev chars)
-
-(** This operates on ASCII *)
-let to_snake_case (s : string) : string =
- (* Note that we rebuild the string in reverse order *)
- let apply ((prev_is_low, prev_is_digit, acc) : bool * bool * char list)
- (c : char) : bool * bool * char list =
- let acc =
- if c = '_' then acc
- else if prev_is_digit then if is_letter_ascii c then '_' :: acc else acc
- else if prev_is_low then
- if (is_lowercase_ascii c || is_digit_ascii c) && c <> '_' then acc
- else '_' :: acc
- else acc
- in
- let prev_is_low = is_lowercase_ascii c in
- let prev_is_digit = is_digit_ascii c in
- let c = lowercase_ascii c in
- (prev_is_low, prev_is_digit, c :: acc)
- in
- let _, _, chars =
- List.fold_left apply (false, false, []) (string_to_chars s)
- in
- string_of_chars (List.rev chars)
-
-(** Applies a map operation.
-
- This is very inefficient, but shouldn't be used much.
- *)
-let map (f : char -> string) (s : string) : string =
- let sl = List.map f (string_to_chars s) in
- let sl = List.map string_to_chars sl in
- string_of_chars (List.concat sl)
-
-let capitalize_first_letter (s : string) : string =
- let s = string_to_chars s in
- let s = match s with [] -> s | c :: s' -> uppercase_ascii c :: s' in
- string_of_chars s
-
-let lowercase_first_letter (s : string) : string =
- let s = string_to_chars s in
- let s = match s with [] -> s | c :: s' -> lowercase_ascii c :: s' in
- string_of_chars s
-
-(** Unit tests *)
-let _ =
- assert (to_camel_case "hello_world" = "HelloWorld");
- assert (to_snake_case "HelloWorld36Hello" = "hello_world36_hello");
- assert (to_snake_case "HELLO" = "hello");
- assert (to_snake_case "T1" = "t1");
- assert (to_camel_case "list" = "List");
- assert (to_snake_case "is_cons" = "is_cons")
+include Charon.StringUtils
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 01509dec..73e7f71d 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -29,7 +29,7 @@ let st_substitute_visitor (subst : subst) =
(* We should never get here because we reimplemented [visit_TypeVar] *)
raise (Failure "Unexpected")
- method! visit_CGVar _ id = subst.cg_subst id
+ method! visit_CgVar _ id = subst.cg_subst id
method! visit_const_generic_var_id _ _ =
(* We should never get here because we reimplemented [visit_Var] *)
@@ -71,7 +71,7 @@ let erase_regions_subst : subst =
{
r_subst = (fun _ -> RErased);
ty_subst = (fun vid -> TVar vid);
- cg_subst = (fun id -> CGVar id);
+ cg_subst = (fun id -> CgVar id);
tr_subst = (fun id -> Clause id);
tr_self = Self;
}
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 7c5d28a7..c9820ba5 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -240,7 +240,7 @@ and value_aggregate =
| VaSingleValue of typed_value (** Regular case *)
| VaArray of typed_value list
(** This is used when introducing array aggregates *)
- | VaCGValue of const_generic_var_id
+ | VaCgValue of const_generic_var_id
(** This is used when evaluating a const generic value: in the interpreter,
we introduce a fresh symbolic value. *)
| VaTraitConstValue of trait_ref * generic_args * string
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7dad54e1..69ff4df1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2475,7 +2475,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
{ struct_id = TAssumed TArray; init = None; updates = values }
in
{ e = StructUpdate su; ty = var.ty }
- | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty }
+ | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
| VaTraitConstValue (trait_ref, generics, const_name) ->
let type_infos = ctx.type_context.type_infos in
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
@@ -2726,7 +2726,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
let const_generics =
List.map
- (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index)
+ (fun (cg : T.const_generic_var) -> T.CgVar cg.T.index)
const_generics
in
let trait_refs =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index cf23fd44..271d19ad 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -477,8 +477,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
let types_map = builtin_types_map () in
List.map
(fun (def : Pure.type_decl) ->
- let sname = name_to_simple_name def.llbc_name in
- SimpleNameMap.find_opt sname types_map <> None)
+ match_name_find_opt ctx.trans_ctx def.llbc_name types_map <> None)
defs
in
@@ -545,9 +544,9 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
(* Check if it is a builtin global - if yes, we ignore it because we
map the definition to one in the standard library *)
let open ExtractBuiltin in
- let sname = name_to_simple_name global.name in
let extract =
- extract && SimpleNameMap.find_opt sname builtin_globals_map = None
+ extract
+ && match_name_find_opt ctx.trans_ctx global.name builtin_globals_map = None
in
if extract then
(* We don't wrap global declaration groups between calls to functions
@@ -661,8 +660,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
let funs_map = builtin_funs_map () in
List.map
(fun (trans : pure_fun_translation) ->
- let sname = name_to_simple_name trans.fwd.f.llbc_name in
- SimpleNameMap.find_opt sname funs_map <> None)
+ match_name_find_opt ctx.trans_ctx trans.fwd.f.llbc_name funs_map <> None)
pure_ls
in
@@ -755,8 +753,11 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
(* Check if the trait declaration is builtin, in which case we ignore it *)
let open ExtractBuiltin in
- let sname = name_to_simple_name trait_decl.llbc_name in
- if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then (
+ if
+ match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+ (builtin_trait_decls_map ())
+ = None
+ then (
let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl;
if extract_extra_info then
@@ -775,9 +776,11 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
(* Check if the trait implementation is builtin *)
let builtin_info =
let open ExtractBuiltin in
- let type_sname = name_to_simple_name trait_impl.llbc_name in
- let trait_sname = name_to_simple_name trait_decl.llbc_name in
- SimpleNamePairMap.find_opt (type_sname, trait_sname)
+ let trait_impl =
+ TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
+ in
+ match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+ trait_impl.impl_trait.decl_generics
(builtin_trait_impls_map ())
in
match builtin_info with
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index a974cdee..f251e169 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -1,6 +1,7 @@
(** Some utilities for the translation *)
open Contexts
+open ExtractName
(** The local logger *)
let log = Logging.translate_log
@@ -29,3 +30,50 @@ let trans_ctx_to_pure_fmt_env (ctx : trans_ctx) : PrintPure.fmt_env =
let name_to_string (ctx : trans_ctx) =
Print.Types.name_to_string (trans_ctx_to_fmt_env ctx)
+
+let match_name_find_opt (ctx : trans_ctx) (name : Types.name)
+ (m : 'a NameMatcherMap.t) : 'a option =
+ let open Charon.NameMatcher in
+ let open ExtractBuiltin in
+ let mctx : ctx =
+ {
+ type_decls = ctx.type_ctx.type_decls;
+ global_decls = ctx.global_ctx.global_decls;
+ trait_decls = ctx.trait_decls_ctx.trait_decls;
+ }
+ in
+ NameMatcherMap.find_opt mctx name m
+
+let match_name_with_generics_find_opt (ctx : trans_ctx) (name : Types.name)
+ (generics : Types.generic_args) (m : 'a NameMatcherMap.t) : 'a option =
+ let open Charon.NameMatcher in
+ let open ExtractBuiltin in
+ let mctx : ctx =
+ {
+ type_decls = ctx.type_ctx.type_decls;
+ global_decls = ctx.global_ctx.global_decls;
+ trait_decls = ctx.trait_decls_ctx.trait_decls;
+ }
+ in
+ NameMatcherMap.find_with_generics_opt mctx name generics m
+
+let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list =
+ let mctx : Charon.NameMatcher.ctx =
+ {
+ type_decls = ctx.type_ctx.type_decls;
+ global_decls = ctx.global_ctx.global_decls;
+ trait_decls = ctx.trait_decls_ctx.trait_decls;
+ }
+ in
+ name_to_simple_name mctx n
+
+let name_with_generics_to_simple_name (ctx : trans_ctx) (n : Types.name)
+ (p : Types.generic_params) (g : Types.generic_args) : string list =
+ let mctx : Charon.NameMatcher.ctx =
+ {
+ type_decls = ctx.type_ctx.type_decls;
+ global_decls = ctx.global_ctx.global_decls;
+ trait_decls = ctx.trait_decls_ctx.trait_decls;
+ }
+ in
+ name_with_generics_to_simple_name mctx n p g
diff --git a/compiler/dune b/compiler/dune
index 43ce86c8..39ad6260 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -10,7 +10,7 @@
(public_name aeneas) ;; The name as revealed to the projects importing this library
(preprocess
(pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries charon core_unix unionFind ocamlgraph)
+ (libraries charon core_unix unionFind ocamlgraph str)
(modules
AssociatedTypes
Assumed
@@ -24,6 +24,7 @@
Extract
ExtractBase
ExtractBuiltin
+ ExtractName
ExtractTypes
FunsAnalysis
Identifiers
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 10:04:29 +0000