MkProjectors: also propagate attributes

FStarLang · Aug 16, 2024 · 3ed17ce · 3ed17ce
1 parent 732b5a0
commit 3ed17ce
Showing 1 changed file with 5 additions and 3 deletions.
diff --git 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))),