trivial_kernel/
table.rs

1use crate::opcode;
2use crate::{Var, Var_};
3use core::ops::Range;
4
5/// A handle to a sort.
6///
7/// Sorts have modifiers that can be queried with this handle.
8/// These modifiers correspond to assertions that are verified by the kernel
9/// during execution.
10pub trait Sort {
11    /// A pure sort does not allow expression constructors.
12    fn is_pure(&self) -> bool;
13
14    /// A strict sort can not be used as a name.
15    ///
16    /// TODO: explain what a name is.
17    fn is_strict(&self) -> bool;
18
19    /// Only statements with a provable sort can be proven by the kernel.
20    fn is_provable(&self) -> bool;
21
22    /// A free sort cannot be used as a dummy variable.
23    fn is_free(&self) -> bool;
24}
25
26/// A handle to a term.
27pub trait Term {
28    type Type: Var;
29
30    /// Returns the index of the sort this term has.
31    fn sort_idx(&self) -> u8;
32
33    /// Returns `true` if this term is a definition, and `false` otherwise.
34    ///
35    /// Definitions are always conservative and can be unfolded in a proof.
36    fn is_definition(&self) -> bool;
37
38    /// Returns the range of the binders (arguments) of the term.
39    ///
40    /// The range can be queried in the `Table` to get the binders themselves.
41    fn binders(&self) -> Range<usize>;
42
43    /// Returns the type of the expression.
44    fn return_type(&self) -> &Self::Type;
45
46    /// Returns the unification command stream if this term is a definition.
47    fn command_stream(&self) -> Range<usize>;
48}
49
50/// A handle to a theorem.
51///
52/// Theorems in the table only contain the list of binders, and a command
53/// stream for unification.
54/// The number of hypotheses can be determined by counting the number of `Hyp`
55/// commands in the unification stream.
56pub trait Theorem {
57    fn binders(&self) -> Range<usize>;
58
59    fn unify_commands(&self) -> Range<usize>;
60}
61
62/// An interface that enables queries for properties of sorts, terms and
63/// theorems.
64pub trait Table {
65    type Sort: Sort;
66    type Term: Term<Type = Self::Var>;
67    type Theorem: Theorem;
68    type Var: Var;
69
70    fn sort(&self, idx: u8) -> Option<&Self::Sort>;
71
72    fn nr_sorts(&self) -> u8;
73
74    fn term(&self, idx: u32) -> Option<&Self::Term>;
75
76    fn nr_terms(&self) -> u32;
77
78    fn theorem(&self, idx: u32) -> Option<&Self::Theorem>;
79
80    fn nr_theorems(&self) -> u32;
81
82    fn unify_commands(&self, idx: Range<usize>) -> Option<&[opcode::Command<opcode::Unify>]>;
83
84    fn unify_command(&self, idx: usize) -> Option<&opcode::Command<opcode::Unify>>;
85
86    fn binders(&self, idx: Range<usize>) -> Option<&[Self::Var]>;
87}
88
89#[derive(Debug, Default, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
90pub struct Sort_(pub u8);
91
92impl From<u8> for Sort_ {
93    fn from(value: u8) -> Sort_ {
94        Sort_(value)
95    }
96}
97
98impl Sort for Sort_ {
99    #[inline(always)]
100    fn is_pure(&self) -> bool {
101        (self.0 & 0x01) != 0
102    }
103
104    #[inline(always)]
105    fn is_strict(&self) -> bool {
106        (self.0 & 0x02) != 0
107    }
108
109    #[inline(always)]
110    fn is_provable(&self) -> bool {
111        (self.0 & 0x04) != 0
112    }
113
114    #[inline(always)]
115    fn is_free(&self) -> bool {
116        (self.0 & 0x08) != 0
117    }
118}
119
120#[derive(Debug, Default, Clone, Eq, PartialEq, Hash)]
121pub struct Term_ {
122    pub sort: u8,
123    pub binders: Range<usize>,
124    pub ret_type: Var_,
125    pub unify_commands: Range<usize>,
126}
127
128impl Term for Term_ {
129    type Type = Var_;
130
131    fn sort_idx(&self) -> u8 {
132        self.sort & 0x7F
133    }
134
135    fn is_definition(&self) -> bool {
136        (self.sort & 0x80) != 0
137    }
138
139    fn binders(&self) -> Range<usize> {
140        self.binders.clone()
141    }
142
143    fn return_type(&self) -> &Self::Type {
144        &self.ret_type
145    }
146
147    fn command_stream(&self) -> Range<usize> {
148        self.unify_commands.clone()
149    }
150}
151
152#[derive(Debug, Default, Clone, Eq, PartialEq, Hash)]
153pub struct Theorem_ {
154    pub binders: Range<usize>,
155    pub unify_commands: Range<usize>,
156}
157
158impl Theorem for Theorem_ {
159    fn binders(&self) -> Range<usize> {
160        self.binders.clone()
161    }
162
163    fn unify_commands(&self) -> Range<usize> {
164        self.unify_commands.clone()
165    }
166}
167
168#[derive(Debug, Default, Clone, Eq, PartialEq, Hash)]
169pub struct Table_ {
170    pub sorts: Vec<Sort_>,
171    pub theorems: Vec<Theorem_>,
172    pub terms: Vec<Term_>,
173    pub unify: Vec<opcode::Command<opcode::Unify>>,
174    pub binders: Vec<Var_>,
175}
176
177impl Table for Table_ {
178    type Sort = Sort_;
179    type Term = Term_;
180    type Theorem = Theorem_;
181    type Var = Var_;
182
183    fn sort(&self, idx: u8) -> Option<&Self::Sort> {
184        self.sorts.get(idx as usize)
185    }
186
187    fn nr_sorts(&self) -> u8 {
188        self.sorts.len() as u8
189    }
190
191    fn term(&self, idx: u32) -> Option<&Self::Term> {
192        self.terms.get(idx as usize)
193    }
194
195    fn nr_terms(&self) -> u32 {
196        self.terms.len() as u32
197    }
198
199    fn theorem(&self, idx: u32) -> Option<&Self::Theorem> {
200        self.theorems.get(idx as usize)
201    }
202
203    fn nr_theorems(&self) -> u32 {
204        self.theorems.len() as u32
205    }
206
207    fn unify_commands(&self, idx: Range<usize>) -> Option<&[opcode::Command<opcode::Unify>]> {
208        self.unify.get(idx)
209    }
210
211    fn unify_command(&self, idx: usize) -> Option<&opcode::Command<opcode::Unify>> {
212        self.unify.get(idx as usize)
213    }
214
215    fn binders(&self, idx: Range<usize>) -> Option<&[Self::Var]> {
216        self.binders.get(idx)
217    }
218}
trivial_kernel/table.rs

trivial_kernel/
table.rs
