From 054d7256ed90f752ae6b39ebba608f89076d38e7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 29 Nov 2023 17:33:52 +0100
Subject: Update the code following changes in the NameMatcher

---
 compiler/ExtractName.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index a916bffb..2ccd4af6 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -3,13 +3,14 @@
 open Charon.NameMatcher
 
 let log = Logging.extract_log
+let match_with_trait_decl_refs = true
 
 module NameMatcherMap = struct
   module NMM = NameMatcherMap
 
   type 'a t = 'a NMM.t
 
-  let config = { map_vars_to_vars = true }
+  let config = { map_vars_to_vars = true; match_with_trait_decl_refs }
 
   let find_opt (ctx : ctx) (name : Types.name) (m : 'a t) : 'a option =
     NMM.find_opt ctx config name m
@@ -85,7 +86,9 @@ let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
    consistent with the extraction names we derive from the Rust names *)
 let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) :
     string list =
-  let c : to_pat_config = { tgt = TkName } in
+  let c : to_pat_config =
+    { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
   pattern_to_extract_name is_trait_impl (name_to_pattern ctx c n)
 
 (** If the [prefix] is Some, we attempt to remove the common prefix
@@ -93,15 +96,17 @@ let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) :
 let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
     ?(prefix : Types.name option = None) (name : Types.name)
     (p : Types.generic_params) (g : Types.generic_args) : string list =
-  let c : to_pat_config = { tgt = TkName } in
-  let name = name_with_generics_to_pattern ctx c name p g in
+  let c : to_pat_config =
+    { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let name = name_with_generics_to_pattern ctx c p name g in
   let name =
     match prefix with
     | None -> name
     | Some prefix ->
         let prefix =
-          name_with_generics_to_pattern ctx c prefix
-            TypesUtils.empty_generic_params TypesUtils.empty_generic_args
+          name_with_generics_to_pattern ctx c TypesUtils.empty_generic_params
+            prefix TypesUtils.empty_generic_args
         in
         let _, _, name = pattern_common_prefix prefix name in
         name
-- 
cgit v1.2.3


From 60ce69b83cbd749781543bb16becb5357f0e1a0a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 5 Dec 2023 15:00:46 +0100
Subject: Update following changes in Charon

---
 compiler/ExtractName.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 2ccd4af6..4c1ffb46 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -62,7 +62,7 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
               | TArray -> "Array"
               | TSlice -> "Slice"
             else expr_to_string c ty
-        | ERef _ | EVar _ ->
+        | ERef _ | EVar _ | EArrow _ | ERawPtr _ ->
             (* We simply convert the pattern to a string. This is not very
                satisfying but we should rarely get there. *)
             expr_to_string c ty)
@@ -108,7 +108,7 @@ let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
           name_with_generics_to_pattern ctx c TypesUtils.empty_generic_params
             prefix TypesUtils.empty_generic_args
         in
-        let _, _, name = pattern_common_prefix prefix name in
+        let _, _, name = pattern_common_prefix { equiv = true } prefix name in
         name
   in
   pattern_to_extract_name is_trait_impl name
-- 
cgit v1.2.3