From 95f6df0d873f2dac7c20dd131e80dcd83e46c1ec Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 16 Jun 2023 16:51:07 +0200
Subject: [PATCH] Propagate attributes from `Pack` Statements

---
 src/loop/parser.ml         | 8 ++++++--
 src/standard/statement.ml  | 3 +++
 src/standard/statement.mli | 3 +++
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/loop/parser.ml b/src/loop/parser.ml
index ad2445ea6..af5a86e90 100644
--- a/src/loop/parser.ml
+++ b/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
diff --git a/src/standard/statement.ml b/src/standard/statement.ml
index 0a166ed99..943ad0974 100644
--- a/src/standard/statement.ml
+++ b/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)
diff --git a/src/standard/statement.mli b/src/standard/statement.mli
index ae3fc0eca..fc567ecb2 100644
--- a/src/standard/statement.mli
+++ b/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 *)