From 8fe21473d4f106a91f97f42c75fb86440e444dfd Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Tue, 21 Nov 2023 14:28:07 +0100
Subject: [PATCH] Add meta information to the trait decls/impls

---
 charon-ml/src/GAst.ml          | 2 ++
 charon-ml/src/GAstOfJson.ml    | 6 ++++++
 charon/src/gast.rs             | 2 ++
 charon/src/translate_traits.rs | 2 ++
 4 files changed, 12 insertions(+)

diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml
index 5d33117f..011c903b 100644
--- a/charon-ml/src/GAst.ml
+++ b/charon-ml/src/GAst.ml
@@ -144,6 +144,7 @@ type trait_decl = {
   def_id : trait_decl_id;
   is_local : bool;
   name : name;
+  meta : meta;
   generics : generic_params;
   preds : predicates;
   parent_clauses : trait_clause list;
@@ -158,6 +159,7 @@ type trait_impl = {
   def_id : trait_impl_id;
   is_local : bool;
   name : name;
+  meta : meta;
   impl_trait : trait_decl_ref;
   generics : generic_params;
   preds : predicates;
diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml
index c9989ca4..66fbbe7f 100644
--- a/charon-ml/src/GAstOfJson.ml
+++ b/charon-ml/src/GAstOfJson.ml
@@ -1053,6 +1053,7 @@ let trait_decl_of_json (id_to_file : id_to_file_map) (js : json) :
           ("def_id", def_id);
           ("is_local", is_local);
           ("name", name);
+          ("meta", meta);
           ("generics", generics);
           ("preds", preds);
           ("parent_clauses", parent_clauses);
@@ -1064,6 +1065,7 @@ let trait_decl_of_json (id_to_file : id_to_file_map) (js : json) :
         let* def_id = TraitDeclId.id_of_json def_id in
         let* is_local = bool_of_json is_local in
         let* name = name_of_json id_to_file name in
+        let* meta = meta_of_json id_to_file meta in
         let* generics = generic_params_of_json id_to_file generics in
         let* preds = predicates_of_json preds in
         let* parent_clauses =
@@ -1099,6 +1101,7 @@ let trait_decl_of_json (id_to_file : id_to_file_map) (js : json) :
             def_id;
             is_local;
             name;
+            meta;
             generics;
             preds;
             parent_clauses;
@@ -1118,6 +1121,7 @@ let trait_impl_of_json (id_to_file : id_to_file_map) (js : json) :
           ("def_id", def_id);
           ("is_local", is_local);
           ("name", name);
+          ("meta", meta);
           ("impl_trait", impl_trait);
           ("generics", generics);
           ("preds", preds);
@@ -1130,6 +1134,7 @@ let trait_impl_of_json (id_to_file : id_to_file_map) (js : json) :
         let* def_id = TraitImplId.id_of_json def_id in
         let* is_local = bool_of_json is_local in
         let* name = name_of_json id_to_file name in
+        let* meta = meta_of_json id_to_file meta in
         let* impl_trait = trait_decl_ref_of_json impl_trait in
         let* generics = generic_params_of_json id_to_file generics in
         let* preds = predicates_of_json preds in
@@ -1158,6 +1163,7 @@ let trait_impl_of_json (id_to_file : id_to_file_map) (js : json) :
              def_id;
              is_local;
              name;
+             meta;
              impl_trait;
              generics;
              preds;
diff --git a/charon/src/gast.rs b/charon/src/gast.rs
index 688a6733..ea79cd19 100644
--- a/charon/src/gast.rs
+++ b/charon/src/gast.rs
@@ -165,6 +165,7 @@ pub struct TraitDecl {
     /// an external crate.
     pub is_local: bool,
     pub name: Name,
+    pub meta: Meta,
     pub generics: GenericParams,
     pub preds: Predicates,
     /// The "parent" clauses: the supertraits.
@@ -223,6 +224,7 @@ pub struct TraitImpl {
     /// an external crate.
     pub is_local: bool,
     pub name: Name,
+    pub meta: Meta,
     /// The information about the implemented trait.
     /// Note that this contains the instantiation of the "parent"
     /// clauses.
diff --git a/charon/src/translate_traits.rs b/charon/src/translate_traits.rs
index c0b77a17..4463ed49 100644
--- a/charon/src/translate_traits.rs
+++ b/charon/src/translate_traits.rs
@@ -394,6 +394,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
             def_id,
             is_local: rust_id.is_local(),
             name,
+            meta: self.translate_meta_from_rid(rust_id),
             generics,
             preds,
             parent_clauses,
@@ -597,6 +598,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
             def_id,
             is_local: rust_id.is_local(),
             name,
+            meta: bt_ctx.t_ctx.translate_meta_from_rid(rust_id),
             impl_trait: implemented_trait,
             generics: bt_ctx.get_generics(),
             preds: bt_ctx.get_predicates(),