From 3ed17cec473986f6aad2f1ff989866b29d8906be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 16 Aug 2024 00:10:36 -0700 Subject: [PATCH] MkProjectors: also propagate attributes --- ulib/FStar.Tactics.MkProjectors.fst | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/ulib/FStar.Tactics.MkProjectors.fst b/ulib/FStar.Tactics.MkProjectors.fst index f27e8bd58c2..7adab02c936 100644 --- a/ulib/FStar.Tactics.MkProjectors.fst +++ b/ulib/FStar.Tactics.MkProjectors.fst @@ -101,6 +101,7 @@ let substitute_attr : term = let mk_proj_decl (is_method:bool) + (attrs : list term) (quals : list qualifier) (tyqn:name) ctorname (univs : list univ_name) @@ -181,13 +182,13 @@ let mk_proj_decl lb_def = lb_def; }]} in - let se = set_sigelt_attrs (substitute_attr :: field.attrs @ sigelt_attrs se_proj) se in + let se = set_sigelt_attrs (substitute_attr :: field.attrs @ attrs @ sigelt_attrs se) se in let se = set_sigelt_quals (filter_quals quals @ sigelt_quals se) se in [se] in (* Propagate binder attributes, i.e. attributes in the field decl, to the method itself. *) - let se_proj = set_sigelt_attrs (substitute_attr :: field.attrs @ sigelt_attrs se_proj) se_proj in + let se_proj = set_sigelt_attrs (substitute_attr :: field.attrs @ attrs @ sigelt_attrs se_proj) se_proj in let se_proj = set_sigelt_quals (filter_quals quals @ sigelt_quals se_proj) se_proj in (* Do we need to set the sigelt's Projector qual? If so, @@ -212,6 +213,7 @@ let mk_projs (is_class:bool) (tyname:string) : Tac decls = raise NotFound | Some se -> let quals = sigelt_quals se in + let attrs = sigelt_attrs se in match inspect_sigelt se with | Sg_Inductive {nm; univs; params; typ; ctors} -> if (length ctors <> 1) then @@ -226,7 +228,7 @@ let mk_projs (is_class:bool) (tyname:string) : Tac decls = let unfold_names_tm = `(Nil #string) in let (decls, _, _, _) = fold_left (fun (decls, smap, unfold_names_tm, idx) (field : binder) -> - let (ds, fv) = mk_proj_decl is_class quals tyqn ctorname univs params idx field unfold_names_tm smap in + let (ds, fv) = mk_proj_decl is_class attrs quals tyqn ctorname univs params idx field unfold_names_tm smap in (decls @ ds, (binder_to_namedv field, fv)::smap, (`(Cons #string (`#(embed_string (implode_qn (inspect_fv fv)))) (`#unfold_names_tm))),