trivial_kernel/context/
mod.rs

1pub mod heap;
2pub mod stack;
3pub mod store;
4
5use crate::error::Kind;
6use crate::table::Sort;
7use crate::KResult;
8use crate::Table;
9use crate::Var;
10pub use heap::Heap;
11pub use stack::Stack;
12pub use store::{PackedPtr, Ptr, Store};
13
14#[derive(Debug, Default, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
15pub struct Context<S: Store> {
16    pub(crate) proof_stack: Stack,
17    pub(crate) proof_heap: Heap,
18    pub(crate) unify_stack: Stack,
19    pub(crate) unify_heap: Heap,
20    pub(crate) hyp_stack: Stack,
21    pub(crate) store: S,
22    pub(crate) next_bv: u64,
23}
24
25impl<S: Store> Context<S> {
26    pub fn proof_stack(&self) -> &Stack {
27        &self.proof_stack
28    }
29
30    pub fn proof_heap(&self) -> &Heap {
31        &self.proof_heap
32    }
33
34    pub fn unify_stack(&self) -> &Stack {
35        &self.unify_stack
36    }
37
38    pub fn unify_heap(&self) -> &Heap {
39        &self.unify_heap
40    }
41
42    pub fn store(&self) -> &S {
43        &self.store
44    }
45
46    pub fn hyp_stack(&self) -> &Stack {
47        &self.hyp_stack
48    }
49
50    pub fn clear_except_store(&mut self) {
51        self.proof_stack.clear();
52        self.proof_heap.clear();
53        self.unify_stack.clear();
54        self.unify_heap.clear();
55        self.hyp_stack.clear();
56    }
57
58    pub fn binder_check<T: Table>(
59        table: &T,
60        ty: &T::Var,
61        current_sort: u8,
62        bv: &mut u64,
63    ) -> KResult {
64        let idx = ty.sort_idx();
65
66        if idx >= current_sort {
67            return Err(Kind::SortOutOfRange);
68        }
69
70        let sort = table.sort(ty.sort_idx()).ok_or(Kind::InvalidSort)?;
71        let deps = ty.dependencies();
72
73        if ty.is_bound() {
74            if sort.is_strict() {
75                return Err(Kind::SortIsStrict);
76            }
77
78            if deps != *bv {
79                return Err(Kind::BindDep);
80            }
81
82            *bv *= 2;
83        } else if (deps & !(*bv - 1)) != 0 {
84            return Err(Kind::BindDep);
85        }
86
87        Ok(())
88    }
89
90    pub fn allocate_binders<T: Table<Var = S::Var>>(
91        &mut self,
92        table: &T,
93        current_sort: u8,
94        binders: &[T::Var],
95    ) -> KResult {
96        let mut next_bv = 1;
97
98        for (i, ty) in binders.iter().enumerate() {
99            Self::binder_check(table, ty, current_sort, &mut next_bv)?;
100
101            let ptr = self.store.alloc_var(*ty, i as u16);
102            self.proof_heap.push(ptr);
103        }
104
105        self.next_bv = next_bv;
106
107        Ok(())
108    }
109}
110
111use core::fmt::{self, Display, Formatter};
112
113impl<S: Store> Display for Context<S> {
114    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
115        let display = self.proof_stack.to_display(&self.store);
116        writeln!(f, " Stack:\n{}", display)?;
117        let display = self.unify_stack.to_display(&self.store);
118        writeln!(f, " UStack:\n{}", display)?;
119        let display = self.hyp_stack.to_display(&self.store);
120        writeln!(f, " HStack:\n{}", display)
121    }
122}
trivial_kernel/context/mod.rs

trivial_kernel/context/
mod.rs
