charon_driver/translate/
translate_predicates.rs

1use super::translate_ctx::*;
2use super::translate_traits::PredicateLocation;
3use charon_lib::ast::*;
4use charon_lib::formatter::IntoFormatter;
5use charon_lib::ids::Vector;
6use charon_lib::pretty::FmtWithCtx;
7use hax_frontend_exporter as hax;
8
9impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
10    /// This function should be called **after** we translated the generics (type parameters,
11    /// regions...).
12    pub(crate) fn register_predicates(
13        &mut self,
14        preds: &hax::GenericPredicates,
15        origin: PredicateOrigin,
16        location: &PredicateLocation,
17    ) -> Result<(), Error> {
18        // Translate the trait predicates first, because associated type constraints may refer to
19        // them. E.g. in `fn foo<I: Iterator<Item=usize>>()`, the `I: Iterator` clause must be
20        // translated before the `<I as Iterator>::Item = usize` predicate.
21        for (clause, span) in &preds.predicates {
22            if matches!(clause.kind.value, hax::ClauseKind::Trait(_)) {
23                self.register_predicate(clause, span, origin.clone(), location)?;
24            }
25        }
26        for (clause, span) in &preds.predicates {
27            if !matches!(clause.kind.value, hax::ClauseKind::Trait(_)) {
28                self.register_predicate(clause, span, origin.clone(), location)?;
29            }
30        }
31        Ok(())
32    }
33
34    pub(crate) fn translate_poly_trait_ref(
35        &mut self,
36        span: Span,
37        bound_trait_ref: &hax::Binder<hax::TraitRef>,
38    ) -> Result<PolyTraitDeclRef, Error> {
39        self.translate_region_binder(span, bound_trait_ref, move |ctx, trait_ref| {
40            ctx.translate_trait_ref(span, trait_ref)
41        })
42    }
43
44    pub(crate) fn translate_trait_predicate(
45        &mut self,
46        span: Span,
47        trait_pred: &hax::TraitPredicate,
48    ) -> Result<TraitDeclRef, Error> {
49        // we don't handle negative trait predicates.
50        assert!(trait_pred.is_positive);
51        self.translate_trait_ref(span, &trait_pred.trait_ref)
52    }
53
54    pub(crate) fn translate_trait_ref(
55        &mut self,
56        span: Span,
57        trait_ref: &hax::TraitRef,
58    ) -> Result<TraitDeclRef, Error> {
59        let trait_id = self.register_trait_decl_id(span, &trait_ref.def_id);
60        // For now a trait has no required bounds, so we pass an empty list.
61        let generics = self.translate_generic_args(
62            span,
63            &trait_ref.generic_args,
64            &[],
65            None,
66            GenericsSource::item(trait_id),
67        )?;
68        Ok(TraitDeclRef { trait_id, generics })
69    }
70
71    pub(crate) fn register_predicate(
72        &mut self,
73        clause: &hax::Clause,
74        hspan: &hax::Span,
75        origin: PredicateOrigin,
76        location: &PredicateLocation,
77    ) -> Result<(), Error> {
78        use hax::ClauseKind;
79        trace!("{:?}", clause);
80        let span = self.translate_span_from_hax(hspan);
81        match clause.kind.hax_skip_binder_ref() {
82            ClauseKind::Trait(trait_pred) => {
83                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
84                    ctx.translate_trait_predicate(span, trait_pred)
85                })?;
86                let location = match location {
87                    PredicateLocation::Base => &mut self.innermost_generics_mut().trait_clauses,
88                    PredicateLocation::Parent => &mut self.parent_trait_clauses,
89                    PredicateLocation::Item(item_name) => self
90                        .item_trait_clauses
91                        .entry(item_name.clone())
92                        .or_default(),
93                };
94                location.push_with(|clause_id| TraitClause {
95                    clause_id,
96                    origin,
97                    span: Some(span),
98                    trait_: pred,
99                });
100            }
101            ClauseKind::RegionOutlives(p) => {
102                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
103                    let r0 = ctx.translate_region(span, &p.lhs)?;
104                    let r1 = ctx.translate_region(span, &p.rhs)?;
105                    Ok(OutlivesPred(r0, r1))
106                })?;
107                self.innermost_generics_mut().regions_outlive.push(pred);
108            }
109            ClauseKind::TypeOutlives(p) => {
110                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
111                    let ty = ctx.translate_ty(span, &p.lhs)?;
112                    let r = ctx.translate_region(span, &p.rhs)?;
113                    Ok(OutlivesPred(ty, r))
114                })?;
115                self.innermost_generics_mut().types_outlive.push(pred);
116            }
117            ClauseKind::Projection(p) => {
118                // This is used to express constraints over associated types.
119                // For instance:
120                // ```
121                // T : Foo<S = String>
122                //         ^^^^^^^^^^
123                // ```
124                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
125                    let trait_ref = ctx.translate_trait_impl_expr(span, &p.impl_expr)?;
126                    let ty = ctx.translate_ty(span, &p.ty)?;
127                    let type_name = TraitItemName(p.assoc_item.name.clone());
128                    Ok(TraitTypeConstraint {
129                        trait_ref,
130                        type_name,
131                        ty,
132                    })
133                })?;
134                self.innermost_generics_mut()
135                    .trait_type_constraints
136                    .push(pred);
137            }
138            ClauseKind::ConstArgHasType(..) => {
139                // I don't really understand that one. Why don't they put
140                // the type information in the const generic parameters
141                // directly? For now we just ignore it.
142            }
143            ClauseKind::WellFormed(_) => {
144                raise_error!(self, span, "Well-formedness clauses are unsupported")
145            }
146            kind => {
147                raise_error!(self, span, "Unsupported clause: {:?}", kind)
148            }
149        }
150        Ok(())
151    }
152
153    pub(crate) fn translate_trait_impl_exprs(
154        &mut self,
155        span: Span,
156        impl_sources: &[hax::ImplExpr],
157    ) -> Result<Vector<TraitClauseId, TraitRef>, Error> {
158        impl_sources
159            .iter()
160            .map(|x| self.translate_trait_impl_expr(span, x))
161            .try_collect()
162    }
163
164    #[tracing::instrument(skip(self, span, impl_expr))]
165    pub(crate) fn translate_trait_impl_expr(
166        &mut self,
167        span: Span,
168        impl_expr: &hax::ImplExpr,
169    ) -> Result<TraitRef, Error> {
170        let trait_decl_ref = self.translate_poly_trait_ref(span, &impl_expr.r#trait)?;
171
172        match self.translate_trait_impl_expr_aux(span, impl_expr, trait_decl_ref.clone()) {
173            Ok(res) => Ok(res),
174            Err(err) => {
175                register_error!(self, span, "Error during trait resolution: {}", &err.msg);
176                Ok(TraitRef {
177                    kind: TraitRefKind::Unknown(err.msg),
178                    trait_decl_ref,
179                })
180            }
181        }
182    }
183
184    pub(crate) fn translate_trait_impl_expr_aux(
185        &mut self,
186        span: Span,
187        impl_source: &hax::ImplExpr,
188        trait_decl_ref: PolyTraitDeclRef,
189    ) -> Result<TraitRef, Error> {
190        trace!("impl_expr: {:#?}", impl_source);
191        use hax::ImplExprAtom;
192
193        let trait_ref = match &impl_source.r#impl {
194            ImplExprAtom::Concrete {
195                id: impl_def_id,
196                generics,
197                impl_exprs,
198            } => {
199                let impl_id = self.register_trait_impl_id(span, impl_def_id);
200                let generics = self.translate_generic_args(
201                    span,
202                    generics,
203                    impl_exprs,
204                    None,
205                    GenericsSource::item(impl_id),
206                )?;
207                TraitRef {
208                    kind: TraitRefKind::TraitImpl(impl_id, generics),
209                    trait_decl_ref,
210                }
211            }
212            // The self clause and the other clauses are handled in a similar manner
213            ImplExprAtom::SelfImpl {
214                r#trait: trait_ref,
215                path,
216            }
217            | ImplExprAtom::LocalBound {
218                r#trait: trait_ref,
219                path,
220                ..
221            } => {
222                trace!(
223                    "impl source (self or clause): param:\n- trait_ref: {:?}\n- path: {:?}",
224                    trait_ref,
225                    path,
226                );
227                // If we are refering to a trait clause, we need to find the
228                // relevant one.
229                let mut trait_id = match &impl_source.r#impl {
230                    ImplExprAtom::SelfImpl { .. } => TraitRefKind::SelfId,
231                    ImplExprAtom::LocalBound { index, .. } => {
232                        let var = self.lookup_clause_var(span, *index)?;
233                        TraitRefKind::Clause(var)
234                    }
235                    _ => unreachable!(),
236                };
237
238                let mut current_trait_decl_id =
239                    self.register_trait_decl_id(span, &trait_ref.hax_skip_binder_ref().def_id);
240
241                // Apply the path
242                for path_elem in path {
243                    use hax::ImplExprPathChunk::*;
244                    match path_elem {
245                        AssocItem {
246                            item,
247                            generic_args,
248                            predicate,
249                            index,
250                            ..
251                        } => {
252                            if !generic_args.is_empty() {
253                                raise_error!(
254                                    self,
255                                    span,
256                                    "Found unsupported GAT `{}` when resolving trait `{}`",
257                                    item.name,
258                                    trait_decl_ref.fmt_with_ctx(&self.into_fmt())
259                                )
260                            }
261                            trait_id = TraitRefKind::ItemClause(
262                                Box::new(trait_id),
263                                current_trait_decl_id,
264                                TraitItemName(item.name.clone()),
265                                TraitClauseId::new(*index),
266                            );
267                            current_trait_decl_id = self.register_trait_decl_id(
268                                span,
269                                &predicate.hax_skip_binder_ref().trait_ref.def_id,
270                            );
271                        }
272                        Parent {
273                            predicate, index, ..
274                        } => {
275                            trait_id = TraitRefKind::ParentClause(
276                                Box::new(trait_id),
277                                current_trait_decl_id,
278                                TraitClauseId::new(*index),
279                            );
280                            current_trait_decl_id = self.register_trait_decl_id(
281                                span,
282                                &predicate.hax_skip_binder_ref().trait_ref.def_id,
283                            );
284                        }
285                    }
286                }
287
288                // Ignore the arguments: we forbid using universal quantifiers
289                // on the trait clauses for now.
290                TraitRef {
291                    kind: trait_id,
292                    trait_decl_ref,
293                }
294            }
295            ImplExprAtom::Dyn => TraitRef {
296                kind: TraitRefKind::Dyn(trait_decl_ref.clone()),
297                trait_decl_ref,
298            },
299            ImplExprAtom::Builtin {
300                impl_exprs, types, ..
301            } => {
302                let parent_trait_refs = self.translate_trait_impl_exprs(span, &impl_exprs)?;
303                let types = types
304                    .iter()
305                    .map(|(def_id, ty)| {
306                        let item_def = self.hax_def(def_id)?;
307                        let ty = self.translate_ty(span, ty)?;
308                        let hax::FullDefKind::AssocTy {
309                            associated_item, ..
310                        } = item_def.kind()
311                        else {
312                            unreachable!()
313                        };
314                        let name = TraitItemName(associated_item.name.clone());
315                        Ok((name, ty))
316                    })
317                    .try_collect()?;
318                TraitRef {
319                    kind: TraitRefKind::BuiltinOrAuto {
320                        trait_decl_ref: trait_decl_ref.clone(),
321                        parent_trait_refs,
322                        types,
323                    },
324                    trait_decl_ref,
325                }
326            }
327            ImplExprAtom::Error(msg) => {
328                let trait_ref = TraitRef {
329                    kind: TraitRefKind::Unknown(msg.clone()),
330                    trait_decl_ref,
331                };
332                if self.error_on_impl_expr_error {
333                    register_error!(self, span, "Error during trait resolution: {}", msg);
334                }
335                trait_ref
336            }
337        };
338        Ok(trait_ref)
339    }
340}
charon_driver/translate/translate_predicates.rs

charon_driver/translate/
translate_predicates.rs
