val for opaque consts in fsti.

cryspen · Dec 16, 2024 · c660aaa · c660aaa
1 parent 50c14ef
commit c660aaa
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 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/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)