charon_driver/translate/
translate_predicates.rs

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

charon_driver/translate/
translate_predicates.rs
