Fix generic type constraints naming bug.

hacspec · Dec 11, 2024 · dbd8432 · dbd8432
1 parent 18ac15e
commit dbd8432
Show file tree

Hide file tree

Showing 3 changed files with 59 additions and 3 deletions.
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
@@ -226,9 +226,14 @@ module Make (F : Features.T) = struct
             ((enabled, s) : bool * (string, string) Hashtbl.t) gc =
           match gc with
           | GCType { goal; name } when enabled ->
-              let data = "i" ^ Int.to_string (Hashtbl.length s) in
-              let _ = Hashtbl.add s ~key:name ~data in
-              GCType { goal; name = data }
+              let value = Hashtbl.find s name in
+              let new_name =
+                Option.value_or_thunk value ~default:(fun () ->
+                    let data = "i" ^ Int.to_string (Hashtbl.length s) in
+                    let _ = Hashtbl.add s ~key:name ~data in
+                    data)
+              in
+              GCType { goal; name = new_name }
           | _ -> super#visit_generic_constraint (enabled, s) gc
 
         method! visit_trait_item (_, s) = super#visit_trait_item (true, s)

diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -37,6 +37,36 @@ type t_Defaults (v_T: Type0) (v_N: usize) = | Defaults : t_Array v_T v_N -> t_De
 
 let f (_: t_Defaults Prims.unit (sz 2)) : Prims.unit = ()
 '''
+"Generics.Impl_generics.fst" = '''
+module Generics.Impl_generics
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Test = | Test : t_Test
+
+let impl__Test__set_alpn_protocols
+      (#v_S #impl_995885649_: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Convert.t_AsRef v_S string)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i3:
+          Core.Iter.Traits.Collect.t_IntoIterator impl_995885649_)
+      (self: t_Test)
+      (v__protocols: impl_995885649_)
+    : Core.Result.t_Result Prims.unit Prims.unit =
+  Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit Prims.unit
+
+let impl__Test__set_ciphersuites
+      (#v_S #impl_995885649_: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Convert.t_AsRef v_S string)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i3:
+          Core.Iter.Traits.Collect.t_IntoIterator impl_995885649_)
+      (self: t_Test)
+      (ciphers: impl_995885649_)
+    : Core.Result.t_Result Prims.unit Prims.unit =
+  Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit Prims.unit
+'''
 "Generics.fst" = '''
 module Generics
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

diff --git a/tests/generics/src/lib.rs b/tests/generics/src/lib.rs
@@ -51,3 +51,24 @@ mod defaults_generics {
     struct Defaults<T = (), const N: usize = 2>([T; N]);
     fn f(_: Defaults) {}
 }
+
+/// See https://github.com/hacspec/hax/issues/1176
+mod impl_generics {
+    struct Test();
+
+    impl Test {
+        fn set_ciphersuites<S>(&self, ciphers: impl IntoIterator<Item = S>) -> Result<(), ()>
+        where
+            S: AsRef<str>,
+        {
+            Ok(())
+        }
+
+        fn set_alpn_protocols<S>(&self, _protocols: impl IntoIterator<Item = S>) -> Result<(), ()>
+        where
+            S: AsRef<str>,
+        {
+            Ok(())
+        }
+    }
+}