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

charon_driver/translate/
translate_predicates.rs
