ttt/
context.rs

1use cons_list::ConsList;
2
3use crate::DeBruijnIndexed;
4
5pub trait Context<Entry> {
6    fn iter(&self) -> impl Iterator<Item = Entry>;
7    fn append(&self, variable: Entry) -> Self;
8    fn empty() -> Self;
9
10    fn get(&self, var: usize) -> Option<Entry> 
11    where 
12        Entry: DeBruijnIndexed
13    {
14        self.iter()
15            .nth(var)
16            .map(|v| v.increment_indices_by(var + 1))
17    }
18}
19
20pub trait PartialContext<Entry> : Context<Option<Entry>> { }
21
22impl<Entry, Ctx> PartialContext<Entry> for Ctx where Ctx: Context<Option<Entry>> {}
23
24
25pub struct ListContext<T>(ConsList<T>);
26
27impl<Entry: Clone> Context<Entry> for ListContext<Entry> {
28    fn iter(&self) -> impl Iterator<Item = Entry> {
29        self.0.iter().cloned()
30    }
31
32    fn append(&self, variable: Entry) -> Self {
33        ListContext(self.0.append(variable))
34    }
35
36    fn empty() -> Self {
37        ListContext(ConsList::new())
38    }
39}
ttt/context.rs

ttt/
context.rs
