flux_middle/
builtin_assoc_refts.rs

1use std::sync::OnceLock;
2
3use flux_arc_interner::List;
4use flux_common::bug;
5use flux_syntax::symbols::sym;
6use rustc_data_structures::unord::UnordMap;
7use rustc_hir::{LangItem, def_id::DefId};
8use rustc_span::DUMMY_SP;
9
10use crate::{
11    def_id::FluxDefId,
12    global_env::GlobalEnv,
13    rty::{self, AliasReft, AssocRefinements, AssocReft, BaseTy},
14};
15
16impl<'tcx> GlobalEnv<'_, 'tcx> {
17    #[allow(
18        clippy::disallowed_methods,
19        reason = "this file is the source of truth for builtin assoc refts def ids"
20    )]
21    pub fn builtin_assoc_refts(self, def_id: DefId) -> Option<AssocRefinements> {
22        static BUILTIN: OnceLock<UnordMap<DefId, AssocRefinements>> = OnceLock::new();
23
24        BUILTIN
25            .get_or_init(|| {
26                let tcx = self.tcx();
27
28                let mut map = UnordMap::default();
29
30                // FnOnce
31                let fn_once_id = tcx.require_lang_item(LangItem::FnOnce, DUMMY_SP);
32                map.insert(
33                    fn_once_id,
34                    AssocRefinements {
35                        items: List::from_arr([AssocReft::new(
36                            FluxDefId::new(fn_once_id, sym::no_panic),
37                            false,
38                            tcx.def_span(fn_once_id),
39                        )]),
40                    },
41                );
42
43                // Sized
44                let sized_id = tcx.require_lang_item(LangItem::Sized, DUMMY_SP);
45                map.insert(
46                    sized_id,
47                    AssocRefinements {
48                        items: List::from_arr([AssocReft::new(
49                            FluxDefId::new(def_id, sym::size_of),
50                            false,
51                            tcx.def_span(sized_id),
52                        )]),
53                    },
54                );
55                map
56            })
57            .get(&def_id)
58            .cloned()
59    }
60
61    #[allow(
62        clippy::disallowed_methods,
63        reason = "this file is the source of truth for builtin assoc refts def ids"
64    )]
65    pub fn builtin_assoc_reft_sort(
66        self,
67        assoc_id: FluxDefId,
68    ) -> Option<rty::EarlyBinder<rty::FuncSort>> {
69        static BUILTIN: OnceLock<UnordMap<FluxDefId, rty::FuncSort>> = OnceLock::new();
70
71        BUILTIN
72            .get_or_init(|| {
73                let tcx = self.tcx();
74
75                let mut map = UnordMap::default();
76
77                // FnOnce
78                let fn_once_id = tcx.require_lang_item(LangItem::FnOnce, DUMMY_SP);
79                map.insert(
80                    FluxDefId::new(fn_once_id, sym::no_panic),
81                    rty::FuncSort::new(vec![], rty::Sort::Bool),
82                );
83
84                // Sized
85                let sized_id = tcx.require_lang_item(LangItem::Sized, DUMMY_SP);
86                map.insert(
87                    FluxDefId::new(sized_id, sym::size_of),
88                    rty::FuncSort::new(vec![], rty::Sort::Int),
89                );
90                map
91            })
92            .get(&assoc_id)
93            .cloned()
94            .map(rty::EarlyBinder)
95    }
96
97    pub fn builtin_assoc_reft_body(
98        self,
99        typing_env: rustc_middle::ty::TypingEnv<'tcx>,
100        alias_reft: &AliasReft,
101    ) -> rty::Lambda {
102        let tcx = self.tcx();
103
104        if tcx.is_lang_item(alias_reft.assoc_id.parent(), LangItem::Sized)
105            && alias_reft.assoc_id.name() == sym::size_of
106        {
107            let self_ty = alias_reft.to_rustc_trait_ref(tcx).self_ty();
108            let size = tcx
109                .layout_of(typing_env.as_query_input(self_ty))
110                .unwrap()
111                .size
112                .bytes();
113            let body = rty::Expr::constant(rty::Constant::from(size));
114            rty::Lambda::bind_with_vars(body, List::empty(), rty::Sort::Int)
115        } else if tcx.is_lang_item(alias_reft.assoc_id.parent(), LangItem::FnOnce)
116            && alias_reft.assoc_id.name() == sym::no_panic
117        {
118            let self_ty = alias_reft.self_ty();
119            let body = match self_ty.as_bty_skipping_binder() {
120                BaseTy::Closure(_, _, _, no_panic) => {
121                    if *no_panic {
122                        rty::Expr::tt()
123                    } else {
124                        rty::Expr::ff()
125                    }
126                }
127                _ => rty::Expr::ff(),
128            };
129            rty::Lambda::bind_with_vars(body, List::empty(), rty::Sort::Bool)
130        } else {
131            bug!("invalid builtin assoc reft {:?}", alias_reft.assoc_id)
132        }
133    }
134}
flux_middle/builtin_assoc_refts.rs

flux_middle/
builtin_assoc_refts.rs
