formality_core/fixed_point/
stack.rs

1use super::Value;
2
3pub struct FixedPointStack<Input, Output> {
4    entries: Vec<StackEntry<Input, Output>>,
5}
6
7impl<Input, Output> Default for FixedPointStack<Input, Output> {
8    fn default() -> Self {
9        Self {
10            entries: Default::default(),
11        }
12    }
13}
14
15struct StackEntry<Input, Output> {
16    /// Input.
17    input: Input,
18
19    /// Current output, updated during computation as we approach a fixed point.
20    output: Output,
21
22    /// Initially false; set to true when the outputs of this rule
23    /// are observed while it is being evaluated.
24    has_dependents: bool,
25}
26
27impl<Input, Output> FixedPointStack<Input, Output>
28where
29    Input: Value,
30    Output: Value,
31{
32    /// Access the top frame on the stack, which should be for `input`.
33    fn top_frame(&mut self, input: &Input) -> &mut StackEntry<Input, Output> {
34        let top = self.entries.last_mut().unwrap();
35        assert_eq!(top.input, *input);
36        top
37    }
38
39    /// Search backwards through the stack, looking for the given input.
40    ///
41    /// If it is found, return `Some` with the current outputs, and mark it
42    /// as needing fixed point iteration.
43    ///
44    /// If not, return `None`.
45    ///
46    /// The fixed-point mark is returned when the stack is [popped](`Self::pop`) and is used
47    /// as part of the fixed point algorithm.
48    pub fn search(&mut self, input: &Input) -> Option<Output> {
49        for entry in &mut self.entries {
50            if entry.input == *input {
51                entry.has_dependents = true;
52                return Some(entry.output.clone());
53            }
54        }
55
56        None
57    }
58
59    /// Push an entry onto the stack, indicating it is currently being evaluated.
60    /// There must not already be an entry for `input`.
61    pub fn push(&mut self, input: &Input, output: Output) {
62        assert!(self.search(input).is_none());
63
64        self.entries.push(StackEntry {
65            input: input.clone(),
66            output,
67            has_dependents: false,
68        });
69    }
70
71    /// Add outputs to the top-most stack entry, which must be for `input`.
72    /// Returns true if another iteration is needed before reaching a fixed point.
73    pub fn update_output(&mut self, input: &Input, output: Output) -> bool {
74        let top = self.top_frame(input);
75        if top.output == output {
76            return false;
77        }
78
79        top.output = output;
80        top.has_dependents
81    }
82
83    /// Pops the top entry from the stack, returning the saved outputs.
84    pub fn pop(&mut self, input: &Input) -> Output {
85        let top = self.entries.pop().unwrap();
86        assert_eq!(top.input, *input);
87        top.output
88    }
89}
formality_core/fixed_point/stack.rs

formality_core/fixed_point/
stack.rs
