]>
Commit | Line | Data |
---|---|---|
f9f354fc XL |
1 | //! An alternative solver based around the SLG algorithm, which |
2 | //! implements the well-formed semantics. For an overview of how the solver | |
f035d41b | 3 | //! works, see [The On-Demand SLG Solver][guide] in the chalk book. |
f9f354fc | 4 | //! |
f035d41b | 5 | //! [guide]: https://rust-lang.github.io/chalk/book/engine/slg.html |
f9f354fc XL |
6 | //! |
7 | //! This algorithm is very closed based on the description found in the | |
8 | //! following paper, which I will refer to in the comments as EWFS: | |
9 | //! | |
10 | //! > Efficient Top-Down Computation of Queries Under the Well-founded Semantics | |
11 | //! > (Chen, Swift, and Warren; Journal of Logic Programming '95) | |
12 | //! | |
13 | //! However, to understand that paper, I would recommend first | |
14 | //! starting with the following paper, which I will refer to in the | |
15 | //! comments as NFTD: | |
16 | //! | |
17 | //! > A New Formulation of Tabled resolution With Delay | |
18 | //! > (Swift; EPIA '99) | |
19 | //! | |
20 | //! In addition, I incorporated extensions from the following papers, | |
21 | //! which I will refer to as SA and RR respectively, that | |
22 | //! describes how to do introduce approximation when processing | |
23 | //! subgoals and so forth: | |
24 | //! | |
25 | //! > Terminating Evaluation of Logic Programs with Finite Three-Valued Models | |
26 | //! > Riguzzi and Swift; ACM Transactions on Computational Logic 2013 | |
27 | //! > (Introduces "subgoal abstraction", hence the name SA) | |
28 | //! > | |
29 | //! > Radial Restraint | |
30 | //! > Grosof and Swift; 2013 | |
31 | //! | |
32 | //! Another useful paper that gives a kind of high-level overview of | |
33 | //! concepts at play is the following, which I will refer to as XSB: | |
34 | //! | |
35 | //! > XSB: Extending Prolog with Tabled Logic Programming | |
36 | //! > (Swift and Warren; Theory and Practice of Logic Programming '10) | |
37 | //! | |
38 | //! While this code is adapted from the algorithms described in those | |
39 | //! papers, it is not the same. For one thing, the approaches there | |
40 | //! had to be extended to our context, and in particular to coping | |
41 | //! with hereditary harrop predicates and our version of unification | |
42 | //! (which produces subgoals). I believe those to be largely faithful | |
43 | //! extensions. However, there are some other places where I | |
44 | //! intentionally diverged from the semantics as described in the | |
45 | //! papers -- e.g. by more aggressively approximating -- which I | |
46 | //! marked them with a comment DIVERGENCE. Those places may want to be | |
47 | //! evaluated in the future. | |
48 | //! | |
49 | //! Glossary of other terms: | |
50 | //! | |
51 | //! - WAM: Warren abstract machine, an efficient way to evaluate Prolog programs. | |
52 | //! See <http://wambook.sourceforge.net/>. | |
53 | //! - HH: Hereditary harrop predicates. What Chalk deals in. | |
54 | //! Popularized by Lambda Prolog. | |
55 | ||
f9f354fc XL |
56 | use std::cmp::min; |
57 | use std::usize; | |
58 | ||
f035d41b XL |
59 | use chalk_derive::{Fold, HasInterner, Visit}; |
60 | use chalk_ir::interner::{Interner, TargetInterner}; | |
61 | use chalk_ir::visit::VisitResult; | |
62 | use chalk_ir::{ | |
63 | AnswerSubst, Canonical, ConstrainedSubst, Constraint, DebruijnIndex, Goal, InEnvironment, | |
64 | Substitution, | |
65 | }; | |
66 | ||
f9f354fc XL |
67 | pub mod context; |
68 | mod derived; | |
f9f354fc | 69 | pub mod forest; |
f9f354fc | 70 | mod logic; |
1b1a35ee | 71 | mod normalize_deep; |
f9f354fc | 72 | mod simplify; |
1b1a35ee XL |
73 | pub mod slg; |
74 | pub mod solve; | |
f9f354fc XL |
75 | mod stack; |
76 | mod strand; | |
77 | mod table; | |
78 | mod tables; | |
79 | ||
80 | index_struct! { | |
81 | pub struct TableIndex { // FIXME: pub b/c Fold | |
82 | value: usize, | |
83 | } | |
84 | } | |
85 | ||
f9f354fc | 86 | /// The paper describes these as `A :- D | G`. |
f035d41b XL |
87 | #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] |
88 | pub struct ExClause<I: Interner> { | |
f9f354fc XL |
89 | /// The substitution which, applied to the goal of our table, |
90 | /// would yield A. | |
f035d41b | 91 | pub subst: Substitution<I>, |
f9f354fc XL |
92 | |
93 | /// True if any subgoals were depended upon negatively and | |
94 | /// were not fully evaluated, or if we encountered a `CannotProve` | |
95 | /// goal. (In the full SLG algorithm, we would use delayed literals here, | |
96 | /// but we don't bother, as we don't need that support.) | |
97 | pub ambiguous: bool, | |
98 | ||
99 | /// Region constraints we have accumulated. | |
f035d41b | 100 | pub constraints: Vec<InEnvironment<Constraint<I>>>, |
f9f354fc XL |
101 | |
102 | /// Subgoals: literals that must be proven | |
f035d41b | 103 | pub subgoals: Vec<Literal<I>>, |
f9f354fc XL |
104 | |
105 | /// We assume that negative literals cannot have coinductive cycles. | |
f035d41b | 106 | pub delayed_subgoals: Vec<InEnvironment<Goal<I>>>, |
f9f354fc XL |
107 | |
108 | /// Time stamp that is incremented each time we find an answer to | |
109 | /// some subgoal. This is used to figure out whether any of the | |
110 | /// floundered subgoals may no longer be floundered: we record the | |
111 | /// current time when we add something to the list of floundered | |
112 | /// subgoals, and then we can compare whether its value has | |
113 | /// changed since then. This is not the same `TimeStamp` of | |
114 | /// `Forest`'s clock. | |
115 | pub answer_time: TimeStamp, | |
116 | ||
117 | /// List of subgoals that have floundered. See `FlounderedSubgoal` | |
118 | /// for more information. | |
f035d41b | 119 | pub floundered_subgoals: Vec<FlounderedSubgoal<I>>, |
f9f354fc XL |
120 | } |
121 | ||
122 | /// The "time stamp" is a simple clock that gets incremented each time | |
123 | /// we encounter a positive answer in processing a particular | |
124 | /// strand. This is used as an optimization to help us figure out when | |
125 | /// we *may* have changed inference variables. | |
126 | #[derive(Copy, Clone, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
127 | pub struct TimeStamp { | |
128 | clock: u64, | |
129 | } | |
130 | ||
131 | impl TimeStamp { | |
132 | const MAX: TimeStamp = TimeStamp { | |
133 | clock: ::std::u64::MAX, | |
134 | }; | |
135 | ||
136 | fn increment(&mut self) { | |
137 | self.clock += 1; | |
138 | } | |
139 | } | |
140 | ||
141 | /// A "floundered" subgoal is one that contains unbound existential | |
142 | /// variables for which it cannot produce a value. The classic example | |
143 | /// of floundering is a negative subgoal: | |
144 | /// | |
145 | /// ```notrust | |
146 | /// not { Implemented(?T: Foo) } | |
147 | /// ``` | |
148 | /// | |
149 | /// The way the prolog solver works, it basically enumerates all the | |
150 | /// ways that a given goal can be *true*. But we can't use this | |
151 | /// technique to find all the ways that `?T: Foo` can be *false* -- so | |
152 | /// we call it floundered. In other words, we can evaluate a negative | |
153 | /// goal, but only if we know what `?T` is -- we can't use the | |
154 | /// negative goal to help us figuring out `?T`. | |
155 | /// | |
156 | /// In addition to negative goals, we use floundering to prevent the | |
157 | /// trait solver from trying to enumerate very large goals with tons | |
158 | /// of answers. For example, we consider a goal like `?T: Sized` to | |
159 | /// "flounder", since we can't hope to enumerate all types that are | |
160 | /// `Sized`. The same is true for other special traits like `Clone`. | |
161 | /// | |
162 | /// Floundering can also occur indirectly. For example: | |
163 | /// | |
164 | /// ```notrust | |
165 | /// trait Foo { } | |
166 | /// impl<T> Foo for T { } | |
167 | /// ``` | |
168 | /// | |
169 | /// trying to solve `?T: Foo` would immediately require solving `?T: | |
170 | /// Sized`, and hence would flounder. | |
f035d41b XL |
171 | #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit)] |
172 | pub struct FlounderedSubgoal<I: Interner> { | |
f9f354fc | 173 | /// Literal that floundered. |
f035d41b | 174 | pub floundered_literal: Literal<I>, |
f9f354fc XL |
175 | |
176 | /// Current value of the strand's clock at the time of | |
177 | /// floundering. | |
178 | pub floundered_time: TimeStamp, | |
179 | } | |
180 | ||
181 | /// An "answer" in the on-demand solver corresponds to a fully solved | |
182 | /// goal for a particular table (modulo delayed literals). It contains | |
183 | /// a substitution | |
184 | #[derive(Clone, Debug)] | |
f035d41b | 185 | pub struct Answer<I: Interner> { |
f9f354fc XL |
186 | /// Contains values for the unbound inference variables for which |
187 | /// the table is true, along with any delayed subgoals (Which must | |
188 | /// still be proven) and region constrained (which must still be | |
189 | /// proven, but not by chalk). | |
f035d41b | 190 | pub subst: Canonical<AnswerSubst<I>>, |
f9f354fc XL |
191 | |
192 | /// If this flag is set, then the answer could be neither proven | |
193 | /// nor disproven. This could be the size of the answer exceeded | |
194 | /// `max_size` or because of a negative loop (e.g., `P :- not { P }`). | |
195 | pub ambiguous: bool, | |
196 | } | |
197 | ||
198 | #[derive(Clone, Debug)] | |
f035d41b | 199 | pub struct CompleteAnswer<I: Interner> { |
f9f354fc XL |
200 | /// Contains values for the unbound inference variables for which |
201 | /// the table is true, along with any region constrained (which must still be | |
202 | /// proven, but not by chalk). | |
f035d41b | 203 | pub subst: Canonical<ConstrainedSubst<I>>, |
f9f354fc XL |
204 | |
205 | /// If this flag is set, then the answer could be neither proven | |
206 | /// nor disproven. This could be the size of the answer exceeded | |
207 | /// `max_size` or because of a negative loop (e.g., `P :- not { P }`). | |
208 | pub ambiguous: bool, | |
209 | } | |
210 | ||
211 | /// Either `A` or `~A`, where `A` is a `Env |- Goal`. | |
f035d41b XL |
212 | #[derive(Clone, Debug, Fold, Visit)] |
213 | pub enum Literal<I: Interner> { | |
f9f354fc | 214 | // FIXME: pub b/c fold |
f035d41b XL |
215 | Positive(InEnvironment<Goal<I>>), |
216 | Negative(InEnvironment<Goal<I>>), | |
f9f354fc XL |
217 | } |
218 | ||
219 | /// The `Minimums` structure is used to track the dependencies between | |
220 | /// some item E on the evaluation stack. In particular, it tracks | |
221 | /// cases where the success of E depends (or may depend) on items | |
222 | /// deeper in the stack than E (i.e., with lower DFNs). | |
223 | /// | |
224 | /// `positive` tracks the lowest index on the stack to which we had a | |
225 | /// POSITIVE dependency (e.g. `foo(X) :- bar(X)`) -- meaning that in | |
226 | /// order for E to succeed, the dependency must succeed. It is | |
227 | /// initialized with the index of the predicate on the stack. So | |
228 | /// imagine we have a stack like this: | |
229 | /// | |
230 | /// ```notrust | |
231 | /// // 0 foo(X) <-- bottom of stack | |
232 | /// // 1 bar(X) | |
233 | /// // 2 baz(X) <-- top of stack | |
234 | /// ``` | |
235 | /// | |
236 | /// In this case, `positive` would be initially 0, 1, and 2 for `foo`, | |
237 | /// `bar`, and `baz` respectively. This reflects the fact that the | |
238 | /// answers for `foo(X)` depend on the answers for `foo(X)`. =) | |
239 | /// | |
240 | /// Now imagine that we had a clause `baz(X) :- foo(X)`, inducing a | |
241 | /// cycle. In this case, we would update `positive` for `baz(X)` to be | |
242 | /// 0, reflecting the fact that its answers depend on the answers for | |
243 | /// `foo(X)`. Similarly, the minimum for `bar` would (eventually) be | |
244 | /// updated, since it too transitively depends on `foo`. `foo` is | |
245 | /// unaffected. | |
246 | /// | |
247 | /// `negative` tracks the lowest index on the stack to which we had a | |
248 | /// NEGATIVE dependency (e.g., `foo(X) :- not { bar(X) }`) -- meaning | |
249 | /// that for E to succeed, the dependency must fail. This is initially | |
250 | /// `usize::MAX`, reflecting the fact that the answers for `foo(X)` do | |
251 | /// not depend on `not(foo(X))`. When negative cycles are encountered, | |
252 | /// however, this value must be updated. | |
253 | #[derive(Copy, Clone, Debug)] | |
254 | struct Minimums { | |
255 | positive: TimeStamp, | |
256 | negative: TimeStamp, | |
257 | } | |
258 | ||
259 | impl Minimums { | |
260 | const MAX: Minimums = Minimums { | |
261 | positive: TimeStamp::MAX, | |
262 | negative: TimeStamp::MAX, | |
263 | }; | |
264 | ||
265 | /// Update our fields to be the minimum of our current value | |
266 | /// and the values from other. | |
267 | fn take_minimums(&mut self, other: &Minimums) { | |
268 | self.positive = min(self.positive, other.positive); | |
269 | self.negative = min(self.negative, other.negative); | |
270 | } | |
271 | ||
272 | fn minimum_of_pos_and_neg(&self) -> TimeStamp { | |
273 | min(self.positive, self.negative) | |
274 | } | |
275 | } | |
f035d41b XL |
276 | |
277 | #[derive(Copy, Clone, Debug)] | |
278 | pub(crate) enum AnswerMode { | |
279 | Complete, | |
280 | Ambiguous, | |
281 | } | |
282 | ||
283 | chalk_ir::copy_fold!(TableIndex); | |
284 | chalk_ir::copy_fold!(TimeStamp); | |
285 | ||
286 | chalk_ir::const_visit!(TableIndex); | |
287 | chalk_ir::const_visit!(TimeStamp); | |
288 | ||
289 | #[macro_export] | |
290 | macro_rules! index_struct { | |
291 | ($(#[$m:meta])* $v:vis struct $n:ident { | |
292 | $vf:vis value: usize, | |
293 | }) => { | |
294 | #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | |
295 | $(#[$m])* | |
296 | $v struct $n { | |
297 | $vf value: usize, | |
298 | } | |
299 | ||
300 | impl $n { | |
301 | // Not all index structs need this, so allow it to be dead | |
302 | // code. | |
303 | #[allow(dead_code)] | |
304 | $v fn get_and_increment(&mut self) -> Self { | |
305 | let old_value = *self; | |
306 | self.increment(); | |
307 | old_value | |
308 | } | |
309 | ||
310 | #[allow(dead_code)] | |
311 | $v fn increment(&mut self) { | |
312 | self.value += 1; | |
313 | } | |
314 | ||
315 | // TODO: Once the Step trait is stabilized (https://github.com/rust-lang/rust/issues/42168), instead implement it and use the Iterator implementation of Range | |
316 | #[allow(dead_code)] | |
317 | pub fn iterate_range(range: ::std::ops::Range<Self>) -> impl Iterator<Item = $n> { | |
318 | (range.start.value..range.end.value).into_iter().map(|i| Self { value: i }) | |
319 | } | |
320 | } | |
321 | ||
322 | impl ::std::fmt::Debug for $n { | |
323 | fn fmt(&self, fmt: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result { | |
324 | write!(fmt, "{}({})", stringify!($n), self.value) | |
325 | } | |
326 | } | |
327 | ||
328 | impl From<usize> for $n { | |
329 | fn from(value: usize) -> Self { | |
330 | Self { value } | |
331 | } | |
332 | } | |
333 | } | |
334 | } |