flux_middle/rty/
reduce.rs

1use super::{ESpan, fold::TypeSuperFoldable};
2use crate::{
3    def_id::FluxDefId,
4    global_env::GlobalEnv,
5    rty::{Expr, ExprKind, SortArg, SpecFunc, expr::SpecFuncKind, fold::TypeFolder},
6};
7
8pub(super) struct Reducer<'genv, 'tcx> {
9    genv: GlobalEnv<'genv, 'tcx>,
10}
11
12impl<'genv, 'tcx> Reducer<'genv, 'tcx> {
13    pub(super) fn new(genv: GlobalEnv<'genv, 'tcx>) -> Self {
14        Self { genv }
15    }
16
17    fn should_inline(&self, did: FluxDefId) -> bool {
18        matches!(self.genv.spec_func(did), SpecFunc::Defined { hide: false, .. })
19            && self.genv.should_inline_fun(did)
20    }
21
22    fn at_base(expr: Expr, espan: Option<ESpan>) -> Expr {
23        match espan {
24            Some(espan) => BaseSpanner::new(espan).fold_expr(&expr),
25            None => expr,
26        }
27    }
28
29    fn app(
30        &mut self,
31        func: &Expr,
32        sort_args: &[SortArg],
33        args: &[Expr],
34        espan: Option<ESpan>,
35    ) -> Expr {
36        match func.kind() {
37            ExprKind::GlobalFunc(SpecFuncKind::Def(did)) if self.should_inline(*did) => {
38                let res = self.genv.inlined_body(*did).replace_bound_refts(args);
39                Self::at_base(res, espan)
40            }
41            ExprKind::Abs(lam) => {
42                let res = lam.apply(args);
43                Self::at_base(res, espan)
44            }
45            _ => Expr::app(func.clone(), sort_args.into(), args.into()).at_opt(espan),
46        }
47    }
48}
49
50impl TypeFolder for Reducer<'_, '_> {
51    fn fold_expr(&mut self, expr: &Expr) -> Expr {
52        let expr = expr.super_fold_with(self);
53        let span = expr.span();
54        match expr.kind() {
55            ExprKind::App(func, sorts, args) => self.app(func, sorts, args, span),
56            ExprKind::FieldProj(e, proj) => e.proj_and_reduce(*proj),
57            _ => expr,
58        }
59    }
60}
61
62struct BaseSpanner {
63    espan: ESpan,
64}
65
66impl BaseSpanner {
67    fn new(espan: ESpan) -> Self {
68        Self { espan }
69    }
70}
71
72impl TypeFolder for BaseSpanner {
73    fn fold_expr(&mut self, expr: &Expr) -> Expr {
74        expr.super_fold_with(self).at_base(self.espan)
75    }
76}
flux_middle/rty/reduce.rs

flux_middle/rty/
reduce.rs
