flux_infer/
evars.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
use std::fmt;

use flux_common::index::IndexVec;
use flux_middle::{
    pretty::{Pretty, PrettyCx, impl_debug_with_default_cx, w},
    rty::{EVid, Expr, fold::TypeFoldable},
};

use crate::refine_tree::Marker;

#[derive(Default, Debug)]
pub(crate) struct EVarStore {
    evars: IndexVec<EVid, EVarState>,
    scopes: Vec<Vec<EVid>>,
}

pub(crate) enum EVarState {
    Solved(Expr),
    Unsolved(Marker),
}

impl EVarStore {
    pub(crate) fn fresh(&mut self, marker: Marker) -> EVid {
        let evid = self.evars.push(EVarState::Unsolved(marker));
        if let Some(scope) = self.scopes.last_mut() {
            scope.push(evid);
        }
        evid
    }

    pub(crate) fn push_scope(&mut self) {
        self.scopes.push(vec![]);
    }

    pub(crate) fn pop_scope(&mut self) -> Result<(), EVid> {
        let Some(scope) = self.scopes.pop() else { return Ok(()) };
        for evid in scope {
            if let EVarState::Unsolved(..) = self.get(evid) {
                return Err(evid);
            }
        }
        Ok(())
    }

    pub(crate) fn replace_evars<T: TypeFoldable>(&self, t: &T) -> Result<T, EVid> {
        t.replace_evars(&mut |evid| {
            match self.get(evid) {
                EVarState::Solved(expr) => Some(expr.clone()),
                EVarState::Unsolved(..) => None,
            }
        })
    }

    pub(crate) fn solve(&mut self, evid: EVid, expr: Expr) {
        debug_assert!(matches!(self.evars[evid], EVarState::Unsolved(_)));
        self.evars[evid] = EVarState::Solved(expr);
    }

    pub(crate) fn get(&self, evid: EVid) -> &EVarState {
        &self.evars[evid]
    }
}

impl Pretty for EVarState {
    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            EVarState::Solved(expr) => w!(cx, f, "Solved({:?})", expr),
            EVarState::Unsolved(_) => w!(cx, f, "Unsolved"),
        }
    }
}

impl_debug_with_default_cx!(EVarState);