Start adding integer functions to the Lean library

7 files changed, 447 insertions, 58 deletions

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 7196d2ec..ad8f2501 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -4,4 +4,4 @@ import Base.Primitives.Scalar
 import Base.Primitives.ArraySlice
 import Base.Primitives.Vec
 import Base.Primitives.Alloc
-import Base.Primitives.CoreOps
+import Base.Primitives.Core
diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/Core.lean
index 1736bfa6..f67da7d7 100644
--- a/backends/lean/Base/Primitives/CoreOps.lean
+++ b/backends/lean/Base/Primitives/Core.lean
@@ -4,7 +4,13 @@ import Base.Primitives.Base
 open Primitives
 open Result
 
-namespace core.ops
+namespace core
+
+/- Trait declaration: [core::convert::From] -/
+structure convert.From (Self T : Type) where
+  from_ : T → Result Self
+
+namespace ops -- core.ops
 
 namespace index -- core.ops.index
 
@@ -32,4 +38,6 @@ structure DerefMut (Self : Type) where
 
 end deref -- core.ops.deref
 
-end core.ops
+end ops -- core.ops
+
+end core
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 8de2b3f2..0ba538b7 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -2,6 +2,7 @@ import Lean
 import Lean.Meta.Tactic.Simp
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
+import Base.Primitives.Core
 import Base.Diverge.Base
 import Base.Progress.Base
 import Base.Arith.Int
@@ -1393,4 +1394,258 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
 @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by
   simp [eq_equiv]
 
