charon_driver/translate/
translate_predicates.rs

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

charon_driver/translate/
translate_predicates.rs
