1use crate::Table;
2
3#[derive(Debug, Default, Clone, Copy, Eq, PartialEq, Ord, PartialOrd, Hash)]
4pub struct State {
5 current_term: u32,
6 current_theorem: u32,
7 current_sort: u8,
8}
9
10impl State {
11 pub fn current_term(&self) -> u32 {
12 self.current_term
13 }
14
15 pub fn increment_current_term(&mut self) {
16 self.current_term += 1;
17 }
18
19 pub fn current_theorem(&self) -> u32 {
20 self.current_theorem
21 }
22
23 pub fn increment_current_theorem(&mut self) {
24 self.current_theorem += 1;
25 }
26
27 pub fn current_sort(&self) -> u8 {
28 self.current_sort
29 }
30
31 pub fn increment_current_sort(&mut self) {
32 self.current_sort += 1;
33 }
34
35 pub fn from_table<T: Table>(table: &T) -> State {
36 State {
37 current_term: table.nr_terms(),
38 current_theorem: table.nr_theorems(),
39 current_sort: table.nr_sorts(),
40 }
41 }
42}