+-- Conversions
+def core.convert.num.FromUsizeBool.from (b : Bool) : Usize :=
+  if b then 1#usize else 0#usize
+
+def core.convert.num.FromU8Bool.from (b : Bool) : U8 :=
+  if b then 1#u8 else 0#u8
+
+def core.convert.num.FromU16Bool.from (b : Bool) : U16 :=
+  if b then 1#u16 else 0#u16
+
+def core.convert.num.FromU32Bool.from (b : Bool) : U32 :=
+  if b then 1#u32 else 0#u32
+
+def core.convert.num.FromU64Bool.from (b : Bool) : U64 :=
+  if b then 1#u64 else 0#u64
+
+def core.convert.num.FromU128Bool.from (b : Bool) : U128 :=
+  if b then 1#u128 else 0#u128
+
+def core.convert.num.FromIsizeBool.from (b : Bool) : Isize :=
+  if b then 1#isize else 0#isize
+
+def core.convert.num.FromI8Bool.from (b : Bool) : I8 :=
+  if b then 1#i8 else 0#i8
+
+def core.convert.num.FromI16Bool.from (b : Bool) : I16 :=
+  if b then 1#i16 else 0#i16
+
+def core.convert.num.FromI32Bool.from (b : Bool) : I32 :=
+  if b then 1#i32 else 0#i32
+
+def core.convert.num.FromI64Bool.from (b : Bool) : I64 :=
+  if b then 1#i64 else 0#i64
+
+def core.convert.num.FromI128Bool.from (b : Bool) : I128 :=
+  if b then 1#i128 else 0#i128
+
+def core.convert.num.FromUsizeU8.from (x : U8) : Usize := sorry
+def core.convert.num.FromUsizeU16.from (x : U16) : Usize := sorry
+def core.convert.num.FromUsizeU32.from (x : U32) : Usize := sorry
+def core.convert.num.FromUsizeUsize.from (x : Usize) : Usize := sorry
+
+def core.convert.num.FromU8U8.from (x : U8) : U8 := sorry
+
+def core.convert.num.FromU16U8.from (x : U8) : U16 := sorry
+def core.convert.num.FromU16U16.from (x : U16) : U16 := sorry
+
+def core.convert.num.FromU32U8.from (x : U8) : U32 := sorry
+def core.convert.num.FromU32U16.from (x : U16) : U32 := sorry
+def core.convert.num.FromU32U32.from (x : U32) : U32 := sorry
+
+def core.convert.num.FromU64U8.from (x : U8) : U64 := sorry
+def core.convert.num.FromU64U16.from (x : U16) : U64 := sorry
+def core.convert.num.FromU64U32.from (x : U32) : U64 := sorry
+def core.convert.num.FromU64U64.from (x : U64) : U64 := sorry
+
+def core.convert.num.FromU128U8.from (x : U8) : U128 := sorry
+def core.convert.num.FromU128U16.from (x : U16) : U128 := sorry
+def core.convert.num.FromU128U32.from (x : U32) : U128 := sorry
+def core.convert.num.FromU128U64.from (x : U64) : U128 := sorry
+def core.convert.num.FromU128U128.from (x : U128) : U128 := sorry
+
+def core.convert.num.FromIsizeI8.from (x : I8) : Isize := sorry
+def core.convert.num.FromIsizeI16.from (x : I16) : Isize := sorry
+def core.convert.num.FromIsizeI32.from (x : I32) : Isize := sorry
+def core.convert.num.FromIsizeIsize.from (x : Isize) : Isize := sorry
+
+def core.convert.num.FromI8I8.from (x : I8) : I8 := sorry
+
+def core.convert.num.FromI16I8.from (x : I8) : I16 := sorry
+def core.convert.num.FromI16I16.from (x : I16) : I16 := sorry
+
+def core.convert.num.FromI32I8.from (x : I8) : I32 := sorry
+def core.convert.num.FromI32I16.from (x : I16) : I32 := sorry
+def core.convert.num.FromI32I32.from (x : I32) : I32 := sorry
+
+def core.convert.num.FromI64I8.from (x : I8) : I64 := sorry
+def core.convert.num.FromI64I16.from (x : I16) : I64 := sorry
+def core.convert.num.FromI64I32.from (x : I32) : I64 := sorry
+def core.convert.num.FromI64I64.from (x : I64) : I64 := sorry
+
+def core.convert.num.FromI128I8.from (x : I8) : I128 := sorry
+def core.convert.num.FromI128I16.from (x : I16) : I128 := sorry
+def core.convert.num.FromI128I32.from (x : I32) : I128 := sorry
+def core.convert.num.FromI128I64.from (x : I64) : I128 := sorry
+def core.convert.num.FromI128I128.from (x : I128) : I128 := sorry
+
+def core.convert.FromUsizeU8 : core.convert.From Usize U8 := {
+  from_ := fun x => ok (core.convert.num.FromUsizeU8.from x)
+}
+
+def core.convert.FromUsizeU16 : core.convert.From Usize U16 := {
+  from_ := fun x => ok (core.convert.num.FromUsizeU16.from x)
+}
+
+def core.convert.FromUsizeU32 : core.convert.From Usize U32 := {
+  from_ := fun x => ok (core.convert.num.FromUsizeU32.from x)
+}
+
+def core.convert.FromUsizeUsize : core.convert.From Usize Usize := {
+  from_ := fun x => ok (core.convert.num.FromUsizeUsize.from x)
+}
+
+def core.convert.FromU8U8 : core.convert.From U8 U8 := {
+  from_ := fun x => ok (core.convert.num.FromU8U8.from x)
+}
+
+def core.convert.FromU16U8 : core.convert.From U16 U8 := {
+  from_ := fun x => ok (core.convert.num.FromU16U8.from x)
+}
+
+def core.convert.FromU16U16 : core.convert.From U16 U16 := {
+  from_ := fun x => ok (core.convert.num.FromU16U16.from x)
+}
+
+def core.convert.FromU32U8 : core.convert.From U32 U8 := {
+  from_ := fun x => ok (core.convert.num.FromU32U8.from x)
+}
+
+def core.convert.FromU32U16 : core.convert.From U32 U16 := {
+  from_ := fun x => ok (core.convert.num.FromU32U16.from x)
+}
+
+def core.convert.FromU32U32 : core.convert.From U32 U32 := {
+  from_ := fun x => ok (core.convert.num.FromU32U32.from x)
+}
+
+def core.convert.FromU64U8 : core.convert.From U64 U8 := {
+  from_ := fun x => ok (core.convert.num.FromU64U8.from x)
+}
+
+def core.convert.FromU64U16 : core.convert.From U64 U16 := {
+  from_ := fun x => ok (core.convert.num.FromU64U16.from x)
+}
+
+def core.convert.FromU64U32 : core.convert.From U64 U32 := {
+  from_ := fun x => ok (core.convert.num.FromU64U32.from x)
+}
+
+def core.convert.FromU64U64 : core.convert.From U64 U64 := {
+  from_ := fun x => ok (core.convert.num.FromU64U64.from x)
+}
+
+def core.convert.FromU128U8 : core.convert.From U128 U8 := {
+  from_ := fun x => ok (core.convert.num.FromU128U8.from x)
+}
+
+def core.convert.FromU128U16 : core.convert.From U128 U16 := {
+  from_ := fun x => ok (core.convert.num.FromU128U16.from x)
+}
+
+def core.convert.FromU128U32 : core.convert.From U128 U32 := {
+  from_ := fun x => ok (core.convert.num.FromU128U32.from x)
+}
+
+def core.convert.FromU128U64 : core.convert.From U128 U64 := {
+  from_ := fun x => ok (core.convert.num.FromU128U64.from x)
+}
+
+def core.convert.FromU128U128 : core.convert.From U128 U128 := {
+  from_ := fun x => ok (core.convert.num.FromU128U128.from x)
+}
+
+def core.convert.FromIsizeI8 : core.convert.From Isize I8 := {
+  from_ := fun x => ok (core.convert.num.FromIsizeI8.from x)
+}
+
+def core.convert.FromIsizeI16 : core.convert.From Isize I16 := {
+  from_ := fun x => ok (core.convert.num.FromIsizeI16.from x)
+}
+
+def core.convert.FromIsizeI32 : core.convert.From Isize I32 := {
+  from_ := fun x => ok (core.convert.num.FromIsizeI32.from x)
+}
+
+def core.convert.FromIsizeIsize : core.convert.From Isize Isize := {
+  from_ := fun x => ok (core.convert.num.FromIsizeIsize.from x)
+}
+
+def core.convert.FromI8I8 : core.convert.From I8 I8 := {
+  from_ := fun x => ok (core.convert.num.FromI8I8.from x)
+}
+
+def core.convert.FromI16I8 : core.convert.From I16 I8 := {
+  from_ := fun x => ok (core.convert.num.FromI16I8.from x)
+}
+
+def core.convert.FromI16I16 : core.convert.From I16 I16 := {
+  from_ := fun x => ok (core.convert.num.FromI16I16.from x)
+}
+
+def core.convert.FromI32I8 : core.convert.From I32 I8 := {
+  from_ := fun x => ok (core.convert.num.FromI32I8.from x)
+}
+
+def core.convert.FromI32I16 : core.convert.From I32 I16 := {
+  from_ := fun x => ok (core.convert.num.FromI32I16.from x)
+}
+
+def core.convert.FromI32I32 : core.convert.From I32 I32 := {
+  from_ := fun x => ok (core.convert.num.FromI32I32.from x)
+}
+
+def core.convert.FromI64I8 : core.convert.From I64 I8 := {
+  from_ := fun x => ok (core.convert.num.FromI64I8.from x)
+}
+
+def core.convert.FromI64I16 : core.convert.From I64 I16 := {
+  from_ := fun x => ok (core.convert.num.FromI64I16.from x)
+}
+
+def core.convert.FromI64I32 : core.convert.From I64 I32 := {
+  from_ := fun x => ok (core.convert.num.FromI64I32.from x)
+}
+
+def core.convert.FromI64I64 : core.convert.From I64 I64 := {
+  from_ := fun x => ok (core.convert.num.FromI64I64.from x)
+}
+
+def core.convert.FromI128I8 : core.convert.From I128 I8 := {
+  from_ := fun x => ok (core.convert.num.FromI128I8.from x)
+}
+
+def core.convert.FromI128I16 : core.convert.From I128 I16 := {
+  from_ := fun x => ok (core.convert.num.FromI128I16.from x)
+}
+
+def core.convert.FromI128I32 : core.convert.From I128 I32 := {
+  from_ := fun x => ok (core.convert.num.FromI128I32.from x)
+}
+
+def core.convert.FromI128I64 : core.convert.From I128 I64 := {
+  from_ := fun x => ok (core.convert.num.FromI128I64.from x)
+}
+
+def core.convert.FromI128I128 : core.convert.From I128 I128 := {
+  from_ := fun x => ok (core.convert.num.FromI128I128.from x)
+}
+
+-- Leading zeros
+def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry
+def core.num.U8.leading_zeros (x : U8) : U32 := sorry
+def core.num.U16.leading_zeros (x : U16) : U32 := sorry
+def core.num.U32.leading_zeros (x : U32) : U32 := sorry
+def core.num.U64.leading_zeros (x : U64) : U32 := sorry
+def core.num.U128.leading_zeros (x : U128) : U32 := sorry
+
+def core.num.Isize.leading_zeros (x : Isize) : U32 := sorry
+def core.num.I8.leading_zeros (x : I8) : U32 := sorry
+def core.num.I16.leading_zeros (x : I16) : U32 := sorry
+def core.num.I32.leading_zeros (x : I32) : U32 := sorry
+def core.num.I64.leading_zeros (x : I64) : U32 := sorry
+def core.num.I128.leading_zeros (x : I128) : U32 := sorry
+
 end Primitives
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 6eeef772..8efb59fb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2644,14 +2644,19 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  (let name =
+  (let name, generics =
      if !Config.extract_external_name_patterns && not impl.is_local then
-       Some impl.llbc_name
-     else None
+       let decl_id = impl.impl_trait.trait_decl_id in
+       let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
+       let decl_ref = impl.llbc_impl_trait in
+       ( Some trait_decl.llbc_name,
+         Some (trait_decl.llbc_generics, decl_ref.decl_generics) )
+     else (None, None)
    in
    extract_comment_with_span ctx fmt
      [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
-     name impl.meta.span);
+     (* TODO: why option option for the generics? Looks like a bug in OCaml!? *)
+     name ?generics:(Some generics) impl.meta.span);
   F.pp_print_break fmt 0 0;
 
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 3ba8d11d..ac7a4a24 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -10,6 +10,22 @@ include ExtractName (* TODO: only open? *)
 
 let log = Logging.builtin_log
 
+let all_int_names =
+  [
+    "usize";
+    "u8";
+    "u16";
+    "u32";
+    "u64";
+    "u128";
+    "isize";
+    "i8";
+    "i16";
+    "i32";
+    "i64";
+    "i128";
+  ]
+
 (** Small utility to memoize some computations *)
 let mk_memoized (f : unit -> 'a) : unit -> 'a =
   let r = ref None in
@@ -215,6 +231,28 @@ let builtin_types_map = mk_memoized mk_builtin_types_map
 
 type builtin_fun_info = { extract_name : string } [@@deriving show]
 
+let int_and_smaller_list : (string * string) list =
+  let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in
+  let int_names = List.rev [ "i8"; "i16"; "i32"; "i64"; "i128" ] in
+  let rec compute_pairs l =
+    match l with
+    | [] -> []
+    | x :: l -> List.map (fun y -> (x, y)) (x :: l) @ compute_pairs l
+  in
+  [
+    (* Usize *)
+    ("usize", "u8");
+    ("usize", "u16");
+    ("usize", "u32");
+    ("usize", "usize");
+    (* Isize *)
+    ("isize", "i8");
+    ("isize", "i16");
+    ("isize", "i32");
+    ("isize", "isize");
+  ]
+  @ compute_pairs uint_names @ compute_pairs int_names
+
 (** The assumed functions.
 
     The optional list of booleans is filtering information for the type
@@ -245,20 +283,7 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
       (pattern * bool list option * builtin_fun_info) list =
     List.map
       (fun ty -> mk_fun (rust_name ty) (Some (extract_name ty)) None)
-      [
-        "usize";
-        "u8";
-        "u16";
-        "u32";
-        "u64";
-        "u128";
-        "isize";
-        "i8";
-        "i16";
-        "i32";
-        "i64";
-        "i128";
-      ]
+      all_int_names
   in
   [
     mk_fun "core::mem::replace" None None;
@@ -353,6 +378,32 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
              (fun ty ->
                StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op))
          [ "add"; "sub"; "mul"; "div"; "rem" ])
+  (* From<INT, bool> *)
+  @ mk_scalar_fun
+      (fun ty ->
+        "core::convert::num::{core::convert::From<" ^ ty ^ ", bool>}::from")
+      (fun ty ->
+        "core.convert.num.From"
+        ^ StringUtils.capitalize_first_letter ty
+        ^ "Bool.from")
+  (* From<INT, INT> *)
+  @ List.map
+      (fun (big, small) ->
+        mk_fun
+          ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
+         ^ ">}::from")
+          (Some
+             ("core.convert.num.From"
+             ^ StringUtils.capitalize_first_letter big
+             ^ StringUtils.capitalize_first_letter small
+             ^ ".from"))
+          None)
+      int_and_smaller_list
+  (* Leading zeros *)
+  @ mk_scalar_fun
+      (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
+      (fun ty ->
+        "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros")
 
 let mk_builtin_funs_map () =
   let m =
@@ -370,36 +421,44 @@ let builtin_funs_map = mk_memoized mk_builtin_funs_map
 type effect_info = { can_fail : bool; stateful : bool }
 
 let builtin_fun_effects =
-  let int_names =
-    [
-      "usize";
-      "u8";
-      "u16";
-      "u32";
-      "u64";
-      "u128";
-      "isize";
-      "i8";
-      "i16";
-      "i32";
-      "i64";
-      "i128";
-    ]
-  in
   let int_ops =
     [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ]
   in
   let int_funs =
     List.map
       (fun int_name ->
+        List.map (fun op -> "core::num::" ^ "{" ^ int_name ^ "}::" ^ op) int_ops)
+      all_int_names
+    @ List.map
+        (fun op ->
+          List.map
+            (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op)
+            all_int_names)
+        [ "add"; "sub"; "mul"; "div"; "rem" ]
+    (* From<INT, bool> *)
+    @ [
+        List.map
+          (fun int_name ->
+            "core::convert::num::{core::convert::From<" ^ int_name
+            ^ ", bool>}::from")
+          all_int_names;
+      ]
+    (* From<INT, INT> *)
+    @ [
+        List.map
+          (fun (big, small) ->
+            "core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
+            ^ ">}::from")
+          int_and_smaller_list;
+      ]
+    (* Leading zeros *)
+    @ [
         List.map
-          (fun op ->
-            "core::num::" ^ "{"
-            ^ StringUtils.capitalize_first_letter int_name
-            ^ "}::" ^ op)
-          int_ops)
-      int_names
+          (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
+          all_int_names;
+      ]
   in
+
   let int_funs = List.concat int_funs in
   let no_fail_no_state_funs =
     [
@@ -454,7 +513,9 @@ type builtin_trait_decl_info = {
 let builtin_trait_decls_info () =
   let mk_trait (rust_name : string) ?(extract_name : string option = None)
       ?(parent_clauses : string list = []) ?(types : string list = [])
-      ?(methods : string list = []) () : builtin_trait_decl_info =
+      ?(methods : string list = [])
+      ?(methods_with_extract : (string * string) list option = None) () :
+      builtin_trait_decl_info =
     let rust_name = parse_pattern rust_name in
     let extract_name =
       match extract_name with
@@ -482,16 +543,22 @@ let builtin_trait_decls_info () =
       List.map mk_type types
     in
     let methods =
-      let mk_method item_name =
-        (* TODO: factor out with builtin_funs_info *)
-        let basename =
-          if !record_fields_short_names then item_name
-          else extract_name ^ "_" ^ item_name
-        in
-        let fwd = { extract_name = basename } in
-        (item_name, fwd)
-      in
-      List.map mk_method methods
+      match methods_with_extract with
+      | None ->
+          let mk_method item_name =
+            (* TODO: factor out with builtin_funs_info *)
+            let basename =
+              if !record_fields_short_names then item_name
+              else extract_name ^ "_" ^ item_name
+            in
+            let fwd = { extract_name = basename } in
+            (item_name, fwd)
+          in
+          List.map mk_method methods
+      | Some methods ->
+          List.map
+            (fun (item_name, extract_name) -> (item_name, { extract_name }))
+            methods
     in
     {
       rust_name;
@@ -531,6 +598,10 @@ let builtin_trait_decls_info () =
           "index_mut";
         ]
       ();
+    (* From *)
+    mk_trait "core::convert::From"
+      ~methods_with_extract:(Some [ ("from", "from_") ])
+      ();
   ]
 
 let mk_builtin_trait_decls_map () =
@@ -602,6 +673,30 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
       ~filter:(Some [ true; true; false ])
       ();
   ]
+  (* From<INT, bool> *)
+  @ List.map
+      (fun ty ->
+        fmt
+          ("core::convert::From<" ^ ty ^ ", bool>")
+          ~extract_name:
+            (Some
+               ("core.convert.From"
+               ^ StringUtils.capitalize_first_letter ty
+               ^ "Bool"))
+          ())
+      all_int_names
+  (* From<INT, INT> *)
+  @ List.map
+      (fun (big, small) ->
+        fmt
+          ("core::convert::From<" ^ big ^ ", " ^ small ^ ">")
+          ~extract_name:
+            (Some
+               ("core.convert.From"
+               ^ StringUtils.capitalize_first_letter big
+               ^ StringUtils.capitalize_first_letter small))
+          ())
+      int_and_smaller_list
 
 let mk_builtin_trait_impls_map () =
   let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 1c3657a3..c2eb8da0 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1141,7 +1141,9 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
   F.pp_close_box fmt ()
 
 let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
-    (sl : string list) (name : Types.name option) (span : Meta.span) : unit =
+    (sl : string list) (name : Types.name option)
+    ?(generics : (Types.generic_params * Types.generic_args) option = None)
+    (span : Meta.span) : unit =
   let file = match span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
@@ -1151,10 +1153,15 @@ let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
     ^ loc_to_string span.end_loc
   in
   let name =
-    match name with
-    | None -> []
-    | Some name ->
+    match (name, generics) with
+    | None, _ -> []
+    | Some name, None ->
         [ "Name pattern: " ^ name_to_pattern_string ctx.trans_ctx name ]
+    | Some name, Some (params, args) ->
+        [
+          "Name pattern: "
+          ^ name_with_generics_to_pattern_string ctx.trans_ctx name params args;
+        ]
   in
   extract_comment fmt (sl @ [ span ] @ name)
 
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index 3e4c7375..688cbe34 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -91,3 +91,22 @@ let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string =
   in
   let pat = Charon.NameMatcher.name_to_pattern mctx c n in
   Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat
+
+let name_with_generics_to_pattern_string (ctx : trans_ctx) (n : Types.name)
+    (params : Types.generic_params) (args : Types.generic_args) : string =
+  let mctx : Charon.NameMatcher.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 c : Charon.NameMatcher.to_pat_config =
+    { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let pat =
+    Charon.NameMatcher.name_with_generics_to_pattern mctx c params n args
+  in
+  Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat