formality_core/
visit.rs

1use std::sync::Arc;
2
3use crate::{collections::Set, language::Language, variable::CoreVariable};
4
5pub trait CoreVisit<L: Language> {
6    /// Extract the list of free variables (for the purposes of this function, defined by `Variable::is_free`).
7    /// The list may contain duplicates and must be in a determinstic order (though the order itself isn't important).
8    fn free_variables(&self) -> Vec<CoreVariable<L>>;
9
10    /// Measures the overall size of the term by counting constructors etc.
11    /// Used to determine overflow.
12    fn size(&self) -> usize;
13
14    /// Asserts various validity constraints and panics if they are not held.
15    /// These validition constraints should never fail unless there is a bug in our logic.
16    /// This is to aid with fuzzing and bug detection.
17    fn assert_valid(&self);
18
19    /// True if this term references only universal variables.
20    /// This means that it contains no existential variables.
21    /// If this is a goal, then when we prove it true, we don't expect any substitution.
22    /// This is similar, but not *identical*, to the commonly used term "ground term",
23    /// which in Prolog refers to a term that contains no variables. The difference here
24    /// is that the term may contain variables, but only those instantiated universally (∀).
25    fn references_only_universal_variables(&self) -> bool {
26        self.free_variables().iter().all(|v| match v {
27            CoreVariable::UniversalVar(_) => true,
28            CoreVariable::ExistentialVar(_) => false,
29            CoreVariable::BoundVar(_) => false,
30        })
31    }
32}
33
34impl<L: Language, T: CoreVisit<L>> CoreVisit<L> for Vec<T> {
35    fn free_variables(&self) -> Vec<CoreVariable<L>> {
36        self.iter().flat_map(|e| e.free_variables()).collect()
37    }
38
39    fn size(&self) -> usize {
40        self.iter().map(|e| e.size()).sum()
41    }
42
43    fn assert_valid(&self) {
44        self.iter().for_each(|e| e.assert_valid());
45    }
46}
47
48impl<L: Language, T: CoreVisit<L> + Ord> CoreVisit<L> for Set<T> {
49    fn free_variables(&self) -> Vec<CoreVariable<L>> {
50        self.iter().flat_map(|e| e.free_variables()).collect()
51    }
52
53    fn size(&self) -> usize {
54        self.iter().map(|e| e.size()).sum()
55    }
56
57    fn assert_valid(&self) {
58        self.iter().for_each(|e| e.assert_valid());
59    }
60}
61
62impl<L: Language, T: CoreVisit<L>> CoreVisit<L> for Option<T> {
63    fn free_variables(&self) -> Vec<CoreVariable<L>> {
64        self.iter().flat_map(|e| e.free_variables()).collect()
65    }
66
67    fn size(&self) -> usize {
68        self.as_ref().map(|e| e.size()).unwrap_or(0)
69    }
70
71    fn assert_valid(&self) {
72        self.iter().for_each(|e| e.assert_valid());
73    }
74}
75
76impl<L: Language, T: CoreVisit<L> + ?Sized> CoreVisit<L> for Arc<T> {
77    fn free_variables(&self) -> Vec<CoreVariable<L>> {
78        T::free_variables(self)
79    }
80
81    fn size(&self) -> usize {
82        T::size(self)
83    }
84
85    fn assert_valid(&self) {
86        T::assert_valid(self)
87    }
88}
89
90impl<L: Language> CoreVisit<L> for usize {
91    fn free_variables(&self) -> Vec<CoreVariable<L>> {
92        vec![]
93    }
94
95    fn size(&self) -> usize {
96        1
97    }
98
99    fn assert_valid(&self) {}
100}
101
102impl<L: Language> CoreVisit<L> for u32 {
103    fn free_variables(&self) -> Vec<CoreVariable<L>> {
104        vec![]
105    }
106
107    fn size(&self) -> usize {
108        1
109    }
110
111    fn assert_valid(&self) {}
112}
113
114impl<L: Language> CoreVisit<L> for u128 {
115    fn free_variables(&self) -> Vec<CoreVariable<L>> {
116        vec![]
117    }
118
119    fn size(&self) -> usize {
120        std::mem::size_of::<Self>()
121    }
122
123    fn assert_valid(&self) {}
124}
125
126impl<L: Language> CoreVisit<L> for () {
127    fn free_variables(&self) -> Vec<CoreVariable<L>> {
128        vec![]
129    }
130
131    fn size(&self) -> usize {
132        0
133    }
134
135    fn assert_valid(&self) {}
136}
137
138impl<L: Language, A: CoreVisit<L>, B: CoreVisit<L>> CoreVisit<L> for (A, B) {
139    fn free_variables(&self) -> Vec<CoreVariable<L>> {
140        let (a, b) = self;
141        let mut fv = vec![];
142        fv.extend(a.free_variables());
143        fv.extend(b.free_variables());
144        fv
145    }
146
147    fn size(&self) -> usize {
148        let (a, b) = self;
149        a.size() + b.size()
150    }
151
152    fn assert_valid(&self) {
153        let (a, b) = self;
154        a.assert_valid();
155        b.assert_valid();
156    }
157}
158
159impl<L: Language, A: CoreVisit<L>, B: CoreVisit<L>, C: CoreVisit<L>> CoreVisit<L> for (A, B, C) {
160    fn free_variables(&self) -> Vec<CoreVariable<L>> {
161        let (a, b, c) = self;
162        let mut fv = vec![];
163        fv.extend(a.free_variables());
164        fv.extend(b.free_variables());
165        fv.extend(c.free_variables());
166        fv
167    }
168
169    fn size(&self) -> usize {
170        let (a, b, c) = self;
171        a.size() + b.size() + c.size()
172    }
173
174    fn assert_valid(&self) {
175        let (a, b, c) = self;
176        a.assert_valid();
177        b.assert_valid();
178        c.assert_valid();
179    }
180}
181
182impl<L: Language, A: CoreVisit<L> + ?Sized> CoreVisit<L> for &A {
183    fn free_variables(&self) -> Vec<CoreVariable<L>> {
184        A::free_variables(self)
185    }
186
187    fn size(&self) -> usize {
188        A::size(self)
189    }
190
191    fn assert_valid(&self) {
192        A::assert_valid(self)
193    }
194}
195
196impl<L: Language, A: CoreVisit<L>> CoreVisit<L> for [A] {
197    fn free_variables(&self) -> Vec<CoreVariable<L>> {
198        self.iter().flat_map(|e| A::free_variables(e)).collect()
199    }
200
201    fn size(&self) -> usize {
202        self.iter().map(|e| A::size(e)).sum()
203    }
204
205    fn assert_valid(&self) {
206        self.iter().for_each(|e| A::assert_valid(e));
207    }
208}
formality_core/visit.rs

formality_core/
visit.rs
