1pub mod struct_compat;
12use std::{borrow::Borrow, iter};
13
14use flux_common::{
15 bug,
16 dbg::{self, SpanTrace},
17 iter::IterExt,
18 result::ResultExt as _,
19 span_bug,
20};
21use flux_middle::{
22 THEORY_FUNCS,
23 def_id::{FluxDefId, MaybeExternId},
24 fhir::{self, FhirId, FluxOwnerId, QPathExpr},
25 global_env::GlobalEnv,
26 queries::{QueryErr, QueryResult},
27 query_bug,
28 rty::{
29 self, AssocReft, BoundReftKind, ESpan, INNERMOST, InternalFuncKind, List, RefineArgsExt,
30 WfckResults,
31 fold::TypeFoldable,
32 refining::{self, Refine, Refiner},
33 },
34};
35use flux_rustc_bridge::{
36 ToRustc,
37 lowering::{Lower, UnsupportedErr},
38};
39use itertools::Itertools;
40use rustc_data_structures::{
41 fx::{FxHashMap, FxIndexMap},
42 unord::UnordMap,
43};
44use rustc_errors::Diagnostic;
45use rustc_hash::FxHashSet;
46use rustc_hir::{self as hir, BodyId, OwnerId, Safety, def::DefKind, def_id::DefId};
47use rustc_index::IndexVec;
48use rustc_middle::{
49 middle::resolve_bound_vars::ResolvedArg,
50 ty::{self, AssocItem, AssocTag, BoundVar, TyCtxt},
51};
52use rustc_span::{
53 DUMMY_SP, ErrorGuaranteed, Span, Symbol,
54 symbol::{Ident, kw},
55};
56use rustc_trait_selection::traits;
57use rustc_type_ir::DebruijnIndex;
58
59#[repr(transparent)]
62pub struct ConvCtxt<P>(P);
63
64pub(crate) struct AfterSortck<'a, 'genv, 'tcx> {
65 genv: GlobalEnv<'genv, 'tcx>,
66 wfckresults: &'a WfckResults,
67 next_sort_index: u32,
68 next_type_index: u32,
69 next_region_index: u32,
70 next_const_index: u32,
71}
72
73pub trait ConvPhase<'genv, 'tcx>: Sized {
77 const EXPAND_TYPE_ALIASES: bool;
79
80 const HAS_ELABORATED_INFORMATION: bool;
83
84 type Results: WfckResultsProvider;
85
86 fn genv(&self) -> GlobalEnv<'genv, 'tcx>;
87
88 fn owner(&self) -> FluxOwnerId;
89
90 fn next_sort_vid(&mut self) -> rty::SortVid;
91
92 fn next_type_vid(&mut self) -> rty::TyVid;
93
94 fn next_region_vid(&mut self) -> rty::RegionVid;
95
96 fn next_const_vid(&mut self) -> rty::ConstVid;
97
98 fn results(&self) -> &Self::Results;
99
100 fn insert_node_sort(&mut self, fhir_id: FhirId, sort: rty::Sort);
106
107 fn insert_path_args(&mut self, fhir_id: FhirId, args: rty::GenericArgs);
110
111 fn insert_alias_reft_sort(&mut self, fhir_id: FhirId, fsort: rty::FuncSort);
114
115 fn into_conv_ctxt(self) -> ConvCtxt<Self> {
116 ConvCtxt(self)
117 }
118
119 fn as_conv_ctxt(&mut self) -> &mut ConvCtxt<Self> {
120 unsafe { std::mem::transmute(self) }
122 }
123}
124
125pub trait WfckResultsProvider: Sized {
128 fn bin_op_sort(&self, fhir_id: FhirId) -> rty::Sort;
129
130 fn coercions_for(&self, fhir_id: FhirId) -> &[rty::Coercion];
131
132 fn field_proj(&self, fhir_id: FhirId) -> rty::FieldProj;
133
134 fn record_ctor(&self, fhir_id: FhirId) -> DefId;
135
136 fn param_sort(&self, param_id: fhir::ParamId) -> rty::Sort;
137
138 fn node_sort(&self, fhir_id: FhirId) -> rty::Sort;
139
140 fn node_sort_args(&self, fhir_id: FhirId) -> List<rty::SortArg>;
141}
142
143impl<'genv, 'tcx> ConvPhase<'genv, 'tcx> for AfterSortck<'_, 'genv, 'tcx> {
144 const EXPAND_TYPE_ALIASES: bool = true;
145 const HAS_ELABORATED_INFORMATION: bool = true;
146
147 type Results = WfckResults;
148
149 fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
150 self.genv
151 }
152
153 fn owner(&self) -> FluxOwnerId {
154 self.wfckresults.owner
155 }
156
157 fn next_sort_vid(&mut self) -> rty::SortVid {
158 self.next_sort_index = self.next_sort_index.checked_add(1).unwrap();
159 rty::SortVid::from_u32(self.next_sort_index - 1)
160 }
161
162 fn next_type_vid(&mut self) -> rty::TyVid {
163 self.next_type_index = self.next_type_index.checked_add(1).unwrap();
164 rty::TyVid::from_u32(self.next_type_index - 1)
165 }
166
167 fn next_region_vid(&mut self) -> rty::RegionVid {
168 self.next_region_index = self.next_region_index.checked_add(1).unwrap();
169 rty::RegionVid::from_u32(self.next_region_index - 1)
170 }
171
172 fn next_const_vid(&mut self) -> rty::ConstVid {
173 self.next_const_index = self.next_const_index.checked_add(1).unwrap();
174 rty::ConstVid::from_u32(self.next_const_index - 1)
175 }
176
177 fn results(&self) -> &Self::Results {
178 self.wfckresults
179 }
180
181 fn insert_node_sort(&mut self, _: FhirId, _: rty::Sort) {}
182
183 fn insert_path_args(&mut self, _: FhirId, _: rty::GenericArgs) {}
184
185 fn insert_alias_reft_sort(&mut self, _: FhirId, _: rty::FuncSort) {}
186}
187
188impl WfckResultsProvider for WfckResults {
189 fn bin_op_sort(&self, fhir_id: FhirId) -> rty::Sort {
190 self.bin_op_sorts()
191 .get(fhir_id)
192 .cloned()
193 .unwrap_or_else(|| bug!("binary relation without elaborated sort `{fhir_id:?}`"))
194 }
195
196 fn coercions_for(&self, fhir_id: FhirId) -> &[rty::Coercion] {
197 self.coercions().get(fhir_id).map_or(&[][..], Vec::as_slice)
198 }
199
200 fn field_proj(&self, fhir_id: FhirId) -> rty::FieldProj {
201 *self
202 .field_projs()
203 .get(fhir_id)
204 .unwrap_or_else(|| bug!("field projection without elaboration `{fhir_id:?}`"))
205 }
206
207 fn record_ctor(&self, fhir_id: FhirId) -> DefId {
208 *self
209 .record_ctors()
210 .get(fhir_id)
211 .unwrap_or_else(|| bug!("unelaborated record constructor `{fhir_id:?}`"))
212 }
213
214 fn param_sort(&self, param_id: fhir::ParamId) -> rty::Sort {
215 self.param_sorts()
216 .get(¶m_id)
217 .unwrap_or_else(|| bug!("unresolved sort for param `{param_id:?}`"))
218 .clone()
219 }
220
221 fn node_sort(&self, fhir_id: FhirId) -> rty::Sort {
222 self.node_sorts()
223 .get(fhir_id)
224 .unwrap_or_else(|| bug!("node without elaborated sort for `{fhir_id:?}`"))
225 .clone()
226 }
227
228 fn node_sort_args(&self, fhir_id: FhirId) -> List<rty::SortArg> {
229 self.fn_app_sorts()
230 .get(fhir_id)
231 .unwrap_or_else(|| bug!("fn-app node without elaborated sort_args for `{fhir_id:?}`"))
232 .clone()
233 }
234}
235
236#[derive(Debug)]
237pub(crate) struct Env {
238 layers: Vec<Layer>,
239 early_params: FxIndexMap<fhir::ParamId, Symbol>,
240}
241
242#[derive(Debug, Clone)]
243struct Layer {
244 map: FxIndexMap<fhir::ParamId, ParamEntry>,
245 kind: LayerKind,
246}
247
248#[derive(Debug, Clone, Copy)]
253enum LayerKind {
254 List {
255 bound_regions: u32,
259 },
260 Coalesce(DefId),
261}
262
263#[derive(Debug, Clone)]
264struct ParamEntry {
265 name: Symbol,
266 sort: rty::Sort,
267 mode: rty::InferMode,
268}
269
270#[derive(Debug)]
271struct LookupResult<'a> {
272 kind: LookupResultKind<'a>,
273 var_span: Span,
275}
276
277#[derive(Debug)]
278enum LookupResultKind<'a> {
279 Bound {
280 debruijn: DebruijnIndex,
281 entry: &'a ParamEntry,
282 kind: LayerKind,
283 index: u32,
285 },
286 EarlyParam {
287 name: Symbol,
288 index: u32,
290 },
291}
292
293pub(crate) fn conv_adt_sort_def(
294 genv: GlobalEnv,
295 def_id: MaybeExternId,
296 kind: &fhir::RefinementKind,
297) -> QueryResult<rty::AdtSortDef> {
298 let wfckresults = &WfckResults::new(OwnerId { def_id: def_id.local_id() });
299 let mut cx = AfterSortck::new(genv, wfckresults).into_conv_ctxt();
300 match kind {
301 fhir::RefinementKind::Refined(refined_by) => {
302 let params = refined_by
303 .sort_params
304 .iter()
305 .map(|def_id| def_id_to_param_ty(genv, *def_id))
306 .collect();
307 let fields = refined_by
308 .fields
309 .iter()
310 .map(|(name, sort)| -> QueryResult<_> { Ok((*name, cx.conv_sort(sort)?)) })
311 .try_collect_vec()?;
312 let variants = IndexVec::from([rty::AdtSortVariant::new(fields)]);
313 let def_id = def_id.resolved_id();
314 Ok(rty::AdtSortDef::new(def_id, params, variants, false, true))
315 }
316 fhir::RefinementKind::Reflected => {
317 let enum_def_id = def_id.resolved_id();
318 let mut variants = IndexVec::new();
319 for variant in genv.tcx().adt_def(enum_def_id).variants() {
320 if let Some(field) = variant.fields.iter().next() {
321 let span = genv.tcx().def_span(field.did);
322 let err = genv
323 .sess()
324 .emit_err(errors::FieldsOnReflectedEnumVariant::new(span));
325 Err(err)?;
326 }
327 variants.push(rty::AdtSortVariant::new(vec![]));
328 }
329 Ok(rty::AdtSortDef::new(enum_def_id, vec![], variants, true, false))
330 }
331 }
332}
333
334pub(crate) fn conv_generics(
335 genv: GlobalEnv,
336 generics: &fhir::Generics,
337 def_id: MaybeExternId,
338 is_trait: bool,
339) -> rty::Generics {
340 let opt_self = is_trait.then(|| {
341 let kind = rty::GenericParamDefKind::Base { has_default: false };
342 rty::GenericParamDef { index: 0, name: kw::SelfUpper, def_id: def_id.resolved_id(), kind }
343 });
344 let rust_generics = genv.tcx().generics_of(def_id.resolved_id());
345 let params = {
346 opt_self
347 .into_iter()
348 .chain(rust_generics.own_params.iter().flat_map(|rust_param| {
349 let param = generics
351 .params
352 .iter()
353 .find(|param| param.def_id.resolved_id() == rust_param.def_id)?;
354 Some(rty::GenericParamDef {
355 kind: conv_generic_param_kind(¶m.kind),
356 def_id: param.def_id.resolved_id(),
357 index: rust_param.index,
358 name: rust_param.name,
359 })
360 }))
361 .collect_vec()
362 };
363
364 let rust_generics = genv.tcx().generics_of(def_id.resolved_id());
365 rty::Generics {
366 own_params: List::from_vec(params),
367 parent: rust_generics.parent,
368 parent_count: rust_generics.parent_count,
369 has_self: rust_generics.has_self,
370 }
371}
372
373pub(crate) fn conv_refinement_generics(
374 params: &[fhir::RefineParam],
375 wfckresults: &WfckResults,
376) -> QueryResult<List<rty::RefineParam>> {
377 params
378 .iter()
379 .map(|param| {
380 let sort = wfckresults.param_sort(param.id);
381 let mode = rty::InferMode::from_param_kind(param.kind);
382 Ok(rty::RefineParam { sort, name: param.name, mode })
383 })
384 .try_collect()
385}
386
387fn conv_generic_param_kind(kind: &fhir::GenericParamKind) -> rty::GenericParamDefKind {
388 match kind {
389 fhir::GenericParamKind::Type { default } => {
390 rty::GenericParamDefKind::Base { has_default: default.is_some() }
391 }
392 fhir::GenericParamKind::Lifetime => rty::GenericParamDefKind::Lifetime,
393 fhir::GenericParamKind::Const { .. } => {
394 rty::GenericParamDefKind::Const { has_default: false }
395 }
396 }
397}
398
399pub(crate) fn conv_constant(genv: GlobalEnv, def_id: DefId) -> QueryResult<rty::ConstantInfo> {
400 let ty = genv.tcx().type_of(def_id).no_bound_vars().unwrap();
401 if ty.is_integral() {
402 let val = genv.tcx().const_eval_poly(def_id).ok().and_then(|val| {
403 let val = val.try_to_scalar_int()?;
404 rty::Constant::from_scalar_int(genv.tcx(), val, &ty)
405 });
406 if let Some(constant_) = val {
407 return Ok(rty::ConstantInfo::Interpreted(
408 rty::Expr::constant(constant_),
409 rty::Sort::Int,
410 ));
411 }
412 }
415 Ok(rty::ConstantInfo::Uninterpreted)
416}
417
418pub(crate) fn conv_default_type_parameter(
419 genv: GlobalEnv,
420 def_id: MaybeExternId,
421 ty: &fhir::Ty,
422 wfckresults: &WfckResults,
423) -> QueryResult<rty::TyOrBase> {
424 let mut env = Env::new(&[]);
425 let idx = genv.def_id_to_param_index(def_id.resolved_id());
426 let owner = ty_param_owner(genv, def_id.resolved_id());
427 let param = genv.generics_of(owner)?.param_at(idx as usize, genv)?;
428 let mut cx = AfterSortck::new(genv, wfckresults).into_conv_ctxt();
429 let rty_ty = cx.conv_ty(&mut env, ty)?;
430 cx.try_to_ty_or_base(param.kind, ty.span, &rty_ty)
431}
432
433impl<'a, 'genv, 'tcx> AfterSortck<'a, 'genv, 'tcx> {
434 pub(crate) fn new(genv: GlobalEnv<'genv, 'tcx>, wfckresults: &'a WfckResults) -> Self {
435 Self {
436 genv,
437 wfckresults,
438 next_sort_index: 1,
441 next_type_index: 1,
442 next_region_index: 0,
443 next_const_index: 0,
444 }
445 }
446}
447
448impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
450 fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
451 self.0.genv()
452 }
453
454 fn tcx(&self) -> TyCtxt<'tcx> {
455 self.0.genv().tcx()
456 }
457
458 fn owner(&self) -> FluxOwnerId {
459 self.0.owner()
460 }
461
462 fn results(&self) -> &P::Results {
463 self.0.results()
464 }
465
466 fn next_sort_vid(&mut self) -> rty::SortVid {
467 self.0.next_sort_vid()
468 }
469
470 fn next_type_vid(&mut self) -> rty::TyVid {
471 self.0.next_type_vid()
472 }
473
474 fn next_region_vid(&mut self) -> rty::RegionVid {
475 self.0.next_region_vid()
476 }
477
478 fn next_const_vid(&mut self) -> rty::ConstVid {
479 self.0.next_const_vid()
480 }
481}
482
483fn variant_idx(tcx: TyCtxt, variant_def_id: DefId) -> rty::VariantIdx {
484 let enum_def_id = tcx.parent(variant_def_id);
485 tcx.adt_def(enum_def_id)
486 .variant_index_with_id(variant_def_id)
487}
488
489impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
491 pub(crate) fn conv_qualifier(
492 &mut self,
493 qualifier: &fhir::Qualifier,
494 ) -> QueryResult<rty::Qualifier> {
495 let mut env = Env::new(&[]);
496 env.push_layer(Layer::list(self.results(), 0, qualifier.args));
497 let body = self.conv_expr(&mut env, &qualifier.expr)?;
498 let body = rty::Binder::bind_with_vars(body, env.pop_layer().into_bound_vars(self.genv())?);
499 Ok(rty::Qualifier { def_id: qualifier.def_id, body, global: qualifier.global })
500 }
501
502 pub(crate) fn conv_defn(
503 &mut self,
504 func: &fhir::SpecFunc,
505 ) -> QueryResult<Option<rty::Binder<rty::Expr>>> {
506 if let Some(body) = &func.body {
507 let mut env = Env::new(&[]);
508 env.push_layer(Layer::list(self.results(), 0, func.args));
509 let expr = self.conv_expr(&mut env, body)?;
510 let body =
511 rty::Binder::bind_with_vars(expr, env.pop_layer().into_bound_vars(self.genv())?);
512 Ok(Some(body))
513 } else {
514 Ok(None)
515 }
516 }
517
518 pub(crate) fn conv_primop_prop(
519 &mut self,
520 primop_prop: &fhir::PrimOpProp,
521 ) -> QueryResult<rty::PrimOpProp> {
522 let mut env = Env::new(&[]);
523 env.push_layer(Layer::list(self.results(), 0, primop_prop.args));
524 let body = self.conv_expr(&mut env, &primop_prop.body)?;
525 let body = rty::Binder::bind_with_vars(body, env.pop_layer().into_bound_vars(self.genv())?);
526 let op = match primop_prop.op {
527 fhir::BinOp::BitAnd => rty::BinOp::BitAnd,
528 fhir::BinOp::BitOr => rty::BinOp::BitOr,
529 fhir::BinOp::BitXor => rty::BinOp::BitXor,
530 fhir::BinOp::BitShl => rty::BinOp::BitShl,
531 fhir::BinOp::BitShr => rty::BinOp::BitShr,
532 _ => {
533 span_bug!(
534 primop_prop.span,
535 "unexpected binary operator in primitive property: {:?}",
536 primop_prop.op
537 )
538 }
539 };
540 Ok(rty::PrimOpProp { def_id: primop_prop.def_id, op, body })
541 }
542}
543
544impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
546 pub(crate) fn conv_constant_expr(&mut self, expr: &fhir::Expr) -> QueryResult<rty::Expr> {
547 let mut env = Env::new(&[]);
548 self.conv_expr(&mut env, expr)
549 }
550
551 pub(crate) fn conv_enum_variants(
552 &mut self,
553 enum_id: MaybeExternId,
554 enum_def: &fhir::EnumDef,
555 ) -> QueryResult<Vec<rty::PolyVariant>> {
556 let reflected = enum_def.refinement.is_reflected();
557 enum_def
558 .variants
559 .iter()
560 .map(|variant| self.conv_enum_variant(enum_id, variant, reflected))
561 .try_collect_vec()
562 }
563
564 fn conv_enum_variant(
565 &mut self,
566 enum_id: MaybeExternId,
567 variant: &fhir::VariantDef,
568 reflected: bool,
569 ) -> QueryResult<rty::PolyVariant> {
570 let mut env = Env::new(&[]);
571 env.push_layer(Layer::list(self.results(), 0, variant.params));
572
573 let fields = variant
575 .fields
576 .iter()
577 .map(|field| self.conv_ty(&mut env, &field.ty))
578 .try_collect()?;
579
580 let adt_def = self.genv().adt_def(enum_id)?;
581 let idxs = if reflected {
582 let enum_def_id = enum_id.resolved_id();
583 let idx = variant_idx(self.tcx(), variant.def_id.to_def_id());
584 rty::Expr::ctor_enum(enum_def_id, idx)
585 } else {
586 self.conv_expr(&mut env, &variant.ret.idx)?
587 };
588 let variant = rty::VariantSig::new(
589 adt_def,
590 rty::GenericArg::identity_for_item(self.genv(), enum_id.resolved_id())?,
591 fields,
592 idxs,
593 List::empty(),
594 );
595
596 Ok(rty::Binder::bind_with_vars(variant, env.pop_layer().into_bound_vars(self.genv())?))
597 }
598
599 pub(crate) fn conv_struct_variant(
600 &mut self,
601 struct_id: MaybeExternId,
602 struct_def: &fhir::StructDef,
603 ) -> QueryResult<rty::Opaqueness<rty::PolyVariant>> {
604 let mut env = Env::new(&[]);
605 env.push_layer(Layer::list(self.results(), 0, struct_def.params));
606
607 if let fhir::StructKind::Transparent { fields } = &struct_def.kind {
608 let adt_def = self.genv().adt_def(struct_id)?;
609
610 let fields = fields
611 .iter()
612 .map(|field_def| self.conv_ty(&mut env, &field_def.ty))
613 .try_collect()?;
614
615 let vars = env.pop_layer().into_bound_vars(self.genv())?;
616 let idx = rty::Expr::ctor_struct(
617 struct_id.resolved_id(),
618 (0..vars.len())
619 .map(|idx| {
620 rty::Expr::bvar(
621 INNERMOST,
622 BoundVar::from_usize(idx),
623 rty::BoundReftKind::Anon,
624 )
625 })
626 .collect(),
627 );
628
629 let requires = adt_def
630 .invariants()
631 .iter_identity()
632 .map(|inv| inv.apply(&idx))
633 .collect();
634
635 let variant = rty::VariantSig::new(
636 adt_def,
637 rty::GenericArg::identity_for_item(self.genv(), struct_id.resolved_id())?,
638 fields,
639 idx,
640 requires,
641 );
642 let variant = rty::Binder::bind_with_vars(variant, vars);
643 Ok(rty::Opaqueness::Transparent(variant))
644 } else {
645 Ok(rty::Opaqueness::Opaque)
646 }
647 }
648
649 pub(crate) fn conv_type_alias(
650 &mut self,
651 ty_alias_id: MaybeExternId,
652 ty_alias: &fhir::TyAlias,
653 ) -> QueryResult<rty::TyCtor> {
654 let generics = self
655 .genv()
656 .fhir_get_generics(ty_alias_id.local_id())?
657 .unwrap();
658
659 let mut env = Env::new(generics.refinement_params);
660
661 if let Some(index) = &ty_alias.index {
662 env.push_layer(Layer::list(self.results(), 0, std::slice::from_ref(index)));
663 let ty = self.conv_ty(&mut env, &ty_alias.ty)?;
664
665 Ok(rty::Binder::bind_with_vars(ty, env.pop_layer().into_bound_vars(self.genv())?))
666 } else {
667 let ctor = self
668 .conv_ty(&mut env, &ty_alias.ty)?
669 .shallow_canonicalize()
670 .as_ty_or_base()
671 .as_base()
672 .ok_or_else(|| self.emit(errors::InvalidBaseInstance::new(ty_alias.span)))?;
673 Ok(ctor.to_ty_ctor())
674 }
675 }
676
677 pub(crate) fn conv_fn_sig(
678 &mut self,
679 fn_id: MaybeExternId,
680 fn_sig: &fhir::FnSig,
681 ) -> QueryResult<rty::PolyFnSig> {
682 let decl = &fn_sig.decl;
683 let header = fn_sig.header;
684
685 let late_bound_regions =
686 refining::refine_bound_variables(&self.genv().lower_late_bound_vars(fn_id.local_id())?);
687
688 let generics = self.genv().fhir_get_generics(fn_id.local_id())?.unwrap();
689 let mut env = Env::new(generics.refinement_params);
690 env.push_layer(Layer::list(self.results(), late_bound_regions.len() as u32, &[]));
691
692 let body_id = self.tcx().hir_node_by_def_id(fn_id.local_id()).body_id();
693 let fn_sig = self.conv_fn_decl(&mut env, header.safety(), header.abi, decl, body_id)?;
694
695 let vars = late_bound_regions
696 .iter()
697 .chain(env.pop_layer().into_bound_vars(self.genv())?.iter())
698 .cloned()
699 .collect();
700
701 Ok(rty::PolyFnSig::bind_with_vars(fn_sig, vars))
702 }
703
704 pub(crate) fn conv_generic_predicates(
705 &mut self,
706 def_id: MaybeExternId,
707 generics: &fhir::Generics,
708 ) -> QueryResult<rty::EarlyBinder<rty::GenericPredicates>> {
709 let env = &mut Env::new(generics.refinement_params);
710
711 let predicates = if let Some(fhir_predicates) = generics.predicates {
712 let mut clauses = vec![];
713 for pred in fhir_predicates {
714 let span = pred.bounded_ty.span;
715 let bounded_ty = self.conv_ty(env, &pred.bounded_ty)?;
716 for clause in self.conv_generic_bounds(env, span, bounded_ty, pred.bounds)? {
717 clauses.push(clause);
718 }
719 }
720 self.match_clauses(def_id, &clauses)?
721 } else {
722 self.genv()
723 .lower_predicates_of(def_id)?
724 .refine(&Refiner::default_for_item(self.genv(), def_id.resolved_id())?)?
725 };
726 Ok(rty::EarlyBinder(predicates))
727 }
728
729 fn match_clauses(
730 &self,
731 def_id: MaybeExternId,
732 refined_clauses: &[rty::Clause],
733 ) -> QueryResult<rty::GenericPredicates> {
734 let tcx = self.genv().tcx();
735 let predicates = tcx.predicates_of(def_id);
736 let unrefined_clauses = predicates.predicates;
737
738 let mut map = UnordMap::default();
741 for (j, clause) in refined_clauses.iter().enumerate() {
742 let clause = clause.to_rustc(tcx);
743 let Some((i, _)) = unrefined_clauses.iter().find_position(|it| it.0 == clause) else {
744 self.emit_fail_to_match_predicates(def_id)?;
745 };
746 if map.insert(i, j).is_some() {
747 self.emit_fail_to_match_predicates(def_id)?;
748 }
749 }
750
751 let refiner = Refiner::default_for_item(self.genv(), def_id.resolved_id())?;
754 let mut clauses = vec![];
755 for (i, (clause, span)) in unrefined_clauses.iter().enumerate() {
756 let clause = if let Some(j) = map.get(&i) {
757 refined_clauses[*j].clone()
758 } else {
759 clause
760 .lower(tcx)
761 .map_err(|reason| {
762 let err = UnsupportedErr::new(reason).with_span(*span);
763 QueryErr::unsupported(def_id.resolved_id(), err)
764 })?
765 .refine(&refiner)?
766 };
767 clauses.push(clause);
768 }
769
770 Ok(rty::GenericPredicates {
771 parent: predicates.parent,
772 predicates: List::from_vec(clauses),
773 })
774 }
775
776 fn emit_fail_to_match_predicates(&self, def_id: MaybeExternId) -> Result<!, ErrorGuaranteed> {
777 let span = self.tcx().def_span(def_id.resolved_id());
778 Err(self.emit(errors::FailToMatchPredicates { span }))
779 }
780
781 pub(crate) fn conv_opaque_ty(
782 &mut self,
783 opaque_ty: &fhir::OpaqueTy,
784 ) -> QueryResult<rty::Clauses> {
785 let def_id = opaque_ty.def_id;
786 let parent = self.tcx().local_parent(def_id.local_id());
787 let refparams = &self
788 .genv()
789 .fhir_get_generics(parent)?
790 .unwrap()
791 .refinement_params;
792
793 let env = &mut Env::new(refparams);
794
795 let args = rty::GenericArg::identity_for_item(self.genv(), def_id.resolved_id())?;
796 let alias_ty = rty::AliasTy::new(def_id.resolved_id(), args, env.to_early_param_args());
797 let self_ty = rty::BaseTy::opaque(alias_ty).to_ty();
798 Ok(self
800 .conv_generic_bounds(env, DUMMY_SP, self_ty, opaque_ty.bounds)?
801 .into_iter()
802 .collect())
803 }
804
805 pub(crate) fn conv_assoc_reft_body(
806 &mut self,
807 params: &[fhir::RefineParam],
808 body: &fhir::Expr,
809 output: &fhir::Sort,
810 ) -> QueryResult<rty::Lambda> {
811 let mut env = Env::new(&[]);
812 env.push_layer(Layer::list(self.results(), 0, params));
813 let expr = self.conv_expr(&mut env, body)?;
814 let output = self.conv_sort(output)?;
815 let inputs = env.pop_layer().into_bound_vars(self.genv())?;
816 Ok(rty::Lambda::bind_with_vars(expr, inputs, output))
817 }
818}
819
820impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
822 pub(crate) fn conv_sort(&mut self, sort: &fhir::Sort) -> QueryResult<rty::Sort> {
823 let sort = match sort {
824 fhir::Sort::Path(path) => self.conv_sort_path(path)?,
825 fhir::Sort::BitVec(size) => rty::Sort::BitVec(rty::BvSize::Fixed(*size)),
826 fhir::Sort::Loc => rty::Sort::Loc,
827 fhir::Sort::Func(fsort) => rty::Sort::Func(self.conv_poly_func_sort(fsort)?),
828 fhir::Sort::SortOf(bty) => {
829 let rty::TyOrCtor::Ctor(ty_ctor) = self.conv_bty(&mut Env::empty(), bty, None)?
830 else {
831 return Err(self.emit(errors::RefinedUnrefinableType::new(bty.span)))?;
833 };
834 ty_ctor.sort()
835 }
836 fhir::Sort::Infer => rty::Sort::Infer(rty::SortVar(self.next_sort_vid())),
837 fhir::Sort::Err(_) => rty::Sort::Err,
838 };
839 Ok(sort)
840 }
841
842 fn conv_poly_func_sort(&mut self, sort: &fhir::PolyFuncSort) -> QueryResult<rty::PolyFuncSort> {
843 let params = iter::repeat_n(rty::SortParamKind::Sort, sort.params).collect();
844 Ok(rty::PolyFuncSort::new(params, self.conv_func_sort(&sort.fsort)?))
845 }
846
847 fn conv_func_sort(&mut self, fsort: &fhir::FuncSort) -> QueryResult<rty::FuncSort> {
848 let inputs = fsort
849 .inputs()
850 .iter()
851 .map(|sort| self.conv_sort(sort))
852 .try_collect()?;
853 Ok(rty::FuncSort::new(inputs, self.conv_sort(fsort.output())?))
854 }
855
856 fn conv_sort_path(&mut self, path: &fhir::SortPath) -> QueryResult<rty::Sort> {
857 let ctor = match path.res {
858 fhir::SortRes::PrimSort(fhir::PrimSort::Int) => {
859 self.check_prim_sort_generics(path, fhir::PrimSort::Int)?;
860 return Ok(rty::Sort::Int);
861 }
862 fhir::SortRes::PrimSort(fhir::PrimSort::Bool) => {
863 self.check_prim_sort_generics(path, fhir::PrimSort::Bool)?;
864 return Ok(rty::Sort::Bool);
865 }
866 fhir::SortRes::PrimSort(fhir::PrimSort::Real) => {
867 self.check_prim_sort_generics(path, fhir::PrimSort::Real)?;
868 return Ok(rty::Sort::Real);
869 }
870 fhir::SortRes::PrimSort(fhir::PrimSort::Char) => {
871 self.check_prim_sort_generics(path, fhir::PrimSort::Char)?;
872 return Ok(rty::Sort::Char);
873 }
874 fhir::SortRes::PrimSort(fhir::PrimSort::Str) => {
875 self.check_prim_sort_generics(path, fhir::PrimSort::Str)?;
876 return Ok(rty::Sort::Str);
877 }
878 fhir::SortRes::SortParam(n) => return Ok(rty::Sort::Var(rty::ParamSort::from(n))),
879 fhir::SortRes::TyParam(def_id) => {
880 if !path.args.is_empty() {
881 let err = errors::GenericsOnSortTyParam::new(
882 path.segments.last().unwrap().span,
883 path.args.len(),
884 );
885 Err(self.emit(err))?;
886 }
887 return Ok(rty::Sort::Param(def_id_to_param_ty(self.genv(), def_id)));
888 }
889 fhir::SortRes::SelfParam { .. } => {
890 if !path.args.is_empty() {
891 let err = errors::GenericsOnSelf::new(
892 path.segments.last().unwrap().span,
893 path.args.len(),
894 );
895 Err(self.emit(err))?;
896 }
897 return Ok(rty::Sort::Param(rty::SELF_PARAM_TY));
898 }
899 fhir::SortRes::SelfAlias { alias_to } => {
900 if !path.args.is_empty() {
901 let err = errors::GenericsOnSelf::new(
902 path.segments.last().unwrap().span,
903 path.args.len(),
904 );
905 Err(self.emit(err))?;
906 }
907 return Ok(self
908 .genv()
909 .sort_of_self_ty_alias(alias_to)?
910 .unwrap_or(rty::Sort::Err));
911 }
912 fhir::SortRes::SelfParamAssoc { trait_id, ident } => {
913 let res = fhir::Res::SelfTyParam { trait_: trait_id };
914 let assoc_segment =
915 fhir::PathSegment { args: &[], constraints: &[], ident, res: fhir::Res::Err };
916 let mut env = Env::empty();
917 let alias_ty =
918 self.conv_type_relative_type_path(&mut env, ident.span, res, &assoc_segment)?;
919 return Ok(rty::Sort::Alias(rty::AliasKind::Projection, alias_ty));
920 }
921 fhir::SortRes::PrimSort(fhir::PrimSort::Set) => {
922 self.check_prim_sort_generics(path, fhir::PrimSort::Set)?;
923 rty::SortCtor::Set
924 }
925 fhir::SortRes::PrimSort(fhir::PrimSort::Map) => {
926 self.check_prim_sort_generics(path, fhir::PrimSort::Map)?;
927 rty::SortCtor::Map
928 }
929 fhir::SortRes::User(def_id) => {
930 self.check_user_defined_sort_param_count(path, def_id)?;
931 rty::SortCtor::User(def_id)
932 }
933 fhir::SortRes::Adt(def_id) => {
934 let sort_def = self.genv().adt_sort_def_of(def_id)?;
935 if path.args.len() != sort_def.param_count() {
936 let err = errors::IncorrectGenericsOnSort::new(
937 self.genv(),
938 def_id,
939 path.segments.last().unwrap().span,
940 path.args.len(),
941 sort_def.param_count(),
942 );
943 Err(self.emit(err))?;
944 }
945 rty::SortCtor::Adt(sort_def)
946 }
947 };
948 let args = path.args.iter().map(|t| self.conv_sort(t)).try_collect()?;
949
950 Ok(rty::Sort::app(ctor, args))
951 }
952
953 fn check_user_defined_sort_param_count(
954 &mut self,
955 path: &fhir::SortPath<'_>,
956 def_id: FluxDefId,
957 ) -> QueryResult {
958 let expected_param_count = self.genv().sort_decl_param_count(def_id);
959 if path.args.len() != expected_param_count {
960 let err = errors::IncorrectGenericsOnUserDefinedOpaqueSort::new(
961 path.segments.last().unwrap().span,
962 def_id.name(),
963 expected_param_count,
964 path.args.len(),
965 );
966 Err(self.emit(err))?;
967 }
968 Ok(())
969 }
970
971 fn check_prim_sort_generics(
972 &mut self,
973 path: &fhir::SortPath<'_>,
974 prim_sort: fhir::PrimSort,
975 ) -> QueryResult {
976 if path.args.len() != prim_sort.generics() {
977 let err = errors::GenericsOnPrimitiveSort::new(
978 path.segments.last().unwrap().span,
979 prim_sort.name_str(),
980 path.args.len(),
981 prim_sort.generics(),
982 );
983 Err(self.emit(err))?;
984 }
985 Ok(())
986 }
987}
988
989impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
991 fn conv_fn_decl(
992 &mut self,
993 env: &mut Env,
994 safety: Safety,
995 abi: rustc_abi::ExternAbi,
996 decl: &fhir::FnDecl,
997 body_id: Option<BodyId>,
998 ) -> QueryResult<rty::FnSig> {
999 let mut requires = vec![];
1000 for req in decl.requires {
1001 requires.push(self.conv_requires(env, req)?);
1002 }
1003
1004 let mut inputs = vec![];
1005 let params =
1006 if let Some(body_id) = body_id { self.tcx().hir_body(body_id).params } else { &[] };
1007 for (i, ty) in decl.inputs.iter().enumerate() {
1008 let ty = if let Some(param) = params.get(i)
1009 && let hir::PatKind::Binding(_, _, ident, _) = param.pat.kind
1010 {
1011 self.conv_ty_with_name(env, ty, ident.name)?
1012 } else {
1013 self.conv_ty(env, ty)?
1014 };
1015 inputs.push(ty);
1016 }
1017
1018 let output = self.conv_fn_output(env, &decl.output)?;
1019
1020 Ok(rty::FnSig::new(safety, abi, requires.into(), inputs.into(), output))
1021 }
1022
1023 fn conv_requires(
1024 &mut self,
1025 env: &mut Env,
1026 requires: &fhir::Requires,
1027 ) -> QueryResult<rty::Expr> {
1028 if requires.params.is_empty() {
1029 self.conv_expr(env, &requires.pred)
1030 } else {
1031 env.push_layer(Layer::list(self.results(), 0, requires.params));
1032 let pred = self.conv_expr(env, &requires.pred)?;
1033 let sorts = env.pop_layer().into_bound_vars(self.genv())?;
1034 Ok(rty::Expr::forall(rty::Binder::bind_with_vars(pred, sorts)))
1035 }
1036 }
1037
1038 fn conv_ensures(
1039 &mut self,
1040 env: &mut Env,
1041 ensures: &fhir::Ensures,
1042 ) -> QueryResult<rty::Ensures> {
1043 match ensures {
1044 fhir::Ensures::Type(loc, ty) => {
1045 Ok(rty::Ensures::Type(self.conv_loc(env, *loc)?, self.conv_ty(env, ty)?))
1046 }
1047 fhir::Ensures::Pred(pred) => Ok(rty::Ensures::Pred(self.conv_expr(env, pred)?)),
1048 }
1049 }
1050
1051 fn conv_fn_output(
1052 &mut self,
1053 env: &mut Env,
1054 output: &fhir::FnOutput,
1055 ) -> QueryResult<rty::Binder<rty::FnOutput>> {
1056 env.push_layer(Layer::list(self.results(), 0, output.params));
1057
1058 let ret = self.conv_ty(env, &output.ret)?;
1059
1060 let ensures: List<rty::Ensures> = output
1061 .ensures
1062 .iter()
1063 .map(|ens| self.conv_ensures(env, ens))
1064 .try_collect()?;
1065 let output = rty::FnOutput::new(ret, ensures);
1066
1067 let vars = env.pop_layer().into_bound_vars(self.genv())?;
1068 Ok(rty::Binder::bind_with_vars(output, vars))
1069 }
1070
1071 fn conv_generic_bounds(
1072 &mut self,
1073 env: &mut Env,
1074 bounded_ty_span: Span,
1075 bounded_ty: rty::Ty,
1076 bounds: fhir::GenericBounds,
1077 ) -> QueryResult<Vec<rty::Clause>> {
1078 let mut clauses = vec![];
1079 for bound in bounds {
1080 match bound {
1081 fhir::GenericBound::Trait(poly_trait_ref) => {
1082 match poly_trait_ref.modifiers {
1083 fhir::TraitBoundModifier::None => {
1084 self.conv_poly_trait_ref(
1085 env,
1086 bounded_ty_span,
1087 &bounded_ty,
1088 poly_trait_ref,
1089 &mut clauses,
1090 )?;
1091 }
1092 fhir::TraitBoundModifier::Maybe => {
1093 }
1097 }
1098 }
1099 fhir::GenericBound::Outlives(lft) => {
1100 let re = self.conv_lifetime(env, *lft, bounded_ty_span);
1101 clauses.push(rty::Clause::new(
1102 List::empty(),
1103 rty::ClauseKind::TypeOutlives(rty::OutlivesPredicate(
1104 bounded_ty.clone(),
1105 re,
1106 )),
1107 ));
1108 }
1109 }
1110 }
1111 Ok(clauses)
1112 }
1113
1114 fn conv_poly_trait_ref(
1116 &mut self,
1117 env: &mut Env,
1118 span: Span,
1119 bounded_ty: &rty::Ty,
1120 poly_trait_ref: &fhir::PolyTraitRef,
1121 clauses: &mut Vec<rty::Clause>,
1122 ) -> QueryResult {
1123 let generic_params = &poly_trait_ref.bound_generic_params;
1124 let layer =
1125 Layer::list(self.results(), generic_params.len() as u32, poly_trait_ref.refine_params);
1126 env.push_layer(layer);
1127
1128 let trait_id = poly_trait_ref.trait_def_id();
1129 let generics = self.genv().generics_of(trait_id)?;
1130 let trait_segment = poly_trait_ref.trait_ref.last_segment();
1131
1132 let self_param = generics.param_at(0, self.genv())?;
1133 let mut args = vec![
1134 self.try_to_ty_or_base(self_param.kind, span, bounded_ty)?
1135 .into(),
1136 ];
1137 self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;
1138
1139 let vars = env.top_layer().to_bound_vars(self.genv())?;
1140 let poly_trait_ref = rty::Binder::bind_with_vars(
1141 rty::TraitRef { def_id: trait_id, args: args.into() },
1142 vars,
1143 );
1144
1145 clauses.push(
1146 poly_trait_ref
1147 .clone()
1148 .map(|trait_ref| {
1149 rty::ClauseKind::Trait(rty::TraitPredicate { trait_ref: trait_ref.clone() })
1150 })
1151 .into(),
1152 );
1153
1154 for cstr in trait_segment.constraints {
1155 self.conv_assoc_item_constraint(env, &poly_trait_ref, cstr, clauses)?;
1156 }
1157
1158 env.pop_layer();
1159
1160 Ok(())
1161 }
1162
1163 fn conv_assoc_item_constraint(
1164 &mut self,
1165 env: &mut Env,
1166 poly_trait_ref: &rty::PolyTraitRef,
1167 constraint: &fhir::AssocItemConstraint,
1168 clauses: &mut Vec<rty::Clause>,
1169 ) -> QueryResult {
1170 let tcx = self.tcx();
1171
1172 let candidate = self.probe_single_bound_for_assoc_item(
1173 || traits::supertraits(tcx, poly_trait_ref.to_rustc(tcx)),
1174 constraint.ident,
1175 AssocTag::Type,
1176 )?;
1177 let assoc_item_id = AssocTag::Type
1178 .trait_defines_item_named(self.genv(), candidate.def_id(), constraint.ident)?
1179 .unwrap()
1180 .def_id;
1181
1182 let fhir::AssocItemConstraintKind::Equality { term } = &constraint.kind;
1183 let span = term.span;
1184 let term = self.conv_ty(env, term)?;
1185 let term = self.ty_to_subset_ty_ctor(span, &term)?;
1186
1187 let clause = poly_trait_ref
1188 .clone()
1189 .map(|trait_ref| {
1190 let args = trait_ref.args;
1192 let refine_args = List::empty();
1193 let projection_ty = rty::AliasTy { def_id: assoc_item_id, args, refine_args };
1194
1195 rty::ClauseKind::Projection(rty::ProjectionPredicate { projection_ty, term })
1196 })
1197 .into();
1198
1199 clauses.push(clause);
1200 Ok(())
1201 }
1202
1203 fn conv_ty_with_name(
1204 &mut self,
1205 env: &mut Env,
1206 ty: &fhir::Ty,
1207 name: Symbol,
1208 ) -> QueryResult<rty::Ty> {
1209 if let fhir::TyKind::BaseTy(bty) = &ty.kind {
1210 Ok(self.conv_bty(env, bty, Some(name))?.to_ty())
1211 } else {
1212 self.conv_ty(env, ty)
1213 }
1214 }
1215
1216 fn conv_ty(&mut self, env: &mut Env, ty: &fhir::Ty) -> QueryResult<rty::Ty> {
1217 match &ty.kind {
1218 fhir::TyKind::BaseTy(bty) => Ok(self.conv_bty(env, bty, None)?.to_ty()),
1219 fhir::TyKind::Indexed(bty, idx) => {
1220 let fhir_id = bty.fhir_id;
1221 let rty::TyOrCtor::Ctor(ty_ctor) = self.conv_bty(env, bty, None)? else {
1222 return Err(self.emit(errors::RefinedUnrefinableType::new(bty.span)))?;
1223 };
1224 let idx = self.conv_expr(env, idx)?;
1225 self.0.insert_node_sort(fhir_id, ty_ctor.sort());
1226 Ok(ty_ctor.replace_bound_reft(&idx))
1227 }
1228 fhir::TyKind::Exists(params, ty) => {
1229 let layer = Layer::list(self.results(), 0, params);
1230 env.push_layer(layer);
1231 let ty = self.conv_ty(env, ty)?;
1232 let sorts = env.pop_layer().into_bound_vars(self.genv())?;
1233 if sorts.is_empty() {
1234 Ok(ty.shift_out_escaping(1))
1235 } else {
1236 Ok(rty::Ty::exists(rty::Binder::bind_with_vars(ty, sorts)))
1237 }
1238 }
1239 fhir::TyKind::StrgRef(lft, loc, ty) => {
1240 let re = self.conv_lifetime(env, *lft, ty.span);
1241 let loc = self.conv_loc(env, **loc)?;
1242 let ty = self.conv_ty(env, ty)?;
1243 Ok(rty::Ty::strg_ref(re, loc, ty))
1244 }
1245 fhir::TyKind::Ref(lft, fhir::MutTy { ty, mutbl }) => {
1246 let region = self.conv_lifetime(env, *lft, ty.span);
1247 Ok(rty::Ty::mk_ref(region, self.conv_ty(env, ty)?, *mutbl))
1248 }
1249 fhir::TyKind::BareFn(bare_fn) => {
1250 let mut env = Env::empty();
1251 env.push_layer(Layer::list(
1252 self.results(),
1253 bare_fn.generic_params.len() as u32,
1254 &[],
1255 ));
1256 let fn_sig =
1257 self.conv_fn_decl(&mut env, bare_fn.safety, bare_fn.abi, bare_fn.decl, None)?;
1258 let vars = bare_fn
1259 .generic_params
1260 .iter()
1261 .map(|param| self.param_as_bound_var(param))
1262 .try_collect()?;
1263 let poly_fn_sig = rty::Binder::bind_with_vars(fn_sig, vars);
1264 Ok(rty::BaseTy::FnPtr(poly_fn_sig).to_ty())
1265 }
1266 fhir::TyKind::Tuple(tys) => {
1267 let tys: List<rty::Ty> =
1268 tys.iter().map(|ty| self.conv_ty(env, ty)).try_collect()?;
1269 Ok(rty::Ty::tuple(tys))
1270 }
1271 fhir::TyKind::Array(ty, len) => {
1272 Ok(rty::Ty::array(self.conv_ty(env, ty)?, self.conv_const_arg(*len)))
1273 }
1274 fhir::TyKind::Never => Ok(rty::Ty::never()),
1275 fhir::TyKind::Constr(pred, ty) => {
1276 let pred = self.conv_expr(env, pred)?;
1277 Ok(rty::Ty::constr(pred, self.conv_ty(env, ty)?))
1278 }
1279 fhir::TyKind::RawPtr(ty, mutability) => {
1280 Ok(rty::Ty::indexed(
1281 rty::BaseTy::RawPtr(self.conv_ty(env, ty)?, *mutability),
1282 rty::Expr::unit(),
1283 ))
1284 }
1285 fhir::TyKind::OpaqueDef(opaque_ty) => self.conv_opaque_def(env, opaque_ty, ty.span),
1286 fhir::TyKind::TraitObject(trait_bounds, lft, syn) => {
1287 if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) {
1288 self.conv_trait_object(env, trait_bounds, *lft, ty.span)
1289 } else {
1290 span_bug!(ty.span, "dyn* traits not supported yet")
1291 }
1292 }
1293 fhir::TyKind::Infer => Ok(rty::Ty::infer(self.next_type_vid())),
1294 fhir::TyKind::Err(err) => Err(QueryErr::Emitted(*err)),
1295 }
1296 }
1297
1298 fn conv_opaque_def(
1300 &mut self,
1301 env: &mut Env,
1302 opaque_ty: &fhir::OpaqueTy,
1303 span: Span,
1304 ) -> QueryResult<rty::Ty> {
1305 let def_id = opaque_ty.def_id;
1306
1307 if P::HAS_ELABORATED_INFORMATION {
1308 let lifetimes = self.tcx().opaque_captured_lifetimes(def_id.local_id());
1309
1310 let generics = self.tcx().generics_of(opaque_ty.def_id);
1311
1312 let offset = generics.parent_count;
1313
1314 let args = rty::GenericArg::for_item(self.genv(), def_id.resolved_id(), |param, _| {
1315 if let Some(i) = (param.index as usize).checked_sub(offset) {
1316 let (lifetime, _) = lifetimes[i];
1317 rty::GenericArg::Lifetime(self.conv_resolved_lifetime(env, lifetime, span))
1318 } else {
1319 rty::GenericArg::from_param_def(param)
1320 }
1321 })?;
1322 let reft_args = rty::RefineArgs::identity_for_item(self.genv(), def_id.resolved_id())?;
1323 let alias_ty = rty::AliasTy::new(def_id.resolved_id(), args, reft_args);
1324 Ok(rty::BaseTy::opaque(alias_ty).to_ty())
1325 } else {
1326 self.conv_opaque_ty(opaque_ty)?;
1330
1331 let alias_ty = rty::AliasTy::new(def_id.resolved_id(), List::empty(), List::empty());
1334 Ok(rty::BaseTy::opaque(alias_ty).to_ty())
1335 }
1336 }
1337
1338 fn conv_trait_object(
1339 &mut self,
1340 env: &mut Env,
1341 trait_bounds: &[fhir::PolyTraitRef],
1342 lifetime: fhir::Lifetime,
1343 span: Span,
1344 ) -> QueryResult<rty::Ty> {
1345 let mut bounds = vec![];
1352 let dummy_self = rty::Ty::trait_object_dummy_self();
1353 for trait_bound in trait_bounds.iter().rev() {
1354 self.conv_poly_trait_ref(env, trait_bound.span, &dummy_self, trait_bound, &mut bounds)?;
1355 }
1356
1357 let mut trait_bounds = vec![];
1359 let mut projection_bounds = vec![];
1360 for pred in bounds {
1361 let bound_pred = pred.kind();
1362 let vars = bound_pred.vars().clone();
1363 match bound_pred.skip_binder() {
1364 rty::ClauseKind::Trait(trait_pred) => {
1365 trait_bounds.push(rty::Binder::bind_with_vars(trait_pred.trait_ref, vars));
1366 }
1367 rty::ClauseKind::Projection(proj) => {
1368 projection_bounds.push(rty::Binder::bind_with_vars(proj, vars));
1369 }
1370 rty::ClauseKind::RegionOutlives(_) => {}
1371 rty::ClauseKind::TypeOutlives(_) => {}
1372 rty::ClauseKind::ConstArgHasType(..) => {
1373 bug!("did not expect {pred:?} clause in object bounds");
1374 }
1375 }
1376 }
1377
1378 let (mut auto_traits, regular_traits): (Vec<_>, Vec<_>) = trait_bounds
1380 .into_iter()
1381 .partition(|trait_ref| self.tcx().trait_is_auto(trait_ref.def_id()));
1382
1383 {
1385 let mut duplicates = FxHashSet::default();
1386 auto_traits.retain(|trait_ref| duplicates.insert(trait_ref.def_id()));
1387 }
1388
1389 let regular_trait_predicates = regular_traits.into_iter().map(|poly_trait_ref| {
1390 poly_trait_ref.map(|trait_ref| {
1391 let args = trait_ref.args.iter().skip(1).cloned().collect();
1393 rty::ExistentialPredicate::Trait(rty::ExistentialTraitRef {
1394 def_id: trait_ref.def_id,
1395 args,
1396 })
1397 })
1398 });
1399
1400 let auto_trait_predicates = auto_traits.into_iter().map(|trait_def| {
1401 rty::Binder::dummy(rty::ExistentialPredicate::AutoTrait(trait_def.def_id()))
1402 });
1403
1404 let existential_projections = projection_bounds.into_iter().map(|bound| {
1405 bound.map(|proj| {
1406 let args = proj.projection_ty.args.iter().skip(1).cloned().collect();
1408 rty::ExistentialPredicate::Projection(rty::ExistentialProjection {
1409 def_id: proj.projection_ty.def_id,
1410 args,
1411 term: proj.term.clone(),
1412 })
1413 })
1414 });
1415
1416 let existential_predicates = {
1417 let mut v = regular_trait_predicates
1418 .chain(existential_projections)
1419 .chain(auto_trait_predicates)
1420 .collect_vec();
1421 v.sort_by(|a, b| {
1422 a.as_ref()
1423 .skip_binder()
1424 .stable_cmp(self.tcx(), b.as_ref().skip_binder())
1425 });
1426 List::from_vec(v)
1427 };
1428
1429 let region = self.conv_lifetime(env, lifetime, span);
1430 Ok(rty::Ty::dynamic(existential_predicates, region))
1431 }
1432
1433 pub(crate) fn conv_bty(
1434 &mut self,
1435 env: &mut Env,
1436 bty: &fhir::BaseTy,
1437 name: Option<Symbol>,
1438 ) -> QueryResult<rty::TyOrCtor> {
1439 match &bty.kind {
1440 fhir::BaseTyKind::Path(fhir::QPath::Resolved(qself, path)) => {
1441 self.conv_qpath(env, *qself, path, name)
1442 }
1443 fhir::BaseTyKind::Path(fhir::QPath::TypeRelative(qself, segment)) => {
1444 let qself_res =
1445 if let Some(path) = qself.as_path() { path.res } else { fhir::Res::Err };
1446 let alias_ty = self
1447 .conv_type_relative_type_path(env, qself.span, qself_res, segment)?
1448 .shift_in_escaping(1);
1449 let bty = rty::BaseTy::Alias(rty::AliasKind::Projection, alias_ty);
1450 let sort = bty.sort();
1451 let ty = rty::Ty::indexed(bty, rty::Expr::nu());
1452 Ok(rty::TyOrCtor::Ctor(rty::Binder::bind_with_sort(ty, sort)))
1453 }
1454 fhir::BaseTyKind::Slice(ty) => {
1455 let bty = rty::BaseTy::Slice(self.conv_ty(env, ty)?).shift_in_escaping(1);
1456 let sort = bty.sort();
1457 let ty = rty::Ty::indexed(bty, rty::Expr::nu());
1458 Ok(rty::TyOrCtor::Ctor(rty::Binder::bind_with_sort(ty, sort)))
1459 }
1460 fhir::BaseTyKind::Err(err) => Err(QueryErr::Emitted(*err)),
1461 }
1462 }
1463
1464 fn conv_type_relative_path<Tag: AssocItemTag>(
1465 &mut self,
1466 tag: Tag,
1467 qself_span: Span,
1468 qself_res: fhir::Res,
1469 assoc_ident: Ident,
1470 ) -> QueryResult<(Tag::AssocItem<'tcx>, rty::TraitRef)> {
1471 let tcx = self.tcx();
1472
1473 let bound = match qself_res {
1474 fhir::Res::SelfTyAlias { alias_to: impl_def_id, is_trait_impl: true } => {
1475 let Some(trait_ref) = tcx.impl_trait_ref(impl_def_id) else {
1476 span_bug!(qself_span, "expected cycle error");
1478 };
1479
1480 self.probe_single_bound_for_assoc_item(
1481 || {
1482 traits::supertraits(
1483 tcx,
1484 ty::Binder::dummy(trait_ref.instantiate_identity()),
1485 )
1486 },
1487 assoc_ident,
1488 tag,
1489 )?
1490 }
1491 fhir::Res::Def(DefKind::TyParam, param_id)
1492 | fhir::Res::SelfTyParam { trait_: param_id } => {
1493 let predicates = type_param_predicates(tcx, param_id);
1494 self.probe_single_bound_for_assoc_item(
1495 || {
1496 tag.transitive_bounds_that_define_assoc_item(
1497 self.genv(),
1498 predicates.map(|pred| pred.map_bound(|t| t.trait_ref)),
1499 assoc_ident,
1500 )
1501 },
1502 assoc_ident,
1503 tag,
1504 )?
1505 }
1506 _ => self.report_assoc_item_not_found(assoc_ident.span, tag)?,
1507 };
1508
1509 let Some(trait_ref) = bound.no_bound_vars() else {
1510 Err(self.emit(
1518 query_bug!("associated path with uninferred generic parameters")
1519 .at(assoc_ident.span),
1520 ))?
1521 };
1522
1523 let trait_ref = trait_ref
1524 .lower(tcx)
1525 .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?
1526 .refine(&self.refiner()?)?;
1527
1528 let assoc_item = tag
1529 .trait_defines_item_named(self.genv(), trait_ref.def_id, assoc_ident)?
1530 .unwrap();
1531
1532 Ok((assoc_item, trait_ref))
1533 }
1534
1535 fn conv_type_relative_type_path(
1536 &mut self,
1537 env: &mut Env,
1538 qself_span: Span,
1539 qself_res: fhir::Res,
1540 assoc_segment: &fhir::PathSegment,
1541 ) -> QueryResult<rty::AliasTy> {
1542 let (assoc_item, trait_ref) = self.conv_type_relative_path(
1543 AssocTag::Type,
1544 qself_span,
1545 qself_res,
1546 assoc_segment.ident,
1547 )?;
1548
1549 let assoc_id = assoc_item.def_id;
1550 let mut args = trait_ref.args.to_vec();
1551 self.conv_generic_args_into(env, assoc_id, assoc_segment, &mut args)?;
1552
1553 let args = List::from_vec(args);
1554 let refine_args = List::empty();
1555 let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id };
1556 Ok(alias_ty)
1557 }
1558
1559 fn conv_type_relative_const_path(
1560 &mut self,
1561 fhir_expr: &fhir::Expr,
1562 qself: &rty::Ty,
1563 assoc: Ident,
1564 ) -> QueryResult<rty::Expr> {
1565 let tcx = self.genv().tcx();
1566
1567 let mut candidates = vec![];
1568 if let Some(simplified_type) = qself.simplify_type() {
1569 candidates = tcx
1570 .incoherent_impls(simplified_type)
1571 .iter()
1572 .filter_map(|impl_id| {
1573 tcx.associated_items(impl_id).find_by_ident_and_kind(
1574 tcx,
1575 assoc,
1576 AssocTag::Const,
1577 *impl_id,
1578 )
1579 })
1580 .collect_vec();
1581 }
1582 let (expr, sort) = match &candidates[..] {
1583 [candidate] => self.conv_const(fhir_expr.span, candidate.def_id)?,
1584 [] => self.report_assoc_item_not_found(fhir_expr.span, AssocTag::Const)?,
1585 _ => self.report_ambiguous_assoc_item(fhir_expr.span, AssocTag::Const, assoc)?,
1586 };
1587 self.0.insert_node_sort(fhir_expr.fhir_id, sort);
1588 Ok(expr)
1589 }
1590
1591 fn refiner(&self) -> QueryResult<Refiner<'genv, 'tcx>> {
1593 match self.owner() {
1594 FluxOwnerId::Rust(owner_id) => {
1595 let def_id = self.genv().maybe_extern_id(owner_id.def_id);
1596 Refiner::default_for_item(self.genv(), def_id.resolved_id())
1597 }
1598 FluxOwnerId::Flux(_) => Err(query_bug!("cannot refine types insicde flux item")),
1599 }
1600 }
1601
1602 fn probe_single_bound_for_assoc_item<I, Tag: AssocItemTag>(
1603 &self,
1604 all_candidates: impl FnOnce() -> I,
1605 assoc_name: Ident,
1606 tag: Tag,
1607 ) -> QueryResult<ty::PolyTraitRef<'tcx>>
1608 where
1609 I: Iterator<Item = ty::PolyTraitRef<'tcx>>,
1610 {
1611 let mut matching_candidates = vec![];
1612 for candidate in all_candidates() {
1613 if tag
1614 .trait_defines_item_named(self.genv(), candidate.def_id(), assoc_name)?
1615 .is_some()
1616 {
1617 matching_candidates.push(candidate);
1618 }
1619 }
1620
1621 let Some(bound) = matching_candidates.pop() else {
1622 self.report_assoc_item_not_found(assoc_name.span, tag)?;
1623 };
1624
1625 if !matching_candidates.is_empty() {
1626 self.report_ambiguous_assoc_item(assoc_name.span, tag, assoc_name)?;
1627 }
1628
1629 Ok(bound)
1630 }
1631
1632 fn conv_lifetime(&mut self, env: &Env, lft: fhir::Lifetime, span: Span) -> rty::Region {
1633 let res = match lft {
1634 fhir::Lifetime::Hole(_) => return rty::Region::ReVar(self.next_region_vid()),
1635 fhir::Lifetime::Resolved(res) => res,
1636 };
1637 self.conv_resolved_lifetime(env, res, span)
1638 }
1639
1640 fn conv_resolved_lifetime(&mut self, env: &Env, res: ResolvedArg, span: Span) -> rty::Region {
1641 let tcx = self.tcx();
1642 let lifetime_name = |def_id| tcx.item_name(def_id);
1643 match res {
1644 ResolvedArg::StaticLifetime => rty::ReStatic,
1645 ResolvedArg::EarlyBound(def_id) => {
1646 let index = self.genv().def_id_to_param_index(def_id.to_def_id());
1647 let name = lifetime_name(def_id.to_def_id());
1648 rty::ReEarlyParam(rty::EarlyParamRegion { index, name })
1649 }
1650 ResolvedArg::LateBound(_, index, def_id) => {
1651 let Some(depth) = env.depth().checked_sub(1) else {
1652 span_bug!(span, "late-bound variable at depth 0")
1653 };
1654 let kind = rty::BoundRegionKind::Named(def_id.to_def_id());
1655 let var = BoundVar::from_u32(index);
1656 let bound_region = rty::BoundRegion { var, kind };
1657 rty::ReBound(rty::DebruijnIndex::from_usize(depth), bound_region)
1658 }
1659 ResolvedArg::Free(scope, id) => {
1660 let kind = rty::LateParamRegionKind::Named(id.to_def_id());
1661 rty::ReLateParam(rty::LateParamRegion { scope: scope.to_def_id(), kind })
1662 }
1663 ResolvedArg::Error(_) => bug!("lifetime resolved to an error"),
1664 }
1665 }
1666
1667 fn conv_const_arg(&mut self, cst: fhir::ConstArg) -> rty::Const {
1668 match cst.kind {
1669 fhir::ConstArgKind::Lit(lit) => rty::Const::from_usize(self.tcx(), lit),
1670 fhir::ConstArgKind::Param(def_id) => {
1671 rty::Const {
1672 kind: rty::ConstKind::Param(def_id_to_param_const(self.genv(), def_id)),
1673 }
1674 }
1675 fhir::ConstArgKind::Infer => {
1676 rty::Const {
1677 kind: rty::ConstKind::Infer(ty::InferConst::Var(self.next_const_vid())),
1678 }
1679 }
1680 }
1681 }
1682
1683 fn conv_qpath(
1684 &mut self,
1685 env: &mut Env,
1686 qself: Option<&fhir::Ty>,
1687 path: &fhir::Path,
1688 name: Option<Symbol>,
1689 ) -> QueryResult<rty::TyOrCtor> {
1690 let bty = match path.res {
1691 fhir::Res::PrimTy(prim_ty) => {
1692 self.check_prim_ty_generics(path, prim_ty)?;
1693 prim_ty_to_bty(prim_ty)
1694 }
1695 fhir::Res::Def(DefKind::Struct | DefKind::Enum | DefKind::Union, did) => {
1696 let adt_def = self.genv().adt_def(did)?;
1697 let args = self.conv_generic_args(env, did, path.last_segment())?;
1698 rty::BaseTy::adt(adt_def, args)
1699 }
1700 fhir::Res::Def(DefKind::TyParam, def_id) => {
1701 let owner_id = ty_param_owner(self.genv(), def_id);
1702 let param_ty = def_id_to_param_ty(self.genv(), def_id);
1703 self.check_ty_param_generics(path, param_ty)?;
1704 let param = self
1705 .genv()
1706 .generics_of(owner_id)?
1707 .param_at(param_ty.index as usize, self.genv())?;
1708 match param.kind {
1709 rty::GenericParamDefKind::Type { .. } => {
1710 return Ok(rty::TyOrCtor::Ty(rty::Ty::param(param_ty)));
1711 }
1712 rty::GenericParamDefKind::Base { .. } => rty::BaseTy::Param(param_ty),
1713 _ => return Err(query_bug!("unexpected param kind")),
1714 }
1715 }
1716 fhir::Res::SelfTyParam { trait_ } => {
1717 self.check_self_ty_generics(path)?;
1718 let param = &self.genv().generics_of(trait_)?.own_params[0];
1719 match param.kind {
1720 rty::GenericParamDefKind::Type { .. } => {
1721 return Ok(rty::TyOrCtor::Ty(rty::Ty::param(rty::SELF_PARAM_TY)));
1722 }
1723 rty::GenericParamDefKind::Base { .. } => rty::BaseTy::Param(rty::SELF_PARAM_TY),
1724 _ => return Err(query_bug!("unexpected param kind")),
1725 }
1726 }
1727 fhir::Res::SelfTyAlias { alias_to, .. } => {
1728 self.check_self_ty_generics(path)?;
1729 if P::EXPAND_TYPE_ALIASES {
1730 return Ok(self.genv().type_of(alias_to)?.instantiate_identity());
1731 } else {
1732 rty::BaseTy::Alias(
1733 rty::AliasKind::Free,
1734 rty::AliasTy {
1735 def_id: alias_to,
1736 args: List::empty(),
1737 refine_args: List::empty(),
1738 },
1739 )
1740 }
1741 }
1742 fhir::Res::Def(DefKind::AssocTy, assoc_id) => {
1743 let trait_id = self.tcx().trait_of_assoc(assoc_id).unwrap();
1744
1745 let [.., trait_segment, assoc_segment] = path.segments else {
1746 span_bug!(path.span, "expected at least two segments");
1747 };
1748
1749 let Some(qself) = qself else {
1750 self.report_ambiguous_assoc_item(
1751 path.span,
1752 AssocTag::Type,
1753 assoc_segment.ident,
1754 )?
1755 };
1756
1757 let trait_generics = self.genv().generics_of(trait_id)?;
1758 let qself =
1759 self.conv_ty_to_generic_arg(env, &trait_generics.own_params[0], qself)?;
1760 let mut args = vec![qself];
1761 self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;
1762 self.conv_generic_args_into(env, assoc_id, assoc_segment, &mut args)?;
1763 let args = List::from_vec(args);
1764
1765 let refine_args = List::empty();
1766 let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id };
1767 rty::BaseTy::Alias(rty::AliasKind::Projection, alias_ty)
1768 }
1769 fhir::Res::Def(DefKind::TyAlias, def_id) => {
1770 self.check_refinement_generics(path, def_id)?;
1771 let args = self.conv_generic_args(env, def_id, path.last_segment())?;
1772 self.0.insert_path_args(path.fhir_id, args.clone());
1773 let refine_args = path
1774 .refine
1775 .iter()
1776 .map(|expr| self.conv_expr(env, expr))
1777 .try_collect_vec()?;
1778
1779 if P::EXPAND_TYPE_ALIASES {
1780 let tcx = self.tcx();
1781 return Ok(self
1782 .genv()
1783 .type_of(def_id)?
1784 .instantiate(tcx, &args, &refine_args));
1785 } else {
1786 rty::BaseTy::Alias(
1787 rty::AliasKind::Free,
1788 rty::AliasTy { def_id, args, refine_args: List::from(refine_args) },
1789 )
1790 }
1791 }
1792 fhir::Res::Def(DefKind::ForeignTy, def_id) => {
1793 self.check_foreign_ty_generics(path)?;
1794 rty::BaseTy::Foreign(def_id)
1795 }
1796 fhir::Res::Def(kind, def_id) => self.report_expected_type(path.span, kind, def_id)?,
1797 fhir::Res::Param(..) | fhir::Res::GlobalFunc(..) | fhir::Res::Err => {
1798 span_bug!(path.span, "unexpected resolution in conv_ty_ctor: {:?}", path.res)
1799 }
1800 };
1801 let sort = bty.sort();
1802 let bty = bty.shift_in_escaping(1);
1803 let kind = match name {
1804 Some(name) => BoundReftKind::Named(name),
1805 None => BoundReftKind::Anon,
1806 };
1807 let var = rty::BoundVariableKind::Refine(sort, rty::InferMode::EVar, kind);
1808 let ctor = rty::Binder::bind_with_vars(
1809 rty::Ty::indexed(bty, rty::Expr::nu()),
1810 List::singleton(var),
1811 );
1812 Ok(rty::TyOrCtor::Ctor(ctor))
1813 }
1814
1815 fn param_as_bound_var(
1816 &mut self,
1817 param: &fhir::GenericParam,
1818 ) -> QueryResult<rty::BoundVariableKind> {
1819 let def_id = param.def_id.resolved_id();
1820 match param.kind {
1821 fhir::GenericParamKind::Lifetime => {
1822 Ok(rty::BoundVariableKind::Region(rty::BoundRegionKind::Named(def_id)))
1823 }
1824 fhir::GenericParamKind::Const { .. } | fhir::GenericParamKind::Type { .. } => {
1825 Err(query_bug!(def_id, "unsupported param kind `{:?}`", param.kind))
1826 }
1827 }
1828 }
1829
1830 fn conv_generic_args(
1831 &mut self,
1832 env: &mut Env,
1833 def_id: DefId,
1834 segment: &fhir::PathSegment,
1835 ) -> QueryResult<List<rty::GenericArg>> {
1836 let mut into = vec![];
1837 self.conv_generic_args_into(env, def_id, segment, &mut into)?;
1838 Ok(List::from(into))
1839 }
1840
1841 fn conv_generic_args_into(
1842 &mut self,
1843 env: &mut Env,
1844 def_id: DefId,
1845 segment: &fhir::PathSegment,
1846 into: &mut Vec<rty::GenericArg>,
1847 ) -> QueryResult {
1848 let generics = self.genv().generics_of(def_id)?;
1849
1850 self.check_generic_arg_count(&generics, def_id, segment)?;
1851
1852 let len = into.len();
1853 for (idx, arg) in segment.args.iter().enumerate() {
1854 let param = generics.param_at(idx + len, self.genv())?;
1855 match arg {
1856 fhir::GenericArg::Lifetime(lft) => {
1857 into.push(rty::GenericArg::Lifetime(self.conv_lifetime(
1858 env,
1859 *lft,
1860 segment.ident.span,
1861 )));
1862 }
1863 fhir::GenericArg::Type(ty) => {
1864 into.push(self.conv_ty_to_generic_arg(env, ¶m, ty)?);
1865 }
1866 fhir::GenericArg::Const(cst) => {
1867 into.push(rty::GenericArg::Const(self.conv_const_arg(*cst)));
1868 }
1869 fhir::GenericArg::Infer => {
1870 into.push(self.conv_generic_arg_hole(env, param, segment.ident.span)?);
1871 }
1872 }
1873 }
1874 self.fill_generic_args_defaults(def_id, into)
1875 }
1876
1877 fn conv_generic_arg_hole(
1878 &mut self,
1879 env: &mut Env,
1880 param: rty::GenericParamDef,
1881 span: Span,
1882 ) -> QueryResult<rty::GenericArg> {
1883 match param.kind {
1884 rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::Base { .. } => {
1885 let ty = fhir::Ty { kind: fhir::TyKind::Infer, span };
1886 Ok(self.conv_ty_to_generic_arg(env, ¶m, &ty)?)
1887 }
1888 rty::GenericParamDefKind::Const { .. } => {
1889 let cst = fhir::ConstArg { kind: fhir::ConstArgKind::Infer, span };
1890 Ok(rty::GenericArg::Const(self.conv_const_arg(cst)))
1891 }
1892 rty::GenericParamDefKind::Lifetime => {
1893 let re = rty::Region::ReVar(self.next_region_vid());
1894 Ok(rty::GenericArg::Lifetime(re))
1895 }
1896 }
1897 }
1898
1899 fn check_generic_arg_count(
1900 &mut self,
1901 generics: &rty::Generics,
1902 def_id: DefId,
1903 segment: &fhir::PathSegment,
1904 ) -> QueryResult {
1905 let found = segment.args.len();
1906 let mut param_count = generics.own_params.len();
1907
1908 if let DefKind::Trait = self.genv().def_kind(def_id) {
1910 param_count -= 1;
1911 }
1912
1913 let min = param_count - generics.own_default_count();
1914 let max = param_count;
1915 if min == max && found != min {
1916 Err(self.emit(errors::GenericArgCountMismatch::new(
1917 self.genv(),
1918 def_id,
1919 segment,
1920 min,
1921 )))?;
1922 }
1923 if found < min {
1924 Err(self.emit(errors::TooFewGenericArgs::new(self.genv(), def_id, segment, min)))?;
1925 }
1926 if found > max {
1927 Err(self.emit(errors::TooManyGenericArgs::new(self.genv(), def_id, segment, min)))?;
1928 }
1929 Ok(())
1930 }
1931
1932 fn fill_generic_args_defaults(
1933 &mut self,
1934 def_id: DefId,
1935 into: &mut Vec<rty::GenericArg>,
1936 ) -> QueryResult {
1937 let generics = self.genv().generics_of(def_id)?;
1938 for param in generics.own_params.iter().skip(into.len()) {
1939 debug_assert!(matches!(
1940 param.kind,
1941 rty::GenericParamDefKind::Type { has_default: true }
1942 | rty::GenericParamDefKind::Base { has_default: true }
1943 ));
1944 let span = self.tcx().def_span(param.def_id);
1945 let ty = self
1948 .genv()
1949 .type_of(param.def_id)?
1950 .instantiate(self.tcx(), into, &[])
1951 .to_ty();
1952 into.push(self.try_to_ty_or_base(param.kind, span, &ty)?.into());
1953 }
1954 Ok(())
1955 }
1956
1957 fn conv_ty_to_generic_arg(
1958 &mut self,
1959 env: &mut Env,
1960 param: &rty::GenericParamDef,
1961 ty: &fhir::Ty,
1962 ) -> QueryResult<rty::GenericArg> {
1963 let rty_ty = self.conv_ty(env, ty)?;
1964 Ok(self.try_to_ty_or_base(param.kind, ty.span, &rty_ty)?.into())
1965 }
1966
1967 fn try_to_ty_or_base(
1968 &mut self,
1969 kind: rty::GenericParamDefKind,
1970 span: Span,
1971 ty: &rty::Ty,
1972 ) -> QueryResult<rty::TyOrBase> {
1973 match kind {
1974 rty::GenericParamDefKind::Type { .. } => Ok(rty::TyOrBase::Ty(ty.clone())),
1975 rty::GenericParamDefKind::Base { .. } => {
1976 Ok(rty::TyOrBase::Base(self.ty_to_subset_ty_ctor(span, ty)?))
1977 }
1978 _ => span_bug!(span, "unexpected param kind `{kind:?}`"),
1979 }
1980 }
1981
1982 fn ty_to_subset_ty_ctor(&mut self, span: Span, ty: &rty::Ty) -> QueryResult<rty::SubsetTyCtor> {
1983 let ctor = if let rty::TyKind::Infer(vid) = ty.kind() {
1984 let sort_vid =
1986 if vid.as_u32() == 0 { rty::SortVid::from_u32(0) } else { self.next_sort_vid() };
1987 rty::SubsetTyCtor::bind_with_sort(
1988 rty::SubsetTy::trivial(rty::BaseTy::Infer(*vid), rty::Expr::nu()),
1989 rty::Sort::Infer(rty::SortInfer::SortVar(sort_vid)),
1990 )
1991 } else {
1992 ty.shallow_canonicalize()
1993 .as_ty_or_base()
1994 .as_base()
1995 .ok_or_else(|| self.emit(errors::InvalidBaseInstance::new(span)))?
1996 };
1997 Ok(ctor)
1998 }
1999
2000 #[track_caller]
2001 fn emit(&self, err: impl Diagnostic<'genv>) -> ErrorGuaranteed {
2002 self.genv().sess().emit_err(err)
2003 }
2004
2005 fn report_assoc_item_not_found<Tag: AssocItemTag>(
2006 &self,
2007 span: Span,
2008 assoc_tag: Tag,
2009 ) -> Result<!, ErrorGuaranteed> {
2010 Err(self.emit(errors::AssocItemNotFound { span, tag: assoc_tag.descr() }))?
2011 }
2012
2013 fn report_ambiguous_assoc_item<Tag: AssocItemTag>(
2014 &self,
2015 span: Span,
2016 assoc_tag: Tag,
2017 assoc_name: Ident,
2018 ) -> Result<!, ErrorGuaranteed> {
2019 Err(self.emit(errors::AmbiguousAssocItem {
2020 span,
2021 name: assoc_name,
2022 tag: assoc_tag.descr(),
2023 }))?
2024 }
2025
2026 #[track_caller]
2027 fn report_expected_type(
2028 &self,
2029 span: Span,
2030 kind: DefKind,
2031 def_id: DefId,
2032 ) -> Result<!, ErrorGuaranteed> {
2033 Err(self.emit(errors::ExpectedType {
2034 span,
2035 def_descr: self.tcx().def_kind_descr(kind, def_id),
2036 name: self.tcx().def_path_str(def_id),
2037 }))?
2038 }
2039}
2040
2041impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
2043 fn check_refinement_generics(&mut self, path: &fhir::Path, def_id: DefId) -> QueryResult {
2044 let generics = self.genv().refinement_generics_of(def_id)?;
2045 if generics.count() != path.refine.len() {
2046 let err = errors::RefineArgMismatch {
2047 span: path.span,
2048 expected: generics.count(),
2049 found: path.refine.len(),
2050 kind: self.tcx().def_descr(def_id),
2051 };
2052 Err(self.emit(err))?;
2053 }
2054 Ok(())
2055 }
2056
2057 fn check_prim_ty_generics(
2058 &mut self,
2059 path: &fhir::Path<'_>,
2060 prim_ty: rustc_hir::PrimTy,
2061 ) -> QueryResult {
2062 if !path.last_segment().args.is_empty() {
2063 let err = errors::GenericsOnPrimTy { span: path.span, name: prim_ty.name_str() };
2064 Err(self.emit(err))?;
2065 }
2066 Ok(())
2067 }
2068
2069 fn check_ty_param_generics(
2070 &mut self,
2071 path: &fhir::Path<'_>,
2072 param_ty: rty::ParamTy,
2073 ) -> QueryResult {
2074 if !path.last_segment().args.is_empty() {
2075 let err = errors::GenericsOnTyParam { span: path.span, name: param_ty.name };
2076 Err(self.emit(err))?;
2077 }
2078 Ok(())
2079 }
2080
2081 fn check_self_ty_generics(&mut self, path: &fhir::Path<'_>) -> QueryResult {
2082 if !path.last_segment().args.is_empty() {
2083 let err = errors::GenericsOnSelfTy { span: path.span };
2084 Err(self.emit(err))?;
2085 }
2086 Ok(())
2087 }
2088
2089 fn check_foreign_ty_generics(&mut self, path: &fhir::Path<'_>) -> QueryResult {
2090 if !path.last_segment().args.is_empty() {
2091 let err = errors::GenericsOnForeignTy { span: path.span };
2092 Err(self.emit(err))?;
2093 }
2094 Ok(())
2095 }
2096}
2097
2098fn prim_ty_to_bty(prim_ty: rustc_hir::PrimTy) -> rty::BaseTy {
2099 match prim_ty {
2100 rustc_hir::PrimTy::Int(int_ty) => rty::BaseTy::Int(int_ty),
2101 rustc_hir::PrimTy::Uint(uint_ty) => rty::BaseTy::Uint(uint_ty),
2102 rustc_hir::PrimTy::Float(float_ty) => rty::BaseTy::Float(float_ty),
2103 rustc_hir::PrimTy::Str => rty::BaseTy::Str,
2104 rustc_hir::PrimTy::Bool => rty::BaseTy::Bool,
2105 rustc_hir::PrimTy::Char => rty::BaseTy::Char,
2106 }
2107}
2108
2109impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
2111 fn conv_lit(&self, lit: fhir::Lit, fhir_id: FhirId, span: Span) -> QueryResult<rty::Constant> {
2112 match lit {
2113 fhir::Lit::Int(n, kind) => {
2114 match kind {
2115 Some(fhir::NumLitKind::Int) => Ok(rty::Constant::from(n)),
2116 Some(fhir::NumLitKind::Real) => Ok(rty::Constant::Real(rty::Real(n))),
2117 None => {
2118 let sort = self.results().node_sort(fhir_id);
2119 if let rty::Sort::BitVec(bvsize) = sort {
2120 if let rty::BvSize::Fixed(size) = bvsize
2121 && (n == 0 || n.ilog2() < size)
2122 {
2123 Ok(rty::Constant::BitVec(n, size))
2124 } else {
2125 Err(self.emit(errors::InvalidBitVectorConstant::new(span, sort)))?
2126 }
2127 } else {
2128 Ok(rty::Constant::from(n))
2129 }
2130 }
2131 }
2132 }
2133 fhir::Lit::Bool(b) => Ok(rty::Constant::from(b)),
2134 fhir::Lit::Str(s) => Ok(rty::Constant::from(s)),
2135 fhir::Lit::Char(c) => Ok(rty::Constant::from(c)),
2136 }
2137 }
2138
2139 fn conv_expr(&mut self, env: &mut Env, expr: &fhir::Expr) -> QueryResult<rty::Expr> {
2140 let fhir_id = expr.fhir_id;
2141 let espan = ESpan::new(expr.span);
2142 let expr = match expr.kind {
2143 fhir::ExprKind::Var(QPathExpr::Resolved(path, _)) => self.conv_path_expr(env, path)?,
2144 fhir::ExprKind::Var(QPathExpr::TypeRelative(qself, assoc)) => {
2145 let qself = self.conv_ty(env, qself)?;
2146 self.conv_type_relative_const_path(expr, &qself, assoc)?
2147 }
2148 fhir::ExprKind::Literal(lit) => {
2149 rty::Expr::constant(self.conv_lit(lit, fhir_id, expr.span)?).at(espan)
2150 }
2151 fhir::ExprKind::BinaryOp(op, e1, e2) => {
2152 rty::Expr::binary_op(
2153 self.conv_bin_op(op, expr.fhir_id),
2154 self.conv_expr(env, e1)?,
2155 self.conv_expr(env, e2)?,
2156 )
2157 .at(espan)
2158 }
2159 fhir::ExprKind::UnaryOp(op, e) => {
2160 rty::Expr::unary_op(conv_un_op(op), self.conv_expr(env, e)?).at(espan)
2161 }
2162
2163 fhir::ExprKind::PrimApp(op, e1, e2) => {
2164 rty::Expr::prim_val(
2165 self.conv_bin_op(op, expr.fhir_id),
2166 self.conv_expr(env, e1)?,
2167 self.conv_expr(env, e2)?,
2168 )
2169 .at(espan)
2170 }
2171 fhir::ExprKind::App(func, args) => {
2172 let sort_args = self.results().node_sort_args(fhir_id);
2173 rty::Expr::app(self.conv_func(env, &func)?, sort_args, self.conv_exprs(env, args)?)
2174 .at(espan)
2175 }
2176 fhir::ExprKind::Alias(alias, args) => {
2177 let args = args
2178 .iter()
2179 .map(|arg| self.conv_expr(env, arg))
2180 .try_collect()?;
2181 let alias = self.conv_alias_reft(env, expr.fhir_id, &alias)?;
2182 rty::Expr::alias(alias, args).at(espan)
2183 }
2184 fhir::ExprKind::IfThenElse(p, e1, e2) => {
2185 rty::Expr::ite(
2186 self.conv_expr(env, p)?,
2187 self.conv_expr(env, e1)?,
2188 self.conv_expr(env, e2)?,
2189 )
2190 .at(espan)
2191 }
2192 fhir::ExprKind::Dot(base, _) => {
2193 let proj = self.results().field_proj(fhir_id);
2194 rty::Expr::field_proj(self.conv_expr(env, base)?, proj)
2195 }
2196 fhir::ExprKind::Abs(params, body) => {
2197 env.push_layer(Layer::list(self.results(), 0, params));
2198 let pred = self.conv_expr(env, body)?;
2199 let vars = env.pop_layer().into_bound_vars(self.genv())?;
2200 let output = self.results().node_sort(body.fhir_id);
2201 let lam = rty::Lambda::bind_with_vars(pred, vars, output);
2202 rty::Expr::abs(lam)
2203 }
2204 fhir::ExprKind::Block(decls, body) => {
2205 for decl in decls {
2206 env.push_layer(Layer::list(self.results(), 0, &[decl.param]));
2207 }
2208 let mut body = self.conv_expr(env, body)?;
2209 for decl in decls.iter().rev() {
2210 let vars = env.pop_layer().into_bound_vars(self.genv())?;
2211 let init = self.conv_expr(env, &decl.init)?;
2212 body = rty::Expr::let_(init, rty::Binder::bind_with_vars(body, vars));
2213 }
2214 body
2215 }
2216 fhir::ExprKind::BoundedQuant(kind, param, rng, body) => {
2217 env.push_layer(Layer::list(self.results(), 0, &[param]));
2218 let pred = self.conv_expr(env, body)?;
2219 let vars = env.pop_layer().into_bound_vars(self.genv())?;
2220 let body = rty::Binder::bind_with_vars(pred, vars);
2221 rty::Expr::bounded_quant(kind, rng, body)
2222 }
2223 fhir::ExprKind::Record(flds) => {
2224 let def_id = self.results().record_ctor(expr.fhir_id);
2225 let flds = flds
2226 .iter()
2227 .map(|expr| self.conv_expr(env, expr))
2228 .try_collect()?;
2229 rty::Expr::ctor_struct(def_id, flds)
2230 }
2231 fhir::ExprKind::Constructor(path, exprs, spread) => {
2232 let def_id = if let Some(path) = path {
2233 match path.res {
2234 fhir::Res::Def(DefKind::Enum | DefKind::Struct, def_id) => def_id,
2235 _ => span_bug!(path.span, "unexpected path in constructor"),
2236 }
2237 } else {
2238 self.results().record_ctor(expr.fhir_id)
2239 };
2240 let assns = self.conv_constructor_exprs(def_id, env, exprs, &spread)?;
2241 rty::Expr::ctor_struct(def_id, assns)
2242 }
2243 fhir::ExprKind::Err(err) => Err(QueryErr::Emitted(err))?,
2244 };
2245 Ok(self.add_coercions(expr, fhir_id))
2246 }
2247
2248 fn conv_loc(&mut self, env: &mut Env, loc: fhir::PathExpr) -> QueryResult<rty::Path> {
2249 Ok(self
2250 .conv_path_expr(env, loc)?
2251 .to_path()
2252 .unwrap_or_else(|| span_bug!(loc.span, "expected path, found `{loc:?}`")))
2253 }
2254
2255 fn conv_path_expr(&mut self, env: &mut Env, path: fhir::PathExpr) -> QueryResult<rty::Expr> {
2256 let genv = self.genv();
2257 let tcx = self.genv().tcx();
2258 let espan = ESpan::new(path.span);
2259 let (expr, sort) = match path.res {
2260 fhir::Res::Param(_, id) => (env.lookup(&path).to_expr(), self.results().param_sort(id)),
2261 fhir::Res::Def(DefKind::Const, def_id) => {
2262 self.hyperlink(path.span, tcx.def_ident_span(def_id));
2263 let (expr, sort) = self.conv_const(path.span, def_id)?;
2264 (expr.at(espan), sort)
2265 }
2266 fhir::Res::Def(DefKind::Ctor(..), ctor_id) => {
2267 let Some(sort) = genv.sort_of_def_id(ctor_id).emit(&genv)? else {
2268 span_bug!(path.span, "unexpected variant {ctor_id:?}")
2269 };
2270
2271 let variant_id = self.tcx().parent(ctor_id);
2272 let enum_id = self.tcx().parent(variant_id);
2273 self.hyperlink(path.span, tcx.def_ident_span(variant_id));
2274 let idx = variant_idx(self.tcx(), variant_id);
2275 (rty::Expr::ctor_enum(enum_id, idx), sort)
2276 }
2277 fhir::Res::Def(DefKind::ConstParam, def_id) => {
2278 self.hyperlink(path.span, tcx.def_ident_span(def_id));
2279 let sort = rty::Sort::Int;
2281 (rty::Expr::const_generic(def_id_to_param_const(genv, def_id)).at(espan), sort)
2282 }
2283 _ => {
2284 Err(self.emit(errors::InvalidRes { span: path.span, res_descr: path.res.descr() }))?
2285 }
2286 };
2287 self.0.insert_node_sort(path.fhir_id, sort);
2288 Ok(expr)
2289 }
2290
2291 fn conv_const(&self, span: Span, def_id: DefId) -> QueryResult<(rty::Expr, rty::Sort)> {
2292 let genv = self.genv();
2293 let Some(sort) = genv.sort_of_def_id(def_id).emit(&genv)? else {
2294 span_bug!(span, "unsupported const: `{def_id:?}`")
2295 };
2296 let info = genv.constant_info(def_id).emit(&genv)?;
2297 if sort != rty::Sort::Int && matches!(info, rty::ConstantInfo::Uninterpreted) {
2299 Err(self.emit(errors::ConstantAnnotationNeeded::new(span)))?;
2300 }
2301 Ok((rty::Expr::const_def_id(def_id).at(ESpan::new(span)), sort))
2302 }
2303
2304 fn conv_constructor_exprs(
2305 &mut self,
2306 struct_def_id: DefId,
2307 env: &mut Env,
2308 exprs: &[fhir::FieldExpr],
2309 spread: &Option<&fhir::Spread>,
2310 ) -> QueryResult<List<rty::Expr>> {
2311 let spread = spread
2312 .map(|spread| self.conv_expr(env, &spread.expr))
2313 .transpose()?;
2314 let mut field_exprs_by_name: FxHashMap<Symbol, rty::Expr> = exprs
2315 .iter()
2316 .map(|field_expr| -> QueryResult<_> {
2317 Ok((field_expr.ident.name, self.conv_expr(env, &field_expr.expr)?))
2318 })
2319 .try_collect()?;
2320
2321 if !P::HAS_ELABORATED_INFORMATION {
2322 return Ok(List::default());
2323 };
2324
2325 let adt_def = self.genv().adt_sort_def_of(struct_def_id)?;
2326 let struct_variant = adt_def.struct_variant();
2327 let mut assns = Vec::new();
2328 for (idx, field_name) in struct_variant.field_names().iter().enumerate() {
2329 if let Some(expr) = field_exprs_by_name.remove(field_name) {
2330 assns.push(expr);
2331 } else if let Some(spread) = &spread {
2332 let proj = rty::FieldProj::Adt { def_id: struct_def_id, field: idx as u32 };
2333 assns.push(rty::Expr::field_proj(spread, proj));
2334 }
2335 }
2336 Ok(List::from_vec(assns))
2337 }
2338
2339 fn conv_exprs(&mut self, env: &mut Env, exprs: &[fhir::Expr]) -> QueryResult<List<rty::Expr>> {
2340 exprs.iter().map(|e| self.conv_expr(env, e)).collect()
2341 }
2342
2343 fn conv_bin_op(&self, op: fhir::BinOp, fhir_id: FhirId) -> rty::BinOp {
2344 match op {
2345 fhir::BinOp::Iff => rty::BinOp::Iff,
2346 fhir::BinOp::Imp => rty::BinOp::Imp,
2347 fhir::BinOp::Or => rty::BinOp::Or,
2348 fhir::BinOp::And => rty::BinOp::And,
2349 fhir::BinOp::Eq => rty::BinOp::Eq,
2350 fhir::BinOp::Ne => rty::BinOp::Ne,
2351 fhir::BinOp::Gt => rty::BinOp::Gt(self.results().bin_op_sort(fhir_id)),
2352 fhir::BinOp::Ge => rty::BinOp::Ge(self.results().bin_op_sort(fhir_id)),
2353 fhir::BinOp::Lt => rty::BinOp::Lt(self.results().bin_op_sort(fhir_id)),
2354 fhir::BinOp::Le => rty::BinOp::Le(self.results().bin_op_sort(fhir_id)),
2355 fhir::BinOp::Add => rty::BinOp::Add(self.results().bin_op_sort(fhir_id)),
2356 fhir::BinOp::Sub => rty::BinOp::Sub(self.results().bin_op_sort(fhir_id)),
2357 fhir::BinOp::Mul => rty::BinOp::Mul(self.results().bin_op_sort(fhir_id)),
2358 fhir::BinOp::Mod => rty::BinOp::Mod(self.results().bin_op_sort(fhir_id)),
2359 fhir::BinOp::Div => rty::BinOp::Div(self.results().bin_op_sort(fhir_id)),
2360 fhir::BinOp::BitAnd => rty::BinOp::BitAnd,
2361 fhir::BinOp::BitOr => rty::BinOp::BitOr,
2362 fhir::BinOp::BitXor => rty::BinOp::BitXor,
2363 fhir::BinOp::BitShl => rty::BinOp::BitShl,
2364 fhir::BinOp::BitShr => rty::BinOp::BitShr,
2365 }
2366 }
2367
2368 fn add_coercions(&self, mut expr: rty::Expr, fhir_id: FhirId) -> rty::Expr {
2369 let span = expr.span();
2370 for coercion in self.results().coercions_for(fhir_id) {
2371 expr = match *coercion {
2372 rty::Coercion::Inject(def_id) => {
2373 rty::Expr::ctor_struct(def_id, List::singleton(expr)).at_opt(span)
2374 }
2375 rty::Coercion::Project(def_id) => {
2376 rty::Expr::field_proj(expr, rty::FieldProj::Adt { def_id, field: 0 })
2377 .at_opt(span)
2378 }
2379 };
2380 }
2381 expr
2382 }
2383
2384 fn hyperlink(&self, span: Span, dst_span: Option<Span>) {
2385 if P::HAS_ELABORATED_INFORMATION
2386 && let Some(dst_span) = dst_span
2387 {
2388 dbg::hyperlink!(self.genv().tcx(), span, dst_span);
2389 }
2390 }
2391
2392 fn conv_func(&mut self, env: &Env, func: &fhir::PathExpr) -> QueryResult<rty::Expr> {
2393 let genv = self.genv();
2394 let span = func.span;
2395 let (expr, sort) = match func.res {
2396 fhir::Res::Param(_, id) => {
2397 let sort = self.results().param_sort(id);
2398 (env.lookup(func).to_expr(), sort)
2399 }
2400 fhir::Res::GlobalFunc(fhir::SpecFuncKind::Def(did)) => {
2401 self.hyperlink(span, Some(genv.func_span(did)));
2402 let sort = rty::Sort::Func(genv.func_sort(did));
2403 (rty::Expr::global_func(rty::SpecFuncKind::Def(did)), sort)
2404 }
2405 fhir::Res::GlobalFunc(fhir::SpecFuncKind::Uif(did)) => {
2406 self.hyperlink(span, Some(genv.func_span(did)));
2407 let sort = rty::Sort::Func(genv.func_sort(did));
2408 (rty::Expr::global_func(rty::SpecFuncKind::Uif(did)), sort)
2409 }
2410 fhir::Res::GlobalFunc(fhir::SpecFuncKind::Thy(itf)) => {
2411 let sort = THEORY_FUNCS.get(&itf).unwrap().sort.clone();
2412 (rty::Expr::global_func(rty::SpecFuncKind::Thy(itf)), rty::Sort::Func(sort))
2413 }
2414 fhir::Res::GlobalFunc(fhir::SpecFuncKind::Cast) => {
2415 let fsort = rty::PolyFuncSort::new(
2416 List::from_arr([rty::SortParamKind::Sort, rty::SortParamKind::Sort]),
2417 rty::FuncSort::new(
2418 vec![rty::Sort::Var(rty::ParamSort::from(0_usize))],
2419 rty::Sort::Var(rty::ParamSort::from(1_usize)),
2420 ),
2421 );
2422 (rty::Expr::internal_func(InternalFuncKind::Cast), rty::Sort::Func(fsort))
2423 }
2424 _ => {
2425 return Err(
2426 self.emit(errors::InvalidRes { span: func.span, res_descr: func.res.descr() })
2427 )?;
2428 }
2429 };
2430 self.0.insert_node_sort(func.fhir_id, sort);
2431 Ok(self.add_coercions(expr, func.fhir_id))
2432 }
2433
2434 fn conv_alias_reft(
2435 &mut self,
2436 env: &mut Env,
2437 fhir_id: FhirId,
2438 alias: &fhir::AliasReft,
2439 ) -> QueryResult<rty::AliasReft> {
2440 let alias_reft = match alias {
2441 fhir::AliasReft::Qualified { qself, trait_, name } => {
2442 let fhir::Res::Def(DefKind::Trait, trait_id) = trait_.res else {
2443 span_bug!(trait_.span, "expected trait")
2444 };
2445 let trait_segment = trait_.last_segment();
2446
2447 let generics = self.genv().generics_of(trait_id)?;
2448 let self_ty =
2449 self.conv_ty_to_generic_arg(env, &generics.param_at(0, self.genv())?, qself)?;
2450 let mut generic_args = vec![self_ty];
2451 self.conv_generic_args_into(env, trait_id, trait_segment, &mut generic_args)?;
2452
2453 let Some(assoc_reft) = self.genv().assoc_refinements_of(trait_id)?.find(name.name)
2454 else {
2455 return Err(self.emit(errors::InvalidAssocReft::new(
2456 trait_.span,
2457 name.name,
2458 format!("{:?}", trait_),
2459 )))?;
2460 };
2461
2462 let assoc_id = assoc_reft.def_id;
2463
2464 dbg::hyperlink!(self.genv().tcx(), name.span, assoc_reft.span);
2465
2466 rty::AliasReft { assoc_id, args: List::from_vec(generic_args) }
2467 }
2468 fhir::AliasReft::TypeRelative { qself, name } => {
2469 let qself_res =
2470 if let Some(path) = qself.as_path() { path.res } else { fhir::Res::Err };
2471 let (assoc_reft, trait_ref) =
2472 self.conv_type_relative_path(AssocReftTag, qself.span, qself_res, *name)?;
2473 rty::AliasReft { assoc_id: assoc_reft.def_id, args: trait_ref.args }
2474 }
2475 };
2476 let fsort = alias_reft.fsort(self.genv())?;
2477 self.0.insert_alias_reft_sort(fhir_id, fsort);
2478 Ok(alias_reft)
2479 }
2480
2481 pub(crate) fn conv_invariants(
2482 &mut self,
2483 adt_id: MaybeExternId,
2484 params: &[fhir::RefineParam],
2485 invariants: &[fhir::Expr],
2486 ) -> QueryResult<Vec<rty::Invariant>> {
2487 let mut env = Env::new(&[]);
2488 env.push_layer(Layer::coalesce(self.results(), adt_id.resolved_id(), params));
2489 invariants
2490 .iter()
2491 .map(|invariant| self.conv_invariant(&mut env, invariant))
2492 .collect()
2493 }
2494
2495 fn conv_invariant(
2496 &mut self,
2497 env: &mut Env,
2498 invariant: &fhir::Expr,
2499 ) -> QueryResult<rty::Invariant> {
2500 Ok(rty::Invariant::new(rty::Binder::bind_with_vars(
2501 self.conv_expr(env, invariant)?,
2502 env.top_layer().to_bound_vars(self.genv())?,
2503 )))
2504 }
2505}
2506
2507impl Env {
2508 fn new(early_params: &[fhir::RefineParam]) -> Self {
2509 let early_params = early_params
2510 .iter()
2511 .map(|param| (param.id, param.name))
2512 .collect();
2513 Self { layers: vec![], early_params }
2514 }
2515
2516 pub(crate) fn empty() -> Self {
2517 Self { layers: vec![], early_params: Default::default() }
2518 }
2519
2520 fn depth(&self) -> usize {
2521 self.layers.len()
2522 }
2523
2524 fn push_layer(&mut self, layer: Layer) {
2525 self.layers.push(layer);
2526 }
2527
2528 fn pop_layer(&mut self) -> Layer {
2529 self.layers.pop().expect("bottom of layer stack")
2530 }
2531
2532 fn top_layer(&self) -> &Layer {
2533 self.layers.last().expect("bottom of layer stack")
2534 }
2535
2536 fn lookup(&self, var: &fhir::PathExpr) -> LookupResult<'_> {
2537 let (_, id) = var.res.expect_param();
2538 for (i, layer) in self.layers.iter().rev().enumerate() {
2539 if let Some((idx, entry)) = layer.get(id) {
2540 let debruijn = DebruijnIndex::from_usize(i);
2541 let kind = LookupResultKind::Bound {
2542 debruijn,
2543 entry,
2544 index: idx as u32,
2545 kind: layer.kind,
2546 };
2547 return LookupResult { var_span: var.span, kind };
2548 }
2549 }
2550 if let Some((idx, _, name)) = self.early_params.get_full(&id) {
2551 LookupResult {
2552 var_span: var.span,
2553 kind: LookupResultKind::EarlyParam { index: idx as u32, name: *name },
2554 }
2555 } else {
2556 span_bug!(var.span, "no entry found for key: `{:?}`", id);
2557 }
2558 }
2559
2560 fn to_early_param_args(&self) -> List<rty::Expr> {
2561 self.early_params
2562 .iter()
2563 .enumerate()
2564 .map(|(idx, (_, name))| rty::Expr::early_param(idx as u32, *name))
2565 .collect()
2566 }
2567}
2568
2569impl Layer {
2570 fn new<R: WfckResultsProvider>(
2571 results: &R,
2572 params: &[fhir::RefineParam],
2573 kind: LayerKind,
2574 ) -> Self {
2575 let map = params
2576 .iter()
2577 .map(|param| {
2578 let sort = results.param_sort(param.id);
2579 let infer_mode = rty::InferMode::from_param_kind(param.kind);
2580 let entry = ParamEntry::new(sort, infer_mode, param.name);
2581 (param.id, entry)
2582 })
2583 .collect();
2584 Self { map, kind }
2585 }
2586
2587 fn list<R: WfckResultsProvider>(
2588 results: &R,
2589 bound_regions: u32,
2590 params: &[fhir::RefineParam],
2591 ) -> Self {
2592 Self::new(results, params, LayerKind::List { bound_regions })
2593 }
2594
2595 fn coalesce<R: WfckResultsProvider>(
2596 results: &R,
2597 def_id: DefId,
2598 params: &[fhir::RefineParam],
2599 ) -> Self {
2600 Self::new(results, params, LayerKind::Coalesce(def_id))
2601 }
2602
2603 fn get(&self, name: impl Borrow<fhir::ParamId>) -> Option<(usize, &ParamEntry)> {
2604 let (idx, _, entry) = self.map.get_full(name.borrow())?;
2605 Some((idx, entry))
2606 }
2607
2608 fn into_bound_vars(self, genv: GlobalEnv) -> QueryResult<List<rty::BoundVariableKind>> {
2609 match self.kind {
2610 LayerKind::List { .. } => {
2611 Ok(self
2612 .into_iter()
2613 .map(|entry| {
2614 let kind = rty::BoundReftKind::Named(entry.name);
2615 rty::BoundVariableKind::Refine(entry.sort, entry.mode, kind)
2616 })
2617 .collect())
2618 }
2619 LayerKind::Coalesce(def_id) => {
2620 let sort_def = genv.adt_sort_def_of(def_id)?;
2621 let args = sort_def.identity_args();
2622 let ctor = rty::SortCtor::Adt(sort_def);
2623 Ok(List::singleton(rty::BoundVariableKind::Refine(
2624 rty::Sort::App(ctor, args),
2625 rty::InferMode::EVar,
2626 rty::BoundReftKind::Anon,
2627 )))
2628 }
2629 }
2630 }
2631
2632 fn to_bound_vars(&self, genv: GlobalEnv) -> QueryResult<List<rty::BoundVariableKind>> {
2633 self.clone().into_bound_vars(genv)
2634 }
2635
2636 fn into_iter(self) -> impl Iterator<Item = ParamEntry> {
2637 self.map.into_values()
2638 }
2639}
2640
2641impl ParamEntry {
2642 fn new(sort: rty::Sort, mode: fhir::InferMode, name: Symbol) -> Self {
2643 ParamEntry { name, sort, mode }
2644 }
2645}
2646
2647impl LookupResult<'_> {
2648 fn to_expr(&self) -> rty::Expr {
2649 let espan = ESpan::new(self.var_span);
2650 match &self.kind {
2651 LookupResultKind::Bound { debruijn, entry: ParamEntry { name, .. }, kind, index } => {
2652 match *kind {
2653 LayerKind::List { bound_regions } => {
2654 rty::Expr::bvar(
2655 *debruijn,
2656 BoundVar::from_u32(bound_regions + *index),
2657 rty::BoundReftKind::Named(*name),
2658 )
2659 .at(espan)
2660 }
2661 LayerKind::Coalesce(def_id) => {
2662 let var =
2663 rty::Expr::bvar(*debruijn, BoundVar::ZERO, rty::BoundReftKind::Anon)
2664 .at(espan);
2665 rty::Expr::field_proj(var, rty::FieldProj::Adt { def_id, field: *index })
2666 .at(espan)
2667 }
2668 }
2669 }
2670 &LookupResultKind::EarlyParam { index, name, .. } => {
2671 rty::Expr::early_param(index, name).at(espan)
2672 }
2673 }
2674 }
2675}
2676
2677pub fn conv_func_decl(genv: GlobalEnv, func: &fhir::SpecFunc) -> QueryResult<rty::PolyFuncSort> {
2678 let wfckresults = WfckResults::new(FluxOwnerId::Flux(func.def_id));
2679 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
2680 let inputs_and_output = func
2681 .args
2682 .iter()
2683 .map(|p| &p.sort)
2684 .chain(iter::once(&func.sort))
2685 .map(|sort| cx.conv_sort(sort))
2686 .try_collect()?;
2687 let params = iter::repeat_n(rty::SortParamKind::Sort, func.params).collect();
2688 Ok(rty::PolyFuncSort::new(params, rty::FuncSort { inputs_and_output }))
2689}
2690
2691fn conv_un_op(op: fhir::UnOp) -> rty::UnOp {
2692 match op {
2693 fhir::UnOp::Not => rty::UnOp::Not,
2694 fhir::UnOp::Neg => rty::UnOp::Neg,
2695 }
2696}
2697
2698fn def_id_to_param_ty(genv: GlobalEnv, def_id: DefId) -> rty::ParamTy {
2699 rty::ParamTy { index: genv.def_id_to_param_index(def_id), name: ty_param_name(genv, def_id) }
2700}
2701
2702fn def_id_to_param_const(genv: GlobalEnv, def_id: DefId) -> rty::ParamConst {
2703 rty::ParamConst { index: genv.def_id_to_param_index(def_id), name: ty_param_name(genv, def_id) }
2704}
2705
2706fn ty_param_owner(genv: GlobalEnv, def_id: DefId) -> DefId {
2707 let def_kind = genv.def_kind(def_id);
2708 match def_kind {
2709 DefKind::Trait | DefKind::TraitAlias => def_id,
2710 DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
2711 genv.tcx().parent(def_id)
2712 }
2713 _ => bug!("ty_param_owner: {:?} is a {:?} not a type parameter", def_id, def_kind),
2714 }
2715}
2716
2717fn ty_param_name(genv: GlobalEnv, def_id: DefId) -> Symbol {
2718 let def_kind = genv.tcx().def_kind(def_id);
2719 match def_kind {
2720 DefKind::Trait | DefKind::TraitAlias => kw::SelfUpper,
2721 DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
2722 genv.tcx().item_name(def_id)
2723 }
2724 _ => bug!("ty_param_name: {:?} is a {:?} not a type parameter", def_id, def_kind),
2725 }
2726}
2727
2728trait AssocItemTag: Copy {
2731 type AssocItem<'tcx>;
2732
2733 fn descr(self) -> &'static str;
2734
2735 fn trait_defines_item_named<'tcx>(
2736 self,
2737 genv: GlobalEnv<'_, 'tcx>,
2738 trait_def_id: DefId,
2739 assoc_name: Ident,
2740 ) -> QueryResult<Option<Self::AssocItem<'tcx>>>;
2741
2742 fn transitive_bounds_that_define_assoc_item<'tcx>(
2743 self,
2744 genv: GlobalEnv<'_, 'tcx>,
2745 trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2746 assoc_name: Ident,
2747 ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>>;
2748}
2749
2750impl AssocItemTag for AssocTag {
2751 type AssocItem<'tcx> = &'tcx AssocItem;
2752
2753 fn descr(self) -> &'static str {
2754 match self {
2755 AssocTag::Const => "constant",
2756 AssocTag::Fn => "function",
2757 AssocTag::Type => "type",
2758 }
2759 }
2760
2761 fn trait_defines_item_named<'tcx>(
2762 self,
2763 genv: GlobalEnv<'_, 'tcx>,
2764 trait_def_id: DefId,
2765 assoc_name: Ident,
2766 ) -> QueryResult<Option<Self::AssocItem<'tcx>>> {
2767 Ok(genv
2768 .tcx()
2769 .associated_items(trait_def_id)
2770 .find_by_ident_and_kind(genv.tcx(), assoc_name, self, trait_def_id))
2771 }
2772
2773 fn transitive_bounds_that_define_assoc_item<'tcx>(
2774 self,
2775 genv: GlobalEnv<'_, 'tcx>,
2776 trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2777 assoc_name: Ident,
2778 ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2779 traits::transitive_bounds_that_define_assoc_item(genv.tcx(), trait_refs, assoc_name)
2780 }
2781}
2782
2783#[derive(Copy, Clone)]
2784struct AssocReftTag;
2785
2786impl AssocItemTag for AssocReftTag {
2787 type AssocItem<'tcx> = AssocReft;
2788
2789 fn descr(self) -> &'static str {
2790 "refinement"
2791 }
2792
2793 fn trait_defines_item_named<'tcx>(
2794 self,
2795 genv: GlobalEnv<'_, 'tcx>,
2796 trait_def_id: DefId,
2797 assoc_name: Ident,
2798 ) -> QueryResult<Option<Self::AssocItem<'tcx>>> {
2799 Ok(genv
2800 .assoc_refinements_of(trait_def_id)?
2801 .find(assoc_name.name))
2802 }
2803
2804 fn transitive_bounds_that_define_assoc_item<'tcx>(
2805 self,
2806 genv: GlobalEnv<'_, 'tcx>,
2807 trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2808 _assoc_name: Ident,
2809 ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2810 transitive_bounds(genv.tcx(), trait_refs)
2811 }
2812}
2813
2814fn type_param_predicates<'tcx>(
2821 tcx: TyCtxt<'tcx>,
2822 param_id: DefId,
2823) -> impl Iterator<Item = ty::PolyTraitPredicate<'tcx>> {
2824 let parent = if tcx.def_kind(param_id) == DefKind::Trait {
2825 param_id
2827 } else {
2828 tcx.parent(param_id)
2829 };
2830 let param_index = tcx
2831 .generics_of(parent)
2832 .param_def_id_to_index(tcx, param_id)
2833 .unwrap();
2834 let predicates = tcx.predicates_of(parent).instantiate_identity(tcx);
2835 predicates.into_iter().filter_map(move |(clause, _)| {
2836 clause
2837 .as_trait_clause()
2838 .filter(|trait_pred| trait_pred.self_ty().skip_binder().is_param(param_index))
2839 })
2840}
2841
2842fn transitive_bounds<'tcx>(
2850 tcx: TyCtxt<'tcx>,
2851 trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2852) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2853 let mut seen = FxHashSet::default();
2854 let mut stack: Vec<_> = trait_refs.collect();
2855
2856 std::iter::from_fn(move || {
2857 while let Some(trait_ref) = stack.pop() {
2858 if !seen.insert(tcx.anonymize_bound_vars(trait_ref)) {
2859 continue;
2860 }
2861
2862 stack.extend(
2863 tcx.explicit_super_predicates_of(trait_ref.def_id())
2864 .iter_identity_copied()
2865 .map(|(clause, _)| clause.instantiate_supertrait(tcx, trait_ref))
2866 .filter_map(|clause| clause.as_trait_clause())
2867 .filter(|clause| clause.polarity() == ty::PredicatePolarity::Positive)
2868 .map(|clause| clause.map_bound(|clause| clause.trait_ref)),
2869 );
2870
2871 return Some(trait_ref);
2872 }
2873
2874 None
2875 })
2876}
2877
2878mod errors {
2879 use flux_errors::E0999;
2880 use flux_macros::Diagnostic;
2881 use flux_middle::{fhir, global_env::GlobalEnv, rty::Sort};
2882 use rustc_hir::def_id::DefId;
2883 use rustc_span::{Span, Symbol, symbol::Ident};
2884
2885 #[derive(Diagnostic)]
2886 #[diag(fhir_analysis_assoc_item_not_found, code = E0999)]
2887 #[note]
2888 pub(super) struct AssocItemNotFound {
2889 #[primary_span]
2890 #[label]
2891 pub span: Span,
2892 pub tag: &'static str,
2893 }
2894
2895 #[derive(Diagnostic)]
2896 #[diag(fhir_analysis_ambiguous_assoc_item, code = E0999)]
2897 pub(super) struct AmbiguousAssocItem {
2898 #[primary_span]
2899 pub span: Span,
2900 pub name: Ident,
2901 pub tag: &'static str,
2902 }
2903
2904 #[derive(Diagnostic)]
2905 #[diag(fhir_analysis_invalid_base_instance, code = E0999)]
2906 pub(super) struct InvalidBaseInstance {
2907 #[primary_span]
2908 span: Span,
2909 }
2910
2911 impl InvalidBaseInstance {
2912 pub(super) fn new(span: Span) -> Self {
2913 Self { span }
2914 }
2915 }
2916
2917 #[derive(Diagnostic)]
2918 #[diag(fhir_analysis_generic_argument_count_mismatch, code = E0999)]
2919 pub(super) struct GenericArgCountMismatch {
2920 #[primary_span]
2921 #[label]
2922 span: Span,
2923 found: usize,
2924 expected: usize,
2925 def_descr: &'static str,
2926 }
2927
2928 impl GenericArgCountMismatch {
2929 pub(super) fn new(
2930 genv: GlobalEnv,
2931 def_id: DefId,
2932 segment: &fhir::PathSegment,
2933 expected: usize,
2934 ) -> Self {
2935 GenericArgCountMismatch {
2936 span: segment.ident.span,
2937 found: segment.args.len(),
2938 expected,
2939 def_descr: genv.tcx().def_descr(def_id),
2940 }
2941 }
2942 }
2943
2944 #[derive(Diagnostic)]
2945 #[diag(fhir_analysis_too_few_generic_args, code = E0999)]
2946 pub(super) struct TooFewGenericArgs {
2947 #[primary_span]
2948 #[label]
2949 span: Span,
2950 found: usize,
2951 min: usize,
2952 def_descr: &'static str,
2953 }
2954
2955 impl TooFewGenericArgs {
2956 pub(super) fn new(
2957 genv: GlobalEnv,
2958 def_id: DefId,
2959 segment: &fhir::PathSegment,
2960 min: usize,
2961 ) -> Self {
2962 Self {
2963 span: segment.ident.span,
2964 found: segment.args.len(),
2965 min,
2966 def_descr: genv.tcx().def_descr(def_id),
2967 }
2968 }
2969 }
2970
2971 #[derive(Diagnostic)]
2972 #[diag(fhir_analysis_too_many_generic_args, code = E0999)]
2973 pub(super) struct TooManyGenericArgs {
2974 #[primary_span]
2975 #[label]
2976 span: Span,
2977 found: usize,
2978 max: usize,
2979 def_descr: &'static str,
2980 }
2981
2982 impl TooManyGenericArgs {
2983 pub(super) fn new(
2984 genv: GlobalEnv,
2985 def_id: DefId,
2986 segment: &fhir::PathSegment,
2987 max: usize,
2988 ) -> Self {
2989 Self {
2990 span: segment.ident.span,
2991 found: segment.args.len(),
2992 max,
2993 def_descr: genv.tcx().def_descr(def_id),
2994 }
2995 }
2996 }
2997
2998 #[derive(Diagnostic)]
2999 #[diag(fhir_analysis_refined_unrefinable_type, code = E0999)]
3000 pub(super) struct RefinedUnrefinableType {
3001 #[primary_span]
3002 span: Span,
3003 }
3004
3005 impl RefinedUnrefinableType {
3006 pub(super) fn new(span: Span) -> Self {
3007 Self { span }
3008 }
3009 }
3010
3011 #[derive(Diagnostic)]
3012 #[diag(fhir_analysis_generics_on_primitive_sort, code = E0999)]
3013 pub(super) struct GenericsOnPrimitiveSort {
3014 #[primary_span]
3015 #[label]
3016 span: Span,
3017 name: &'static str,
3018 found: usize,
3019 expected: usize,
3020 }
3021
3022 impl GenericsOnPrimitiveSort {
3023 pub(super) fn new(span: Span, name: &'static str, found: usize, expected: usize) -> Self {
3024 Self { span, found, expected, name }
3025 }
3026 }
3027
3028 #[derive(Diagnostic)]
3029 #[diag(fhir_analysis_incorrect_generics_on_sort, code = E0999)]
3030 pub(super) struct IncorrectGenericsOnSort {
3031 #[primary_span]
3032 #[label]
3033 span: Span,
3034 found: usize,
3035 expected: usize,
3036 def_descr: &'static str,
3037 }
3038
3039 impl IncorrectGenericsOnSort {
3040 pub(super) fn new(
3041 genv: GlobalEnv,
3042 def_id: DefId,
3043 span: Span,
3044 found: usize,
3045 expected: usize,
3046 ) -> Self {
3047 Self { span, found, expected, def_descr: genv.tcx().def_descr(def_id) }
3048 }
3049 }
3050
3051 #[derive(Diagnostic)]
3052 #[diag(fhir_analysis_generics_on_sort_ty_param, code = E0999)]
3053 pub(super) struct GenericsOnSortTyParam {
3054 #[primary_span]
3055 #[label]
3056 span: Span,
3057 found: usize,
3058 }
3059
3060 impl GenericsOnSortTyParam {
3061 pub(super) fn new(span: Span, found: usize) -> Self {
3062 Self { span, found }
3063 }
3064 }
3065
3066 #[derive(Diagnostic)]
3067 #[diag(fhir_analysis_generics_on_self_alias, code = E0999)]
3068 pub(super) struct GenericsOnSelf {
3069 #[primary_span]
3070 #[label]
3071 span: Span,
3072 found: usize,
3073 }
3074
3075 impl GenericsOnSelf {
3076 pub(super) fn new(span: Span, found: usize) -> Self {
3077 Self { span, found }
3078 }
3079 }
3080
3081 #[derive(Diagnostic)]
3082 #[diag(fhir_analysis_fields_on_reflected_enum_variant, code = E0999)]
3083 pub(super) struct FieldsOnReflectedEnumVariant {
3084 #[primary_span]
3085 #[label]
3086 span: Span,
3087 }
3088
3089 impl FieldsOnReflectedEnumVariant {
3090 pub(super) fn new(span: Span) -> Self {
3091 Self { span }
3092 }
3093 }
3094
3095 #[derive(Diagnostic)]
3096 #[diag(fhir_analysis_incorrect_generics_on_opaque_sort, code = E0999)]
3097 pub(super) struct IncorrectGenericsOnUserDefinedOpaqueSort {
3098 #[primary_span]
3099 #[label]
3100 span: Span,
3101 name: Symbol,
3102 expected: usize,
3103 found: usize,
3104 }
3105
3106 impl IncorrectGenericsOnUserDefinedOpaqueSort {
3107 pub(super) fn new(span: Span, name: Symbol, expected: usize, found: usize) -> Self {
3108 Self { span, name, expected, found }
3109 }
3110 }
3111
3112 #[derive(Diagnostic)]
3113 #[diag(fhir_analysis_generics_on_prim_ty, code = E0999)]
3114 pub(super) struct GenericsOnPrimTy {
3115 #[primary_span]
3116 pub span: Span,
3117 pub name: &'static str,
3118 }
3119
3120 #[derive(Diagnostic)]
3121 #[diag(fhir_analysis_generics_on_ty_param, code = E0999)]
3122 pub(super) struct GenericsOnTyParam {
3123 #[primary_span]
3124 pub span: Span,
3125 pub name: Symbol,
3126 }
3127
3128 #[derive(Diagnostic)]
3129 #[diag(fhir_analysis_generics_on_self_ty, code = E0999)]
3130 pub(super) struct GenericsOnSelfTy {
3131 #[primary_span]
3132 pub span: Span,
3133 }
3134
3135 #[derive(Diagnostic)]
3136 #[diag(fhir_analysis_generics_on_foreign_ty, code = E0999)]
3137 pub(super) struct GenericsOnForeignTy {
3138 #[primary_span]
3139 pub span: Span,
3140 }
3141
3142 #[derive(Diagnostic)]
3143 #[diag(fhir_analysis_invalid_bitvector_constant, code = E0999)]
3144 pub struct InvalidBitVectorConstant {
3145 #[primary_span]
3146 #[label]
3147 span: Span,
3148 sort: Sort,
3149 }
3150
3151 impl InvalidBitVectorConstant {
3152 pub(crate) fn new(span: Span, sort: Sort) -> Self {
3153 Self { span, sort }
3154 }
3155 }
3156
3157 #[derive(Diagnostic)]
3158 #[diag(fhir_analysis_invalid_assoc_reft, code = E0999)]
3159 pub struct InvalidAssocReft {
3160 #[primary_span]
3161 span: Span,
3162 trait_: String,
3163 name: Symbol,
3164 }
3165
3166 impl InvalidAssocReft {
3167 pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
3168 Self { span, trait_, name }
3169 }
3170 }
3171
3172 #[derive(Diagnostic)]
3173 #[diag(fhir_analysis_refine_arg_mismatch, code = E0999)]
3174 pub(super) struct RefineArgMismatch {
3175 #[primary_span]
3176 #[label]
3177 pub span: Span,
3178 pub expected: usize,
3179 pub found: usize,
3180 pub kind: &'static str,
3181 }
3182
3183 #[derive(Diagnostic)]
3184 #[diag(fhir_analysis_expected_type, code = E0999)]
3185 pub(super) struct ExpectedType {
3186 #[primary_span]
3187 pub span: Span,
3188 pub def_descr: &'static str,
3189 pub name: String,
3190 }
3191
3192 #[derive(Diagnostic)]
3193 #[diag(fhir_analysis_fail_to_match_predicates, code = E0999)]
3194 pub(super) struct FailToMatchPredicates {
3195 #[primary_span]
3196 pub span: Span,
3197 }
3198
3199 #[derive(Diagnostic)]
3200 #[diag(fhir_analysis_invalid_res, code = E0999)]
3201 pub(super) struct InvalidRes {
3202 #[primary_span]
3203 pub span: Span,
3204 pub res_descr: &'static str,
3205 }
3206
3207 #[derive(Diagnostic)]
3208 #[diag(fhir_analysis_constant_annotation_needed, code = E0999)]
3209 pub(super) struct ConstantAnnotationNeeded {
3210 #[primary_span]
3211 #[label]
3212 span: Span,
3213 }
3214 impl ConstantAnnotationNeeded {
3215 pub(super) fn new(span: Span) -> Self {
3216 Self { span }
3217 }
3218 }
3219}