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

flux_middle/
sort_of.rs
