Merge pull request #468 from Nadrieril/keep_method_trait_args

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.49"
+let supported_charon_version = "0.1.50"

charon-ml/src/GAst.ml

@@ -131,21 +131,21 @@ and 'a0 gexpr_body = {
 and item_kind =
   | RegularItem
       (** A function/const at the top level or in an inherent impl block. *)
-  | TraitDeclItem of trait_decl_id * trait_item_name * bool
+  | TraitDeclItem of trait_decl_ref * trait_item_name * bool
       (** Function/const that is part of a trait declaration. It has a body if and only if the trait
           provided a default implementation.
 
           Fields:
-          - [trait_id]:  The trait declaration this item belongs to.
+          - [trait_ref]:  The trait declaration this item belongs to.
           - [item_name]:  The name of the item.
           - [has_default]:  Whether the trait declaration provides a default implementation.
        *)
-  | TraitImplItem of trait_impl_id * trait_decl_id * trait_item_name * bool
+  | TraitImplItem of trait_impl_ref * trait_decl_ref * trait_item_name * bool
       (** Function/const that is part of a trait implementation.
 
           Fields:
-          - [impl_id]:  The trait implementation the method belongs to
-          - [trait_id]:  The trait declaration this item belongs to.
+          - [impl_ref]:  The trait implementation the method belongs to.
+          - [trait_ref]:  The trait declaration that the impl block implements.
           - [item_name]:  The name of the item
           - [reuses_default]:  True if the trait decl had a default implementation for this function/const and this
           item is a copy of the default item.

charon-ml/src/GAstOfJson.ml

@@ -394,31 +394,31 @@ and item_kind_of_json (ctx : of_json_ctx) (js : json) :
           ( "TraitDecl",
             `Assoc
               [
-                ("trait_id", trait_id);
+                ("trait_ref", trait_ref);
                 ("item_name", item_name);
                 ("has_default", has_default);
               ] );
         ] ->
-        let* trait_id = trait_decl_id_of_json ctx trait_id in
+        let* trait_ref = trait_decl_ref_of_json ctx trait_ref in
         let* item_name = trait_item_name_of_json ctx item_name in
         let* has_default = bool_of_json ctx has_default in
-        Ok (TraitDeclItem (trait_id, item_name, has_default))
+        Ok (TraitDeclItem (trait_ref, item_name, has_default))
     | `Assoc
         [
           ( "TraitImpl",
             `Assoc
               [
-                ("impl_id", impl_id);
-                ("trait_id", trait_id);
+                ("impl_ref", impl_ref);
+                ("trait_ref", trait_ref);
                 ("item_name", item_name);
                 ("reuses_default", reuses_default);
               ] );
         ] ->
-        let* impl_id = trait_impl_id_of_json ctx impl_id in
-        let* trait_id = trait_decl_id_of_json ctx trait_id in
+        let* impl_ref = trait_impl_ref_of_json ctx impl_ref in
+        let* trait_ref = trait_decl_ref_of_json ctx trait_ref in
         let* item_name = trait_item_name_of_json ctx item_name in
         let* reuses_default = bool_of_json ctx reuses_default in
-        Ok (TraitImplItem (impl_id, trait_id, item_name, reuses_default))
+        Ok (TraitImplItem (impl_ref, trait_ref, item_name, reuses_default))
     | _ -> Error "")
 
 and global_decl_of_json (ctx : of_json_ctx) (js : json) :
@@ -974,6 +974,16 @@ and trait_decl_ref_of_json (ctx : of_json_ctx) (js : json) :
         Ok ({ trait_decl_id; decl_generics } : trait_decl_ref)
     | _ -> Error "")
 
+and trait_impl_ref_of_json (ctx : of_json_ctx) (js : json) :
+    (trait_impl_ref, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("impl_id", impl_id); ("generics", generics) ] ->
+        let* trait_impl_id = trait_impl_id_of_json ctx impl_id in
+        let* impl_generics = generic_args_of_json ctx generics in
+        Ok ({ trait_impl_id; impl_generics } : trait_impl_ref)
+    | _ -> Error "")
+
 and outlives_pred_of_json :
       'a0 'a1.
       (of_json_ctx -> json -> ('a0, string) result) ->

charon-ml/src/Types.ml

@@ -399,6 +399,12 @@ and trait_decl_ref = {
   decl_generics : generic_args;
 }
 
+(** A reference to a tait impl, using the provided arguments. *)
+and trait_impl_ref = {
+  trait_impl_id : trait_impl_id;
+  impl_generics : generic_args;
+}
+
 and generic_args = {
   regions : region list;
   types : ty list;

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.49"
+version = "0.1.50"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"

charon/src/ast/gast.rs

@@ -115,18 +115,18 @@ pub enum ItemKind {
     /// provided a default implementation.
     TraitDecl {
         /// The trait declaration this item belongs to.
-        trait_id: TraitDeclId,
+        trait_ref: TraitDeclRef,
         /// The name of the item.
         item_name: TraitItemName,
         /// Whether the trait declaration provides a default implementation.
         has_default: bool,
     },
     /// Function/const that is part of a trait implementation.
     TraitImpl {
-        /// The trait implementation the method belongs to
-        impl_id: TraitImplId,
-        /// The trait declaration this item belongs to.
-        trait_id: TraitDeclId,
+        /// The trait implementation the method belongs to.
+        impl_ref: TraitImplRef,
+        /// The trait declaration that the impl block implements.
+        trait_ref: TraitDeclRef,
         /// The name of the item
         item_name: TraitItemName,
         /// True if the trait decl had a default implementation for this function/const and this

charon/src/ast/types.rs

@@ -250,6 +250,15 @@ pub struct TraitDeclRef {
 /// A quantified trait predicate, e.g. `for<'a> Type<'a>: Trait<'a, Args>`.
 pub type PolyTraitDeclRef = RegionBinder<TraitDeclRef>;
 
+/// A reference to a tait impl, using the provided arguments.
+#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
+pub struct TraitImplRef {
+    #[charon::rename("trait_impl_id")]
+    pub impl_id: TraitImplId,
+    #[charon::rename("impl_generics")]
+    pub generics: GenericArgs,
+}
+
 /// .0 outlives .1
 #[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
 pub struct OutlivesPred<T, U>(pub T, pub U);

charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs

@@ -121,15 +121,25 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             // ```
             hax::AssocItemContainer::TraitImplContainer {
                 impl_id,
+                impl_generics,
+                impl_required_impl_exprs,
                 implemented_trait_ref,
                 overrides_default,
                 ..
             } => {
-                let trait_id = self.register_trait_decl_id(span, &implemented_trait_ref.def_id);
-                let impl_id = self.register_trait_impl_id(span, impl_id);
+                let impl_ref = TraitImplRef {
+                    impl_id: self.register_trait_impl_id(span, impl_id),
+                    generics: self.translate_generic_args(
+                        span,
+                        None,
+                        impl_generics,
+                        impl_required_impl_exprs,
+                    )?,
+                };
+                let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
                 ItemKind::TraitImpl {
-                    impl_id,
-                    trait_id,
+                    impl_ref,
+                    trait_ref,
                     item_name: TraitItemName(assoc.name.clone()),
                     reuses_default: !overrides_default,
                 }
@@ -144,11 +154,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
                 // The trait id should be Some(...): trait markers (that we may eliminate)
                 // don't have associated items.
-                let trait_id = self.register_trait_decl_id(span, &trait_ref.def_id);
+                let trait_ref = self.translate_trait_ref(span, trait_ref)?;
                 let item_name = TraitItemName(assoc.name.clone());
-
                 ItemKind::TraitDecl {
-                    trait_id,
+                    trait_ref,
                     item_name,
                     has_default: assoc.has_value,
                 }

charon/src/bin/generate-ml/main.rs

@@ -1343,6 +1343,7 @@ fn generate_ml(
                     "TraitRef",
                     "TraitRefKind",
                     "TraitDeclRef",
+                    "TraitImplRef",
                     "GlobalDeclRef",
                     "GenericArgs",
                 ]),

charon/src/transform/check_generics.rs

@@ -15,6 +15,7 @@ use super::{ctx::TransformPass, TransformCtx};
     FnPtr(enter),
     GlobalDeclRef(enter),
     TraitDeclRef(enter),
+    TraitImplRef(enter),
     TraitRefKind(enter),
     Ty(enter)
 )]
@@ -102,6 +103,9 @@ impl CheckGenericsVisitor<'_> {
     fn enter_trait_decl_ref(&mut self, tref: &TraitDeclRef) {
         self.generics_should_match_item(&tref.generics, tref.trait_id);
     }
+    fn enter_trait_impl_ref(&mut self, impl_ref: &TraitImplRef) {
+        self.generics_should_match_item(&impl_ref.generics, impl_ref.impl_id);
+    }
     fn enter_trait_ref_kind(&mut self, kind: &TraitRefKind) {
         match kind {
             TraitRefKind::TraitImpl(id, args) => self.generics_should_match_item(args, *id),

charon/src/transform/reorder_decls.rs

@@ -224,8 +224,10 @@ impl<'tcx> Deps<'tcx> {
     fn set_impl_or_trait_id(&mut self, kind: &ItemKind) {
         match kind {
             ItemKind::Regular => {}
-            ItemKind::TraitDecl { trait_id, .. } => self.parent_trait_decl = Some(*trait_id),
-            ItemKind::TraitImpl { impl_id, .. } => self.parent_trait_impl = Some(*impl_id),
+            ItemKind::TraitDecl { trait_ref, .. } => {
+                self.parent_trait_decl = Some(trait_ref.trait_id)
+            }
+            ItemKind::TraitImpl { impl_ref, .. } => self.parent_trait_impl = Some(impl_ref.impl_id),
         }
     }
     fn set_current_id(&mut self, ctx: &TransformCtx, id: AnyTransId) {