Skip to content

Commit

Permalink
fix(backends/fstar): no __marker_trait if parent bounds
Browse files Browse the repository at this point in the history
Parent bounds are translated as record fields in F*.  Also, F* classes
are records, and F* records cannot be empty. Thus, we insert a dummy
field `__marker_trait` on empty traits (marker traits).

On trait definitions, we were inserting this `__marker_trait` fields
only when a trait had no parent bounds and no associated item (method,
assoc. type, assoc fun.).

On instance definitons, we were inserting `__marker_trait` when the
trait was empty, disregarding parent bounds.

This difference of treatments lead to TC issues in F*.

This PR fixes this discrepancy.
  • Loading branch information
W95Psp committed Jun 12, 2024
1 parent 3958de4 commit 430237c
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions engine/backends/fstar/fstar_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1324,18 +1324,18 @@ struct
parent_bounds)
items
in
let fields =
if List.is_empty fields then
[ (F.lid [ "__marker_trait" ], pexpr (U.unit_expr e.span)) ]
else fields
in
let parent_bounds_fields =
List.map
~f:(fun (_impl_expr, impl_ident) ->
(F.lid [ "_super_" ^ impl_ident.name ], F.tc_solve))
parent_bounds
in
let fields = parent_bounds_fields @ fields in
let fields =
if List.is_empty fields then
[ (F.lid [ "__marker_trait" ], pexpr (U.unit_expr e.span)) ]
else fields
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 ]
Expand Down

0 comments on commit 430237c

Please sign in to comment.