liquid_fixpoint/
constraint_fragments.rs

1use crate::{
2    Types,
3    constraint::{Bind, Constraint, Pred},
4};
5
6pub enum Fragment<'a, T: Types> {
7    Constraint(&'a Constraint<T>),
8    Predicate(&'a Pred<T>),
9}
10
11pub struct ConstraintFragments<'a, T: Types> {
12    stack: Vec<(Fragment<'a, T>, Vec<Bind<T>>)>,
13}
14
15impl<'a, T: Types> ConstraintFragments<'a, T> {
16    pub fn new(cstr: &'a Constraint<T>) -> Self {
17        ConstraintFragments { stack: vec![(Fragment::Constraint(cstr), vec![])] }
18    }
19}
20
21impl<T: Types> Iterator for ConstraintFragments<'_, T> {
22    type Item = Constraint<T>;
23
24    fn next(&mut self) -> Option<Self::Item> {
25        while let Some((node, binders)) = self.stack.pop() {
26            match node {
27                Fragment::Predicate(Pred::And(preds)) => {
28                    for p in preds.into_iter().rev() {
29                        self.stack.push((Fragment::Predicate(&p), binders.clone()));
30                    }
31                }
32                Fragment::Predicate(pred) => {
33                    let mut result = Constraint::Pred(pred.clone(), None);
34                    for b in binders.iter().rev() {
35                        result = Constraint::ForAll(b.clone(), Box::new(result));
36                    }
37                    return Some(result);
38                }
39                Fragment::Constraint(Constraint::Pred(pred, _tag)) => {
40                    self.stack
41                        .push((Fragment::Predicate(pred), binders.clone()));
42                }
43                Fragment::Constraint(Constraint::Conj(children)) => {
44                    for child in children.into_iter().rev() {
45                        self.stack
46                            .push((Fragment::Constraint(child), binders.clone()));
47                    }
48                }
49                Fragment::Constraint(Constraint::ForAll(bind, inner)) => {
50                    let mut new_binders = binders.clone();
51                    new_binders.push(bind.clone());
52                    self.stack
53                        .push((Fragment::Constraint(&**inner), new_binders));
54                }
55            }
56        }
57        None
58    }
59}
liquid_fixpoint/constraint_fragments.rs

liquid_fixpoint/
constraint_fragments.rs
