New snapshot with val interfaces for trait implementations.

cryspen · Nov 13, 2024 · 62ac3b8 · 62ac3b8
1 parent 58aaa19
commit 62ac3b8
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 20 deletions.
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
@@ -495,11 +495,11 @@ module Make (F : Features.T) = struct
     let bundle_of_item =
       Hashtbl.of_alist_exn (module ComparableItem) bundle_transforms
     in
-    let maybe_transform_item it =
-      match Hashtbl.find bundle_of_item it with
+    let maybe_transform_item item =
+      match Hashtbl.find bundle_of_item item with
       | Some (homogeneous_bundle, transform_bundle) ->
-          if homogeneous_bundle then [ it ] else transform_bundle it
-      | None -> [ it ]
+          if homogeneous_bundle then [ item ] else transform_bundle item
+      | None -> [ item ]
     in
     List.concat_map items ~f:maybe_transform_item
 

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -1640,7 +1640,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                       generics =
                         U.concat_generics (c_generics generics)
                           (c_generics item.generics);
-                      body = c_expr body;
+                      body = c_body body;
                       params;
                       safety = csafety safety;
                     }
@@ -1650,7 +1650,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                       name = item_def_id;
                       generics = c_generics generics;
                       (* does that make sense? can we have `const<T>`? *)
-                      body = c_expr e;
+                      body = c_body e;
                       params = [];
                       safety = Safe;
                     }

diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
@@ -39,23 +39,13 @@ type t_Bar = | Bar : t_Bar
 /// dropped. This might be a bit surprising: see
 /// https://github.com/hacspec/hax/issues/616.
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Convert.t_From t_Bar Prims.unit =
-  {
-    f_from_pre = (fun ((): Prims.unit) -> true);
-    f_from_post = (fun ((): Prims.unit) (out: t_Bar) -> true);
-    f_from = fun ((): Prims.unit) -> Bar <: t_Bar
-  }
-
-val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
+val impl:Core.Convert.t_From t_Bar Prims.unit
 
 /// If you need to drop the body of a method, please hoist it:
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Convert.t_From t_Bar u8 =
-  {
-    f_from_pre = (fun (x: u8) -> true);
-    f_from_post = (fun (x: u8) (out: t_Bar) -> true);
-    f_from = fun (x: u8) -> from__from x
-  }
+val impl_1:Core.Convert.t_From t_Bar u8
+
+val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
 /// This item contains unsafe blocks and raw references, two features
 /// not supported by hax. Thanks to the `-i` flag and the `+:`