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 +++++++++++------
 compiler/FunsAnalysis.ml  |  2 ++
 compiler/LlbcAstUtils.ml  |  2 ++
 compiler/TranslateCore.ml |  8 ++++++++
 4 files changed, 23 insertions(+), 6 deletions(-)

(limited to 'compiler')

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
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 9ae6ce86..2f950083 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -62,7 +62,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
       {
         type_decls = m.type_decls;
         global_decls = m.global_decls;
+        fun_decls = m.fun_decls;
         trait_decls = m.trait_decls;
+        trait_impls = m.trait_impls;
       }
     in
 
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index ffdce481..d3fac032 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -35,7 +35,9 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
     {
       type_decls = k.type_decls;
       global_decls = k.global_decls;
+      fun_decls = k.fun_decls;
       trait_decls = k.trait_decls;
+      trait_impls = k.trait_impls;
     }
   in
   let is_opaque_fun (d : fun_decl) : bool =
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index abf4fcf7..88438872 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -39,7 +39,9 @@ let match_name_find_opt (ctx : trans_ctx) (name : Types.name)
     {
       type_decls = ctx.type_ctx.type_decls;
       global_decls = ctx.global_ctx.global_decls;
+      fun_decls = ctx.fun_ctx.fun_decls;
       trait_decls = ctx.trait_decls_ctx.trait_decls;
+      trait_impls = ctx.trait_impls_ctx.trait_impls;
     }
   in
   NameMatcherMap.find_opt mctx name m
@@ -52,7 +54,9 @@ let match_name_with_generics_find_opt (ctx : trans_ctx) (name : Types.name)
     {
       type_decls = ctx.type_ctx.type_decls;
       global_decls = ctx.global_ctx.global_decls;
+      fun_decls = ctx.fun_ctx.fun_decls;
       trait_decls = ctx.trait_decls_ctx.trait_decls;
+      trait_impls = ctx.trait_impls_ctx.trait_impls;
     }
   in
   NameMatcherMap.find_with_generics_opt mctx name generics m
@@ -62,7 +66,9 @@ let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list =
     {
       type_decls = ctx.type_ctx.type_decls;
       global_decls = ctx.global_ctx.global_decls;
+      fun_decls = ctx.fun_ctx.fun_decls;
       trait_decls = ctx.trait_decls_ctx.trait_decls;
+      trait_impls = ctx.trait_impls_ctx.trait_impls;
     }
   in
   let is_trait_impl = false in
@@ -75,7 +81,9 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx)
     {
       type_decls = ctx.type_ctx.type_decls;
       global_decls = ctx.global_ctx.global_decls;
+      fun_decls = ctx.fun_ctx.fun_decls;
       trait_decls = ctx.trait_decls_ctx.trait_decls;
+      trait_impls = ctx.trait_impls_ctx.trait_impls;
     }
   in
   let is_trait_impl = true in
-- 
cgit v1.2.3