vendor/chalk-engine/src/lib.rs

   1 //! An alternative solver based around the SLG algorithm, which
   2 //! implements the well-formed semantics. This algorithm is very
   3 //! closed based on the description found in the following paper,
   4 //! which I will refer to in the comments as EWFS:
   5 //!
   6 //! > Efficient Top-Down Computation of Queries Under the Well-formed Semantics
   7 //! > (Chen, Swift, and Warren; Journal of Logic Programming '95)
   8 //!
   9 //! However, to understand that paper, I would recommend first
  10 //! starting with the following paper, which I will refer to in the
  11 //! comments as NFTD:
  12 //!
  13 //! > A New Formulation of Tabled resolution With Delay
  14 //! > (Swift; EPIA '99)
  15 //!
  16 //! In addition, I incorporated extensions from the following papers,
  17 //! which I will refer to as SA and RR respectively, that
  18 //! describes how to do introduce approximation when processing
  19 //! subgoals and so forth:
  20 //!
  21 //! > Terminating Evaluation of Logic Programs with Finite Three-Valued Models
  22 //! > Riguzzi and Swift; ACM Transactions on Computational Logic 2013
  23 //! > (Introduces "subgoal abstraction", hence the name SA)
  24 //! >
  25 //! > Radial Restraint
  26 //! > Grosof and Swift; 2013
  27 //!
  28 //! Another useful paper that gives a kind of high-level overview of
  29 //! concepts at play is the following, which I will refer to as XSB:
  30 //!
  31 //! > XSB: Extending Prolog with Tabled Logic Programming
  32 //! > (Swift and Warren; Theory and Practice of Logic Programming '10)
  33 //!
  34 //! While this code is adapted from the algorithms described in those
  35 //! papers, it is not the same. For one thing, the approaches there
  36 //! had to be extended to our context, and in particular to coping
  37 //! with hereditary harrop predicates and our version of unification
  38 //! (which produces subgoals). I believe those to be largely faithful
  39 //! extensions. However, there are some other places where I
  40 //! intentionally dieverged from the semantics as described in the
  41 //! papers -- e.g. by more aggressively approximating -- which I
  42 //! marked them with a comment DIVERGENCE. Those places may want to be
  43 //! evaluated in the future.
  44 //!
  45 //! Glossary of other terms:
  46 //!
  47 //! - WAM: Warren abstract machine, an efficient way to evaluate Prolog programs.
  48 //!   See <http://wambook.sourceforge.net/>.
  49 //! - HH: Hereditary harrop predicates. What Chalk deals in.
  50 //!   Popularized by Lambda Prolog.
  51
  52 #![feature(in_band_lifetimes)]
  53 #![feature(step_trait)]
  54 #![feature(non_modrs_mods)]
  55
  56 #[macro_use]
  57 extern crate chalk_macros;
  58
  59 #[cfg(feature = "stack_protection")]
  60 extern crate stacker;
  61
  62 extern crate rustc_hash;
  63
  64 use context::Context;
  65 use rustc_hash::FxHashSet;
  66 use std::cmp::min;
  67 use std::usize;
  68
  69 pub mod context;
  70 mod derived;
  71 pub mod fallible;
  72 pub mod forest;
  73 pub mod hh;
  74 mod logic;
  75 mod simplify;
  76 mod stack;
  77 mod strand;
  78 mod table;
  79 mod tables;
  80
  81 index_struct! {
  82     pub struct TableIndex { // FIXME: pub b/c Fold
  83         value: usize,
  84     }
  85 }
  86
  87 /// The StackIndex identifies the position of a table's goal in the
  88 /// stack of goals that are actively being processed. Note that once a
  89 /// table is completely evaluated, it may be popped from the stack,
  90 /// and hence no longer have a stack index.
  91 index_struct! {
  92     struct StackIndex {
  93         value: usize,
  94     }
  95 }
  96
  97 /// The `DepthFirstNumber` (DFN) is a sequential number assigned to
  98 /// each goal when it is first encountered. The naming (taken from
  99 /// EWFS) refers to the idea that this number tracks the index of when
 100 /// we encounter the goal during a depth-first traversal of the proof
 101 /// tree.
 102 #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
 103 struct DepthFirstNumber {
 104     value: u64,
 105 }
 106
 107 /// The paper describes these as `A :- D | G`.
 108 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 109 pub struct ExClause<C: Context> {
 110     /// The substitution which, applied to the goal of our table,
 111     /// would yield A.
 112     pub subst: C::Substitution,
 113
 114     /// Delayed literals: things that we depend on negatively,
 115     /// but which have not yet been fully evaluated.
 116     pub delayed_literals: Vec<DelayedLiteral<C>>,
 117
 118     /// Region constraints we have accumulated.
 119     pub constraints: Vec<C::RegionConstraint>,
 120
 121     /// Subgoals: literals that must be proven
 122     pub subgoals: Vec<Literal<C>>,
 123 }
 124
 125 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 126 struct SimplifiedAnswers<C: Context> {
 127     answers: Vec<SimplifiedAnswer<C>>,
 128 }
 129
 130 #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
 131 pub struct SimplifiedAnswer<C: Context> {
 132     /// A fully instantiated version of the goal for which the query
 133     /// is true (including region constraints).
 134     pub subst: C::CanonicalConstrainedSubst,
 135
 136     /// If this flag is set, then the answer could be neither proven
 137     /// nor disproven. In general, the existence of a non-empty set of
 138     /// delayed literals simply means the answer's status is UNKNOWN,
 139     /// either because the size of the answer exceeded `max_size` or
 140     /// because of a negative loop (e.g., `P :- not { P }`).
 141     pub ambiguous: bool,
 142 }
 143
 144 #[derive(Debug)]
 145 struct DelayedLiteralSets<C: Context>(InnerDelayedLiteralSets<C>);
 146
 147 #[derive(Clone, Debug, PartialEq, Eq)]
 148 enum InnerDelayedLiteralSets<C: Context> {
 149     /// Corresponds to a single, empty set.
 150     None,
 151
 152     /// Some (non-zero) number of non-empty sets.
 153     /// Must be a set of sets, but HashSets are not Hash so we manually ensure uniqueness.
 154     Some(Vec<DelayedLiteralSet<C>>),
 155 }
 156
 157 /// A set of delayed literals.
 158 ///
 159 /// (One might expect delayed literals to always be ground, since
 160 /// non-ground negative literals result in flounded
 161 /// executions. However, due to the approximations introduced via RR
 162 /// to ensure termination, it *is* in fact possible for delayed goals
 163 /// to contain free variables. For example, what could happen is that
 164 /// we get back an approximated answer with `Goal::CannotProve` as a
 165 /// delayed literal, which in turn forces its subgoal to be delayed,
 166 /// and so forth. Therefore, we store canonicalized goals.)
 167 #[derive(Clone, Debug, Default)]
 168 struct DelayedLiteralSet<C: Context> {
 169     delayed_literals: FxHashSet<DelayedLiteral<C>>,
 170 }
 171
 172 #[derive(Clone, Debug)]
 173 pub enum DelayedLiteral<C: Context> {
 174     /// Something which can never be proven nor disproven. Inserted
 175     /// when truncation triggers; doesn't arise normally.
 176     CannotProve(()),
 177
 178     /// We are blocked on a negative literal `~G`, where `G` is the
 179     /// goal of the given table. Because negative goals must always be
 180     /// ground, we don't need any other information.
 181     Negative(TableIndex),
 182
 183     /// We are blocked on a positive literal `Li`; we found a
 184     /// **conditional** answer (the `CanonicalConstrainedSubst`) within the
 185     /// given table, but we have to come back later and see whether
 186     /// that answer turns out to be true.
 187     Positive(TableIndex, C::CanonicalConstrainedSubst),
 188 }
 189
 190 /// Either `A` or `~A`, where `A` is a `Env |- Goal`.
 191 #[derive(Clone, Debug)]
 192 pub enum Literal<C: Context> { // FIXME: pub b/c fold
 193     Positive(C::GoalInEnvironment),
 194     Negative(C::GoalInEnvironment),
 195 }
 196
 197 /// The `Minimums` structure is used to track the dependencies between
 198 /// some item E on the evaluation stack. In particular, it tracks
 199 /// cases where the success of E depends (or may depend) on items
 200 /// deeper in the stack than E (i.e., with lower DFNs).
 201 ///
 202 /// `positive` tracks the lowest index on the stack to which we had a
 203 /// POSITIVE dependency (e.g. `foo(X) :- bar(X)`) -- meaning that in
 204 /// order for E to succeed, the dependency must succeed. It is
 205 /// initialized with the index of the predicate on the stack. So
 206 /// imagine we have a stack like this:
 207 ///
 208 ///     // 0 foo(X)   <-- bottom of stack
 209 ///     // 1 bar(X)
 210 ///     // 2 baz(X)   <-- top of stack
 211 ///
 212 /// In this case, `positive` would be initially 0, 1, and 2 for `foo`,
 213 /// `bar`, and `baz` respectively. This reflects the fact that the
 214 /// answers for `foo(X)` depend on the answers for `foo(X)`. =)
 215 ///
 216 /// Now imagine that we had a clause `baz(X) :- foo(X)`, inducing a
 217 /// cycle. In this case, we would update `positive` for `baz(X)` to be
 218 /// 0, reflecting the fact that its answers depend on the answers for
 219 /// `foo(X)`. Similarly, the minimum for `bar` would (eventually) be
 220 /// updated, since it too transitively depends on `foo`. `foo` is
 221 /// unaffected.
 222 ///
 223 /// `negative` tracks the lowest index on the stack to which we had a
 224 /// NEGATIVE dependency (e.g., `foo(X) :- not { bar(X) }`) -- meaning
 225 /// that for E to succeed, the dependency must fail. This is initially
 226 /// `usize::MAX`, reflecting the fact that the answers for `foo(X)` do
 227 /// not depend on `not(foo(X))`. When negative cycles are encountered,
 228 /// however, this value must be updated.
 229 #[derive(Copy, Clone, Debug)]
 230 struct Minimums {
 231     positive: DepthFirstNumber,
 232     negative: DepthFirstNumber,
 233 }
 234
 235 impl<C: Context> DelayedLiteralSets<C> {
 236     fn singleton(set: DelayedLiteralSet<C>) -> Self {
 237         if set.is_empty() {
 238             DelayedLiteralSets(InnerDelayedLiteralSets::None)
 239         } else {
 240             DelayedLiteralSets(InnerDelayedLiteralSets::Some(vec![set]))
 241         }
 242     }
 243
 244     /// Inserts the set if it is minimal in the family.
 245     /// Returns true iff the set was inserted.
 246     fn insert_if_minimal(&mut self, set: &DelayedLiteralSet<C>) -> bool {
 247         match self.0 {
 248             // The empty set is always minimal.
 249             InnerDelayedLiteralSets::None => false,
 250             // Are we inserting an empty set?
 251             InnerDelayedLiteralSets::Some(_) if set.is_empty() => {
 252                 self.0 = InnerDelayedLiteralSets::None;
 253                 true
 254             }
 255             InnerDelayedLiteralSets::Some(ref mut sets) => {
 256                 // Look for a subset.
 257                 if sets.iter().any(|set| set.is_subset(&set)) {
 258                     false
 259                 } else {
 260                     // No subset therefore `set` is minimal, discard supersets and insert.
 261                     sets.retain(|set| !set.is_subset(set));
 262                     sets.push(set.clone());
 263                     true
 264                 }
 265             }
 266         }
 267     }
 268 }
 269
 270 impl<C: Context> DelayedLiteralSet<C> {
 271     fn is_empty(&self) -> bool {
 272         self.delayed_literals.is_empty()
 273     }
 274
 275     fn is_subset(&self, other: &DelayedLiteralSet<C>) -> bool {
 276         self.delayed_literals
 277             .iter()
 278             .all(|elem| other.delayed_literals.contains(elem))
 279     }
 280 }
 281
 282 impl Minimums {
 283     const MAX: Minimums = Minimums {
 284         positive: DepthFirstNumber::MAX,
 285         negative: DepthFirstNumber::MAX,
 286     };
 287
 288     /// Update our fields to be the minimum of our current value
 289     /// and the values from other.
 290     fn take_minimums(&mut self, other: &Minimums) {
 291         self.positive = min(self.positive, other.positive);
 292         self.negative = min(self.negative, other.negative);
 293     }
 294
 295     fn minimum_of_pos_and_neg(&self) -> DepthFirstNumber {
 296         min(self.positive, self.negative)
 297     }
 298 }
 299
 300 impl DepthFirstNumber {
 301     const MIN: DepthFirstNumber = DepthFirstNumber { value: 0 };
 302     const MAX: DepthFirstNumber = DepthFirstNumber {
 303         value: ::std::u64::MAX,
 304     };
 305
 306     fn next(&mut self) -> DepthFirstNumber {
 307         let value = self.value;
 308         assert!(value < ::std::u64::MAX);
 309         self.value += 1;
 310         DepthFirstNumber { value }
 311     }
 312 }
 313
 314 /// Because we recurse so deeply, we rely on stacker to
 315 /// avoid overflowing the stack.
 316 #[cfg(feature = "stack_protection")]
 317 fn maybe_grow_stack<F, R>(op: F) -> R
 318 where
 319     F: FnOnce() -> R,
 320 {
 321     // These numbers are somewhat randomly chosen to make tests work
 322     // well enough on my system. In particular, because we only test
 323     // for growing the stack in `new_clause`, a red zone of 32K was
 324     // insufficient to prevent stack overflow. - nikomatsakis
 325     stacker::maybe_grow(256 * 1024, 2 * 1024 * 1024, op)
 326 }
 327
 328 #[cfg(not(feature = "stack_protection"))]
 329 fn maybe_grow_stack<F, R>(op: F) -> R
 330 where
 331     F: FnOnce() -> R,
 332 {
 333     op()
 334 }