From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 20 Nov 2023 21:58:25 +0100
Subject: Use the name matcher implemented in Charon

---
 compiler/ExtractName.ml | 177 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 177 insertions(+)
 create mode 100644 compiler/ExtractName.ml

(limited to 'compiler/ExtractName.ml')

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
+*)
-- 
cgit v1.2.3


From dcd34ceed0c52738b1bb8139e7130db9bad1a774 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 10:22:51 +0100
Subject: Fix issues with the builtin names

---
 compiler/ExtractName.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 4f5ca0d1..6d50ed73 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -35,7 +35,7 @@ end
  *)
 let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
     string list =
-  let c = { tgt_kind = TkName } in
+  let c = { tgt = TkName } in
   let is_var (g : generic_arg) : bool =
     match g with
     | GExpr (EVar _) -> true
@@ -83,11 +83,13 @@ let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
    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 c : to_pat_config = { tgt = TkName } in
+  pattern_to_extract_name false (name_to_pattern ctx c 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)
+  let c : to_pat_config = { tgt = TkName } in
+  pattern_to_extract_name true (name_with_generics_to_pattern ctx c n p g)
 
 (*
   (* Prepare a name.
-- 
cgit v1.2.3


From 66e05354d0b5669f010aa6ebcdcd65437d6e2e35 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 18:57:31 +0100
Subject: Improve the generation of parent clause names

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

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 6d50ed73..f7177223 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -82,14 +82,30 @@ 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 =
+let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) :
+    string list =
   let c : to_pat_config = { tgt = TkName } in
-  pattern_to_extract_name false (name_to_pattern ctx c n)
+  pattern_to_extract_name is_trait_impl (name_to_pattern ctx c n)
 
-let name_with_generics_to_simple_name (ctx : ctx) (n : Types.name)
+(** If the [prefix] is Some, we attempt to remove the common prefix
+    between [prefix] and [name] from [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
-  pattern_to_extract_name true (name_with_generics_to_pattern ctx c n p g)
+  let name = name_with_generics_to_pattern ctx c name p 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
+        in
+        let _, _, name = pattern_common_prefix prefix name in
+        name
+  in
+  pattern_to_extract_name is_trait_impl name
 
 (*
   (* Prepare a name.
-- 
cgit v1.2.3


From ba66f35a0e196c17757e06187cf2563abec253e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 22 Nov 2023 09:09:46 +0100
Subject: Improve further the generation of parent clause/trait clause names

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

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index f7177223..0943aefe 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -2,6 +2,8 @@
 
 open Charon.NameMatcher
 
+let log = Logging.extract_log
+
 module NameMatcherMap = struct
   type 'a t = (pattern * 'a) list
 
-- 
cgit v1.2.3


From 724ff98309444537cf03ba7ccab06d432e2eb376 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 22 Nov 2023 11:14:13 +0100
Subject: Use NameMatcher.NameMatcherMap instead of associative lists

---
 compiler/ExtractName.ml | 21 ++++++++-------------
 1 file changed, 8 insertions(+), 13 deletions(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 0943aefe..94222ae1 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -5,29 +5,24 @@ open Charon.NameMatcher
 let log = Logging.extract_log
 
 module NameMatcherMap = struct
-  type 'a t = (pattern * 'a) list
+  module NMM = NameMatcherMap
+
+  type 'a t = 'a NMM.t
 
   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
+    NMM.find_opt ctx config name m
 
   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
+    NMM.find_with_generics_opt ctx config name g m
 
   let mem (ctx : ctx) (name : Types.name) (m : 'a t) : bool =
-    find_opt ctx name m <> None
+    NMM.mem ctx config name m
 
-  let of_list (ls : (pattern * 'a) list) : 'a t = ls
+  let of_list (ls : (pattern * 'a) list) : 'a t = NMM.of_list ls
+  let to_string = NMM.to_string
 end
 
 (** Helper to convert name patterns to names for extraction.
-- 
cgit v1.2.3


From 5c3a7986a818446cbf008a87f57b2eb51e0bf861 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 22 Nov 2023 11:47:48 +0100
Subject: Cleanup a bit

---
 compiler/ExtractName.ml | 87 -------------------------------------------------
 1 file changed, 87 deletions(-)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 94222ae1..41c81207 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -103,90 +103,3 @@ let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
         name
   in
   pattern_to_extract_name is_trait_impl name
-
-(*
-  (* 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
-*)
-- 
cgit v1.2.3


From 1b446285bbbe356ead7c0e521799b35020f08147 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 Nov 2023 17:04:26 +0100
Subject: Make a minor update in ExtractName.pattern_to_extract_name

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

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 41c81207..c0a23080 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -61,7 +61,10 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
               | TArray -> "Array"
               | TSlice -> "Slice"
             else expr_to_string c ty
-        | ERef _ | EVar _ -> raise (Failure ""))
+        | ERef _ | EVar _ ->
+            (* We simply convert the pattern to a string. This is not very
+               satisfying but we should rarely get there. *)
+            expr_to_string c ty)
   in
   let rec pattern_to_string (n : pattern) : string list =
     match n with
-- 
cgit v1.2.3


From 1c8187d7f4129e09f23d3b5caf33938a0c91ea77 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 Nov 2023 17:38:44 +0100
Subject: Add the alloc::string::String type in the builtins

---
 compiler/ExtractName.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'compiler/ExtractName.ml')

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index c0a23080..a916bffb 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -76,6 +76,7 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
   in
   pattern_to_string name
 
+let pattern_to_type_extract_name = pattern_to_extract_name false
 let pattern_to_fun_extract_name = pattern_to_extract_name false
 let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
 
-- 
cgit v1.2.3


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