flux_middle/
sort_of.rs

1use flux_arc_interner::List;
2use flux_common::tracked_span_bug;
3use rustc_hir::def::DefKind;
4use rustc_span::def_id::DefId;
5
6use crate::{global_env::GlobalEnv, queries::QueryResult, query_bug, rty};
7
8impl GlobalEnv<'_, '_> {
9    pub fn sort_of_self_ty_alias(self, alias_to: DefId) -> QueryResult<Option<rty::Sort>> {
10        let self_ty = self.tcx().type_of(alias_to).instantiate_identity();
11        self.sort_of_rust_ty(alias_to, self_ty)
12    }
13
14    pub fn sort_of_def_id(self, def_id: DefId) -> QueryResult<Option<rty::Sort>> {
15        if let Some(ty) = self.tcx().type_of(def_id).no_bound_vars() {
16            self.sort_of_rust_ty(def_id, ty)
17        } else {
18            Ok(None)
19        }
20    }
21
22    fn sort_of_rust_ty(
23        self,
24        def_id: DefId,
25        ty: rustc_middle::ty::Ty,
26    ) -> QueryResult<Option<rty::Sort>> {
27        use rustc_middle::ty;
28        let sort = match ty.kind() {
29            ty::TyKind::Bool => Some(rty::Sort::Bool),
30            ty::TyKind::Slice(_) | ty::TyKind::Int(_) | ty::TyKind::Uint(_) => Some(rty::Sort::Int),
31            ty::TyKind::Char => Some(rty::Sort::Char),
32            ty::TyKind::Str => Some(rty::Sort::Str),
33            ty::TyKind::Adt(adt_def, args) => {
34                let mut sort_args = vec![];
35                let sort_def = self.adt_sort_def_of(adt_def.did())?;
36                for arg in sort_def.filter_generic_args(args) {
37                    let Some(sort) = self.sort_of_rust_ty(def_id, arg.expect_ty())? else {
38                        return Ok(None);
39                    };
40                    sort_args.push(sort);
41                }
42                let ctor = rty::SortCtor::Adt(self.adt_sort_def_of(adt_def.did())?);
43                Some(rty::Sort::App(ctor, List::from_vec(sort_args)))
44            }
45            ty::TyKind::Param(p) => {
46                let param_def = self.generics_of(def_id)?.param_at(p.index as usize, self)?;
47                if let rty::GenericParamDefKind::Base { .. } = param_def.kind {
48                    Some(rty::Sort::Param(*p))
49                } else {
50                    None
51                }
52            }
53            ty::TyKind::Float(_)
54            | ty::TyKind::RawPtr(..)
55            | ty::TyKind::Ref(..)
56            | ty::TyKind::Tuple(_)
57            | ty::TyKind::Array(..)
58            | ty::TyKind::Alias(..)
59            | ty::TyKind::Never => Some(rty::Sort::unit()),
60            _ => None,
61        };
62        Ok(sort)
63    }
64
65    pub fn normalize_free_alias_sort(self, alias_ty: &rty::AliasTy) -> QueryResult<rty::Sort> {
66        match self.def_kind(alias_ty.def_id) {
67            DefKind::Impl { .. } => Ok(self.sort_of_self_ty_alias(alias_ty.def_id)?.unwrap()),
68            DefKind::TyAlias => {
69                Ok(self
70                    .type_of(alias_ty.def_id)?
71                    .instantiate(self.tcx(), &alias_ty.args, &alias_ty.refine_args)
72                    .expect_ctor()
73                    .sort())
74            }
75            DefKind::Struct | DefKind::Enum => {
76                Ok(self
77                    .adt_sort_def_of(alias_ty.def_id)?
78                    .to_sort(&alias_ty.args))
79            }
80            _ => Err(query_bug!(alias_ty.def_id, "unexpected weak alias `{:?}`", alias_ty.def_id)),
81        }
82    }
83}
84
85impl rty::BaseTy {
86    pub fn sort(&self) -> rty::Sort {
87        match self {
88            rty::BaseTy::Int(_) | rty::BaseTy::Uint(_) | rty::BaseTy::Slice(_) => rty::Sort::Int,
89            rty::BaseTy::Bool => rty::Sort::Bool,
90            rty::BaseTy::Char => rty::Sort::Char,
91            rty::BaseTy::Adt(adt_def, args) => adt_def.sort(args),
92            rty::BaseTy::Param(param_ty) => rty::Sort::Param(*param_ty),
93            rty::BaseTy::Str => rty::Sort::Str,
94            rty::BaseTy::Alias(kind, alias_ty) => {
95                // HACK(nilehmann) The refinement arguments in `alias_ty` should not influence the
96                // sort. However, we must explicitly remove them because they can contain expression
97                // holes. If we don't remove them, we would generate inference variables for them
98                // which we won't be able to solve.
99                let alias_ty =
100                    rty::AliasTy::new(alias_ty.def_id, alias_ty.args.clone(), List::empty());
101                rty::Sort::Alias(*kind, alias_ty)
102            }
103            rty::BaseTy::Float(_)
104            | rty::BaseTy::RawPtr(..)
105            | rty::BaseTy::RawPtrMetadata(..) // TODO(RJ): This should be `int` for slice?
106            | rty::BaseTy::Ref(..)
107            | rty::BaseTy::FnPtr(..)
108            | rty::BaseTy::FnDef(..)
109            | rty::BaseTy::Tuple(_)
110            | rty::BaseTy::Array(_, _)
111            | rty::BaseTy::Closure(..)
112            | rty::BaseTy::Coroutine(..)
113            | rty::BaseTy::Dynamic(_, _)
114            | rty::BaseTy::Never
115            | rty::BaseTy::Foreign(..) => rty::Sort::unit(),
116            rty::BaseTy::Infer(_) => tracked_span_bug!(),
117        }
118    }
119}
120
121impl rty::AliasReft {
122    pub fn fsort(&self, genv: GlobalEnv) -> QueryResult<rty::FuncSort> {
123        Ok(genv
124            .sort_of_assoc_reft(self.assoc_id)?
125            .instantiate(genv.tcx(), &self.args, &[]))
126    }
127}
flux_middle/sort_of.rs

flux_middle/
sort_of.rs
