1#![feature(rustc_private)]
2
3extern crate rustc_abi;
4extern crate rustc_ast;
5extern crate rustc_data_structures;
6extern crate rustc_errors;
7extern crate rustc_hir;
8extern crate rustc_index;
9extern crate rustc_infer;
10extern crate rustc_middle;
11extern crate rustc_span;
12extern crate rustc_trait_selection;
13extern crate rustc_type_ir;
14
15mod conv;
16mod wf;
17use std::{iter, rc::Rc};
18
19use conv::{AfterSortck, ConvPhase, struct_compat};
20use flux_common::{
21 bug, dbg,
22 iter::IterExt,
23 result::{ErrorEmitter as _, ResultExt},
24};
25use flux_config as config;
26use flux_errors::Errors;
27use flux_middle::{
28 def_id::{FluxDefId, FluxId, MaybeExternId},
29 fhir::{
30 self, ForeignItem, ForeignItemKind, ImplItem, ImplItemKind, Item, ItemKind, TraitItem,
31 TraitItemKind, visit::Visitor as _,
32 },
33 global_env::GlobalEnv,
34 queries::{Providers, QueryErr, QueryResult},
35 query_bug,
36 rty::{
37 self, AssocReft, Binder, WfckResults,
38 fold::TypeFoldable,
39 refining::{self, Refiner},
40 },
41};
42use flux_rustc_bridge::lowering::Lower;
43use itertools::Itertools;
44use rustc_abi::FIRST_VARIANT;
45use rustc_data_structures::unord::{UnordMap, UnordSet};
46use rustc_errors::ErrorGuaranteed;
47use rustc_hir::{
48 OwnerId,
49 def::{CtorOf, DefKind},
50 def_id::{DefId, LocalDefId},
51};
52use rustc_span::Span;
53
54pub fn provide(providers: &mut Providers) {
55 providers.spec_funcs = spec_funcs;
56 providers.func_sort = func_sort;
57 providers.func_span = flux_def_ident_span;
58 providers.qualifiers = qualifiers;
59 providers.prim_rel = prim_rel;
60 providers.adt_sort_def_of = adt_sort_def_of;
61 providers.check_wf = check_wf;
62 providers.late_bound_refinement_params = late_bound_refinement_params;
63 providers.adt_def = adt_def;
64 providers.invariants_of = invariants_of;
65 providers.constant_info = constant_info;
66 providers.static_info = static_info;
67 providers.type_of = type_of;
68 providers.variants_of = variants_of;
69 providers.fn_sig = fn_sig;
70 providers.generics_of = generics_of;
71 providers.refinement_generics_of = refinement_generics_of;
72 providers.predicates_of = predicates_of;
73 providers.assoc_refinements_of = assoc_refinements_of;
74 providers.sort_of_assoc_reft = sort_of_assoc_reft;
75 providers.assoc_refinement_body = assoc_refinement_body;
76 providers.default_assoc_refinement_body = default_assoc_refinement_body;
77 providers.item_bounds = item_bounds;
78 providers.sort_decl_param_count = sort_decl_param_count;
79}
80
81fn sort_decl_param_count(genv: GlobalEnv, def_id: FluxId<MaybeExternId>) -> usize {
82 genv.fhir_sort_decl(def_id.local_id()).unwrap().params
83}
84
85fn adt_sort_def_of(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::AdtSortDef> {
86 let kind = genv.fhir_expect_refinement_kind(def_id.local_id())?;
87 conv::conv_adt_sort_def(genv, def_id, kind)
88}
89
90fn func_sort(genv: GlobalEnv, def_id: FluxId<MaybeExternId>) -> rty::PolyFuncSort {
91 let func = genv.fhir_spec_func_body(def_id.local_id()).unwrap();
92 match conv::conv_func_decl(genv, func).emit(&genv) {
93 Ok(normalized) => normalized,
94 Err(err) => {
95 genv.sess().abort(err);
96 }
97 }
98}
99
100fn flux_def_ident_span(genv: GlobalEnv, def_id: FluxId<MaybeExternId>) -> Span {
101 genv.fhir_spec_func_body(def_id.local_id())
102 .unwrap()
103 .ident_span
104}
105
106fn spec_funcs(genv: GlobalEnv) -> rty::SpecFuncs {
107 match try_spec_funcs(genv) {
108 Ok(funcs) => funcs,
109 Err(err) => {
110 genv.sess().abort(err);
111 }
112 }
113}
114
115fn try_spec_funcs(genv: GlobalEnv) -> Result<rty::SpecFuncs, ErrorGuaranteed> {
116 let mut funcs = vec![];
117
118 let mut errors = Errors::new(genv.sess());
120 for (_, item) in genv.fhir_iter_flux_items() {
121 let fhir::FluxItem::Func(func) = item else { continue };
122 let Some(wfckresults) = wf::check_flux_item(genv, item).collect_err(&mut errors) else {
123 continue;
124 };
125 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
126 let Ok(spec_func) = cx.conv_spec_func(func).emit(&errors) else { continue };
127 funcs.push((func.def_id, spec_func));
128 }
129 errors.to_result()?;
130
131 rty::SpecFuncs::new(funcs)
132 .map_err(|cycle| {
133 let span = genv
134 .fhir_spec_func_body(cycle[0])
135 .unwrap()
136 .body
137 .unwrap()
138 .span;
139 errors::DefinitionCycle::new(span, cycle)
140 })
141 .emit(&genv)
142}
143
144fn qualifiers(genv: GlobalEnv) -> QueryResult<Vec<rty::Qualifier>> {
145 genv.fhir_qualifiers()
146 .map(|qualifier| {
147 let wfckresults = wf::check_flux_item(genv, fhir::FluxItem::Qualifier(qualifier))?;
148 Ok(AfterSortck::new(genv, &wfckresults)
149 .into_conv_ctxt()
150 .conv_qualifier(qualifier)?
151 .reduce(genv))
152 })
153 .try_collect()
154}
155
156fn primop_props(genv: GlobalEnv) -> QueryResult<Vec<rty::PrimOpProp>> {
157 genv.fhir_primop_props()
158 .map(|primop_prop| {
159 let wfckresults = wf::check_flux_item(genv, fhir::FluxItem::PrimOpProp(primop_prop))?;
160 Ok(AfterSortck::new(genv, &wfckresults)
161 .into_conv_ctxt()
162 .conv_primop_prop(primop_prop)?
163 .reduce(genv))
164 })
165 .try_collect()
166}
167
168fn conjoin_bind_exprs(exprs: Vec<Binder<rty::Expr>>) -> Binder<rty::Expr> {
169 let mut iter = exprs.into_iter();
170 let first = iter.next().unwrap();
171 let sorts = first.sorts();
172 let bodies = iter::once(first.skip_binder()).chain(iter.map(|expr| expr.skip_binder()));
173 let expr = rty::Expr::and_from_iter(bodies);
174 Binder::bind_with_sorts(expr, &sorts)
175}
176
177fn prim_rel(genv: GlobalEnv) -> QueryResult<UnordMap<rty::BinOp, rty::PrimRel>> {
178 let primop_props = primop_props(genv)?
179 .into_iter()
180 .into_group_map_by(|primop_prop| primop_prop.op.clone());
181
182 let mut res = UnordMap::default();
183 for (op, props) in primop_props {
184 let exprs = props
185 .iter()
186 .map(|prop| prop.body.clone())
187 .collect::<Vec<_>>();
188 let body = conjoin_bind_exprs(exprs);
189 res.insert(op, rty::PrimRel { body });
190 }
191 Ok(res)
192}
193
194fn adt_def(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::AdtDef> {
195 let item = genv.fhir_expect_item(def_id.local_id())?;
196
197 let adt_def = genv.tcx().adt_def(def_id.resolved_id()).lower(genv.tcx());
198
199 let is_opaque = matches!(item.kind, fhir::ItemKind::Struct(def) if def.is_opaque());
200
201 Ok(rty::AdtDef::new(adt_def, genv.adt_sort_def_of(def_id)?, is_opaque))
202}
203
204fn constant_info(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::ConstantInfo> {
205 let node = genv.fhir_node(def_id.local_id())?;
206 let Some(sort) = genv.sort_of_def_id(def_id.resolved_id()).emit(&genv)? else {
207 return Ok(rty::ConstantInfo::Uninterpreted);
208 };
209 let tcx = genv.tcx();
210 match node {
211 fhir::Node::Item(fhir::Item { kind: fhir::ItemKind::Const(Some(expr)), .. }) => {
212 let owner = def_id.map(|def_id| rustc_hir::OwnerId { def_id });
214 let wfckresults = wf::check_constant_expr(genv, owner, expr, &sort)?;
215 let expr = AfterSortck::new(genv, &wfckresults)
216 .into_conv_ctxt()
217 .conv_constant_expr(expr)?;
218 Ok(rty::ConstantInfo::Interpreted(expr, sort))
219 }
220 fhir::Node::Item(fhir::Item { kind: fhir::ItemKind::Const(None), .. })
221 | fhir::Node::AnonConst
222 | fhir::Node::ImplItem(fhir::ImplItem { kind: fhir::ImplItemKind::Const, .. }) => {
223 if let Some(ty) = tcx.type_of(def_id).no_bound_vars()
225 && ty.is_integral()
226 && let Ok(val) = tcx.const_eval_poly(def_id.resolved_id())
227 && let Some(val) = val.try_to_scalar_int()
228 && let Some(constant_) = rty::Constant::from_scalar_int(tcx, val, &ty)
229 {
230 Ok(rty::ConstantInfo::Interpreted(rty::Expr::constant(constant_), rty::Sort::Int))
233 } else {
234 Ok(rty::ConstantInfo::Uninterpreted)
235 }
236 }
237 fhir::Node::TraitItem(fhir::TraitItem { kind: fhir::TraitItemKind::Const, .. }) => {
238 Ok(rty::ConstantInfo::Uninterpreted)
239 }
240 _ => Err(query_bug!(def_id.local_id(), "expected const item"))?,
241 }
242}
243
244fn static_info(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::Ty> {
246 if let fhir::Node::Item(fhir::Item { kind: fhir::ItemKind::Static(Some(ty)), .. }) =
247 genv.fhir_node(def_id.local_id())?
248 {
249 let wfckresults = genv.check_wf(def_id.local_id())?;
250 AfterSortck::new(genv, &wfckresults)
251 .into_conv_ctxt()
252 .conv_static_ty(ty)
253 } else {
254 rty::refining::default_static_ty(genv, def_id.resolved_id())
255 }
256}
257
258fn invariants_of(
262 genv: GlobalEnv,
263 def_id: MaybeExternId,
264) -> rty::EarlyBinder<rty::List<rty::Invariant>> {
265 let invariants = try_invariants_of(genv, def_id).unwrap_or_else(|err| {
266 if !matches!(err, QueryErr::Emitted(_)) {
267 genv.emit(err);
268 }
269 vec![]
270 });
271 rty::EarlyBinder(rty::List::from_vec(invariants))
272}
273
274fn try_invariants_of(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<Vec<rty::Invariant>> {
275 let item = genv.fhir_expect_item(def_id.local_id())?;
276 let (params, invariants) = match &item.kind {
277 fhir::ItemKind::Enum(enum_def) => (enum_def.params, enum_def.invariants),
278 fhir::ItemKind::Struct(struct_def) => (struct_def.params, struct_def.invariants),
279 _ => Err(query_bug!(item.owner_id.local_id(), "expected struct or enum"))?,
280 };
281 let wfckresults = wf::check_invariants(genv, item.owner_id, params, invariants)?;
282 AfterSortck::new(genv, &wfckresults)
283 .into_conv_ctxt()
284 .conv_invariants(item.owner_id.map(|it| it.def_id), params, invariants)
285}
286
287fn predicates_of(
288 genv: GlobalEnv,
289 def_id: MaybeExternId,
290) -> QueryResult<rty::EarlyBinder<rty::GenericPredicates>> {
291 match genv.def_kind(def_id) {
292 DefKind::Impl { .. }
293 | DefKind::Struct
294 | DefKind::Enum
295 | DefKind::Union
296 | DefKind::TyAlias
297 | DefKind::AssocFn
298 | DefKind::AssocTy
299 | DefKind::Trait
300 | DefKind::Fn => {
301 let did = def_id.local_id();
302 let generics = genv
303 .fhir_get_generics(did)?
304 .ok_or_else(|| query_bug!(did, "no generics for {def_id:?}"))?;
305 let wfckresults = genv.check_wf(did)?;
306 AfterSortck::new(genv, &wfckresults)
307 .into_conv_ctxt()
308 .conv_generic_predicates(def_id, generics)
309 }
310 DefKind::OpaqueTy | DefKind::Closure | DefKind::Static { .. } => {
311 Ok(rty::EarlyBinder(rty::GenericPredicates {
312 parent: genv.tcx().clauses_of(def_id).parent,
313 predicates: rty::List::empty(),
314 }))
315 }
316 kind => {
317 Err(query_bug!(
318 def_id.local_id(),
319 "predicates_of called on `{def_id:?}` with kind `{kind:?}`"
320 ))?
321 }
322 }
323}
324
325fn assoc_refinements_of(
326 genv: GlobalEnv,
327 def_id: MaybeExternId,
328) -> QueryResult<rty::AssocRefinements> {
329 #[allow(
330 clippy::disallowed_methods,
331 reason = "We are iterationg over associated refinemens in fhir, so this is the *source of of truth*"
332 )]
333 let predicates = match &genv.fhir_expect_item(def_id.local_id())?.kind {
334 fhir::ItemKind::Trait(trait_) => {
335 trait_
336 .assoc_refinements
337 .iter()
338 .map(|assoc_reft| {
339 AssocReft::new(
340 FluxDefId::new(def_id.resolved_id(), assoc_reft.name),
341 assoc_reft.final_,
342 assoc_reft.span,
343 )
344 })
345 .collect()
346 }
347 fhir::ItemKind::Impl(impl_) => {
348 impl_
349 .assoc_refinements
350 .iter()
351 .map(|assoc_reft| {
352 AssocReft::new(
353 FluxDefId::new(def_id.resolved_id(), assoc_reft.name),
354 false,
355 assoc_reft.span,
356 )
357 })
358 .collect()
359 }
360 _ => Err(query_bug!(def_id.resolved_id(), "expected trait or impl"))?,
361 };
362 Ok(rty::AssocRefinements { items: predicates })
363}
364
365fn default_assoc_refinement_body(
366 genv: GlobalEnv,
367 trait_assoc_id: FluxId<MaybeExternId>,
368) -> QueryResult<Option<rty::EarlyBinder<rty::Lambda>>> {
369 let trait_id = trait_assoc_id.parent();
370 let assoc_reft = genv
371 .fhir_expect_item(trait_id.local_id())?
372 .expect_trait()
373 .find_assoc_reft(trait_assoc_id.name())
374 .unwrap();
375 let Some(body) = assoc_reft.body else { return Ok(None) };
376 let wfckresults = genv.check_wf(trait_id.local_id())?;
377 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
378 let body = cx.conv_assoc_reft_body(assoc_reft.params, &body, &assoc_reft.output)?;
379 Ok(Some(rty::EarlyBinder(body)))
380}
381
382fn assoc_refinement_body(
383 genv: GlobalEnv,
384 impl_assoc_id: FluxId<MaybeExternId>,
385) -> QueryResult<rty::EarlyBinder<rty::Lambda>> {
386 let impl_id = impl_assoc_id.parent();
387
388 let assoc_reft = genv
389 .fhir_expect_item(impl_id.local_id())?
390 .expect_impl()
391 .find_assoc_reft(impl_assoc_id.name())
392 .unwrap();
393
394 let wfckresults = genv.check_wf(impl_id.local_id())?;
395 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
396 let body = cx.conv_assoc_reft_body(assoc_reft.params, &assoc_reft.body, &assoc_reft.output)?;
397 Ok(rty::EarlyBinder(body))
398}
399
400fn sort_of_assoc_reft(
401 genv: GlobalEnv,
402 assoc_id: FluxId<MaybeExternId>,
403) -> QueryResult<rty::EarlyBinder<rty::FuncSort>> {
404 let container_id = assoc_id.parent();
405
406 match &genv.fhir_expect_item(container_id.local_id())?.kind {
407 fhir::ItemKind::Trait(trait_) => {
408 let assoc_reft = trait_.find_assoc_reft(assoc_id.name()).unwrap();
409 let wfckresults = WfckResults::new(container_id.map(|def_id| OwnerId { def_id }));
410 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
411 let inputs = assoc_reft
412 .params
413 .iter()
414 .map(|p| cx.conv_sort(&p.sort))
415 .try_collect_vec()?;
416 let output = cx.conv_sort(&assoc_reft.output)?;
417 Ok(rty::EarlyBinder(rty::FuncSort::new(inputs, output)))
418 }
419 fhir::ItemKind::Impl(impl_) => {
420 let assoc_reft = impl_.find_assoc_reft(assoc_id.name()).unwrap();
421 let wfckresults = WfckResults::new(container_id.map(|def_id| OwnerId { def_id }));
422 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
423 let inputs = assoc_reft
424 .params
425 .iter()
426 .map(|p| cx.conv_sort(&p.sort))
427 .try_collect_vec()?;
428 let output = cx.conv_sort(&assoc_reft.output)?;
429 Ok(rty::EarlyBinder(rty::FuncSort::new(inputs, output)))
430 }
431 _ => Err(query_bug!(container_id.local_id(), "expected trait or impl")),
432 }
433}
434
435fn item_bounds(
436 genv: GlobalEnv,
437 def_id: MaybeExternId,
438) -> QueryResult<rty::EarlyBinder<rty::Clauses>> {
439 let parent = genv.tcx().local_parent(def_id.local_id());
440 let wfckresults = genv.check_wf(parent)?;
441 let opaque_ty = genv.fhir_node(def_id.local_id())?.expect_opaque_ty();
442 Ok(rty::EarlyBinder(
443 AfterSortck::new(genv, &wfckresults)
444 .into_conv_ctxt()
445 .conv_opaque_ty(opaque_ty)?,
446 ))
447}
448
449fn generics_of(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::Generics> {
450 let def_kind = genv.def_kind(def_id);
451 let generics = match def_kind {
452 DefKind::Impl { .. }
453 | DefKind::Struct
454 | DefKind::Enum
455 | DefKind::Union
456 | DefKind::TyAlias
457 | DefKind::AssocFn
458 | DefKind::AssocTy
459 | DefKind::Trait
460 | DefKind::Fn => {
461 let is_trait = def_kind == DefKind::Trait;
462 let generics = genv
463 .fhir_get_generics(def_id.local_id())?
464 .ok_or_else(|| query_bug!(def_id.local_id(), "no generics for {def_id:?}"))?;
465 conv::conv_generics(genv, generics, def_id, is_trait)
466 }
467 DefKind::OpaqueTy
468 | DefKind::Closure
469 | DefKind::TraitAlias
470 | DefKind::Ctor(..)
471 | DefKind::Static { .. } => refining::refine_generics(&genv.lower_generics_of(def_id)),
472 kind => {
473 Err(query_bug!(
474 def_id.local_id(),
475 "generics_of called on `{def_id:?}` with kind `{kind:?}`"
476 ))?
477 }
478 };
479 if config::dump_rty() {
480 dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), "generics.rty", &generics).unwrap();
481 }
482 Ok(generics)
483}
484
485fn late_bound_refinement_params<'genv>(
487 genv: GlobalEnv<'genv, '_>,
488 def_id: LocalDefId,
489) -> QueryResult<&'genv [fhir::ParamId]> {
490 let node = genv.fhir_expect_owner_node(def_id)?;
491 let Some(fn_sig) = node.fn_sig() else { return Ok(&[]) };
492 let generics = node.generics();
493
494 let mut appears_in_clauses = ParamCollector::default();
497 for pred in generics.predicates.unwrap_or_default() {
498 appears_in_clauses.visit_where_predicate(pred);
499 }
500 OpaqueTyParamCollector(&mut appears_in_clauses).visit_fn_sig(fn_sig);
501
502 let late_bound = generics
503 .refinement_params
504 .iter()
505 .filter(|param| !param.kind.is_loc() && !matches!(param.sort, fhir::Sort::Loc))
507 .filter(|param| !appears_in_clauses.params.contains(¶m.id))
508 .map(|param| param.id)
509 .collect_vec();
510 Ok(genv.alloc_slice(&late_bound))
511}
512
513#[derive(Default)]
515struct ParamCollector {
516 params: UnordSet<fhir::ParamId>,
517}
518
519impl<'fhir> fhir::visit::Visitor<'fhir> for ParamCollector {
520 fn visit_path_expr(&mut self, path: &fhir::PathExpr<'fhir>) {
521 if let fhir::Res::Param(_, id) = path.res {
522 self.params.insert(id);
523 }
524 }
525}
526
527struct OpaqueTyParamCollector<'a>(&'a mut ParamCollector);
529
530impl<'fhir> fhir::visit::Visitor<'fhir> for OpaqueTyParamCollector<'_> {
531 fn visit_opaque_ty(&mut self, opaque_ty: &fhir::OpaqueTy<'fhir>) {
532 self.0.visit_opaque_ty(opaque_ty);
533 }
534}
535
536fn refinement_generics_of(
537 genv: GlobalEnv,
538 def_id: MaybeExternId,
539) -> QueryResult<rty::EarlyBinder<rty::RefinementGenerics>> {
540 let parent = genv.tcx().generics_of(def_id).parent;
541 let parent_count =
542 if let Some(def_id) = parent { genv.refinement_generics_of(def_id)?.count() } else { 0 };
543 let generics = match genv.fhir_node(def_id.local_id())? {
544 fhir::Node::Item(fhir::Item {
545 kind: fhir::ItemKind::Fn(..) | fhir::ItemKind::TyAlias(..),
546 ..
547 })
548 | fhir::Node::TraitItem(fhir::TraitItem { kind: fhir::TraitItemKind::Fn(..), .. })
549 | fhir::Node::ImplItem(fhir::ImplItem { kind: fhir::ImplItemKind::Fn(..), .. })
550 | fhir::Node::ForeignItem(fhir::ForeignItem {
551 kind: fhir::ForeignItemKind::Fn(..), ..
552 }) => {
553 let wfckresults = genv.check_wf(def_id.local_id())?;
554 let (early, _) = genv.fhir_split_refinement_params(def_id.local_id())?;
555 let params = conv::conv_refinement_generics(&early, &wfckresults)?;
556 rty::RefinementGenerics { parent, parent_count, own_params: params }
557 }
558 _ => rty::RefinementGenerics { parent, parent_count, own_params: rty::List::empty() },
559 };
560 Ok(rty::EarlyBinder(generics))
561}
562
563fn type_of(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::EarlyBinder<rty::TyOrCtor>> {
564 let ty = match genv.def_kind(def_id) {
565 DefKind::TyAlias => {
566 let fhir_ty_alias = genv
567 .fhir_expect_item(def_id.local_id())?
568 .expect_type_alias();
569 let wfckresults = genv.check_wf(def_id.local_id())?;
570 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
571 let ty_alias = cx.conv_type_alias(def_id, fhir_ty_alias)?;
572 struct_compat::type_alias(genv, fhir_ty_alias, &ty_alias, def_id)?;
573 rty::TyOrCtor::Ctor(ty_alias)
574 }
575 DefKind::TyParam => {
576 match def_id {
577 MaybeExternId::Local(local_id) => {
578 let owner = genv.tcx().hir_ty_param_owner(local_id);
579 let param = genv.fhir_get_generics(owner)?.unwrap().get_param(local_id);
580 match param.kind {
581 fhir::GenericParamKind::Type { default: Some(ty) } => {
582 let parent = genv.tcx().local_parent(local_id);
583 let wfckresults = genv.check_wf(parent)?;
584 conv::conv_default_type_parameter(genv, def_id, &ty, &wfckresults)?
585 .into()
586 }
587 k => Err(query_bug!(local_id, "non-type def def {k:?} {def_id:?}"))?,
588 }
589 }
590 MaybeExternId::Extern(_, extern_id) => {
591 let ty = genv.lower_type_of(extern_id)?.skip_binder();
592 Refiner::default_for_item(genv, ty_param_owner(genv, extern_id))?
593 .refine_ty_or_base(&ty)?
594 .into()
595 }
596 }
597 }
598 DefKind::Impl { .. } | DefKind::Struct | DefKind::Enum | DefKind::AssocTy => {
599 let ty = genv.lower_type_of(def_id)?.skip_binder();
600 Refiner::default_for_item(genv, def_id.resolved_id())?
601 .refine_ty_or_base(&ty)?
602 .into()
603 }
604 kind => {
605 Err(query_bug!(
606 def_id.local_id(),
607 "`{:?}` not supported",
608 kind.descr(def_id.resolved_id())
609 ))?
610 }
611 };
612 Ok(rty::EarlyBinder(ty))
613}
614
615fn ty_param_owner(genv: GlobalEnv, def_id: DefId) -> DefId {
616 let def_kind = genv.def_kind(def_id);
617 match def_kind {
618 DefKind::Trait | DefKind::TraitAlias => def_id,
619 DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
620 genv.tcx().parent(def_id)
621 }
622 _ => bug!("ty_param_owner: {:?} is a {:?} not a type parameter", def_id, def_kind),
623 }
624}
625
626fn variants_of(
627 genv: GlobalEnv,
628 def_id: MaybeExternId,
629) -> QueryResult<rty::Opaqueness<rty::EarlyBinder<rty::PolyVariants>>> {
630 let local_id = def_id.local_id();
631
632 let item = &genv.fhir_expect_item(local_id)?;
633 let variants = match &item.kind {
634 fhir::ItemKind::Enum(enum_def) => {
635 let wfckresults = genv.check_wf(local_id)?;
636 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
637 let variants = cx.conv_enum_variants(def_id, enum_def)?;
638 let variants = rty::List::from_vec(struct_compat::variants(genv, &variants, def_id)?);
639 rty::Opaqueness::Transparent(rty::EarlyBinder(variants))
640 }
641 fhir::ItemKind::Struct(struct_def) => {
642 let wfckresults = genv.check_wf(local_id)?;
643 let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
644 cx.conv_struct_variant(def_id, struct_def)?
645 .map(|variant| -> QueryResult<_> {
646 let variants = struct_compat::variants(genv, &[variant], def_id)?;
647 Ok(rty::List::from_vec(variants))
648 })
649 .transpose()?
650 .map(rty::EarlyBinder)
651 }
652 _ => Err(query_bug!(def_id.local_id(), "expected struct or enum"))?,
653 };
654 if config::dump_rty() {
655 dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), "rty", &variants).unwrap();
656 }
657 Ok(variants)
658}
659
660fn fn_sig(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::EarlyBinder<rty::PolyFnSig>> {
661 let fhir_node = genv.fhir_node(def_id.local_id())?;
662 match &fhir_node {
663 fhir::Node::Item(Item { kind: ItemKind::Fn(fhir_fn_sig, ..), .. })
664 | fhir::Node::TraitItem(TraitItem { kind: TraitItemKind::Fn(fhir_fn_sig), .. })
665 | fhir::Node::ImplItem(ImplItem { kind: ImplItemKind::Fn(fhir_fn_sig), .. })
666 | fhir::Node::ForeignItem(ForeignItem {
667 kind: ForeignItemKind::Fn(fhir_fn_sig, ..), ..
668 }) => {
669 let wfckresults = genv.check_wf(def_id.local_id())?;
670 let fn_sig = AfterSortck::new(genv, &wfckresults)
671 .into_conv_ctxt()
672 .conv_fn_sig(def_id, fhir_fn_sig)?;
673 let fn_sig = struct_compat::fn_sig(genv, fhir_fn_sig.decl, &fn_sig, def_id)?;
674 #[cfg(feature = "suggestions")]
675 let mut fn_sig = fn_sig.hoist_input_binders();
676 #[cfg(feature = "suggestions")]
677 if !genv.no_suggestions(def_id.local_id())
684 && !matches!(fhir_node, fhir::Node::TraitItem(..) | fhir::Node::ForeignItem(..))
685 {
686 fn_sig = fn_sig.add_weak_kvars(genv, def_id.local_id().into())?;
687 }
688
689 if config::dump_rty() {
690 let generics = genv.generics_of(def_id)?;
691 let refinement_generics = genv.refinement_generics_of(def_id)?;
692 dbg::dump_item_info(
693 genv.tcx(),
694 def_id.resolved_id(),
695 "rty",
696 (generics, refinement_generics, &fn_sig),
697 )
698 .unwrap();
699 }
700 Ok(rty::EarlyBinder(fn_sig))
701 }
702 fhir::Node::Ctor => {
703 let tcx = genv.tcx();
704 let (adt_id, variant_idx) = match tcx.def_kind(def_id) {
705 DefKind::Ctor(CtorOf::Struct, _) => {
706 let struct_id = tcx.parent(def_id.resolved_id());
707 (struct_id, FIRST_VARIANT)
708 }
709 DefKind::Ctor(CtorOf::Variant, _) => {
710 let variant_id = tcx.parent(def_id.resolved_id());
711 let enum_id = tcx.parent(variant_id);
712 let variant_idx = tcx.adt_def(enum_id).variant_index_with_id(variant_id);
713 (enum_id, variant_idx)
714 }
715 _ => return Err(query_bug!("invalid `DefKind` for ctor node")),
716 };
717 genv.variant_sig(adt_id, variant_idx)?
718 .map(|sig| sig.to_poly_fn_sig(None))
719 .ok_or_query_err(adt_id)
720 }
721 node => Err(query_bug!("fn_sig called on unsupported node {node:?}")),
722 }
723}
724
725fn check_wf(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<Rc<WfckResults>> {
726 let node = genv.fhir_expect_owner_node(def_id)?;
727 let wfckresults = wf::check_node(genv, &node)?;
728 Ok(Rc::new(wfckresults))
729}
730
731mod errors {
732 use flux_errors::E0999;
733 use flux_macros::Diagnostic;
734 use flux_middle::def_id::FluxLocalDefId;
735 use rustc_span::Span;
736
737 #[derive(Diagnostic)]
738 #[diag("cycle in definitions", code = E0999)]
739 pub struct DefinitionCycle {
740 #[primary_span]
741 #[label("{$msg}")]
742 span: Span,
743 msg: String,
744 }
745
746 impl DefinitionCycle {
747 pub(super) fn new(span: Span, cycle: Vec<FluxLocalDefId>) -> Self {
748 let root = format!("`{}`", cycle[0].name());
749 let names: Vec<String> = cycle.iter().map(|s| format!("`{}`", s.name())).collect();
750 let msg = format!("{} -> {}", names.join(" -> "), root);
751 Self { span, msg }
752 }
753 }
754}