Use a Vector for TraitImpl.type_clauses

AeneasVerif · Oct 31, 2024 · 73c98b3 · 73c98b3
1 parent 16a37de
commit 73c98b3
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 10 deletions.
diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs
@@ -294,7 +294,7 @@ pub struct TraitImpl {
     /// The `Vec` corresponds to the same `Vector` in `TraitDecl`. In the same way, this is
     /// empty after the `lift_associated_item_clauses` pass.
     #[charon::opaque]
-    pub type_clauses: Vec<(TraitItemName, Vec<TraitRef>)>,
+    pub type_clauses: Vec<(TraitItemName, Vector<TraitClauseId, TraitRef>)>,
     /// The implemented required methods
     pub required_methods: Vec<(TraitItemName, FunDeclId)>,
     /// The re-implemented provided methods

diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -285,15 +285,11 @@ impl BodyTransCtx<'_, '_, '_> {
                     let ty = self.translate_ty(item_span, erase_regions, &ty)?;
                     types.push((name.clone(), ty));
 
-                    // TODO: use clause ids
-                    let trait_refs = self
-                        .translate_trait_impl_exprs(
-                            item_span,
-                            erase_regions,
-                            &impl_item.required_impl_exprs,
-                        )?
-                        .into_iter()
-                        .collect();
+                    let trait_refs = self.translate_trait_impl_exprs(
+                        item_span,
+                        erase_regions,
+                        &impl_item.required_impl_exprs,
+                    )?;
                     type_clauses.push((name, trait_refs));
                 }
                 _ => panic!("Unexpected definition for trait item: {item_def:?}"),