Merge pull request #1114 from hacspec/val-instance

feat(engine) Extract vals for trait impls in interface only mode.

engine/backends/fstar/fstar_backend.ml

@@ -1471,8 +1471,19 @@ struct
         in
         let body = F.term @@ F.AST.Record (None, fields) in
         let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in
-        F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ]
-        @@ F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ])
+        let has_type =
+          List.exists items ~f:(fun { ii_v; _ } ->
+              match ii_v with IIType _ -> true | _ -> false)
+        in
+        let impl_val = ctx.interface_mode && not has_type in
+        let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in
+        if impl_val then
+          let generics_binders = List.map ~f:FStarBinder.to_binder generics in
+          let val_type = F.term @@ F.AST.Product (generics_binders, typ) in
+          let v = F.AST.Val (name, val_type) in
+          (F.decls ~fsti:true ~attrs:[ tcinst ] @@ v)
+          @ F.decls ~fsti:false ~attrs:[ tcinst ] let_impl
+        else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl
     | Quote { quote; _ } ->
         let fstar_opts =
           Attrs.find_unique_attr e.attrs ~f:(function

engine/lib/dependencies.ml

@@ -412,7 +412,7 @@ module Make (F : Features.T) = struct
       List.map ~f bundles
     in
 
-    let transform (bundle : item list) it =
+    let transform (bundle : item list) =
       let ns : Concrete_ident.t =
         Concrete_ident.Create.fresh_module ~from:(List.map ~f:ident_of bundle)
       in
@@ -473,21 +473,33 @@ module Make (F : Features.T) = struct
         let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in
         (U.Mappers.rename_concrete_idents renamer)#visit_item ExprLevel
       in
-      shallow_copy rename variants_renamings it
+      fun it -> shallow_copy rename variants_renamings it
     in
-    let maybe_transform_item it =
-      match
-        List.find
-          ~f:(fun bundle -> List.mem bundle it ~equal:[%eq: item])
-          mut_rec_bundles
-      with
-      | Some bundle ->
-          if
-            List.map ~f:ident_of bundle
-            |> ItemGraph.MutRec.Bundle.homogeneous_namespace
-          then [ it ]
-          else transform bundle it
-      | None -> [ it ]
+    let bundle_transforms =
+      List.concat_map mut_rec_bundles ~f:(fun bundle ->
+          let bundle_value =
+            ( List.map ~f:ident_of bundle
+              |> ItemGraph.MutRec.Bundle.homogeneous_namespace,
+              transform bundle )
+          in
+          List.map bundle ~f:(fun item -> (item, bundle_value)))
+    in
+    let module ComparableItem = struct
+      module T = struct
+        type t = item [@@deriving sexp_of, compare, hash]
+      end
+
+      include T
+      include Comparable.Make (T)
+    end in
+    let bundle_of_item =
+      Hashtbl.of_alist_exn (module ComparableItem) bundle_transforms
+    in
+    let maybe_transform_item item =
+      match Hashtbl.find bundle_of_item item with
+      | Some (homogeneous_bundle, transform_bundle) ->
+          if homogeneous_bundle then [ item ] else transform_bundle item
+      | None -> [ item ]
     in
     List.concat_map items ~f:maybe_transform_item
 

engine/lib/import_thir.ml

@@ -1642,7 +1642,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;
                     }
@@ -1652,7 +1652,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;
                     }
@@ -1681,6 +1681,11 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
             ~f:(fun { attributes; _ } -> not (should_skip attributes))
             items
         in
+        let has_type =
+          List.exists items ~f:(fun item ->
+              match item.kind with Type _ -> true | _ -> false)
+        in
+        let c_e = if has_type then c_expr else c_body in
         mk
         @@ Impl
              {
@@ -1711,9 +1716,8 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                                  [ U.make_unit_param span ]
                                else List.map ~f:(c_param item.span) params
                              in
-                             IIFn { body = c_expr body; params }
-                         | Const (_ty, e) ->
-                             IIFn { body = c_expr e; params = [] }
+                             IIFn { body = c_e body; params }
+                         | Const (_ty, e) -> IIFn { body = c_e e; params = [] }
                          | Type { ty; parent_bounds } ->
                              IIType
                                {

test-harness/src/snapshots/toolchain__interface-only into-fstar.snap

@@ -35,27 +35,27 @@ open FStar.Mul
 
 type t_Bar = | Bar : t_Bar
 
+type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global }
+
+type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
+
 /// Non-inherent implementations are extracted, their bodies are not
 /// 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 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]
+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)
 
-/// 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_2 (#v_T: Type0) : Core.Convert.t_From (t_Holder v_T) Prims.unit
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit
 
 /// This item contains unsafe blocks and raw references, two features
 /// not supported by hax. Thanks to the `-i` flag and the `+:`

tests/cli/interface-only/src/lib.rs

@@ -45,3 +45,23 @@ impl From<u8> for Bar {
         from(x)
     }
 }
+
+pub struct Holder<T> {
+    pub(crate) value: Vec<T>,
+}
+
+impl<T> From<()> for Holder<T> {
+    fn from((): ()) -> Self {
+        Holder { value: Vec::new() }
+    }
+}
+
+pub struct Param<const SIZE: usize> {
+    pub(crate) value: [u8; SIZE],
+}
+
+impl<const SIZE: usize> From<()> for Param<SIZE> {
+    fn from((): ()) -> Self {
+        Param { value: [0; SIZE] }
+    }
+}