dada_ir_sym/check/env/
infer_bounds.rs

1use dada_util::FromImpls;
2use serde::Serialize;
3
4use crate::{
5    check::{
6        inference::{Direction, InferVarKind, InferenceVarData},
7        red::{RedPerm, RedTy},
8        report::ArcOrElse,
9    },
10    ir::{
11        indices::InferVarIndex,
12        types::{SymGenericTerm, SymPerm},
13    },
14};
15
16use super::Env;
17
18/// Iterates over bounds on an inference variable in a given permission context.
19/// Carries a permission that is applied to each bound as extract it.
20pub struct SymGenericTermBoundIterator<'db> {
21    /// The permission context in which this infer variable appears.
22    /// This permission will eb applied to the bounds we extract.
23    perm: SymPerm<'db>,
24
25    /// Remember the inference variable
26    infer: InferVarIndex,
27
28    /// A bounds iterator of suitable kind, depending on the kind of inference variable.
29    kind: SymGenericTermBoundIteratorKind<'db>,
30}
31
32#[derive(FromImpls)]
33enum SymGenericTermBoundIteratorKind<'db> {
34    Ty(RedTyBoundIterator<'db>),
35    Perm(RedPermBoundIterator<'db>),
36}
37
38impl<'db> SymGenericTermBoundIterator<'db> {
39    pub fn new(env: &Env<'db>, perm: SymPerm<'db>, infer: InferVarIndex) -> Self {
40        Self {
41            perm,
42            infer,
43            kind: match env.infer_var_kind(infer) {
44                InferVarKind::Type => RedTyBoundIterator::new(env, infer).into(),
45                InferVarKind::Perm => RedPermBoundIterator::new(env, infer).into(),
46            },
47        }
48    }
49
50    pub async fn next(&mut self, env: &Env<'db>) -> Option<(Direction, SymGenericTerm<'db>)> {
51        let db = env.db();
52        match &mut self.kind {
53            SymGenericTermBoundIteratorKind::Ty(iter) => {
54                let (direction, red_ty) = iter.next(env).await?;
55                let sym_ty = red_ty.into_sym_ty(db);
56                let result = self.perm.apply_to(db, sym_ty);
57                env.log(
58                    "next_bound",
59                    &[&self.infer, &InferVarKind::Type, &direction, &result],
60                );
61                Some((direction, result.into()))
62            }
63            SymGenericTermBoundIteratorKind::Perm(iter) => {
64                let (direction, red_perm) = iter.next(env).await?;
65                let sym_perm = red_perm.to_sym_perm(db);
66                let result = self.perm.apply_to(db, sym_perm);
67                env.log(
68                    "next_bound",
69                    &[&self.infer, &InferVarKind::Perm, &direction, &result],
70                );
71                Some((direction, result.into()))
72            }
73        }
74    }
75}
76
77/// Iterator over the red-ty bounds applied to `infer`
78/// that are coming from a given direction (above/below).
79pub struct RedTyBoundIterator<'db> {
80    infer: InferVarIndex,
81    storage: [Option<RedTy<'db>>; 2],
82}
83
84impl<'db> RedTyBoundIterator<'db> {
85    pub fn new(env: &Env<'db>, infer: InferVarIndex) -> Self {
86        assert_eq!(env.infer_var_kind(infer), InferVarKind::Type);
87        Self {
88            infer,
89            storage: [None, None],
90        }
91    }
92
93    #[track_caller]
94    pub fn next(
95        &mut self,
96        env: &Env<'db>,
97    ) -> impl Future<Output = Option<(Direction, RedTy<'db>)>> {
98        env.log("next", &[&self.infer]);
99        next_bound(
100            env,
101            self.infer,
102            InferenceVarData::red_ty_bound,
103            &mut self.storage,
104        )
105    }
106}
107
108/// Iterator over the red-perm bounds applied to `infer`
109/// that are coming from a given direction (above/below).
110pub struct RedPermBoundIterator<'db> {
111    infer: InferVarIndex,
112    storage: [Option<RedPerm<'db>>; 2],
113}
114
115impl<'db> RedPermBoundIterator<'db> {
116    pub fn new(env: &Env<'db>, infer: InferVarIndex) -> Self {
117        assert_eq!(env.infer_var_kind(infer), InferVarKind::Perm);
118        Self {
119            infer,
120            storage: [None, None],
121        }
122    }
123
124    #[track_caller]
125    pub fn next(
126        &mut self,
127        env: &Env<'db>,
128    ) -> impl Future<Output = Option<(Direction, RedPerm<'db>)>> {
129        env.log("next", &[&self.infer]);
130        next_bound(
131            env,
132            self.infer,
133            InferenceVarData::red_perm_bound,
134            &mut self.storage,
135        )
136    }
137}
138
139#[track_caller]
140fn next_bound<'db, B>(
141    env: &Env<'db>,
142    infer: InferVarIndex,
143    bound_op: impl Fn(&InferenceVarData<'db>, Direction) -> Option<(B, ArcOrElse<'db>)>,
144    storage: &mut [Option<B>; 2],
145) -> impl Future<Output = Option<(Direction, B)>>
146where
147    B: PartialEq + Serialize + 'db + Clone,
148{
149    env.loop_on_inference_var(infer, move |data| {
150        if let Some((bound, _)) = bound_op(data, Direction::FromAbove)
151            && Some(&bound) != storage[0].as_ref()
152        {
153            storage[0] = Some(bound.clone());
154            Some((Direction::FromAbove, bound))
155        } else if let Some((bound, _)) = bound_op(data, Direction::FromBelow)
156            && Some(&bound) != storage[1].as_ref()
157        {
158            storage[1] = Some(bound.clone());
159            Some((Direction::FromBelow, bound))
160        } else {
161            None
162        }
163    })
164}
dada_ir_sym/check/env/infer_bounds.rs

dada_ir_sym/check/env/
infer_bounds.rs
