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