charon_driver/translate/
translate_predicates.rs

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        self.translate_trait_decl_ref(span, trait_ref)
70    }
71
72    pub(crate) fn register_predicate(
73        &mut self,
74        clause: &hax::Clause,
75        hspan: &hax::Span,
76        origin: PredicateOrigin,
77        location: &PredicateLocation,
78    ) -> Result<(), Error> {
79        use hax::ClauseKind;
80        trace!("{:?}", clause);
81        let span = self.translate_span_from_hax(hspan);
82        match clause.kind.hax_skip_binder_ref() {
83            ClauseKind::Trait(trait_pred) => {
84                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
85                    ctx.translate_trait_predicate(span, trait_pred)
86                })?;
87                let location = match location {
88                    PredicateLocation::Base => &mut self.innermost_generics_mut().trait_clauses,
89                    PredicateLocation::Parent => &mut self.parent_trait_clauses,
90                    PredicateLocation::Item(item_name) => self
91                        .item_trait_clauses
92                        .entry(item_name.clone())
93                        .or_default(),
94                };
95                location.push_with(|clause_id| TraitClause {
96                    clause_id,
97                    origin,
98                    span: Some(span),
99                    trait_: pred,
100                });
101            }
102            ClauseKind::RegionOutlives(p) => {
103                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
104                    let r0 = ctx.translate_region(span, &p.lhs)?;
105                    let r1 = ctx.translate_region(span, &p.rhs)?;
106                    Ok(OutlivesPred(r0, r1))
107                })?;
108                self.innermost_generics_mut().regions_outlive.push(pred);
109            }
110            ClauseKind::TypeOutlives(p) => {
111                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
112                    let ty = ctx.translate_ty(span, &p.lhs)?;
113                    let r = ctx.translate_region(span, &p.rhs)?;
114                    Ok(OutlivesPred(ty, r))
115                })?;
116                self.innermost_generics_mut().types_outlive.push(pred);
117            }
118            ClauseKind::Projection(p) => {
119                // This is used to express constraints over associated types.
120                // For instance:
121                // ```
122                // T : Foo<S = String>
123                //         ^^^^^^^^^^
124                // ```
125                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
126                    let trait_ref = ctx.translate_trait_impl_expr(span, &p.impl_expr)?;
127                    let ty = ctx.translate_ty(span, &p.ty)?;
128                    let type_name = ctx.t_ctx.translate_trait_item_name(&p.assoc_item.def_id)?;
129                    Ok(TraitTypeConstraint {
130                        trait_ref,
131                        type_name,
132                        ty,
133                    })
134                })?;
135                self.innermost_generics_mut()
136                    .trait_type_constraints
137                    .push(pred);
138            }
139            ClauseKind::ConstArgHasType(..) => {
140                // I don't really understand that one. Why don't they put
141                // the type information in the const generic parameters
142                // directly? For now we just ignore it.
143            }
144            ClauseKind::WellFormed(_) => {
145                raise_error!(self, span, "Well-formedness clauses are unsupported")
146            }
147            kind => {
148                raise_error!(self, span, "Unsupported clause: {:?}", kind)
149            }
150        }
151        Ok(())
152    }
153
154    pub(crate) fn translate_trait_impl_exprs(
155        &mut self,
156        span: Span,
157        impl_sources: &[hax::ImplExpr],
158    ) -> Result<Vector<TraitClauseId, TraitRef>, Error> {
159        impl_sources
160            .iter()
161            .map(|x| self.translate_trait_impl_expr(span, x))
162            .try_collect()
163    }
164
165    #[tracing::instrument(skip(self, span, impl_expr))]
166    pub(crate) fn translate_trait_impl_expr(
167        &mut self,
168        span: Span,
169        impl_expr: &hax::ImplExpr,
170    ) -> Result<TraitRef, Error> {
171        let trait_decl_ref = self.translate_poly_trait_ref(span, &impl_expr.r#trait)?;
172
173        match self.translate_trait_impl_expr_aux(span, impl_expr, trait_decl_ref.clone()) {
174            Ok(res) => Ok(res),
175            Err(err) => {
176                register_error!(self, span, "Error during trait resolution: {}", &err.msg);
177                Ok(TraitRef {
178                    kind: TraitRefKind::Unknown(err.msg),
179                    trait_decl_ref,
180                })
181            }
182        }
183    }
184
185    pub(crate) fn translate_trait_impl_expr_aux(
186        &mut self,
187        span: Span,
188        impl_source: &hax::ImplExpr,
189        trait_decl_ref: PolyTraitDeclRef,
190    ) -> Result<TraitRef, Error> {
191        trace!("impl_expr: {:#?}", impl_source);
192        use hax::DropData;
193        use hax::ImplExprAtom;
194
195        let trait_ref = match &impl_source.r#impl {
196            ImplExprAtom::Concrete(item) => {
197                let impl_ref = self.translate_trait_impl_ref(span, item)?;
198                TraitRef {
199                    kind: TraitRefKind::TraitImpl(impl_ref),
200                    trait_decl_ref,
201                }
202            }
203            ImplExprAtom::SelfImpl {
204                r#trait: trait_ref,
205                path,
206            }
207            | ImplExprAtom::LocalBound {
208                r#trait: trait_ref,
209                path,
210                ..
211            } => {
212                trace!(
213                    "impl source (self or clause): param:\n- trait_ref: {:?}\n- path: {:?}",
214                    trait_ref, path,
215                );
216                // If we are refering to a trait clause, we need to find the relevant one.
217                let mut trait_id = match &impl_source.r#impl {
218                    ImplExprAtom::SelfImpl { .. } => TraitRefKind::SelfId,
219                    ImplExprAtom::LocalBound { index, .. } => {
220                        let var = self.lookup_clause_var(span, *index)?;
221                        TraitRefKind::Clause(var)
222                    }
223                    _ => unreachable!(),
224                };
225
226                let mut current_trait_decl_id =
227                    self.register_trait_decl_id(span, &trait_ref.hax_skip_binder_ref().def_id);
228
229                // Apply the path
230                for path_elem in path {
231                    use hax::ImplExprPathChunk::*;
232                    match path_elem {
233                        AssocItem {
234                            item,
235                            predicate,
236                            index,
237                            ..
238                        } => {
239                            let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
240                            if !item.generic_args.is_empty() {
241                                raise_error!(
242                                    self,
243                                    span,
244                                    "Found unsupported GAT `{}` when resolving trait `{}`",
245                                    name,
246                                    trait_decl_ref.with_ctx(&self.into_fmt())
247                                )
248                            }
249                            trait_id = TraitRefKind::ItemClause(
250                                Box::new(trait_id),
251                                current_trait_decl_id,
252                                name,
253                                TraitClauseId::new(*index),
254                            );
255                            current_trait_decl_id = self.register_trait_decl_id(
256                                span,
257                                &predicate.hax_skip_binder_ref().trait_ref.def_id,
258                            );
259                        }
260                        Parent {
261                            predicate, index, ..
262                        } => {
263                            trait_id = TraitRefKind::ParentClause(
264                                Box::new(trait_id),
265                                current_trait_decl_id,
266                                TraitClauseId::new(*index),
267                            );
268                            current_trait_decl_id = self.register_trait_decl_id(
269                                span,
270                                &predicate.hax_skip_binder_ref().trait_ref.def_id,
271                            );
272                        }
273                    }
274                }
275
276                // Ignore the arguments: we forbid using universal quantifiers
277                // on the trait clauses for now.
278                TraitRef {
279                    kind: trait_id,
280                    trait_decl_ref,
281                }
282            }
283            ImplExprAtom::Dyn => TraitRef {
284                kind: TraitRefKind::Dyn(trait_decl_ref.clone()),
285                trait_decl_ref,
286            },
287            ImplExprAtom::Builtin {
288                impl_exprs, types, ..
289            } => {
290                let trait_def_id = &impl_source.r#trait.hax_skip_binder_ref().def_id;
291                let trait_def = self.hax_def(trait_def_id)?;
292                let closure_kind = trait_def.lang_item.as_deref().and_then(|lang| match lang {
293                    "fn_once" => Some(ClosureKind::FnOnce),
294                    "fn_mut" => Some(ClosureKind::FnMut),
295                    "r#fn" => Some(ClosureKind::Fn),
296                    _ => None,
297                });
298
299                // TODO: here, if closure_ty is a FnDef, we need to generate the matching
300                // trait impls, with an empty state as the first argument.
301                let kind = if let Some(closure_kind) = closure_kind
302                    && let Some(hax::GenericArg::Type(closure_ty)) = impl_source
303                        .r#trait
304                        .hax_skip_binder_ref()
305                        .generic_args
306                        .first()
307                    && let hax::TyKind::Closure(closure_args) = closure_ty.kind()
308                {
309                    let binder =
310                        self.translate_region_binder(span, &impl_source.r#trait, |ctx, _tref| {
311                            ctx.translate_closure_impl_ref(span, closure_args, closure_kind)
312                        })?;
313                    TraitRefKind::TraitImpl(binder.erase())
314                } else if let hax::FullDefKind::TraitAlias { .. } = trait_def.kind() {
315                    // We reuse the same `def_id` to generate a blanket impl for the trait.
316                    let impl_id = self.register_trait_impl_id(span, trait_def_id);
317                    let mut generics = trait_decl_ref.clone().erase().generics;
318                    assert!(
319                        generics.trait_refs.is_empty(),
320                        "found trait alias with non-empty required predicates"
321                    );
322                    generics.trait_refs = self.translate_trait_impl_exprs(span, &impl_exprs)?;
323                    TraitRefKind::TraitImpl(TraitImplRef {
324                        id: impl_id,
325                        generics,
326                    })
327                } else {
328                    let parent_trait_refs = self.translate_trait_impl_exprs(span, &impl_exprs)?;
329                    let types = types
330                        .iter()
331                        .map(|(def_id, ty, impl_exprs)| {
332                            let name = self.t_ctx.translate_trait_item_name(def_id)?;
333                            let ty = self.translate_ty(span, ty)?;
334                            let trait_refs = self.translate_trait_impl_exprs(span, impl_exprs)?;
335                            Ok((name, ty, trait_refs))
336                        })
337                        .try_collect()?;
338                    TraitRefKind::BuiltinOrAuto {
339                        trait_decl_ref: trait_decl_ref.clone(),
340                        parent_trait_refs,
341                        types,
342                    }
343                };
344                TraitRef {
345                    kind,
346                    trait_decl_ref,
347                }
348            }
349            ImplExprAtom::Drop(DropData::Glue { ty, .. })
350                if let hax::TyKind::Adt(item) = ty.kind() =>
351            {
352                let impl_ref = self.translate_drop_trait_impl_ref(span, item)?;
353                TraitRef {
354                    kind: TraitRefKind::TraitImpl(impl_ref),
355                    trait_decl_ref,
356                }
357            }
358            ImplExprAtom::Drop(..) => {
359                let meta_sized_trait = self.get_lang_item(rustc_hir::LangItem::MetaSized);
360                let meta_sized_trait = self.register_trait_decl_id(span, &meta_sized_trait);
361                let self_ty = trait_decl_ref.clone().erase().generics.types[0].clone();
362                TraitRef {
363                    kind: TraitRefKind::BuiltinOrAuto {
364                        trait_decl_ref: trait_decl_ref.clone(),
365                        parent_trait_refs: [TraitRef::new_builtin(
366                            meta_sized_trait,
367                            self_ty,
368                            Default::default(),
369                        )]
370                        .into(),
371                        types: vec![],
372                    },
373                    trait_decl_ref,
374                }
375            }
376            ImplExprAtom::Error(msg) => {
377                let trait_ref = TraitRef {
378                    kind: TraitRefKind::Unknown(msg.clone()),
379                    trait_decl_ref,
380                };
381                if self.error_on_impl_expr_error {
382                    register_error!(self, span, "Error during trait resolution: {}", msg);
383                }
384                trait_ref
385            }
386        };
387        Ok(trait_ref)
388    }
389}
charon_driver/translate/translate_predicates.rs

charon_driver/translate/
translate_predicates.rs
