Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(engine) Opaque consts #1189

Merged
merged 2 commits into from
Dec 17, 2024
Merged

fix(engine) Opaque consts #1189

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
50c14ef
Avoid making consts inside impls opaque by default.
maximebuyse Dec 16, 2024
c660aaa
val for opaque consts in fsti.
maximebuyse Dec 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions engine/backends/fstar/fstar_backend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
9 changes: 7 additions & 2 deletions engine/lib/import_thir.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 2 additions & 0 deletions test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Loading