1use super::translate_ctx::*;
2use charon_lib::ast::*;
3use charon_lib::ids::Vector;
4
5impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
6 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 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 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 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 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 }
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 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 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 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 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}