flux_infer/
evars.rs

Help
1use std::fmt;
2
3use flux_common::index::IndexVec;
4use flux_middle::{
5    pretty::{Pretty, PrettyCx, impl_debug_with_default_cx, w},
6    rty::{EVid, Expr, fold::TypeFoldable},
7};
8
9use crate::refine_tree::Marker;
10
11#[derive(Default, Debug)]
12pub(crate) struct EVarStore {
13    evars: IndexVec<EVid, EVarState>,
14    scopes: Vec<Vec<EVid>>,
15}
16
17pub(crate) enum EVarState {
18    Solved(Expr),
19    Unsolved(Marker),
20}
21
22impl EVarStore {
23    pub(crate) fn fresh(&mut self, marker: Marker) -> EVid {
24        let evid = self.evars.push(EVarState::Unsolved(marker));
25        if let Some(scope) = self.scopes.last_mut() {
26            scope.push(evid);
27        }
28        evid
29    }
30
31    pub(crate) fn push_scope(&mut self) {
32        self.scopes.push(vec![]);
33    }
34
35    pub(crate) fn pop_scope(&mut self) -> Result<(), EVid> {
36        let Some(scope) = self.scopes.pop() else { return Ok(()) };
37        for evid in scope {
38            if let EVarState::Unsolved(..) = self.get(evid) {
39                return Err(evid);
40            }
41        }
42        Ok(())
43    }
44
45    pub(crate) fn replace_evars<T: TypeFoldable>(&self, t: &T) -> Result<T, EVid> {
46        t.replace_evars(&mut |evid| {
47            match self.get(evid) {
48                EVarState::Solved(expr) => Some(expr.clone()),
49                EVarState::Unsolved(..) => None,
50            }
51        })
52    }
53
54    pub(crate) fn solve(&mut self, evid: EVid, expr: Expr) {
55        debug_assert!(matches!(self.evars[evid], EVarState::Unsolved(_)));
56        self.evars[evid] = EVarState::Solved(expr);
57    }
58
59    pub(crate) fn get(&self, evid: EVid) -> &EVarState {
60        &self.evars[evid]
61    }
62}
63
64impl Pretty for EVarState {
65    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
66        match self {
67            EVarState::Solved(expr) => w!(cx, f, "Solved({:?})", expr),
68            EVarState::Unsolved(_) => w!(cx, f, "Unsolved"),
69        }
70    }
71}
72
73impl_debug_with_default_cx!(EVarState);
flux_infer/evars.rs

flux_infer/
evars.rs
