Merge pull request #1189 from hacspec/opaque-consts

fix(engine) Opaque consts
hacspec · Dec 17, 2024 · daaeb8e · daaeb8e
2 parents 62f7bfa + c660aaa
commit daaeb8e
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 6 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -929,10 +929,11 @@ struct
           F.decl ~fsti:false
           @@ F.AST.TopLevelLet (qualifier, [ (pat, pexpr body) ])
         in
-        let interface_mode = ctx.interface_mode && not (List.is_empty params) in
+        let is_const = List.is_empty params in
         let ty =
-          add_clauses_effect_type ~no_tot_abbrev:interface_mode e.attrs
-            (pty body.span body.typ)
+          add_clauses_effect_type
+            ~no_tot_abbrev:(ctx.interface_mode && not is_const)
+            e.attrs (pty body.span body.typ)
         in
         let arrow_typ =
           F.term
@@ -968,7 +969,8 @@ struct
         let impl, full =
           if is_erased then (erased, erased) else ([ impl ], [ full ])
         in
-        if interface_mode then intf :: impl else full
+        if ctx.interface_mode && ((not is_const) || is_erased) then intf :: impl
+        else full
     | TyAlias { name; generics; ty } ->
         let pat =
           F.pat

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -1659,9 +1659,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
           let item_def_id = Concrete_ident.of_def_id Impl item.owner_id in
           let attrs = c_item_attrs item.attributes in
           let sub_item_erased_by_user = erased_by_user attrs in
-          let sub_item_erased = sub_item_erased_by_user || type_only in
+          let erased_by_type_only =
+            type_only && match item.kind with Fn _ -> true | _ -> false
+          in
+          let sub_item_erased =
+            sub_item_erased_by_user || erased_by_type_only
+          in
           let attrs =
-            attrs_with_erased type_only sub_item_erased_by_user attrs
+            attrs_with_erased erased_by_type_only sub_item_erased_by_user attrs
           in
           let c_body = if sub_item_erased then c_expr_drop_body else c_body in
 

diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -123,6 +123,8 @@ val impl_2 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U
 
 val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
+val v_C:u8
+
 val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 
 val ff_generic (v_X: usize) (#v_T #v_U: Type0) (x: v_U)