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::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 { name } => {
930 if !path.args.is_empty() {
931 let err = errors::GenericsOnUserDefinedOpaqueSort::new(
932 path.segments.last().unwrap().span,
933 path.args.len(),
934 );
935 Err(self.emit(err))?;
936 }
937 rty::SortCtor::User { name }
938 }
939 fhir::SortRes::Adt(def_id) => {
940 let sort_def = self.genv().adt_sort_def_of(def_id)?;
941 if path.args.len() != sort_def.param_count() {
942 let err = errors::IncorrectGenericsOnSort::new(
943 self.genv(),
944 def_id,
945 path.segments.last().unwrap().span,
946 path.args.len(),
947 sort_def.param_count(),
948 );
949 Err(self.emit(err))?;
950 }
951 rty::SortCtor::Adt(sort_def)
952 }
953 };
954 let args = path.args.iter().map(|t| self.conv_sort(t)).try_collect()?;
955
956 Ok(rty::Sort::app(ctor, args))
957 }
958
959 fn check_prim_sort_generics(
960 &mut self,
961 path: &fhir::SortPath<'_>,
962 prim_sort: fhir::PrimSort,
963 ) -> QueryResult {
964 if path.args.len() != prim_sort.generics() {
965 let err = errors::GenericsOnPrimitiveSort::new(
966 path.segments.last().unwrap().span,
967 prim_sort.name_str(),
968 path.args.len(),
969 prim_sort.generics(),
970 );
971 Err(self.emit(err))?;
972 }
973 Ok(())
974 }
975}
976
977impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
979 fn conv_fn_decl(
980 &mut self,
981 env: &mut Env,
982 safety: Safety,
983 abi: rustc_abi::ExternAbi,
984 decl: &fhir::FnDecl,
985 body_id: Option<BodyId>,
986 ) -> QueryResult<rty::FnSig> {
987 let mut requires = vec![];
988 for req in decl.requires {
989 requires.push(self.conv_requires(env, req)?);
990 }
991
992 let mut inputs = vec![];
993 let params =
994 if let Some(body_id) = body_id { self.tcx().hir_body(body_id).params } else { &[] };
995 for (i, ty) in decl.inputs.iter().enumerate() {
996 let ty = if let Some(param) = params.get(i)
997 && let hir::PatKind::Binding(_, _, ident, _) = param.pat.kind
998 {
999 self.conv_ty_with_name(env, ty, ident.name)?
1000 } else {
1001 self.conv_ty(env, ty)?
1002 };
1003 inputs.push(ty);
1004 }
1005
1006 let output = self.conv_fn_output(env, &decl.output)?;
1007
1008 Ok(rty::FnSig::new(safety, abi, requires.into(), inputs.into(), output))
1009 }
1010
1011 fn conv_requires(
1012 &mut self,
1013 env: &mut Env,
1014 requires: &fhir::Requires,
1015 ) -> QueryResult<rty::Expr> {
1016 if requires.params.is_empty() {
1017 self.conv_expr(env, &requires.pred)
1018 } else {
1019 env.push_layer(Layer::list(self.results(), 0, requires.params));
1020 let pred = self.conv_expr(env, &requires.pred)?;
1021 let sorts = env.pop_layer().into_bound_vars(self.genv())?;
1022 Ok(rty::Expr::forall(rty::Binder::bind_with_vars(pred, sorts)))
1023 }
1024 }
1025
1026 fn conv_ensures(
1027 &mut self,
1028 env: &mut Env,
1029 ensures: &fhir::Ensures,
1030 ) -> QueryResult<rty::Ensures> {
1031 match ensures {
1032 fhir::Ensures::Type(loc, ty) => {
1033 Ok(rty::Ensures::Type(self.conv_loc(env, *loc)?, self.conv_ty(env, ty)?))
1034 }
1035 fhir::Ensures::Pred(pred) => Ok(rty::Ensures::Pred(self.conv_expr(env, pred)?)),
1036 }
1037 }
1038
1039 fn conv_fn_output(
1040 &mut self,
1041 env: &mut Env,
1042 output: &fhir::FnOutput,
1043 ) -> QueryResult<rty::Binder<rty::FnOutput>> {
1044 env.push_layer(Layer::list(self.results(), 0, output.params));
1045
1046 let ret = self.conv_ty(env, &output.ret)?;
1047
1048 let ensures: List<rty::Ensures> = output
1049 .ensures
1050 .iter()
1051 .map(|ens| self.conv_ensures(env, ens))
1052 .try_collect()?;
1053 let output = rty::FnOutput::new(ret, ensures);
1054
1055 let vars = env.pop_layer().into_bound_vars(self.genv())?;
1056 Ok(rty::Binder::bind_with_vars(output, vars))
1057 }
1058
1059 fn conv_generic_bounds(
1060 &mut self,
1061 env: &mut Env,
1062 bounded_ty_span: Span,
1063 bounded_ty: rty::Ty,
1064 bounds: fhir::GenericBounds,
1065 ) -> QueryResult<Vec<rty::Clause>> {
1066 let mut clauses = vec![];
1067 for bound in bounds {
1068 match bound {
1069 fhir::GenericBound::Trait(poly_trait_ref) => {
1070 match poly_trait_ref.modifiers {
1071 fhir::TraitBoundModifier::None => {
1072 self.conv_poly_trait_ref(
1073 env,
1074 bounded_ty_span,
1075 &bounded_ty,
1076 poly_trait_ref,
1077 &mut clauses,
1078 )?;
1079 }
1080 fhir::TraitBoundModifier::Maybe => {
1081 }
1085 }
1086 }
1087 fhir::GenericBound::Outlives(lft) => {
1088 let re = self.conv_lifetime(env, *lft, bounded_ty_span);
1089 clauses.push(rty::Clause::new(
1090 List::empty(),
1091 rty::ClauseKind::TypeOutlives(rty::OutlivesPredicate(
1092 bounded_ty.clone(),
1093 re,
1094 )),
1095 ));
1096 }
1097 }
1098 }
1099 Ok(clauses)
1100 }
1101
1102 fn conv_poly_trait_ref(
1104 &mut self,
1105 env: &mut Env,
1106 span: Span,
1107 bounded_ty: &rty::Ty,
1108 poly_trait_ref: &fhir::PolyTraitRef,
1109 clauses: &mut Vec<rty::Clause>,
1110 ) -> QueryResult {
1111 let generic_params = &poly_trait_ref.bound_generic_params;
1112 let layer =
1113 Layer::list(self.results(), generic_params.len() as u32, poly_trait_ref.refine_params);
1114 env.push_layer(layer);
1115
1116 let trait_id = poly_trait_ref.trait_def_id();
1117 let generics = self.genv().generics_of(trait_id)?;
1118 let trait_segment = poly_trait_ref.trait_ref.last_segment();
1119
1120 let self_param = generics.param_at(0, self.genv())?;
1121 let mut args = vec![
1122 self.try_to_ty_or_base(self_param.kind, span, bounded_ty)?
1123 .into(),
1124 ];
1125 self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;
1126
1127 let vars = env.top_layer().to_bound_vars(self.genv())?;
1128 let poly_trait_ref = rty::Binder::bind_with_vars(
1129 rty::TraitRef { def_id: trait_id, args: args.into() },
1130 vars,
1131 );
1132
1133 clauses.push(
1134 poly_trait_ref
1135 .clone()
1136 .map(|trait_ref| {
1137 rty::ClauseKind::Trait(rty::TraitPredicate { trait_ref: trait_ref.clone() })
1138 })
1139 .into(),
1140 );
1141
1142 for cstr in trait_segment.constraints {
1143 self.conv_assoc_item_constraint(env, &poly_trait_ref, cstr, clauses)?;
1144 }
1145
1146 env.pop_layer();
1147
1148 Ok(())
1149 }
1150
1151 fn conv_assoc_item_constraint(
1152 &mut self,
1153 env: &mut Env,
1154 poly_trait_ref: &rty::PolyTraitRef,
1155 constraint: &fhir::AssocItemConstraint,
1156 clauses: &mut Vec<rty::Clause>,
1157 ) -> QueryResult {
1158 let tcx = self.tcx();
1159
1160 let candidate = self.probe_single_bound_for_assoc_item(
1161 || traits::supertraits(tcx, poly_trait_ref.to_rustc(tcx)),
1162 constraint.ident,
1163 AssocTag::Type,
1164 )?;
1165 let assoc_item_id = AssocTag::Type
1166 .trait_defines_item_named(self.genv(), candidate.def_id(), constraint.ident)?
1167 .unwrap()
1168 .def_id;
1169
1170 let fhir::AssocItemConstraintKind::Equality { term } = &constraint.kind;
1171 let span = term.span;
1172 let term = self.conv_ty(env, term)?;
1173 let term = self.ty_to_subset_ty_ctor(span, &term)?;
1174
1175 let clause = poly_trait_ref
1176 .clone()
1177 .map(|trait_ref| {
1178 let args = trait_ref.args;
1180 let refine_args = List::empty();
1181 let projection_ty = rty::AliasTy { def_id: assoc_item_id, args, refine_args };
1182
1183 rty::ClauseKind::Projection(rty::ProjectionPredicate { projection_ty, term })
1184 })
1185 .into();
1186
1187 clauses.push(clause);
1188 Ok(())
1189 }
1190
1191 fn conv_ty_with_name(
1192 &mut self,
1193 env: &mut Env,
1194 ty: &fhir::Ty,
1195 name: Symbol,
1196 ) -> QueryResult<rty::Ty> {
1197 if let fhir::TyKind::BaseTy(bty) = &ty.kind {
1198 Ok(self.conv_bty(env, bty, Some(name))?.to_ty())
1199 } else {
1200 self.conv_ty(env, ty)
1201 }
1202 }
1203
1204 fn conv_ty(&mut self, env: &mut Env, ty: &fhir::Ty) -> QueryResult<rty::Ty> {
1205 match &ty.kind {
1206 fhir::TyKind::BaseTy(bty) => Ok(self.conv_bty(env, bty, None)?.to_ty()),
1207 fhir::TyKind::Indexed(bty, idx) => {
1208 let fhir_id = bty.fhir_id;
1209 let rty::TyOrCtor::Ctor(ty_ctor) = self.conv_bty(env, bty, None)? else {
1210 return Err(self.emit(errors::RefinedUnrefinableType::new(bty.span)))?;
1211 };
1212 let idx = self.conv_expr(env, idx)?;
1213 self.0.insert_node_sort(fhir_id, ty_ctor.sort());
1214 Ok(ty_ctor.replace_bound_reft(&idx))
1215 }
1216 fhir::TyKind::Exists(params, ty) => {
1217 let layer = Layer::list(self.results(), 0, params);
1218 env.push_layer(layer);
1219 let ty = self.conv_ty(env, ty)?;
1220 let sorts = env.pop_layer().into_bound_vars(self.genv())?;
1221 if sorts.is_empty() {
1222 Ok(ty.shift_out_escaping(1))
1223 } else {
1224 Ok(rty::Ty::exists(rty::Binder::bind_with_vars(ty, sorts)))
1225 }
1226 }
1227 fhir::TyKind::StrgRef(lft, loc, ty) => {
1228 let re = self.conv_lifetime(env, *lft, ty.span);
1229 let loc = self.conv_loc(env, **loc)?;
1230 let ty = self.conv_ty(env, ty)?;
1231 Ok(rty::Ty::strg_ref(re, loc, ty))
1232 }
1233 fhir::TyKind::Ref(lft, fhir::MutTy { ty, mutbl }) => {
1234 let region = self.conv_lifetime(env, *lft, ty.span);
1235 Ok(rty::Ty::mk_ref(region, self.conv_ty(env, ty)?, *mutbl))
1236 }
1237 fhir::TyKind::BareFn(bare_fn) => {
1238 let mut env = Env::empty();
1239 env.push_layer(Layer::list(
1240 self.results(),
1241 bare_fn.generic_params.len() as u32,
1242 &[],
1243 ));
1244 let fn_sig =
1245 self.conv_fn_decl(&mut env, bare_fn.safety, bare_fn.abi, bare_fn.decl, None)?;
1246 let vars = bare_fn
1247 .generic_params
1248 .iter()
1249 .map(|param| self.param_as_bound_var(param))
1250 .try_collect()?;
1251 let poly_fn_sig = rty::Binder::bind_with_vars(fn_sig, vars);
1252 Ok(rty::BaseTy::FnPtr(poly_fn_sig).to_ty())
1253 }
1254 fhir::TyKind::Tuple(tys) => {
1255 let tys: List<rty::Ty> =
1256 tys.iter().map(|ty| self.conv_ty(env, ty)).try_collect()?;
1257 Ok(rty::Ty::tuple(tys))
1258 }
1259 fhir::TyKind::Array(ty, len) => {
1260 Ok(rty::Ty::array(self.conv_ty(env, ty)?, self.conv_const_arg(*len)))
1261 }
1262 fhir::TyKind::Never => Ok(rty::Ty::never()),
1263 fhir::TyKind::Constr(pred, ty) => {
1264 let pred = self.conv_expr(env, pred)?;
1265 Ok(rty::Ty::constr(pred, self.conv_ty(env, ty)?))
1266 }
1267 fhir::TyKind::RawPtr(ty, mutability) => {
1268 Ok(rty::Ty::indexed(
1269 rty::BaseTy::RawPtr(self.conv_ty(env, ty)?, *mutability),
1270 rty::Expr::unit(),
1271 ))
1272 }
1273 fhir::TyKind::OpaqueDef(opaque_ty) => self.conv_opaque_def(env, opaque_ty, ty.span),
1274 fhir::TyKind::TraitObject(trait_bounds, lft, syn) => {
1275 if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) {
1276 self.conv_trait_object(env, trait_bounds, *lft, ty.span)
1277 } else {
1278 span_bug!(ty.span, "dyn* traits not supported yet")
1279 }
1280 }
1281 fhir::TyKind::Infer => Ok(rty::Ty::infer(self.next_type_vid())),
1282 fhir::TyKind::Err(err) => Err(QueryErr::Emitted(*err)),
1283 }
1284 }
1285
1286 fn conv_opaque_def(
1288 &mut self,
1289 env: &mut Env,
1290 opaque_ty: &fhir::OpaqueTy,
1291 span: Span,
1292 ) -> QueryResult<rty::Ty> {
1293 let def_id = opaque_ty.def_id;
1294
1295 if P::HAS_ELABORATED_INFORMATION {
1296 let lifetimes = self.tcx().opaque_captured_lifetimes(def_id.local_id());
1297
1298 let generics = self.tcx().generics_of(opaque_ty.def_id);
1299
1300 let offset = generics.parent_count;
1301
1302 let args = rty::GenericArg::for_item(self.genv(), def_id.resolved_id(), |param, _| {
1303 if let Some(i) = (param.index as usize).checked_sub(offset) {
1304 let (lifetime, _) = lifetimes[i];
1305 rty::GenericArg::Lifetime(self.conv_resolved_lifetime(env, lifetime, span))
1306 } else {
1307 rty::GenericArg::from_param_def(param)
1308 }
1309 })?;
1310 let reft_args = rty::RefineArgs::identity_for_item(self.genv(), def_id.resolved_id())?;
1311 let alias_ty = rty::AliasTy::new(def_id.resolved_id(), args, reft_args);
1312 Ok(rty::BaseTy::opaque(alias_ty).to_ty())
1313 } else {
1314 self.conv_opaque_ty(opaque_ty)?;
1318
1319 let alias_ty = rty::AliasTy::new(def_id.resolved_id(), List::empty(), List::empty());
1322 Ok(rty::BaseTy::opaque(alias_ty).to_ty())
1323 }
1324 }
1325
1326 fn conv_trait_object(
1327 &mut self,
1328 env: &mut Env,
1329 trait_bounds: &[fhir::PolyTraitRef],
1330 lifetime: fhir::Lifetime,
1331 span: Span,
1332 ) -> QueryResult<rty::Ty> {
1333 let mut bounds = vec![];
1340 let dummy_self = rty::Ty::trait_object_dummy_self();
1341 for trait_bound in trait_bounds.iter().rev() {
1342 self.conv_poly_trait_ref(env, trait_bound.span, &dummy_self, trait_bound, &mut bounds)?;
1343 }
1344
1345 let mut trait_bounds = vec![];
1347 let mut projection_bounds = vec![];
1348 for pred in bounds {
1349 let bound_pred = pred.kind();
1350 let vars = bound_pred.vars().clone();
1351 match bound_pred.skip_binder() {
1352 rty::ClauseKind::Trait(trait_pred) => {
1353 trait_bounds.push(rty::Binder::bind_with_vars(trait_pred.trait_ref, vars));
1354 }
1355 rty::ClauseKind::Projection(proj) => {
1356 projection_bounds.push(rty::Binder::bind_with_vars(proj, vars));
1357 }
1358 rty::ClauseKind::RegionOutlives(_) => {}
1359 rty::ClauseKind::TypeOutlives(_) => {}
1360 rty::ClauseKind::ConstArgHasType(..) => {
1361 bug!("did not expect {pred:?} clause in object bounds");
1362 }
1363 }
1364 }
1365
1366 let (mut auto_traits, regular_traits): (Vec<_>, Vec<_>) = trait_bounds
1368 .into_iter()
1369 .partition(|trait_ref| self.tcx().trait_is_auto(trait_ref.def_id()));
1370
1371 {
1373 let mut duplicates = FxHashSet::default();
1374 auto_traits.retain(|trait_ref| duplicates.insert(trait_ref.def_id()));
1375 }
1376
1377 let regular_trait_predicates = regular_traits.into_iter().map(|poly_trait_ref| {
1378 poly_trait_ref.map(|trait_ref| {
1379 let args = trait_ref.args.iter().skip(1).cloned().collect();
1381 rty::ExistentialPredicate::Trait(rty::ExistentialTraitRef {
1382 def_id: trait_ref.def_id,
1383 args,
1384 })
1385 })
1386 });
1387
1388 let auto_trait_predicates = auto_traits.into_iter().map(|trait_def| {
1389 rty::Binder::dummy(rty::ExistentialPredicate::AutoTrait(trait_def.def_id()))
1390 });
1391
1392 let existential_projections = projection_bounds.into_iter().map(|bound| {
1393 bound.map(|proj| {
1394 let args = proj.projection_ty.args.iter().skip(1).cloned().collect();
1396 rty::ExistentialPredicate::Projection(rty::ExistentialProjection {
1397 def_id: proj.projection_ty.def_id,
1398 args,
1399 term: proj.term.clone(),
1400 })
1401 })
1402 });
1403
1404 let existential_predicates = {
1405 let mut v = regular_trait_predicates
1406 .chain(existential_projections)
1407 .chain(auto_trait_predicates)
1408 .collect_vec();
1409 v.sort_by(|a, b| {
1410 a.as_ref()
1411 .skip_binder()
1412 .stable_cmp(self.tcx(), b.as_ref().skip_binder())
1413 });
1414 List::from_vec(v)
1415 };
1416
1417 let region = self.conv_lifetime(env, lifetime, span);
1418 Ok(rty::Ty::dynamic(existential_predicates, region))
1419 }
1420
1421 pub(crate) fn conv_bty(
1422 &mut self,
1423 env: &mut Env,
1424 bty: &fhir::BaseTy,
1425 name: Option<Symbol>,
1426 ) -> QueryResult<rty::TyOrCtor> {
1427 match &bty.kind {
1428 fhir::BaseTyKind::Path(fhir::QPath::Resolved(qself, path)) => {
1429 self.conv_qpath(env, *qself, path, name)
1430 }
1431 fhir::BaseTyKind::Path(fhir::QPath::TypeRelative(qself, segment)) => {
1432 let qself_res =
1433 if let Some(path) = qself.as_path() { path.res } else { fhir::Res::Err };
1434 let alias_ty = self
1435 .conv_type_relative_type_path(env, qself.span, qself_res, segment)?
1436 .shift_in_escaping(1);
1437 let bty = rty::BaseTy::Alias(rty::AliasKind::Projection, alias_ty);
1438 let sort = bty.sort();
1439 let ty = rty::Ty::indexed(bty, rty::Expr::nu());
1440 Ok(rty::TyOrCtor::Ctor(rty::Binder::bind_with_sort(ty, sort)))
1441 }
1442 fhir::BaseTyKind::Slice(ty) => {
1443 let bty = rty::BaseTy::Slice(self.conv_ty(env, ty)?).shift_in_escaping(1);
1444 let sort = bty.sort();
1445 let ty = rty::Ty::indexed(bty, rty::Expr::nu());
1446 Ok(rty::TyOrCtor::Ctor(rty::Binder::bind_with_sort(ty, sort)))
1447 }
1448 fhir::BaseTyKind::Err(err) => Err(QueryErr::Emitted(*err)),
1449 }
1450 }
1451
1452 fn conv_type_relative_path<Tag: AssocItemTag>(
1453 &mut self,
1454 tag: Tag,
1455 qself_span: Span,
1456 qself_res: fhir::Res,
1457 assoc_ident: Ident,
1458 ) -> QueryResult<(Tag::AssocItem<'tcx>, rty::TraitRef)> {
1459 let tcx = self.tcx();
1460
1461 let bound = match qself_res {
1462 fhir::Res::SelfTyAlias { alias_to: impl_def_id, is_trait_impl: true } => {
1463 let Some(trait_ref) = tcx.impl_trait_ref(impl_def_id) else {
1464 span_bug!(qself_span, "expected cycle error");
1466 };
1467
1468 self.probe_single_bound_for_assoc_item(
1469 || {
1470 traits::supertraits(
1471 tcx,
1472 ty::Binder::dummy(trait_ref.instantiate_identity()),
1473 )
1474 },
1475 assoc_ident,
1476 tag,
1477 )?
1478 }
1479 fhir::Res::Def(DefKind::TyParam, param_id)
1480 | fhir::Res::SelfTyParam { trait_: param_id } => {
1481 let predicates = type_param_predicates(tcx, param_id);
1482 self.probe_single_bound_for_assoc_item(
1483 || {
1484 tag.transitive_bounds_that_define_assoc_item(
1485 self.genv(),
1486 predicates.map(|pred| pred.map_bound(|t| t.trait_ref)),
1487 assoc_ident,
1488 )
1489 },
1490 assoc_ident,
1491 tag,
1492 )?
1493 }
1494 _ => self.report_assoc_item_not_found(assoc_ident.span, tag)?,
1495 };
1496
1497 let Some(trait_ref) = bound.no_bound_vars() else {
1498 Err(self.emit(
1506 query_bug!("associated path with uninferred generic parameters")
1507 .at(assoc_ident.span),
1508 ))?
1509 };
1510
1511 let trait_ref = trait_ref
1512 .lower(tcx)
1513 .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?
1514 .refine(&self.refiner()?)?;
1515
1516 let assoc_item = tag
1517 .trait_defines_item_named(self.genv(), trait_ref.def_id, assoc_ident)?
1518 .unwrap();
1519
1520 Ok((assoc_item, trait_ref))
1521 }
1522
1523 fn conv_type_relative_type_path(
1524 &mut self,
1525 env: &mut Env,
1526 qself_span: Span,
1527 qself_res: fhir::Res,
1528 assoc_segment: &fhir::PathSegment,
1529 ) -> QueryResult<rty::AliasTy> {
1530 let (assoc_item, trait_ref) = self.conv_type_relative_path(
1531 AssocTag::Type,
1532 qself_span,
1533 qself_res,
1534 assoc_segment.ident,
1535 )?;
1536
1537 let assoc_id = assoc_item.def_id;
1538 let mut args = trait_ref.args.to_vec();
1539 self.conv_generic_args_into(env, assoc_id, assoc_segment, &mut args)?;
1540
1541 let args = List::from_vec(args);
1542 let refine_args = List::empty();
1543 let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id };
1544 Ok(alias_ty)
1545 }
1546
1547 fn conv_type_relative_const_path(
1548 &mut self,
1549 fhir_expr: &fhir::Expr,
1550 qself: &rty::Ty,
1551 assoc: Ident,
1552 ) -> QueryResult<rty::Expr> {
1553 let tcx = self.genv().tcx();
1554
1555 let mut candidates = vec![];
1556 if let Some(simplified_type) = qself.simplify_type() {
1557 candidates = tcx
1558 .incoherent_impls(simplified_type)
1559 .iter()
1560 .filter_map(|impl_id| {
1561 tcx.associated_items(impl_id).find_by_ident_and_kind(
1562 tcx,
1563 assoc,
1564 AssocTag::Const,
1565 *impl_id,
1566 )
1567 })
1568 .collect_vec();
1569 }
1570 let (expr, sort) = match &candidates[..] {
1571 [candidate] => self.conv_const(fhir_expr.span, candidate.def_id)?,
1572 [] => self.report_assoc_item_not_found(fhir_expr.span, AssocTag::Const)?,
1573 _ => self.report_ambiguous_assoc_item(fhir_expr.span, AssocTag::Const, assoc)?,
1574 };
1575 self.0.insert_node_sort(fhir_expr.fhir_id, sort);
1576 Ok(expr)
1577 }
1578
1579 fn refiner(&self) -> QueryResult<Refiner<'genv, 'tcx>> {
1581 match self.owner() {
1582 FluxOwnerId::Rust(owner_id) => {
1583 let def_id = self.genv().maybe_extern_id(owner_id.def_id);
1584 Refiner::default_for_item(self.genv(), def_id.resolved_id())
1585 }
1586 FluxOwnerId::Flux(_) => Err(query_bug!("cannot refine types insicde flux item")),
1587 }
1588 }
1589
1590 fn probe_single_bound_for_assoc_item<I, Tag: AssocItemTag>(
1591 &self,
1592 all_candidates: impl FnOnce() -> I,
1593 assoc_name: Ident,
1594 tag: Tag,
1595 ) -> QueryResult<ty::PolyTraitRef<'tcx>>
1596 where
1597 I: Iterator<Item = ty::PolyTraitRef<'tcx>>,
1598 {
1599 let mut matching_candidates = vec![];
1600 for candidate in all_candidates() {
1601 if tag
1602 .trait_defines_item_named(self.genv(), candidate.def_id(), assoc_name)?
1603 .is_some()
1604 {
1605 matching_candidates.push(candidate);
1606 }
1607 }
1608
1609 let Some(bound) = matching_candidates.pop() else {
1610 self.report_assoc_item_not_found(assoc_name.span, tag)?;
1611 };
1612
1613 if !matching_candidates.is_empty() {
1614 self.report_ambiguous_assoc_item(assoc_name.span, tag, assoc_name)?;
1615 }
1616
1617 Ok(bound)
1618 }
1619
1620 fn conv_lifetime(&mut self, env: &Env, lft: fhir::Lifetime, span: Span) -> rty::Region {
1621 let res = match lft {
1622 fhir::Lifetime::Hole(_) => return rty::Region::ReVar(self.next_region_vid()),
1623 fhir::Lifetime::Resolved(res) => res,
1624 };
1625 self.conv_resolved_lifetime(env, res, span)
1626 }
1627
1628 fn conv_resolved_lifetime(&mut self, env: &Env, res: ResolvedArg, span: Span) -> rty::Region {
1629 let tcx = self.tcx();
1630 let lifetime_name = |def_id| tcx.item_name(def_id);
1631 match res {
1632 ResolvedArg::StaticLifetime => rty::ReStatic,
1633 ResolvedArg::EarlyBound(def_id) => {
1634 let index = self.genv().def_id_to_param_index(def_id.to_def_id());
1635 let name = lifetime_name(def_id.to_def_id());
1636 rty::ReEarlyParam(rty::EarlyParamRegion { index, name })
1637 }
1638 ResolvedArg::LateBound(_, index, def_id) => {
1639 let Some(depth) = env.depth().checked_sub(1) else {
1640 span_bug!(span, "late-bound variable at depth 0")
1641 };
1642 let kind = rty::BoundRegionKind::Named(def_id.to_def_id());
1643 let var = BoundVar::from_u32(index);
1644 let bound_region = rty::BoundRegion { var, kind };
1645 rty::ReBound(rty::DebruijnIndex::from_usize(depth), bound_region)
1646 }
1647 ResolvedArg::Free(scope, id) => {
1648 let kind = rty::LateParamRegionKind::Named(id.to_def_id());
1649 rty::ReLateParam(rty::LateParamRegion { scope: scope.to_def_id(), kind })
1650 }
1651 ResolvedArg::Error(_) => bug!("lifetime resolved to an error"),
1652 }
1653 }
1654
1655 fn conv_const_arg(&mut self, cst: fhir::ConstArg) -> rty::Const {
1656 match cst.kind {
1657 fhir::ConstArgKind::Lit(lit) => rty::Const::from_usize(self.tcx(), lit),
1658 fhir::ConstArgKind::Param(def_id) => {
1659 rty::Const {
1660 kind: rty::ConstKind::Param(def_id_to_param_const(self.genv(), def_id)),
1661 }
1662 }
1663 fhir::ConstArgKind::Infer => {
1664 rty::Const {
1665 kind: rty::ConstKind::Infer(ty::InferConst::Var(self.next_const_vid())),
1666 }
1667 }
1668 }
1669 }
1670
1671 fn conv_qpath(
1672 &mut self,
1673 env: &mut Env,
1674 qself: Option<&fhir::Ty>,
1675 path: &fhir::Path,
1676 name: Option<Symbol>,
1677 ) -> QueryResult<rty::TyOrCtor> {
1678 let bty = match path.res {
1679 fhir::Res::PrimTy(prim_ty) => {
1680 self.check_prim_ty_generics(path, prim_ty)?;
1681 prim_ty_to_bty(prim_ty)
1682 }
1683 fhir::Res::Def(DefKind::Struct | DefKind::Enum | DefKind::Union, did) => {
1684 let adt_def = self.genv().adt_def(did)?;
1685 let args = self.conv_generic_args(env, did, path.last_segment())?;
1686 rty::BaseTy::adt(adt_def, args)
1687 }
1688 fhir::Res::Def(DefKind::TyParam, def_id) => {
1689 let owner_id = ty_param_owner(self.genv(), def_id);
1690 let param_ty = def_id_to_param_ty(self.genv(), def_id);
1691 self.check_ty_param_generics(path, param_ty)?;
1692 let param = self
1693 .genv()
1694 .generics_of(owner_id)?
1695 .param_at(param_ty.index as usize, self.genv())?;
1696 match param.kind {
1697 rty::GenericParamDefKind::Type { .. } => {
1698 return Ok(rty::TyOrCtor::Ty(rty::Ty::param(param_ty)));
1699 }
1700 rty::GenericParamDefKind::Base { .. } => rty::BaseTy::Param(param_ty),
1701 _ => return Err(query_bug!("unexpected param kind")),
1702 }
1703 }
1704 fhir::Res::SelfTyParam { trait_ } => {
1705 self.check_self_ty_generics(path)?;
1706 let param = &self.genv().generics_of(trait_)?.own_params[0];
1707 match param.kind {
1708 rty::GenericParamDefKind::Type { .. } => {
1709 return Ok(rty::TyOrCtor::Ty(rty::Ty::param(rty::SELF_PARAM_TY)));
1710 }
1711 rty::GenericParamDefKind::Base { .. } => rty::BaseTy::Param(rty::SELF_PARAM_TY),
1712 _ => return Err(query_bug!("unexpected param kind")),
1713 }
1714 }
1715 fhir::Res::SelfTyAlias { alias_to, .. } => {
1716 self.check_self_ty_generics(path)?;
1717 if P::EXPAND_TYPE_ALIASES {
1718 return Ok(self.genv().type_of(alias_to)?.instantiate_identity());
1719 } else {
1720 rty::BaseTy::Alias(
1721 rty::AliasKind::Free,
1722 rty::AliasTy {
1723 def_id: alias_to,
1724 args: List::empty(),
1725 refine_args: List::empty(),
1726 },
1727 )
1728 }
1729 }
1730 fhir::Res::Def(DefKind::AssocTy, assoc_id) => {
1731 let trait_id = self.tcx().trait_of_assoc(assoc_id).unwrap();
1732
1733 let [.., trait_segment, assoc_segment] = path.segments else {
1734 span_bug!(path.span, "expected at least two segments");
1735 };
1736
1737 let Some(qself) = qself else {
1738 self.report_ambiguous_assoc_item(
1739 path.span,
1740 AssocTag::Type,
1741 assoc_segment.ident,
1742 )?
1743 };
1744
1745 let trait_generics = self.genv().generics_of(trait_id)?;
1746 let qself =
1747 self.conv_ty_to_generic_arg(env, &trait_generics.own_params[0], qself)?;
1748 let mut args = vec![qself];
1749 self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;
1750 self.conv_generic_args_into(env, assoc_id, assoc_segment, &mut args)?;
1751 let args = List::from_vec(args);
1752
1753 let refine_args = List::empty();
1754 let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id };
1755 rty::BaseTy::Alias(rty::AliasKind::Projection, alias_ty)
1756 }
1757 fhir::Res::Def(DefKind::TyAlias, def_id) => {
1758 self.check_refinement_generics(path, def_id)?;
1759 let args = self.conv_generic_args(env, def_id, path.last_segment())?;
1760 self.0.insert_path_args(path.fhir_id, args.clone());
1761 let refine_args = path
1762 .refine
1763 .iter()
1764 .map(|expr| self.conv_expr(env, expr))
1765 .try_collect_vec()?;
1766
1767 if P::EXPAND_TYPE_ALIASES {
1768 let tcx = self.tcx();
1769 return Ok(self
1770 .genv()
1771 .type_of(def_id)?
1772 .instantiate(tcx, &args, &refine_args));
1773 } else {
1774 rty::BaseTy::Alias(
1775 rty::AliasKind::Free,
1776 rty::AliasTy { def_id, args, refine_args: List::from(refine_args) },
1777 )
1778 }
1779 }
1780 fhir::Res::Def(DefKind::ForeignTy, def_id) => {
1781 self.check_foreign_ty_generics(path)?;
1782 rty::BaseTy::Foreign(def_id)
1783 }
1784 fhir::Res::Def(kind, def_id) => self.report_expected_type(path.span, kind, def_id)?,
1785 fhir::Res::Param(..) | fhir::Res::GlobalFunc(..) | fhir::Res::Err => {
1786 span_bug!(path.span, "unexpected resolution in conv_ty_ctor: {:?}", path.res)
1787 }
1788 };
1789 let sort = bty.sort();
1790 let bty = bty.shift_in_escaping(1);
1791 let kind = match name {
1792 Some(name) => BoundReftKind::Named(name),
1793 None => BoundReftKind::Anon,
1794 };
1795 let var = rty::BoundVariableKind::Refine(sort, rty::InferMode::EVar, kind);
1796 let ctor = rty::Binder::bind_with_vars(
1797 rty::Ty::indexed(bty, rty::Expr::nu()),
1798 List::singleton(var),
1799 );
1800 Ok(rty::TyOrCtor::Ctor(ctor))
1801 }
1802
1803 fn param_as_bound_var(
1804 &mut self,
1805 param: &fhir::GenericParam,
1806 ) -> QueryResult<rty::BoundVariableKind> {
1807 let def_id = param.def_id.resolved_id();
1808 match param.kind {
1809 fhir::GenericParamKind::Lifetime => {
1810 Ok(rty::BoundVariableKind::Region(rty::BoundRegionKind::Named(def_id)))
1811 }
1812 fhir::GenericParamKind::Const { .. } | fhir::GenericParamKind::Type { .. } => {
1813 Err(query_bug!(def_id, "unsupported param kind `{:?}`", param.kind))
1814 }
1815 }
1816 }
1817
1818 fn conv_generic_args(
1819 &mut self,
1820 env: &mut Env,
1821 def_id: DefId,
1822 segment: &fhir::PathSegment,
1823 ) -> QueryResult<List<rty::GenericArg>> {
1824 let mut into = vec![];
1825 self.conv_generic_args_into(env, def_id, segment, &mut into)?;
1826 Ok(List::from(into))
1827 }
1828
1829 fn conv_generic_args_into(
1830 &mut self,
1831 env: &mut Env,
1832 def_id: DefId,
1833 segment: &fhir::PathSegment,
1834 into: &mut Vec<rty::GenericArg>,
1835 ) -> QueryResult {
1836 let generics = self.genv().generics_of(def_id)?;
1837
1838 self.check_generic_arg_count(&generics, def_id, segment)?;
1839
1840 let len = into.len();
1841 for (idx, arg) in segment.args.iter().enumerate() {
1842 let param = generics.param_at(idx + len, self.genv())?;
1843 match arg {
1844 fhir::GenericArg::Lifetime(lft) => {
1845 into.push(rty::GenericArg::Lifetime(self.conv_lifetime(
1846 env,
1847 *lft,
1848 segment.ident.span,
1849 )));
1850 }
1851 fhir::GenericArg::Type(ty) => {
1852 into.push(self.conv_ty_to_generic_arg(env, ¶m, ty)?);
1853 }
1854 fhir::GenericArg::Const(cst) => {
1855 into.push(rty::GenericArg::Const(self.conv_const_arg(*cst)));
1856 }
1857 fhir::GenericArg::Infer => {
1858 into.push(self.conv_generic_arg_hole(env, param, segment.ident.span)?);
1859 }
1860 }
1861 }
1862 self.fill_generic_args_defaults(def_id, into)
1863 }
1864
1865 fn conv_generic_arg_hole(
1866 &mut self,
1867 env: &mut Env,
1868 param: rty::GenericParamDef,
1869 span: Span,
1870 ) -> QueryResult<rty::GenericArg> {
1871 match param.kind {
1872 rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::Base { .. } => {
1873 let ty = fhir::Ty { kind: fhir::TyKind::Infer, span };
1874 Ok(self.conv_ty_to_generic_arg(env, ¶m, &ty)?)
1875 }
1876 rty::GenericParamDefKind::Const { .. } => {
1877 let cst = fhir::ConstArg { kind: fhir::ConstArgKind::Infer, span };
1878 Ok(rty::GenericArg::Const(self.conv_const_arg(cst)))
1879 }
1880 rty::GenericParamDefKind::Lifetime => {
1881 let re = rty::Region::ReVar(self.next_region_vid());
1882 Ok(rty::GenericArg::Lifetime(re))
1883 }
1884 }
1885 }
1886
1887 fn check_generic_arg_count(
1888 &mut self,
1889 generics: &rty::Generics,
1890 def_id: DefId,
1891 segment: &fhir::PathSegment,
1892 ) -> QueryResult {
1893 let found = segment.args.len();
1894 let mut param_count = generics.own_params.len();
1895
1896 if let DefKind::Trait = self.genv().def_kind(def_id) {
1898 param_count -= 1;
1899 }
1900
1901 let min = param_count - generics.own_default_count();
1902 let max = param_count;
1903 if min == max && found != min {
1904 Err(self.emit(errors::GenericArgCountMismatch::new(
1905 self.genv(),
1906 def_id,
1907 segment,
1908 min,
1909 )))?;
1910 }
1911 if found < min {
1912 Err(self.emit(errors::TooFewGenericArgs::new(self.genv(), def_id, segment, min)))?;
1913 }
1914 if found > max {
1915 Err(self.emit(errors::TooManyGenericArgs::new(self.genv(), def_id, segment, min)))?;
1916 }
1917 Ok(())
1918 }
1919
1920 fn fill_generic_args_defaults(
1921 &mut self,
1922 def_id: DefId,
1923 into: &mut Vec<rty::GenericArg>,
1924 ) -> QueryResult {
1925 let generics = self.genv().generics_of(def_id)?;
1926 for param in generics.own_params.iter().skip(into.len()) {
1927 debug_assert!(matches!(
1928 param.kind,
1929 rty::GenericParamDefKind::Type { has_default: true }
1930 | rty::GenericParamDefKind::Base { has_default: true }
1931 ));
1932 let span = self.tcx().def_span(param.def_id);
1933 let ty = self
1936 .genv()
1937 .type_of(param.def_id)?
1938 .instantiate(self.tcx(), into, &[])
1939 .to_ty();
1940 into.push(self.try_to_ty_or_base(param.kind, span, &ty)?.into());
1941 }
1942 Ok(())
1943 }
1944
1945 fn conv_ty_to_generic_arg(
1946 &mut self,
1947 env: &mut Env,
1948 param: &rty::GenericParamDef,
1949 ty: &fhir::Ty,
1950 ) -> QueryResult<rty::GenericArg> {
1951 let rty_ty = self.conv_ty(env, ty)?;
1952 Ok(self.try_to_ty_or_base(param.kind, ty.span, &rty_ty)?.into())
1953 }
1954
1955 fn try_to_ty_or_base(
1956 &mut self,
1957 kind: rty::GenericParamDefKind,
1958 span: Span,
1959 ty: &rty::Ty,
1960 ) -> QueryResult<rty::TyOrBase> {
1961 match kind {
1962 rty::GenericParamDefKind::Type { .. } => Ok(rty::TyOrBase::Ty(ty.clone())),
1963 rty::GenericParamDefKind::Base { .. } => {
1964 Ok(rty::TyOrBase::Base(self.ty_to_subset_ty_ctor(span, ty)?))
1965 }
1966 _ => span_bug!(span, "unexpected param kind `{kind:?}`"),
1967 }
1968 }
1969
1970 fn ty_to_subset_ty_ctor(&mut self, span: Span, ty: &rty::Ty) -> QueryResult<rty::SubsetTyCtor> {
1971 let ctor = if let rty::TyKind::Infer(vid) = ty.kind() {
1972 let sort_vid =
1974 if vid.as_u32() == 0 { rty::SortVid::from_u32(0) } else { self.next_sort_vid() };
1975 rty::SubsetTyCtor::bind_with_sort(
1976 rty::SubsetTy::trivial(rty::BaseTy::Infer(*vid), rty::Expr::nu()),
1977 rty::Sort::Infer(rty::SortInfer::SortVar(sort_vid)),
1978 )
1979 } else {
1980 ty.shallow_canonicalize()
1981 .as_ty_or_base()
1982 .as_base()
1983 .ok_or_else(|| self.emit(errors::InvalidBaseInstance::new(span)))?
1984 };
1985 Ok(ctor)
1986 }
1987
1988 #[track_caller]
1989 fn emit(&self, err: impl Diagnostic<'genv>) -> ErrorGuaranteed {
1990 self.genv().sess().emit_err(err)
1991 }
1992
1993 fn report_assoc_item_not_found<Tag: AssocItemTag>(
1994 &self,
1995 span: Span,
1996 assoc_tag: Tag,
1997 ) -> Result<!, ErrorGuaranteed> {
1998 Err(self.emit(errors::AssocItemNotFound { span, tag: assoc_tag.descr() }))?
1999 }
2000
2001 fn report_ambiguous_assoc_item<Tag: AssocItemTag>(
2002 &self,
2003 span: Span,
2004 assoc_tag: Tag,
2005 assoc_name: Ident,
2006 ) -> Result<!, ErrorGuaranteed> {
2007 Err(self.emit(errors::AmbiguousAssocItem {
2008 span,
2009 name: assoc_name,
2010 tag: assoc_tag.descr(),
2011 }))?
2012 }
2013
2014 #[track_caller]
2015 fn report_expected_type(
2016 &self,
2017 span: Span,
2018 kind: DefKind,
2019 def_id: DefId,
2020 ) -> Result<!, ErrorGuaranteed> {
2021 Err(self.emit(errors::ExpectedType {
2022 span,
2023 def_descr: self.tcx().def_kind_descr(kind, def_id),
2024 name: self.tcx().def_path_str(def_id),
2025 }))?
2026 }
2027}
2028
2029impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
2031 fn check_refinement_generics(&mut self, path: &fhir::Path, def_id: DefId) -> QueryResult {
2032 let generics = self.genv().refinement_generics_of(def_id)?;
2033 if generics.count() != path.refine.len() {
2034 let err = errors::RefineArgMismatch {
2035 span: path.span,
2036 expected: generics.count(),
2037 found: path.refine.len(),
2038 kind: self.tcx().def_descr(def_id),
2039 };
2040 Err(self.emit(err))?;
2041 }
2042 Ok(())
2043 }
2044
2045 fn check_prim_ty_generics(
2046 &mut self,
2047 path: &fhir::Path<'_>,
2048 prim_ty: rustc_hir::PrimTy,
2049 ) -> QueryResult {
2050 if !path.last_segment().args.is_empty() {
2051 let err = errors::GenericsOnPrimTy { span: path.span, name: prim_ty.name_str() };
2052 Err(self.emit(err))?;
2053 }
2054 Ok(())
2055 }
2056
2057 fn check_ty_param_generics(
2058 &mut self,
2059 path: &fhir::Path<'_>,
2060 param_ty: rty::ParamTy,
2061 ) -> QueryResult {
2062 if !path.last_segment().args.is_empty() {
2063 let err = errors::GenericsOnTyParam { span: path.span, name: param_ty.name };
2064 Err(self.emit(err))?;
2065 }
2066 Ok(())
2067 }
2068
2069 fn check_self_ty_generics(&mut self, path: &fhir::Path<'_>) -> QueryResult {
2070 if !path.last_segment().args.is_empty() {
2071 let err = errors::GenericsOnSelfTy { span: path.span };
2072 Err(self.emit(err))?;
2073 }
2074 Ok(())
2075 }
2076
2077 fn check_foreign_ty_generics(&mut self, path: &fhir::Path<'_>) -> QueryResult {
2078 if !path.last_segment().args.is_empty() {
2079 let err = errors::GenericsOnForeignTy { span: path.span };
2080 Err(self.emit(err))?;
2081 }
2082 Ok(())
2083 }
2084}
2085
2086fn prim_ty_to_bty(prim_ty: rustc_hir::PrimTy) -> rty::BaseTy {
2087 match prim_ty {
2088 rustc_hir::PrimTy::Int(int_ty) => rty::BaseTy::Int(int_ty),
2089 rustc_hir::PrimTy::Uint(uint_ty) => rty::BaseTy::Uint(uint_ty),
2090 rustc_hir::PrimTy::Float(float_ty) => rty::BaseTy::Float(float_ty),
2091 rustc_hir::PrimTy::Str => rty::BaseTy::Str,
2092 rustc_hir::PrimTy::Bool => rty::BaseTy::Bool,
2093 rustc_hir::PrimTy::Char => rty::BaseTy::Char,
2094 }
2095}
2096
2097impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
2099 fn conv_lit(&self, lit: fhir::Lit, fhir_id: FhirId, span: Span) -> QueryResult<rty::Constant> {
2100 match lit {
2101 fhir::Lit::Int(n, kind) => {
2102 match kind {
2103 Some(fhir::NumLitKind::Int) => Ok(rty::Constant::from(n)),
2104 Some(fhir::NumLitKind::Real) => Ok(rty::Constant::Real(rty::Real(n))),
2105 None => {
2106 let sort = self.results().node_sort(fhir_id);
2107 if let rty::Sort::BitVec(bvsize) = sort {
2108 if let rty::BvSize::Fixed(size) = bvsize
2109 && (n == 0 || n.ilog2() < size)
2110 {
2111 Ok(rty::Constant::BitVec(n, size))
2112 } else {
2113 Err(self.emit(errors::InvalidBitVectorConstant::new(span, sort)))?
2114 }
2115 } else {
2116 Ok(rty::Constant::from(n))
2117 }
2118 }
2119 }
2120 }
2121 fhir::Lit::Bool(b) => Ok(rty::Constant::from(b)),
2122 fhir::Lit::Str(s) => Ok(rty::Constant::from(s)),
2123 fhir::Lit::Char(c) => Ok(rty::Constant::from(c)),
2124 }
2125 }
2126
2127 fn conv_expr(&mut self, env: &mut Env, expr: &fhir::Expr) -> QueryResult<rty::Expr> {
2128 let fhir_id = expr.fhir_id;
2129 let espan = ESpan::new(expr.span);
2130 let expr = match expr.kind {
2131 fhir::ExprKind::Var(QPathExpr::Resolved(path, _)) => self.conv_path_expr(env, path)?,
2132 fhir::ExprKind::Var(QPathExpr::TypeRelative(qself, assoc)) => {
2133 let qself = self.conv_ty(env, qself)?;
2134 self.conv_type_relative_const_path(expr, &qself, assoc)?
2135 }
2136 fhir::ExprKind::Literal(lit) => {
2137 rty::Expr::constant(self.conv_lit(lit, fhir_id, expr.span)?).at(espan)
2138 }
2139 fhir::ExprKind::BinaryOp(op, e1, e2) => {
2140 rty::Expr::binary_op(
2141 self.conv_bin_op(op, expr.fhir_id),
2142 self.conv_expr(env, e1)?,
2143 self.conv_expr(env, e2)?,
2144 )
2145 .at(espan)
2146 }
2147 fhir::ExprKind::UnaryOp(op, e) => {
2148 rty::Expr::unary_op(conv_un_op(op), self.conv_expr(env, e)?).at(espan)
2149 }
2150
2151 fhir::ExprKind::PrimApp(op, e1, e2) => {
2152 rty::Expr::prim_val(
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::App(func, args) => {
2160 let sort_args = self.results().node_sort_args(fhir_id);
2161 rty::Expr::app(self.conv_func(env, &func)?, sort_args, self.conv_exprs(env, args)?)
2162 .at(espan)
2163 }
2164 fhir::ExprKind::Alias(alias, args) => {
2165 let args = args
2166 .iter()
2167 .map(|arg| self.conv_expr(env, arg))
2168 .try_collect()?;
2169 let alias = self.conv_alias_reft(env, expr.fhir_id, &alias)?;
2170 rty::Expr::alias(alias, args).at(espan)
2171 }
2172 fhir::ExprKind::IfThenElse(p, e1, e2) => {
2173 rty::Expr::ite(
2174 self.conv_expr(env, p)?,
2175 self.conv_expr(env, e1)?,
2176 self.conv_expr(env, e2)?,
2177 )
2178 .at(espan)
2179 }
2180 fhir::ExprKind::Dot(base, _) => {
2181 let proj = self.results().field_proj(fhir_id);
2182 rty::Expr::field_proj(self.conv_expr(env, base)?, proj)
2183 }
2184 fhir::ExprKind::Abs(params, body) => {
2185 env.push_layer(Layer::list(self.results(), 0, params));
2186 let pred = self.conv_expr(env, body)?;
2187 let vars = env.pop_layer().into_bound_vars(self.genv())?;
2188 let output = self.results().node_sort(body.fhir_id);
2189 let lam = rty::Lambda::bind_with_vars(pred, vars, output);
2190 rty::Expr::abs(lam)
2191 }
2192 fhir::ExprKind::Block(decls, body) => {
2193 for decl in decls {
2194 env.push_layer(Layer::list(self.results(), 0, &[decl.param]));
2195 }
2196 let mut body = self.conv_expr(env, body)?;
2197 for decl in decls.iter().rev() {
2198 let vars = env.pop_layer().into_bound_vars(self.genv())?;
2199 let init = self.conv_expr(env, &decl.init)?;
2200 body = rty::Expr::let_(init, rty::Binder::bind_with_vars(body, vars));
2201 }
2202 body
2203 }
2204 fhir::ExprKind::BoundedQuant(kind, param, rng, body) => {
2205 env.push_layer(Layer::list(self.results(), 0, &[param]));
2206 let pred = self.conv_expr(env, body)?;
2207 let vars = env.pop_layer().into_bound_vars(self.genv())?;
2208 let body = rty::Binder::bind_with_vars(pred, vars);
2209 rty::Expr::bounded_quant(kind, rng, body)
2210 }
2211 fhir::ExprKind::Record(flds) => {
2212 let def_id = self.results().record_ctor(expr.fhir_id);
2213 let flds = flds
2214 .iter()
2215 .map(|expr| self.conv_expr(env, expr))
2216 .try_collect()?;
2217 rty::Expr::ctor_struct(def_id, flds)
2218 }
2219 fhir::ExprKind::Constructor(path, exprs, spread) => {
2220 let def_id = if let Some(path) = path {
2221 match path.res {
2222 fhir::Res::Def(DefKind::Enum | DefKind::Struct, def_id) => def_id,
2223 _ => span_bug!(path.span, "unexpected path in constructor"),
2224 }
2225 } else {
2226 self.results().record_ctor(expr.fhir_id)
2227 };
2228 let assns = self.conv_constructor_exprs(def_id, env, exprs, &spread)?;
2229 rty::Expr::ctor_struct(def_id, assns)
2230 }
2231 fhir::ExprKind::Err(err) => Err(QueryErr::Emitted(err))?,
2232 };
2233 Ok(self.add_coercions(expr, fhir_id))
2234 }
2235
2236 fn conv_loc(&mut self, env: &mut Env, loc: fhir::PathExpr) -> QueryResult<rty::Path> {
2237 Ok(self
2238 .conv_path_expr(env, loc)?
2239 .to_path()
2240 .unwrap_or_else(|| span_bug!(loc.span, "expected path, found `{loc:?}`")))
2241 }
2242
2243 fn conv_path_expr(&mut self, env: &mut Env, path: fhir::PathExpr) -> QueryResult<rty::Expr> {
2244 let genv = self.genv();
2245 let tcx = self.genv().tcx();
2246 let espan = ESpan::new(path.span);
2247 let (expr, sort) = match path.res {
2248 fhir::Res::Param(_, id) => (env.lookup(&path).to_expr(), self.results().param_sort(id)),
2249 fhir::Res::Def(DefKind::Const, def_id) => {
2250 self.hyperlink(path.span, tcx.def_ident_span(def_id));
2251 let (expr, sort) = self.conv_const(path.span, def_id)?;
2252 (expr.at(espan), sort)
2253 }
2254 fhir::Res::Def(DefKind::Ctor(..), ctor_id) => {
2255 let Some(sort) = genv.sort_of_def_id(ctor_id).emit(&genv)? else {
2256 span_bug!(path.span, "unexpected variant {ctor_id:?}")
2257 };
2258
2259 let variant_id = self.tcx().parent(ctor_id);
2260 let enum_id = self.tcx().parent(variant_id);
2261 self.hyperlink(path.span, tcx.def_ident_span(variant_id));
2262 let idx = variant_idx(self.tcx(), variant_id);
2263 (rty::Expr::ctor_enum(enum_id, idx), sort)
2264 }
2265 fhir::Res::Def(DefKind::ConstParam, def_id) => {
2266 self.hyperlink(path.span, tcx.def_ident_span(def_id));
2267 let sort = rty::Sort::Int;
2269 (rty::Expr::const_generic(def_id_to_param_const(genv, def_id)).at(espan), sort)
2270 }
2271 _ => {
2272 Err(self.emit(errors::InvalidRes { span: path.span, res_descr: path.res.descr() }))?
2273 }
2274 };
2275 self.0.insert_node_sort(path.fhir_id, sort);
2276 Ok(expr)
2277 }
2278
2279 fn conv_const(&self, span: Span, def_id: DefId) -> QueryResult<(rty::Expr, rty::Sort)> {
2280 let genv = self.genv();
2281 let Some(sort) = genv.sort_of_def_id(def_id).emit(&genv)? else {
2282 span_bug!(span, "unsupported const: `{def_id:?}`")
2283 };
2284 let info = genv.constant_info(def_id).emit(&genv)?;
2285 if sort != rty::Sort::Int && matches!(info, rty::ConstantInfo::Uninterpreted) {
2287 Err(self.emit(errors::ConstantAnnotationNeeded::new(span)))?;
2288 }
2289 Ok((rty::Expr::const_def_id(def_id).at(ESpan::new(span)), sort))
2290 }
2291
2292 fn conv_constructor_exprs(
2293 &mut self,
2294 struct_def_id: DefId,
2295 env: &mut Env,
2296 exprs: &[fhir::FieldExpr],
2297 spread: &Option<&fhir::Spread>,
2298 ) -> QueryResult<List<rty::Expr>> {
2299 let spread = spread
2300 .map(|spread| self.conv_expr(env, &spread.expr))
2301 .transpose()?;
2302 let mut field_exprs_by_name: FxHashMap<Symbol, rty::Expr> = exprs
2303 .iter()
2304 .map(|field_expr| -> QueryResult<_> {
2305 Ok((field_expr.ident.name, self.conv_expr(env, &field_expr.expr)?))
2306 })
2307 .try_collect()?;
2308
2309 if !P::HAS_ELABORATED_INFORMATION {
2310 return Ok(List::default());
2311 };
2312
2313 let adt_def = self.genv().adt_sort_def_of(struct_def_id)?;
2314 let struct_variant = adt_def.struct_variant();
2315 let mut assns = Vec::new();
2316 for (idx, field_name) in struct_variant.field_names().iter().enumerate() {
2317 if let Some(expr) = field_exprs_by_name.remove(field_name) {
2318 assns.push(expr);
2319 } else if let Some(spread) = &spread {
2320 let proj = rty::FieldProj::Adt { def_id: struct_def_id, field: idx as u32 };
2321 assns.push(rty::Expr::field_proj(spread, proj));
2322 }
2323 }
2324 Ok(List::from_vec(assns))
2325 }
2326
2327 fn conv_exprs(&mut self, env: &mut Env, exprs: &[fhir::Expr]) -> QueryResult<List<rty::Expr>> {
2328 exprs.iter().map(|e| self.conv_expr(env, e)).collect()
2329 }
2330
2331 fn conv_bin_op(&self, op: fhir::BinOp, fhir_id: FhirId) -> rty::BinOp {
2332 match op {
2333 fhir::BinOp::Iff => rty::BinOp::Iff,
2334 fhir::BinOp::Imp => rty::BinOp::Imp,
2335 fhir::BinOp::Or => rty::BinOp::Or,
2336 fhir::BinOp::And => rty::BinOp::And,
2337 fhir::BinOp::Eq => rty::BinOp::Eq,
2338 fhir::BinOp::Ne => rty::BinOp::Ne,
2339 fhir::BinOp::Gt => rty::BinOp::Gt(self.results().bin_op_sort(fhir_id)),
2340 fhir::BinOp::Ge => rty::BinOp::Ge(self.results().bin_op_sort(fhir_id)),
2341 fhir::BinOp::Lt => rty::BinOp::Lt(self.results().bin_op_sort(fhir_id)),
2342 fhir::BinOp::Le => rty::BinOp::Le(self.results().bin_op_sort(fhir_id)),
2343 fhir::BinOp::Add => rty::BinOp::Add(self.results().bin_op_sort(fhir_id)),
2344 fhir::BinOp::Sub => rty::BinOp::Sub(self.results().bin_op_sort(fhir_id)),
2345 fhir::BinOp::Mul => rty::BinOp::Mul(self.results().bin_op_sort(fhir_id)),
2346 fhir::BinOp::Mod => rty::BinOp::Mod(self.results().bin_op_sort(fhir_id)),
2347 fhir::BinOp::Div => rty::BinOp::Div(self.results().bin_op_sort(fhir_id)),
2348 fhir::BinOp::BitAnd => rty::BinOp::BitAnd,
2349 fhir::BinOp::BitOr => rty::BinOp::BitOr,
2350 fhir::BinOp::BitXor => rty::BinOp::BitXor,
2351 fhir::BinOp::BitShl => rty::BinOp::BitShl,
2352 fhir::BinOp::BitShr => rty::BinOp::BitShr,
2353 }
2354 }
2355
2356 fn add_coercions(&self, mut expr: rty::Expr, fhir_id: FhirId) -> rty::Expr {
2357 let span = expr.span();
2358 for coercion in self.results().coercions_for(fhir_id) {
2359 expr = match *coercion {
2360 rty::Coercion::Inject(def_id) => {
2361 rty::Expr::ctor_struct(def_id, List::singleton(expr)).at_opt(span)
2362 }
2363 rty::Coercion::Project(def_id) => {
2364 rty::Expr::field_proj(expr, rty::FieldProj::Adt { def_id, field: 0 })
2365 .at_opt(span)
2366 }
2367 };
2368 }
2369 expr
2370 }
2371
2372 fn hyperlink(&self, span: Span, dst_span: Option<Span>) {
2373 if P::HAS_ELABORATED_INFORMATION
2374 && let Some(dst_span) = dst_span
2375 {
2376 dbg::hyperlink!(self.genv().tcx(), span, dst_span);
2377 }
2378 }
2379
2380 fn conv_func(&mut self, env: &Env, func: &fhir::PathExpr) -> QueryResult<rty::Expr> {
2381 let genv = self.genv();
2382 let span = func.span;
2383 let (expr, sort) = match func.res {
2384 fhir::Res::Param(_, id) => {
2385 let sort = self.results().param_sort(id);
2386 (env.lookup(func).to_expr(), sort)
2387 }
2388 fhir::Res::GlobalFunc(fhir::SpecFuncKind::Def(did)) => {
2389 self.hyperlink(span, Some(genv.func_span(did)));
2390 let sort = rty::Sort::Func(genv.func_sort(did));
2391 (rty::Expr::global_func(rty::SpecFuncKind::Def(did)), sort)
2392 }
2393 fhir::Res::GlobalFunc(fhir::SpecFuncKind::Uif(did)) => {
2394 self.hyperlink(span, Some(genv.func_span(did)));
2395 let sort = rty::Sort::Func(genv.func_sort(did));
2396 (rty::Expr::global_func(rty::SpecFuncKind::Uif(did)), sort)
2397 }
2398 fhir::Res::GlobalFunc(fhir::SpecFuncKind::Thy(itf)) => {
2399 let sort = THEORY_FUNCS.get(&itf).unwrap().sort.clone();
2400 (rty::Expr::global_func(rty::SpecFuncKind::Thy(itf)), rty::Sort::Func(sort))
2401 }
2402 fhir::Res::GlobalFunc(fhir::SpecFuncKind::Cast) => {
2403 let fsort = rty::PolyFuncSort::new(
2404 List::from_arr([rty::SortParamKind::Sort, rty::SortParamKind::Sort]),
2405 rty::FuncSort::new(
2406 vec![rty::Sort::Var(rty::ParamSort::from(0_usize))],
2407 rty::Sort::Var(rty::ParamSort::from(1_usize)),
2408 ),
2409 );
2410 (rty::Expr::internal_func(InternalFuncKind::Cast), rty::Sort::Func(fsort))
2411 }
2412 _ => {
2413 return Err(
2414 self.emit(errors::InvalidRes { span: func.span, res_descr: func.res.descr() })
2415 )?;
2416 }
2417 };
2418 self.0.insert_node_sort(func.fhir_id, sort);
2419 Ok(self.add_coercions(expr, func.fhir_id))
2420 }
2421
2422 fn conv_alias_reft(
2423 &mut self,
2424 env: &mut Env,
2425 fhir_id: FhirId,
2426 alias: &fhir::AliasReft,
2427 ) -> QueryResult<rty::AliasReft> {
2428 let alias_reft = match alias {
2429 fhir::AliasReft::Qualified { qself, trait_, name } => {
2430 let fhir::Res::Def(DefKind::Trait, trait_id) = trait_.res else {
2431 span_bug!(trait_.span, "expected trait")
2432 };
2433 let trait_segment = trait_.last_segment();
2434
2435 let generics = self.genv().generics_of(trait_id)?;
2436 let self_ty =
2437 self.conv_ty_to_generic_arg(env, &generics.param_at(0, self.genv())?, qself)?;
2438 let mut generic_args = vec![self_ty];
2439 self.conv_generic_args_into(env, trait_id, trait_segment, &mut generic_args)?;
2440
2441 let Some(assoc_reft) = self.genv().assoc_refinements_of(trait_id)?.find(name.name)
2442 else {
2443 return Err(self.emit(errors::InvalidAssocReft::new(
2444 trait_.span,
2445 name.name,
2446 format!("{:?}", trait_),
2447 )))?;
2448 };
2449
2450 let assoc_id = assoc_reft.def_id;
2451
2452 dbg::hyperlink!(self.genv().tcx(), name.span, assoc_reft.span);
2453
2454 rty::AliasReft { assoc_id, args: List::from_vec(generic_args) }
2455 }
2456 fhir::AliasReft::TypeRelative { qself, name } => {
2457 let qself_res =
2458 if let Some(path) = qself.as_path() { path.res } else { fhir::Res::Err };
2459 let (assoc_reft, trait_ref) =
2460 self.conv_type_relative_path(AssocReftTag, qself.span, qself_res, *name)?;
2461 rty::AliasReft { assoc_id: assoc_reft.def_id, args: trait_ref.args }
2462 }
2463 };
2464 let fsort = alias_reft.fsort(self.genv())?;
2465 self.0.insert_alias_reft_sort(fhir_id, fsort);
2466 Ok(alias_reft)
2467 }
2468
2469 pub(crate) fn conv_invariants(
2470 &mut self,
2471 adt_id: MaybeExternId,
2472 params: &[fhir::RefineParam],
2473 invariants: &[fhir::Expr],
2474 ) -> QueryResult<Vec<rty::Invariant>> {
2475 let mut env = Env::new(&[]);
2476 env.push_layer(Layer::coalesce(self.results(), adt_id.resolved_id(), params));
2477 invariants
2478 .iter()
2479 .map(|invariant| self.conv_invariant(&mut env, invariant))
2480 .collect()
2481 }
2482
2483 fn conv_invariant(
2484 &mut self,
2485 env: &mut Env,
2486 invariant: &fhir::Expr,
2487 ) -> QueryResult<rty::Invariant> {
2488 Ok(rty::Invariant::new(rty::Binder::bind_with_vars(
2489 self.conv_expr(env, invariant)?,
2490 env.top_layer().to_bound_vars(self.genv())?,
2491 )))
2492 }
2493}
2494
2495impl Env {
2496 fn new(early_params: &[fhir::RefineParam]) -> Self {
2497 let early_params = early_params
2498 .iter()
2499 .map(|param| (param.id, param.name))
2500 .collect();
2501 Self { layers: vec![], early_params }
2502 }
2503
2504 pub(crate) fn empty() -> Self {
2505 Self { layers: vec![], early_params: Default::default() }
2506 }
2507
2508 fn depth(&self) -> usize {
2509 self.layers.len()
2510 }
2511
2512 fn push_layer(&mut self, layer: Layer) {
2513 self.layers.push(layer);
2514 }
2515
2516 fn pop_layer(&mut self) -> Layer {
2517 self.layers.pop().expect("bottom of layer stack")
2518 }
2519
2520 fn top_layer(&self) -> &Layer {
2521 self.layers.last().expect("bottom of layer stack")
2522 }
2523
2524 fn lookup(&self, var: &fhir::PathExpr) -> LookupResult<'_> {
2525 let (_, id) = var.res.expect_param();
2526 for (i, layer) in self.layers.iter().rev().enumerate() {
2527 if let Some((idx, entry)) = layer.get(id) {
2528 let debruijn = DebruijnIndex::from_usize(i);
2529 let kind = LookupResultKind::Bound {
2530 debruijn,
2531 entry,
2532 index: idx as u32,
2533 kind: layer.kind,
2534 };
2535 return LookupResult { var_span: var.span, kind };
2536 }
2537 }
2538 if let Some((idx, _, name)) = self.early_params.get_full(&id) {
2539 LookupResult {
2540 var_span: var.span,
2541 kind: LookupResultKind::EarlyParam { index: idx as u32, name: *name },
2542 }
2543 } else {
2544 span_bug!(var.span, "no entry found for key: `{:?}`", id);
2545 }
2546 }
2547
2548 fn to_early_param_args(&self) -> List<rty::Expr> {
2549 self.early_params
2550 .iter()
2551 .enumerate()
2552 .map(|(idx, (_, name))| rty::Expr::early_param(idx as u32, *name))
2553 .collect()
2554 }
2555}
2556
2557impl Layer {
2558 fn new<R: WfckResultsProvider>(
2559 results: &R,
2560 params: &[fhir::RefineParam],
2561 kind: LayerKind,
2562 ) -> Self {
2563 let map = params
2564 .iter()
2565 .map(|param| {
2566 let sort = results.param_sort(param.id);
2567 let infer_mode = rty::InferMode::from_param_kind(param.kind);
2568 let entry = ParamEntry::new(sort, infer_mode, param.name);
2569 (param.id, entry)
2570 })
2571 .collect();
2572 Self { map, kind }
2573 }
2574
2575 fn list<R: WfckResultsProvider>(
2576 results: &R,
2577 bound_regions: u32,
2578 params: &[fhir::RefineParam],
2579 ) -> Self {
2580 Self::new(results, params, LayerKind::List { bound_regions })
2581 }
2582
2583 fn coalesce<R: WfckResultsProvider>(
2584 results: &R,
2585 def_id: DefId,
2586 params: &[fhir::RefineParam],
2587 ) -> Self {
2588 Self::new(results, params, LayerKind::Coalesce(def_id))
2589 }
2590
2591 fn get(&self, name: impl Borrow<fhir::ParamId>) -> Option<(usize, &ParamEntry)> {
2592 let (idx, _, entry) = self.map.get_full(name.borrow())?;
2593 Some((idx, entry))
2594 }
2595
2596 fn into_bound_vars(self, genv: GlobalEnv) -> QueryResult<List<rty::BoundVariableKind>> {
2597 match self.kind {
2598 LayerKind::List { .. } => {
2599 Ok(self
2600 .into_iter()
2601 .map(|entry| {
2602 let kind = rty::BoundReftKind::Named(entry.name);
2603 rty::BoundVariableKind::Refine(entry.sort, entry.mode, kind)
2604 })
2605 .collect())
2606 }
2607 LayerKind::Coalesce(def_id) => {
2608 let sort_def = genv.adt_sort_def_of(def_id)?;
2609 let args = sort_def.identity_args();
2610 let ctor = rty::SortCtor::Adt(sort_def);
2611 Ok(List::singleton(rty::BoundVariableKind::Refine(
2612 rty::Sort::App(ctor, args),
2613 rty::InferMode::EVar,
2614 rty::BoundReftKind::Anon,
2615 )))
2616 }
2617 }
2618 }
2619
2620 fn to_bound_vars(&self, genv: GlobalEnv) -> QueryResult<List<rty::BoundVariableKind>> {
2621 self.clone().into_bound_vars(genv)
2622 }
2623
2624 fn into_iter(self) -> impl Iterator<Item = ParamEntry> {
2625 self.map.into_values()
2626 }
2627}
2628
2629impl ParamEntry {
2630 fn new(sort: rty::Sort, mode: fhir::InferMode, name: Symbol) -> Self {
2631 ParamEntry { name, sort, mode }
2632 }
2633}
2634
2635impl LookupResult<'_> {
2636 fn to_expr(&self) -> rty::Expr {
2637 let espan = ESpan::new(self.var_span);
2638 match &self.kind {
2639 LookupResultKind::Bound { debruijn, entry: ParamEntry { name, .. }, kind, index } => {
2640 match *kind {
2641 LayerKind::List { bound_regions } => {
2642 rty::Expr::bvar(
2643 *debruijn,
2644 BoundVar::from_u32(bound_regions + *index),
2645 rty::BoundReftKind::Named(*name),
2646 )
2647 .at(espan)
2648 }
2649 LayerKind::Coalesce(def_id) => {
2650 let var =
2651 rty::Expr::bvar(*debruijn, BoundVar::ZERO, rty::BoundReftKind::Anon)
2652 .at(espan);
2653 rty::Expr::field_proj(var, rty::FieldProj::Adt { def_id, field: *index })
2654 .at(espan)
2655 }
2656 }
2657 }
2658 &LookupResultKind::EarlyParam { index, name, .. } => {
2659 rty::Expr::early_param(index, name).at(espan)
2660 }
2661 }
2662 }
2663}
2664
2665pub fn conv_func_decl(genv: GlobalEnv, func: &fhir::SpecFunc) -> QueryResult<rty::PolyFuncSort> {
2666 let wfckresults = WfckResults::new(FluxOwnerId::Flux(func.def_id));
2667 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
2668 let inputs_and_output = func
2669 .args
2670 .iter()
2671 .map(|p| &p.sort)
2672 .chain(iter::once(&func.sort))
2673 .map(|sort| cx.conv_sort(sort))
2674 .try_collect()?;
2675 let params = iter::repeat_n(rty::SortParamKind::Sort, func.params).collect();
2676 Ok(rty::PolyFuncSort::new(params, rty::FuncSort { inputs_and_output }))
2677}
2678
2679fn conv_un_op(op: fhir::UnOp) -> rty::UnOp {
2680 match op {
2681 fhir::UnOp::Not => rty::UnOp::Not,
2682 fhir::UnOp::Neg => rty::UnOp::Neg,
2683 }
2684}
2685
2686fn def_id_to_param_ty(genv: GlobalEnv, def_id: DefId) -> rty::ParamTy {
2687 rty::ParamTy { index: genv.def_id_to_param_index(def_id), name: ty_param_name(genv, def_id) }
2688}
2689
2690fn def_id_to_param_const(genv: GlobalEnv, def_id: DefId) -> rty::ParamConst {
2691 rty::ParamConst { index: genv.def_id_to_param_index(def_id), name: ty_param_name(genv, def_id) }
2692}
2693
2694fn ty_param_owner(genv: GlobalEnv, def_id: DefId) -> DefId {
2695 let def_kind = genv.def_kind(def_id);
2696 match def_kind {
2697 DefKind::Trait | DefKind::TraitAlias => def_id,
2698 DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
2699 genv.tcx().parent(def_id)
2700 }
2701 _ => bug!("ty_param_owner: {:?} is a {:?} not a type parameter", def_id, def_kind),
2702 }
2703}
2704
2705fn ty_param_name(genv: GlobalEnv, def_id: DefId) -> Symbol {
2706 let def_kind = genv.tcx().def_kind(def_id);
2707 match def_kind {
2708 DefKind::Trait | DefKind::TraitAlias => kw::SelfUpper,
2709 DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
2710 genv.tcx().item_name(def_id)
2711 }
2712 _ => bug!("ty_param_name: {:?} is a {:?} not a type parameter", def_id, def_kind),
2713 }
2714}
2715
2716trait AssocItemTag: Copy {
2719 type AssocItem<'tcx>;
2720
2721 fn descr(self) -> &'static str;
2722
2723 fn trait_defines_item_named<'tcx>(
2724 self,
2725 genv: GlobalEnv<'_, 'tcx>,
2726 trait_def_id: DefId,
2727 assoc_name: Ident,
2728 ) -> QueryResult<Option<Self::AssocItem<'tcx>>>;
2729
2730 fn transitive_bounds_that_define_assoc_item<'tcx>(
2731 self,
2732 genv: GlobalEnv<'_, 'tcx>,
2733 trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2734 assoc_name: Ident,
2735 ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>>;
2736}
2737
2738impl AssocItemTag for AssocTag {
2739 type AssocItem<'tcx> = &'tcx AssocItem;
2740
2741 fn descr(self) -> &'static str {
2742 match self {
2743 AssocTag::Const => "constant",
2744 AssocTag::Fn => "function",
2745 AssocTag::Type => "type",
2746 }
2747 }
2748
2749 fn trait_defines_item_named<'tcx>(
2750 self,
2751 genv: GlobalEnv<'_, 'tcx>,
2752 trait_def_id: DefId,
2753 assoc_name: Ident,
2754 ) -> QueryResult<Option<Self::AssocItem<'tcx>>> {
2755 Ok(genv
2756 .tcx()
2757 .associated_items(trait_def_id)
2758 .find_by_ident_and_kind(genv.tcx(), assoc_name, self, trait_def_id))
2759 }
2760
2761 fn transitive_bounds_that_define_assoc_item<'tcx>(
2762 self,
2763 genv: GlobalEnv<'_, 'tcx>,
2764 trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2765 assoc_name: Ident,
2766 ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2767 traits::transitive_bounds_that_define_assoc_item(genv.tcx(), trait_refs, assoc_name)
2768 }
2769}
2770
2771#[derive(Copy, Clone)]
2772struct AssocReftTag;
2773
2774impl AssocItemTag for AssocReftTag {
2775 type AssocItem<'tcx> = AssocReft;
2776
2777 fn descr(self) -> &'static str {
2778 "refinement"
2779 }
2780
2781 fn trait_defines_item_named<'tcx>(
2782 self,
2783 genv: GlobalEnv<'_, 'tcx>,
2784 trait_def_id: DefId,
2785 assoc_name: Ident,
2786 ) -> QueryResult<Option<Self::AssocItem<'tcx>>> {
2787 Ok(genv
2788 .assoc_refinements_of(trait_def_id)?
2789 .find(assoc_name.name))
2790 }
2791
2792 fn transitive_bounds_that_define_assoc_item<'tcx>(
2793 self,
2794 genv: GlobalEnv<'_, 'tcx>,
2795 trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2796 _assoc_name: Ident,
2797 ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2798 transitive_bounds(genv.tcx(), trait_refs)
2799 }
2800}
2801
2802fn type_param_predicates<'tcx>(
2809 tcx: TyCtxt<'tcx>,
2810 param_id: DefId,
2811) -> impl Iterator<Item = ty::PolyTraitPredicate<'tcx>> {
2812 let parent = if tcx.def_kind(param_id) == DefKind::Trait {
2813 param_id
2815 } else {
2816 tcx.parent(param_id)
2817 };
2818 let param_index = tcx
2819 .generics_of(parent)
2820 .param_def_id_to_index(tcx, param_id)
2821 .unwrap();
2822 let predicates = tcx.predicates_of(parent).instantiate_identity(tcx);
2823 predicates.into_iter().filter_map(move |(clause, _)| {
2824 clause
2825 .as_trait_clause()
2826 .filter(|trait_pred| trait_pred.self_ty().skip_binder().is_param(param_index))
2827 })
2828}
2829
2830fn transitive_bounds<'tcx>(
2838 tcx: TyCtxt<'tcx>,
2839 trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2840) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2841 let mut seen = FxHashSet::default();
2842 let mut stack: Vec<_> = trait_refs.collect();
2843
2844 std::iter::from_fn(move || {
2845 while let Some(trait_ref) = stack.pop() {
2846 if !seen.insert(tcx.anonymize_bound_vars(trait_ref)) {
2847 continue;
2848 }
2849
2850 stack.extend(
2851 tcx.explicit_super_predicates_of(trait_ref.def_id())
2852 .iter_identity_copied()
2853 .map(|(clause, _)| clause.instantiate_supertrait(tcx, trait_ref))
2854 .filter_map(|clause| clause.as_trait_clause())
2855 .filter(|clause| clause.polarity() == ty::PredicatePolarity::Positive)
2856 .map(|clause| clause.map_bound(|clause| clause.trait_ref)),
2857 );
2858
2859 return Some(trait_ref);
2860 }
2861
2862 None
2863 })
2864}
2865
2866mod errors {
2867 use flux_errors::E0999;
2868 use flux_macros::Diagnostic;
2869 use flux_middle::{fhir, global_env::GlobalEnv, rty::Sort};
2870 use rustc_hir::def_id::DefId;
2871 use rustc_span::{Span, Symbol, symbol::Ident};
2872
2873 #[derive(Diagnostic)]
2874 #[diag(fhir_analysis_assoc_item_not_found, code = E0999)]
2875 #[note]
2876 pub(super) struct AssocItemNotFound {
2877 #[primary_span]
2878 #[label]
2879 pub span: Span,
2880 pub tag: &'static str,
2881 }
2882
2883 #[derive(Diagnostic)]
2884 #[diag(fhir_analysis_ambiguous_assoc_item, code = E0999)]
2885 pub(super) struct AmbiguousAssocItem {
2886 #[primary_span]
2887 pub span: Span,
2888 pub name: Ident,
2889 pub tag: &'static str,
2890 }
2891
2892 #[derive(Diagnostic)]
2893 #[diag(fhir_analysis_invalid_base_instance, code = E0999)]
2894 pub(super) struct InvalidBaseInstance {
2895 #[primary_span]
2896 span: Span,
2897 }
2898
2899 impl InvalidBaseInstance {
2900 pub(super) fn new(span: Span) -> Self {
2901 Self { span }
2902 }
2903 }
2904
2905 #[derive(Diagnostic)]
2906 #[diag(fhir_analysis_generic_argument_count_mismatch, code = E0999)]
2907 pub(super) struct GenericArgCountMismatch {
2908 #[primary_span]
2909 #[label]
2910 span: Span,
2911 found: usize,
2912 expected: usize,
2913 def_descr: &'static str,
2914 }
2915
2916 impl GenericArgCountMismatch {
2917 pub(super) fn new(
2918 genv: GlobalEnv,
2919 def_id: DefId,
2920 segment: &fhir::PathSegment,
2921 expected: usize,
2922 ) -> Self {
2923 GenericArgCountMismatch {
2924 span: segment.ident.span,
2925 found: segment.args.len(),
2926 expected,
2927 def_descr: genv.tcx().def_descr(def_id),
2928 }
2929 }
2930 }
2931
2932 #[derive(Diagnostic)]
2933 #[diag(fhir_analysis_too_few_generic_args, code = E0999)]
2934 pub(super) struct TooFewGenericArgs {
2935 #[primary_span]
2936 #[label]
2937 span: Span,
2938 found: usize,
2939 min: usize,
2940 def_descr: &'static str,
2941 }
2942
2943 impl TooFewGenericArgs {
2944 pub(super) fn new(
2945 genv: GlobalEnv,
2946 def_id: DefId,
2947 segment: &fhir::PathSegment,
2948 min: usize,
2949 ) -> Self {
2950 Self {
2951 span: segment.ident.span,
2952 found: segment.args.len(),
2953 min,
2954 def_descr: genv.tcx().def_descr(def_id),
2955 }
2956 }
2957 }
2958
2959 #[derive(Diagnostic)]
2960 #[diag(fhir_analysis_too_many_generic_args, code = E0999)]
2961 pub(super) struct TooManyGenericArgs {
2962 #[primary_span]
2963 #[label]
2964 span: Span,
2965 found: usize,
2966 max: usize,
2967 def_descr: &'static str,
2968 }
2969
2970 impl TooManyGenericArgs {
2971 pub(super) fn new(
2972 genv: GlobalEnv,
2973 def_id: DefId,
2974 segment: &fhir::PathSegment,
2975 max: usize,
2976 ) -> Self {
2977 Self {
2978 span: segment.ident.span,
2979 found: segment.args.len(),
2980 max,
2981 def_descr: genv.tcx().def_descr(def_id),
2982 }
2983 }
2984 }
2985
2986 #[derive(Diagnostic)]
2987 #[diag(fhir_analysis_refined_unrefinable_type, code = E0999)]
2988 pub(super) struct RefinedUnrefinableType {
2989 #[primary_span]
2990 span: Span,
2991 }
2992
2993 impl RefinedUnrefinableType {
2994 pub(super) fn new(span: Span) -> Self {
2995 Self { span }
2996 }
2997 }
2998
2999 #[derive(Diagnostic)]
3000 #[diag(fhir_analysis_generics_on_primitive_sort, code = E0999)]
3001 pub(super) struct GenericsOnPrimitiveSort {
3002 #[primary_span]
3003 #[label]
3004 span: Span,
3005 name: &'static str,
3006 found: usize,
3007 expected: usize,
3008 }
3009
3010 impl GenericsOnPrimitiveSort {
3011 pub(super) fn new(span: Span, name: &'static str, found: usize, expected: usize) -> Self {
3012 Self { span, found, expected, name }
3013 }
3014 }
3015
3016 #[derive(Diagnostic)]
3017 #[diag(fhir_analysis_incorrect_generics_on_sort, code = E0999)]
3018 pub(super) struct IncorrectGenericsOnSort {
3019 #[primary_span]
3020 #[label]
3021 span: Span,
3022 found: usize,
3023 expected: usize,
3024 def_descr: &'static str,
3025 }
3026
3027 impl IncorrectGenericsOnSort {
3028 pub(super) fn new(
3029 genv: GlobalEnv,
3030 def_id: DefId,
3031 span: Span,
3032 found: usize,
3033 expected: usize,
3034 ) -> Self {
3035 Self { span, found, expected, def_descr: genv.tcx().def_descr(def_id) }
3036 }
3037 }
3038
3039 #[derive(Diagnostic)]
3040 #[diag(fhir_analysis_generics_on_sort_ty_param, code = E0999)]
3041 pub(super) struct GenericsOnSortTyParam {
3042 #[primary_span]
3043 #[label]
3044 span: Span,
3045 found: usize,
3046 }
3047
3048 impl GenericsOnSortTyParam {
3049 pub(super) fn new(span: Span, found: usize) -> Self {
3050 Self { span, found }
3051 }
3052 }
3053
3054 #[derive(Diagnostic)]
3055 #[diag(fhir_analysis_generics_on_self_alias, code = E0999)]
3056 pub(super) struct GenericsOnSelf {
3057 #[primary_span]
3058 #[label]
3059 span: Span,
3060 found: usize,
3061 }
3062
3063 impl GenericsOnSelf {
3064 pub(super) fn new(span: Span, found: usize) -> Self {
3065 Self { span, found }
3066 }
3067 }
3068
3069 #[derive(Diagnostic)]
3070 #[diag(fhir_analysis_fields_on_reflected_enum_variant, code = E0999)]
3071 pub(super) struct FieldsOnReflectedEnumVariant {
3072 #[primary_span]
3073 #[label]
3074 span: Span,
3075 }
3076
3077 impl FieldsOnReflectedEnumVariant {
3078 pub(super) fn new(span: Span) -> Self {
3079 Self { span }
3080 }
3081 }
3082
3083 #[derive(Diagnostic)]
3084 #[diag(fhir_analysis_generics_on_opaque_sort, code = E0999)]
3085 pub(super) struct GenericsOnUserDefinedOpaqueSort {
3086 #[primary_span]
3087 #[label]
3088 span: Span,
3089 found: usize,
3090 }
3091
3092 impl GenericsOnUserDefinedOpaqueSort {
3093 pub(super) fn new(span: Span, found: usize) -> Self {
3094 Self { span, found }
3095 }
3096 }
3097
3098 #[derive(Diagnostic)]
3099 #[diag(fhir_analysis_generics_on_prim_ty, code = E0999)]
3100 pub(super) struct GenericsOnPrimTy {
3101 #[primary_span]
3102 pub span: Span,
3103 pub name: &'static str,
3104 }
3105
3106 #[derive(Diagnostic)]
3107 #[diag(fhir_analysis_generics_on_ty_param, code = E0999)]
3108 pub(super) struct GenericsOnTyParam {
3109 #[primary_span]
3110 pub span: Span,
3111 pub name: Symbol,
3112 }
3113
3114 #[derive(Diagnostic)]
3115 #[diag(fhir_analysis_generics_on_self_ty, code = E0999)]
3116 pub(super) struct GenericsOnSelfTy {
3117 #[primary_span]
3118 pub span: Span,
3119 }
3120
3121 #[derive(Diagnostic)]
3122 #[diag(fhir_analysis_generics_on_foreign_ty, code = E0999)]
3123 pub(super) struct GenericsOnForeignTy {
3124 #[primary_span]
3125 pub span: Span,
3126 }
3127
3128 #[derive(Diagnostic)]
3129 #[diag(fhir_analysis_invalid_bitvector_constant, code = E0999)]
3130 pub struct InvalidBitVectorConstant {
3131 #[primary_span]
3132 #[label]
3133 span: Span,
3134 sort: Sort,
3135 }
3136
3137 impl InvalidBitVectorConstant {
3138 pub(crate) fn new(span: Span, sort: Sort) -> Self {
3139 Self { span, sort }
3140 }
3141 }
3142
3143 #[derive(Diagnostic)]
3144 #[diag(fhir_analysis_invalid_assoc_reft, code = E0999)]
3145 pub struct InvalidAssocReft {
3146 #[primary_span]
3147 span: Span,
3148 trait_: String,
3149 name: Symbol,
3150 }
3151
3152 impl InvalidAssocReft {
3153 pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
3154 Self { span, trait_, name }
3155 }
3156 }
3157
3158 #[derive(Diagnostic)]
3159 #[diag(fhir_analysis_refine_arg_mismatch, code = E0999)]
3160 pub(super) struct RefineArgMismatch {
3161 #[primary_span]
3162 #[label]
3163 pub span: Span,
3164 pub expected: usize,
3165 pub found: usize,
3166 pub kind: &'static str,
3167 }
3168
3169 #[derive(Diagnostic)]
3170 #[diag(fhir_analysis_expected_type, code = E0999)]
3171 pub(super) struct ExpectedType {
3172 #[primary_span]
3173 pub span: Span,
3174 pub def_descr: &'static str,
3175 pub name: String,
3176 }
3177
3178 #[derive(Diagnostic)]
3179 #[diag(fhir_analysis_fail_to_match_predicates, code = E0999)]
3180 pub(super) struct FailToMatchPredicates {
3181 #[primary_span]
3182 pub span: Span,
3183 }
3184
3185 #[derive(Diagnostic)]
3186 #[diag(fhir_analysis_invalid_res, code = E0999)]
3187 pub(super) struct InvalidRes {
3188 #[primary_span]
3189 pub span: Span,
3190 pub res_descr: &'static str,
3191 }
3192
3193 #[derive(Diagnostic)]
3194 #[diag(fhir_analysis_constant_annotation_needed, code = E0999)]
3195 pub(super) struct ConstantAnnotationNeeded {
3196 #[primary_span]
3197 #[label]
3198 span: Span,
3199 }
3200 impl ConstantAnnotationNeeded {
3201 pub(super) fn new(span: Span) -> Self {
3202 Self { span }
3203 }
3204 }
3205}