Propagate attributes from Pack Statements

src/loop/parser.ml

@@ -376,9 +376,13 @@ module Make(State : State.S) = struct
 
   let expand st c =
     let ret = match c with
-      | { S.descr = S.Pack l; _ } ->
+      | { S.descr = S.Pack l; attrs; _ } ->
         let file = State.get State.logic_file st in
-        st, `Gen (merge, wrap_parser ~file (Gen.of_list l))
+        let g =
+          Gen.of_list l
+          |> Gen.map (S.add_attrs attrs)
+        in
+        st, `Gen (merge, wrap_parser ~file g)
       (* TODO: filter the statements by passing some options *)
       | { S.descr = S.Include file; _ } ->
         let logic_file = State.get State.logic_file st in

src/standard/statement.ml

@@ -329,6 +329,9 @@ let annot = Term.apply
 let mk ?id ?(loc=Loc.no_loc) ?(attrs=[]) descr =
   { id; descr; loc; attrs; }
 
+let add_attrs attrs t =
+  { t with attrs = attrs @ t.attrs; }
+
 (* Pack *)
 let pack ?id ?loc ?attrs l =
   mk ?id ?loc ?attrs (Pack l)

src/standard/statement.mli

@@ -171,6 +171,9 @@ include Dolmen_intf.Stmt.Logic
 
 (** {2 Additional functions} *)
 
+val add_attrs : term list -> t -> t
+(** Add some attributes to a statement. *)
+
 val mk_decls :
   ?loc:location -> ?attrs:term list -> recursive:bool -> decl list -> t
 (** Create a group of declarations *)