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

flux_middle/
sort_of.rs
