diff options
Diffstat (limited to 'vendor/chalk-engine')
| -rw-r--r-- | vendor/chalk-engine/.cargo-checksum.json | 1 | ||||
| -rw-r--r-- | vendor/chalk-engine/Cargo.toml | 48 | ||||
| -rw-r--r-- | vendor/chalk-engine/README.md | 3 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/README.md | 405 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/context.rs | 72 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/derived.rs | 34 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/forest.rs | 116 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/lib.rs | 334 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/logic.rs | 1648 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/normalize_deep.rs | 172 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/simplify.rs | 141 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/slg.rs | 378 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/slg/aggregate.rs | 642 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/slg/resolvent.rs | 729 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/solve.rs | 89 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/stack.rs | 175 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/strand.rs | 50 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/table.rs | 173 | ||||
| -rw-r--r-- | vendor/chalk-engine/src/tables.rs | 72 |
19 files changed, 0 insertions, 5282 deletions
diff --git a/vendor/chalk-engine/.cargo-checksum.json b/vendor/chalk-engine/.cargo-checksum.json deleted file mode 100644 index 62892242b..000000000 --- a/vendor/chalk-engine/.cargo-checksum.json +++ /dev/null @@ -1 +0,0 @@ -{"files":{"Cargo.toml":"94f6635bf5c8c722968aa645a87788dbc784f776008bf048ebab99e421a250a3","README.md":"d8d9a21a6700b554e110030288fb94ca98fa6c6398fa6a5a1dafa52b3f7dd545","src/README.md":"6606b446db6a271e99f1019cd6e59a44af50e7b1ee995718d30fde11c09bbc80","src/context.rs":"89dcf1a74cb22604f32265bcce7f93376cf299101337368d0191f4d1cd598de7","src/derived.rs":"a59fe981325e664865bf21407e4a24e317b00cc2545b380d1140b4fddc86ede3","src/forest.rs":"d6d59557b8ff4fbdcdd3474d214b6e455993996224a14773929ee0e295c02984","src/lib.rs":"3b3e9fd0210471f42d1d1a405877aa248dcf6194099461637cfdce7bed07000b","src/logic.rs":"45747ba7d9a7b14f8c652659ac2e31854f962c613346c23ba55b972fdd548c75","src/normalize_deep.rs":"3fb8ab2f1e2bd2c65b739f57d1b18175205bdba30dee8c04033180cb9ea4d975","src/simplify.rs":"fbc006c2974dfef17d8849b6cd21b9510805bafce1217721eb43479cf02572d1","src/slg.rs":"2fbdce2aaebe3342f3af5d7b4ccbdef969009c0e0d302c9201bf30b7efb1ae5f","src/slg/aggregate.rs":"52b51f86e837b8219bb84935f870d47f6c5c0c1765cfea3e32a75b1055fa0761","src/slg/resolvent.rs":"5edb5247e842379313b4162bf07c7417d5b2453a40ed38ceabaa97e111e24230","src/solve.rs":"ed054d4a9b132fa8c5a6ff1c8c4a435207412eaee30fc992ed0d4a668543584c","src/stack.rs":"0eb11b6f40575aff6784ab10d5f027a9e52ee05e818d7c77fdccf9a59fd18a60","src/strand.rs":"c7f3b68ba182f046112c100c4d2192f3928f4d5c3bf63c39ae29393741da520a","src/table.rs":"253197ca4a700cdc8132e04171a00603c65d5db6794e7779073a8412131dd7cf","src/tables.rs":"c140ea3b7ada35c097f578dc81873164c2c36f41adfb5f7d0d71cd9978974a23"},"package":"7e54ac43048cb31c470d7b3e3acd409090ef4a5abddfe02455187aebc3d6879f"}
\ No newline at end of file diff --git a/vendor/chalk-engine/Cargo.toml b/vendor/chalk-engine/Cargo.toml deleted file mode 100644 index 7497cac9e..000000000 --- a/vendor/chalk-engine/Cargo.toml +++ /dev/null @@ -1,48 +0,0 @@ -# THIS FILE IS AUTOMATICALLY GENERATED BY CARGO -# -# When uploading crates to the registry Cargo will automatically -# "normalize" Cargo.toml files for maximal compatibility -# with all versions of Cargo and also rewrite `path` dependencies -# to registry (e.g., crates.io) dependencies. -# -# If you are reading this file be aware that the original Cargo.toml -# will likely look very different (and much more reasonable). -# See Cargo.toml.orig for the original contents. - -[package] -edition = "2018" -name = "chalk-engine" -version = "0.87.0" -authors = [ - "Rust Compiler Team", - "Chalk developers", -] -description = "Core trait engine from Chalk project" -readme = "README.md" -keywords = [ - "compiler", - "traits", - "prolog", -] -license = "MIT OR Apache-2.0" -repository = "https://github.com/rust-lang/chalk" - -[dependencies.chalk-derive] -version = "=0.87.0" - -[dependencies.chalk-ir] -version = "=0.87.0" - -[dependencies.chalk-solve] -version = "=0.87.0" - -[dependencies.rustc-hash] -version = "1.1.0" - -[dependencies.tracing] -version = "0.1" - -[dev-dependencies] - -[features] -default = [] diff --git a/vendor/chalk-engine/README.md b/vendor/chalk-engine/README.md deleted file mode 100644 index b396aa456..000000000 --- a/vendor/chalk-engine/README.md +++ /dev/null @@ -1,3 +0,0 @@ -The core crate for Chalk. - -See [Github](https://github.com/rust-lang/chalk) for up-to-date information. diff --git a/vendor/chalk-engine/src/README.md b/vendor/chalk-engine/src/README.md deleted file mode 100644 index b7cf2d453..000000000 --- a/vendor/chalk-engine/src/README.md +++ /dev/null @@ -1,405 +0,0 @@ -# The on-demand SLG solver - -The basis of the solver is the `Forest` type. A *forest* stores a -collection of *tables* as well as a *stack*. Each *table* represents -the stored results of a particular query that is being performed, as -well as the various *strands*, which are basically suspended -computations that may be used to find more answers. Tables are -interdependent: solving one query may require solving others. - -## Walkthrough - -Perhaps the easiest way to explain how the solver works is to walk -through an example. Let's imagine that we have the following program: - -```rust -trait Debug { } - -struct u32 { } -impl Debug for u32 { } - -struct Rc<T> { } -impl<T: Debug> Debug for Rc<T> { } - -struct Vec<T> { } -impl<T: Debug> Debug for Vec<T> { } -``` - -Now imagine that we want to find answers for the query `exists<T> { -Rc<T>: Debug }`. The first step would be to u-canonicalize this query; this -is the act of giving canonical names to all the unbound inference variables based on the -order of their left-most appearance, as well as canonicalizing the universes of any -universally bound names (e.g., the `T` in `forall<T> { ... }`). In this case, there are no -universally bound names, but the canonical form Q of the query might look something like: - - Rc<?0>: Debug - -where `?0` is a variable in the root universe U0. We would then go and -look for a table with this as the key: since the forest is empty, this -lookup will fail, and we will create a new table T0, corresponding to -the u-canonical goal Q. - -### Ignoring negative reasoning and regions - -To start, we'll ignore the possibility of negative goals like `not { -Foo }`. We'll phase them in later, as they bring several -complications. - -### Creating a table - -When we first create a table, we also initialize it with a set of -*initial strands*. A "strand" is kind of like a "thread" for the -solver: it contains a particular way to produce an answer. The initial -set of strands for a goal like `Rc<?0>: Debug` (i.e., a "domain goal") -is determined by looking for *clauses* in the environment. In Rust, -these clauses derive from impls, but also from where-clauses that are -in scope. In the case of our example, there would be three clauses, -each coming from the program. Using a Prolog-like notation, these look -like: - -``` -(u32: Debug). -(Rc<T>: Debug) :- (T: Debug). -(Vec<T>: Debug) :- (T: Debug). -``` - -To create our initial strands, then, we will try to apply each of -these clauses to our goal of `Rc<?0>: Debug`. The first and third -clauses are inapplicable because `u32` and `Vec<?0>` cannot be unified -with `Rc<?0>`. The second clause, however, will work. - -### What is a strand? - -Let's talk a bit more about what a strand *is*. In the code, a strand -is the combination of an inference table, an X-clause, and (possibly) -a selected subgoal from that X-clause. But what is an X-clause -(`ExClause`, in the code)? An X-clause pulls together a few things: - -- The current state of the goal we are trying to prove; -- A set of subgoals that have yet to be proven; -- A set of floundered subgoals (see the section on floundering below); -- There are also a few things we're ignoring for now: - - delayed literals, region constraints - -The general form of an X-clause is written much like a Prolog clause, -but with somewhat different semantics. Since we're ignoring delayed -literals and region constraints, an X-clause just looks like this: - - G :- L - -where G is a goal and L is a set of subgoals that must be proven. -(The L stands for *literal* -- when we address negative reasoning, a -literal will be either a positive or negative subgoal.) The idea is -that if we are able to prove L then the goal G can be considered true. - -In the case of our example, we would wind up creating one strand, with -an X-clause like so: - - (Rc<?T>: Debug) :- (?T: Debug) - -Here, the `?T` refers to one of the inference variables created in the -inference table that accompanies the strand. (I'll use named variables -to refer to inference variables, and numbered variables like `?0` to -refer to variables in a canonicalized goal; in the code, however, they -are both represented with an index.) - -For each strand, we also optionally store a *selected subgoal*. This -is the subgoal after the turnstile (`:-`) that we are currently trying -to prove in this strand. Initially, when a strand is first created, -there is no selected subgoal. - -### Activating a strand - -Now that we have created the table T0 and initialized it with strands, -we have to actually try and produce an answer. We do this by invoking -the `ensure_answer` operation on the table: specifically, we say -`ensure_answer(T0, A0)`, meaning "ensure that there is a 0th answer". - -Remember that tables store not only strands, but also a vector of -cached answers. The first thing that `ensure_answer` does is to check -whether answer 0 is in this vector. If so, we can just return -immediately. In this case, the vector will be empty, and hence that -does not apply (this becomes important for cyclic checks later on). - -When there is no cached answer, `ensure_answer` will try to produce -one. It does this by selecting a strand from the set of active -strands -- the strands are stored in a `VecDeque` and hence processed -in a round-robin fashion. Right now, we have only one strand, storing -the following X-clause with no selected subgoal: - - (Rc<?T>: Debug) :- (?T: Debug) - -When we activate the strand, we see that we have no selected subgoal, -and so we first pick one of the subgoals to process. Here, there is only -one (`?T: Debug`), so that becomes the selected subgoal, changing -the state of the strand to: - - (Rc<?T>: Debug) :- selected(?T: Debug, A0) - -Here, we write `selected(L, An)` to indicate that (a) the literal `L` -is the selected subgoal and (b) which answer `An` we are looking for. We -start out looking for `A0`. - -### Processing the selected subgoal - -Next, we have to try and find an answer to this selected goal. To do -that, we will u-canonicalize it and try to find an associated -table. In this case, the u-canonical form of the subgoal is `?0: -Debug`: we don't have a table yet for that, so we can create a new -one, T1. As before, we'll initialize T1 with strands. In this case, -there will be three strands, because all the program clauses are -potentially applicable. Those three strands will be: - -- `(u32: Debug) :-`, derived from the program clause `(u32: Debug).`. - - Note: This strand has no subgoals. -- `(Vec<?U>: Debug) :- (?U: Debug)`, derived from the `Vec` impl. -- `(Rc<?U>: Debug) :- (?U: Debug)`, derived from the `Rc` impl. - -We can thus summarize the state of the whole forest at this point as -follows: - -``` -Table T0 [Rc<?0>: Debug] - Strands: - (Rc<?T>: Debug) :- selected(?T: Debug, A0) - -Table T1 [?0: Debug] - Strands: - (u32: Debug) :- - (Vec<?U>: Debug) :- (?U: Debug) - (Rc<?V>: Debug) :- (?V: Debug) -``` - -### Delegation between tables - -Now that the active strand from T0 has created the table T1, it can -try to extract an answer. It does this via that same `ensure_answer` -operation we saw before. In this case, the strand would invoke -`ensure_answer(T1, A0)`, since we will start with the first -answer. This will cause T1 to activate its first strand, `u32: Debug -:-`. - -This strand is somewhat special: it has no subgoals at all. This means -that the goal is proven. We can therefore add `u32: Debug` to the set -of *answers* for our table, calling it answer A0 (it is the first -answer). The strand is then removed from the list of strands. - -The state of table T1 is therefore: - -``` -Table T1 [?0: Debug] - Answers: - A0 = [?0 = u32] - Strand: - (Vec<?U>: Debug) :- (?U: Debug) - (Rc<?V>: Debug) :- (?V: Debug) -``` - -Note that I am writing out the answer A0 as a substitution that can be -applied to the table goal; actually, in the code, the goals for each -X-clause are also represented as substitutions, but in this exposition -I've chosen to write them as full goals, following NFTD. - -Since we now have an answer, `ensure_answer(T1, A0)` will return `Ok` -to the table T0, indicating that answer A0 is available. T0 now has -the job of incorporating that result into its active strand. It does -this in two ways. First, it creates a new strand that is looking for -the next possible answer of T1. Next, it incorporates the answer from -A0 and removes the subgoal. The resulting state of table T0 is: - -``` -Table T0 [Rc<?0>: Debug] - Strands: - (Rc<?T>: Debug) :- selected(?T: Debug, A1) - (Rc<u32>: Debug) :- -``` - -We then immediately activate the strand that incorporated the answer -(the `Rc<u32>: Debug` one). In this case, that strand has no further -subgoals, so it becomes an answer to the table T0. This answer can -then be returned up to our caller, and the whole forest goes quiescent -at this point (remember, we only do enough work to generate *one* -answer). The ending state of the forest at this point will be: - -``` -Table T0 [Rc<?0>: Debug] - Answer: - A0 = [?0 = u32] - Strands: - (Rc<?T>: Debug) :- selected(?T: Debug, A1) - -Table T1 [?0: Debug] - Answers: - A0 = [?0 = u32] - Strand: - (Vec<?U>: Debug) :- (?U: Debug) - (Rc<?V>: Debug) :- (?V: Debug) -``` - -Here you can see how the forest captures both the answers we have -created thus far *and* the strands that will let us try to produce -more answers later on. - -### Floundering - -The first thing we do when we create a table is to initialize it with -a set of strands. These strands represent all the ways that one can -solve the table's associated goal. For an ordinary trait, we would -effectively create one strand per "relevant impl". But sometimes the -goals are too vague for this to be possible; other times, it may be possible -but just really inefficient, since all of those strands must be explored. - -As an example of when it may not be possible, consider a goal like -`?T: Sized`. This goal can in principle enumerate **every sized type** -that exists -- that includes not only struct/enum types, but also -closure types, fn types with arbitrary arity, tuple types with -arbitrary arity, and so forth. In other words, there are not only an -infinite set of **answers** but actually an infinite set of -**strands**. The same applies to auto traits like `Send` as well as -"hybrid" traits like `Clone`, which contain *some* auto-generated sets -of impls. - -Another example of floundering comes from negative logic. In general, -we cannot process negative subgoals if they have unbound existential -variables, such as `not { Vec<?T>: Foo }`. This is because we can only -enumerate things that *do* match a given trait (or which *are* -provable, more generally). We cannot enumerate out possible types `?T` -that *are not* provable (there is an infinite set, to be sure). - -To handle this, we allow tables to enter a **floundered** state. This -state begins when we try to create the program clauses for a table -- -if that is not possible (e.g., in one of the cases above) then the -table enters a floundered state. Attempts to get an answer from a -floundered table result in an error (e.g., -`RecursiveSearchFail::Floundered`). - -Whenever a goal results in a floundered result, that goal is placed -into a distinct list (the "floundered subgoals"). We then go on and -process the rest of the subgoals. Once all the normal subgoals have -completed, floundered subgoals are removed from the floundered list -and re-attempted: the idea is that we may have accumulated more type -information in the meantime. If they continue to flounder, then we -stop. - -Let's look at an example. Imagine that we have: - -```rust -trait Foo { } -trait Bar { } - -impl<T: Send + Bar> Foo for T { } - -impl Bar for u32 { } -impl Bar for i32 { } -``` - -Now imagine we are trying to prove `?T: Foo`. There is only one impl, -so we will create a state like: - -``` -(?T: Foo) :- (?T: Send), (?T: Bar) -``` - -When we attempt to solve `?T: Send`, however, that subgoal will -flounder, because `Send` is an auto-trait. So it will be put into a -floundered list: - -``` -(?T: Foo) :- (?T: Bar) [ floundered: (?T: Send) ] -``` - -and we will go on to solve `?T: Bar`. `Bar` is an ordinary trait -- so -we can enumerate two strands (one for `u32` and one for `i32`). When -we process the first answer, we wind up with: - -``` -(u32: Foo) :- [ floundered: (u32: Send) ] -``` - -At this point we can move the floundered subgoal back into the main -list and process: - -``` -(u32: Foo) :- (u32: Send) -``` - -This time, the goal does not flounder. - -But how do we detect when it makes sense to move a floundered subgoal -into the main list? To handle this, we use a timestamp scheme. We -keep a counter as part of the strand -- each time we succeed in -solving some subgoal, we increment the counter, as that *may* have -provided more information about some type variables. When we move a -goal to the floundered list, we also track the current value of the -timestamp. Then, when it comes time to move things *from* the -floundered list, we can compare if the timestamp has been changed -since the goal was marked as floundering. If not, then no new -information can have been attempted, and we can mark the current table -as being floundered itself. - -This mechanism allows floundered to propagate up many levels, e.g. -in an example like this: - -```rust -trait Foo { } -trait Bar { } -trait Baz { } - -impl<T: Baz + Bar> Foo for T { } - -impl Bar for u32 { } -impl Bar for i32 { } - -impl<T: Sized> Baz for T { } -``` - -Here, solving `?T: Baz` will in turn invoke `?T: Sized` -- this -floundering state will be propagated up to the `?T: Foo` table. - -## Heritage and acronyms - -This solver implements the SLG solving technique, though extended to -accommodate hereditary harrop (HH) predicates, as well as the needs of -lazy normalization. - -Its design is kind of a fusion of [MiniKanren] and the following -papers, which I will refer to as EWFS and NTFD respectively: - -> Efficient Top-Down Computation of Queries Under the Well-formed Semantics -> (Chen, Swift, and Warren; Journal of Logic Programming '95) - -> A New Formulation of Tabled resolution With Delay -> (Swift; EPIA '99) - -[MiniKanren]: http://minikanren.org/ - -In addition, I incorporated extensions from the following papers, -which I will refer to as SA and RR respectively, that describes how to -do introduce approximation when processing subgoals and so forth: - -> Terminating Evaluation of Logic Programs with Finite Three-Valued Models -> Riguzzi and Swift; ACM Transactions on Computational Logic 2013 -> (Introduces "subgoal abstraction", hence the name SA) -> -> Radial Restraint -> Grosof and Swift; 2013 - -Another useful paper that gives a kind of high-level overview of -concepts at play is the following: - -> XSB: Extending Prolog with Tabled Logic Programming -> (Swift and Warren; Theory and Practice of Logic Programming '10) - -There are a places where I intentionally diverged from the semantics -as described in the papers -- e.g. by more aggressively approximating --- which I marked them with a comment DIVERGENCE. Those places may -want to be evaluated in the future. - -A few other acronyms that I use: - -- WAM: Warren abstract machine, an efficient way to evaluate Prolog programs. - See <http://wambook.sourceforge.net/>. -- HH: Hereditary harrop predicates. What Chalk deals in. - Popularized by Lambda Prolog. - - diff --git a/vendor/chalk-engine/src/context.rs b/vendor/chalk-engine/src/context.rs deleted file mode 100644 index fa418dfd4..000000000 --- a/vendor/chalk-engine/src/context.rs +++ /dev/null @@ -1,72 +0,0 @@ -//! Defines traits used to embed the chalk-engine in another crate. -//! -//! chalk and rustc both define types which implement the traits in this -//! module. This allows each user of chalk-engine to define their own -//! `DomainGoal` type, add arena lifetime parameters, and more. See -//! [`Context`] trait for a list of types. - -use crate::CompleteAnswer; -use chalk_ir::interner::Interner; -use chalk_ir::Substitution; -use std::fmt::Debug; - -pub enum AnswerResult<I: Interner> { - /// The next available answer. - Answer(CompleteAnswer<I>), - - /// No answer could be returned because there are no more solutions. - NoMoreSolutions, - - /// No answer could be returned because the goal has floundered. - Floundered, - - // No answer could be returned *yet*, because we exceeded our - // quantum (`should_continue` returned false). - QuantumExceeded, -} - -impl<I: Interner> AnswerResult<I> { - pub fn is_answer(&self) -> bool { - matches!(self, Self::Answer(_)) - } - - pub fn answer(self) -> CompleteAnswer<I> { - match self { - Self::Answer(answer) => answer, - _ => panic!("Not an answer."), - } - } - - pub fn is_no_more_solutions(&self) -> bool { - matches!(self, Self::NoMoreSolutions) - } - - pub fn is_quantum_exceeded(&self) -> bool { - matches!(self, Self::QuantumExceeded) - } -} - -impl<I: Interner> Debug for AnswerResult<I> { - fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - match self { - AnswerResult::Answer(answer) => write!(fmt, "{:?}", answer), - AnswerResult::Floundered => write!(fmt, "Floundered"), - AnswerResult::NoMoreSolutions => write!(fmt, "None"), - AnswerResult::QuantumExceeded => write!(fmt, "QuantumExceeded"), - } - } -} - -pub trait AnswerStream<I: Interner> { - /// Gets the next answer for a given goal, but doesn't increment the answer index. - /// Calling this or `next_answer` again will give the same answer. - fn peek_answer(&mut self, should_continue: impl Fn() -> bool) -> AnswerResult<I>; - - /// Gets the next answer for a given goal, incrementing the answer index. - /// Calling this or `peek_answer` again will give the next answer. - fn next_answer(&mut self, should_continue: impl Fn() -> bool) -> AnswerResult<I>; - - /// Invokes `test` with each possible future answer, returning true immediately - /// if we find any answer for which `test` returns true. - fn any_future_answer(&self, test: impl Fn(&Substitution<I>) -> bool) -> bool; -} diff --git a/vendor/chalk-engine/src/derived.rs b/vendor/chalk-engine/src/derived.rs deleted file mode 100644 index b3cdc3d0d..000000000 --- a/vendor/chalk-engine/src/derived.rs +++ /dev/null @@ -1,34 +0,0 @@ -// These impls for PartialEq, Eq, etc are written by hand. This is -// because the `#[derive()]` would add requirements onto the context -// object that are not needed. - -use super::*; -use std::cmp::{Eq, PartialEq}; -use std::hash::{Hash, Hasher}; -use std::mem; - -/////////////////////////////////////////////////////////////////////////// - -impl<I: Interner> PartialEq for Literal<I> { - fn eq(&self, other: &Literal<I>) -> bool { - match (self, other) { - (Literal::Positive(goal1), Literal::Positive(goal2)) - | (Literal::Negative(goal1), Literal::Negative(goal2)) => goal1 == goal2, - - _ => false, - } - } -} - -impl<I: Interner> Eq for Literal<I> {} - -impl<I: Interner> Hash for Literal<I> { - fn hash<H: Hasher>(&self, state: &mut H) { - mem::discriminant(self).hash(state); - match self { - Literal::Positive(goal) | Literal::Negative(goal) => { - goal.hash(state); - } - } - } -} diff --git a/vendor/chalk-engine/src/forest.rs b/vendor/chalk-engine/src/forest.rs deleted file mode 100644 index 410b9cd0a..000000000 --- a/vendor/chalk-engine/src/forest.rs +++ /dev/null @@ -1,116 +0,0 @@ -use crate::context::{AnswerResult, AnswerStream}; -use crate::logic::RootSearchFail; -use crate::slg::SlgContextOps; -use crate::table::AnswerIndex; -use crate::tables::Tables; -use crate::{TableIndex, TimeStamp}; - -use chalk_ir::interner::Interner; -use chalk_ir::{Goal, InEnvironment, Substitution, UCanonical}; -use tracing::debug; - -pub(crate) struct Forest<I: Interner> { - pub(crate) tables: Tables<I>, - - /// This is a clock which always increases. It is - /// incremented every time a new subgoal is followed. - /// This effectively gives us way to track what depth - /// and loop a table or strand was last followed. - pub(crate) clock: TimeStamp, -} - -impl<I: Interner> Forest<I> { - pub fn new() -> Self { - Forest { - tables: Tables::new(), - clock: TimeStamp::default(), - } - } - - // Gets the next clock TimeStamp. This will never decrease. - pub(crate) fn increment_clock(&mut self) -> TimeStamp { - self.clock.increment(); - self.clock - } - - /// Returns a "solver" for a given goal in the form of an - /// iterator. Each time you invoke `next`, it will do the work to - /// extract one more answer. These answers are cached in between - /// invocations. Invoking `next` fewer times is preferable =) - pub fn iter_answers<'f>( - &'f mut self, - context: &'f SlgContextOps<'f, I>, - goal: &UCanonical<InEnvironment<Goal<I>>>, - ) -> impl AnswerStream<I> + 'f { - let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone()); - let answer = AnswerIndex::ZERO; - ForestSolver { - forest: self, - context, - table, - answer, - } - } -} - -struct ForestSolver<'me, I: Interner> { - forest: &'me mut Forest<I>, - context: &'me SlgContextOps<'me, I>, - table: TableIndex, - answer: AnswerIndex, -} - -impl<'me, I: Interner> AnswerStream<I> for ForestSolver<'me, I> { - /// # Panics - /// - /// Panics if a negative cycle was detected. - fn peek_answer(&mut self, should_continue: impl Fn() -> bool) -> AnswerResult<I> { - loop { - match self - .forest - .root_answer(self.context, self.table, self.answer) - { - Ok(answer) => { - debug!(answer = ?(&answer)); - return AnswerResult::Answer(answer); - } - - Err(RootSearchFail::InvalidAnswer) => { - self.answer.increment(); - } - Err(RootSearchFail::Floundered) => { - return AnswerResult::Floundered; - } - - Err(RootSearchFail::NoMoreSolutions) => { - return AnswerResult::NoMoreSolutions; - } - - Err(RootSearchFail::QuantumExceeded) => { - if !should_continue() { - return AnswerResult::QuantumExceeded; - } - } - - Err(RootSearchFail::NegativeCycle) => { - // Negative cycles *ought* to be avoided by construction. Hence panic - // if we find one, as that likely indicates a problem in the chalk-solve - // lowering rules. (In principle, we could propagate this error out, - // and let chalk-solve do the asserting, but that seemed like it would - // complicate the function signature more than it's worth.) - panic!("negative cycle was detected"); - } - } - } - } - - fn next_answer(&mut self, should_continue: impl Fn() -> bool) -> AnswerResult<I> { - let answer = self.peek_answer(should_continue); - self.answer.increment(); - answer - } - - fn any_future_answer(&self, test: impl Fn(&Substitution<I>) -> bool) -> bool { - self.forest.any_future_answer(self.table, self.answer, test) - } -} diff --git a/vendor/chalk-engine/src/lib.rs b/vendor/chalk-engine/src/lib.rs deleted file mode 100644 index f139f5cc0..000000000 --- a/vendor/chalk-engine/src/lib.rs +++ /dev/null @@ -1,334 +0,0 @@ -//! An alternative solver based around the SLG algorithm, which -//! implements the well-formed semantics. For an overview of how the solver -//! works, see [The On-Demand SLG Solver][guide] in the chalk book. -//! -//! [guide]: https://rust-lang.github.io/chalk/book/engine/slg.html -//! -//! This algorithm is very closed based on the description found in the -//! following paper, which I will refer to in the comments as EWFS: -//! -//! > Efficient Top-Down Computation of Queries Under the Well-founded Semantics -//! > (Chen, Swift, and Warren; Journal of Logic Programming '95) -//! -//! However, to understand that paper, I would recommend first -//! starting with the following paper, which I will refer to in the -//! comments as NFTD: -//! -//! > A New Formulation of Tabled resolution With Delay -//! > (Swift; EPIA '99) -//! -//! In addition, I incorporated extensions from the following papers, -//! which I will refer to as SA and RR respectively, that -//! describes how to do introduce approximation when processing -//! subgoals and so forth: -//! -//! > Terminating Evaluation of Logic Programs with Finite Three-Valued Models -//! > Riguzzi and Swift; ACM Transactions on Computational Logic 2013 -//! > (Introduces "subgoal abstraction", hence the name SA) -//! > -//! > Radial Restraint -//! > Grosof and Swift; 2013 -//! -//! Another useful paper that gives a kind of high-level overview of -//! concepts at play is the following, which I will refer to as XSB: -//! -//! > XSB: Extending Prolog with Tabled Logic Programming -//! > (Swift and Warren; Theory and Practice of Logic Programming '10) -//! -//! While this code is adapted from the algorithms described in those -//! papers, it is not the same. For one thing, the approaches there -//! had to be extended to our context, and in particular to coping -//! with hereditary harrop predicates and our version of unification -//! (which produces subgoals). I believe those to be largely faithful -//! extensions. However, there are some other places where I -//! intentionally diverged from the semantics as described in the -//! papers -- e.g. by more aggressively approximating -- which I -//! marked them with a comment DIVERGENCE. Those places may want to be -//! evaluated in the future. -//! -//! Glossary of other terms: -//! -//! - WAM: Warren abstract machine, an efficient way to evaluate Prolog programs. -//! See <http://wambook.sourceforge.net/>. -//! - HH: Hereditary harrop predicates. What Chalk deals in. -//! Popularized by Lambda Prolog. - -use std::cmp::min; -use std::usize; - -use chalk_derive::{HasInterner, TypeFoldable, TypeVisitable}; -use chalk_ir::interner::Interner; -use chalk_ir::{ - AnswerSubst, Canonical, ConstrainedSubst, Constraint, DebruijnIndex, Goal, InEnvironment, - Substitution, -}; -use std::ops::ControlFlow; - -pub mod context; -mod derived; -pub mod forest; -mod logic; -mod normalize_deep; -mod simplify; -pub mod slg; -pub mod solve; -mod stack; -mod strand; -mod table; -mod tables; - -index_struct! { - pub struct TableIndex { // FIXME: pub b/c TypeFoldable - value: usize, - } -} - -/// The paper describes these as `A :- D | G`. -#[derive(Clone, Debug, PartialEq, Eq, Hash, TypeFoldable, TypeVisitable, HasInterner)] -pub struct ExClause<I: Interner> { - /// The substitution which, applied to the goal of our table, - /// would yield A. - pub subst: Substitution<I>, - - /// True if any subgoals were depended upon negatively and - /// were not fully evaluated, or if we encountered a `CannotProve` - /// goal. (In the full SLG algorithm, we would use delayed literals here, - /// but we don't bother, as we don't need that support.) - pub ambiguous: bool, - - /// Region constraints we have accumulated. - pub constraints: Vec<InEnvironment<Constraint<I>>>, - - /// Subgoals: literals that must be proven - pub subgoals: Vec<Literal<I>>, - - /// We assume that negative literals cannot have coinductive cycles. - pub delayed_subgoals: Vec<InEnvironment<Goal<I>>>, - - /// Time stamp that is incremented each time we find an answer to - /// some subgoal. This is used to figure out whether any of the - /// floundered subgoals may no longer be floundered: we record the - /// current time when we add something to the list of floundered - /// subgoals, and then we can compare whether its value has - /// changed since then. This is not the same `TimeStamp` of - /// `Forest`'s clock. - pub answer_time: TimeStamp, - - /// List of subgoals that have floundered. See `FlounderedSubgoal` - /// for more information. - pub floundered_subgoals: Vec<FlounderedSubgoal<I>>, -} - -/// The "time stamp" is a simple clock that gets incremented each time -/// we encounter a positive answer in processing a particular -/// strand. This is used as an optimization to help us figure out when -/// we *may* have changed inference variables. -#[derive(Copy, Clone, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct TimeStamp { - clock: u64, -} - -impl TimeStamp { - const MAX: TimeStamp = TimeStamp { - clock: ::std::u64::MAX, - }; - - fn increment(&mut self) { - self.clock += 1; - } -} - -/// A "floundered" subgoal is one that contains unbound existential -/// variables for which it cannot produce a value. The classic example -/// of floundering is a negative subgoal: -/// -/// ```notrust -/// not { Implemented(?T: Foo) } -/// ``` -/// -/// The way the prolog solver works, it basically enumerates all the -/// ways that a given goal can be *true*. But we can't use this -/// technique to find all the ways that `?T: Foo` can be *false* -- so -/// we call it floundered. In other words, we can evaluate a negative -/// goal, but only if we know what `?T` is -- we can't use the -/// negative goal to help us figuring out `?T`. -/// -/// In addition to negative goals, we use floundering to prevent the -/// trait solver from trying to enumerate very large goals with tons -/// of answers. For example, we consider a goal like `?T: Sized` to -/// "flounder", since we can't hope to enumerate all types that are -/// `Sized`. The same is true for other special traits like `Clone`. -/// -/// Floundering can also occur indirectly. For example: -/// -/// ```notrust -/// trait Foo { } -/// impl<T> Foo for T { } -/// ``` -/// -/// trying to solve `?T: Foo` would immediately require solving `?T: -/// Sized`, and hence would flounder. -#[derive(Clone, Debug, PartialEq, Eq, Hash, TypeFoldable, TypeVisitable)] -pub struct FlounderedSubgoal<I: Interner> { - /// Literal that floundered. - pub floundered_literal: Literal<I>, - - /// Current value of the strand's clock at the time of - /// floundering. - pub floundered_time: TimeStamp, -} - -/// An "answer" in the on-demand solver corresponds to a fully solved -/// goal for a particular table (modulo delayed literals). It contains -/// a substitution -#[derive(Clone, Debug)] -pub struct Answer<I: Interner> { - /// Contains values for the unbound inference variables for which - /// the table is true, along with any delayed subgoals (Which must - /// still be proven) and region constrained (which must still be - /// proven, but not by chalk). - pub subst: Canonical<AnswerSubst<I>>, - - /// If this flag is set, then the answer could be neither proven - /// nor disproven. This could be the size of the answer exceeded - /// `max_size` or because of a negative loop (e.g., `P :- not { P }`). - pub ambiguous: bool, -} - -#[derive(Clone, Debug)] -pub struct CompleteAnswer<I: Interner> { - /// Contains values for the unbound inference variables for which - /// the table is true, along with any region constrained (which must still be - /// proven, but not by chalk). - pub subst: Canonical<ConstrainedSubst<I>>, - - /// If this flag is set, then the answer could be neither proven - /// nor disproven. This could be the size of the answer exceeded - /// `max_size` or because of a negative loop (e.g., `P :- not { P }`). - pub ambiguous: bool, -} - -/// Either `A` or `~A`, where `A` is a `Env |- Goal`. -#[derive(Clone, Debug, TypeFoldable, TypeVisitable)] -pub enum Literal<I: Interner> { - // FIXME: pub b/c fold - Positive(InEnvironment<Goal<I>>), - Negative(InEnvironment<Goal<I>>), -} - -/// The `Minimums` structure is used to track the dependencies between -/// some item E on the evaluation stack. In particular, it tracks -/// cases where the success of E depends (or may depend) on items -/// deeper in the stack than E (i.e., with lower DFNs). -/// -/// `positive` tracks the lowest index on the stack to which we had a -/// POSITIVE dependency (e.g. `foo(X) :- bar(X)`) -- meaning that in -/// order for E to succeed, the dependency must succeed. It is -/// initialized with the index of the predicate on the stack. So -/// imagine we have a stack like this: -/// -/// ```notrust -/// // 0 foo(X) <-- bottom of stack -/// // 1 bar(X) -/// // 2 baz(X) <-- top of stack -/// ``` -/// -/// In this case, `positive` would be initially 0, 1, and 2 for `foo`, -/// `bar`, and `baz` respectively. This reflects the fact that the -/// answers for `foo(X)` depend on the answers for `foo(X)`. =) -/// -/// Now imagine that we had a clause `baz(X) :- foo(X)`, inducing a -/// cycle. In this case, we would update `positive` for `baz(X)` to be -/// 0, reflecting the fact that its answers depend on the answers for -/// `foo(X)`. Similarly, the minimum for `bar` would (eventually) be -/// updated, since it too transitively depends on `foo`. `foo` is -/// unaffected. -/// -/// `negative` tracks the lowest index on the stack to which we had a -/// NEGATIVE dependency (e.g., `foo(X) :- not { bar(X) }`) -- meaning -/// that for E to succeed, the dependency must fail. This is initially -/// `usize::MAX`, reflecting the fact that the answers for `foo(X)` do -/// not depend on `not(foo(X))`. When negative cycles are encountered, -/// however, this value must be updated. -#[derive(Copy, Clone, Debug)] -struct Minimums { - positive: TimeStamp, - negative: TimeStamp, -} - -impl Minimums { - const MAX: Minimums = Minimums { - positive: TimeStamp::MAX, - negative: TimeStamp::MAX, - }; - - /// Update our fields to be the minimum of our current value - /// and the values from other. - fn take_minimums(&mut self, other: &Minimums) { - self.positive = min(self.positive, other.positive); - self.negative = min(self.negative, other.negative); - } - - fn minimum_of_pos_and_neg(&self) -> TimeStamp { - min(self.positive, self.negative) - } -} - -#[derive(Copy, Clone, Debug)] -pub(crate) enum AnswerMode { - Complete, - Ambiguous, -} - -chalk_ir::copy_fold!(TableIndex); -chalk_ir::copy_fold!(TimeStamp); - -chalk_ir::const_visit!(TableIndex); -chalk_ir::const_visit!(TimeStamp); - -#[macro_export] -macro_rules! index_struct { - ($(#[$m:meta])* $v:vis struct $n:ident { - $vf:vis value: usize, - }) => { - #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] - $(#[$m])* - $v struct $n { - $vf value: usize, - } - - impl $n { - // Not all index structs need this, so allow it to be dead - // code. - #[allow(dead_code)] - $v fn get_and_increment(&mut self) -> Self { - let old_value = *self; - self.increment(); - old_value - } - - #[allow(dead_code)] - $v fn increment(&mut self) { - self.value += 1; - } - - // 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 - #[allow(dead_code)] - pub fn iterate_range(range: ::std::ops::Range<Self>) -> impl Iterator<Item = $n> { - (range.start.value..range.end.value).into_iter().map(|i| Self { value: i }) - } - } - - impl ::std::fmt::Debug for $n { - fn fmt(&self, fmt: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result { - write!(fmt, "{}({})", stringify!($n), self.value) - } - } - - impl From<usize> for $n { - fn from(value: usize) -> Self { - Self { value } - } - } - } -} diff --git a/vendor/chalk-engine/src/logic.rs b/vendor/chalk-engine/src/logic.rs deleted file mode 100644 index 681f6e7ed..000000000 --- a/vendor/chalk-engine/src/logic.rs +++ /dev/null @@ -1,1648 +0,0 @@ -use crate::forest::Forest; -use crate::normalize_deep::DeepNormalizer; -use crate::slg::{ResolventOps, SlgContext, SlgContextOps}; -use crate::stack::{Stack, StackIndex}; -use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand}; -use crate::table::{AnswerIndex, Table}; -use crate::{ - Answer, AnswerMode, CompleteAnswer, ExClause, FlounderedSubgoal, Literal, Minimums, TableIndex, - TimeStamp, -}; - -use chalk_ir::could_match::CouldMatch; -use chalk_ir::interner::Interner; -use chalk_ir::{ - AnswerSubst, Canonical, ConstrainedSubst, Constraints, FallibleOrFloundered, Floundered, Goal, - GoalData, InEnvironment, NoSolution, ProgramClause, Substitution, UCanonical, UniverseMap, -}; -use chalk_solve::clauses::program_clauses_that_could_match; -use chalk_solve::coinductive_goal::IsCoinductive; -use chalk_solve::infer::ucanonicalize::UCanonicalized; -use chalk_solve::infer::InferenceTable; -use chalk_solve::solve::truncate; -use tracing::{debug, debug_span, info, instrument}; - -type RootSearchResult<T> = Result<T, RootSearchFail>; - -/// The different ways that a *root* search (which potentially pursues -/// many strands) can fail. A root search is one that begins with an -/// empty stack. -#[derive(Debug)] -pub(super) enum RootSearchFail { - /// The table we were trying to solve cannot succeed. - NoMoreSolutions, - - /// The table cannot be solved without more type information. - Floundered, - - /// We did not find a solution, but we still have things to try. - /// Repeat the request, and we'll give one of those a spin. - /// - /// (In a purely depth-first-based solver, like Prolog, this - /// doesn't appear.) - QuantumExceeded, - - /// A negative cycle was found. This is fail-fast, so even if there was - /// possibly a solution (ambiguous or not), it may not have been found. - NegativeCycle, - - /// The current answer index is not useful. Currently, this is returned - /// because the current answer needs refining. - InvalidAnswer, -} - -/// This is returned when we try to select a subgoal for a strand. -#[derive(PartialEq)] -enum SubGoalSelection { - /// A subgoal was successfully selected. It has already been checked - /// to not be floundering. However, it may have an answer already, be - /// coinductive, or create a cycle. - Selected, - - /// This strand has no remaining subgoals, but there may still be - /// floundered subgoals. - NotSelected, -} - -/// This is returned `on_no_remaining_subgoals` -enum NoRemainingSubgoalsResult { - /// There is an answer available for the root table - RootAnswerAvailable, - - /// There was a `RootSearchFail` - RootSearchFail(RootSearchFail), - - // This was a success - Success, -} - -impl<I: Interner> Forest<I> { - /// Returns an answer with a given index for the given table. This - /// may require activating a strand and following it. It returns - /// `Ok(answer)` if they answer is available and otherwise a - /// `RootSearchFail` result. - pub(super) fn root_answer( - &mut self, - context: &SlgContextOps<I>, - table: TableIndex, - answer_index: AnswerIndex, - ) -> RootSearchResult<CompleteAnswer<I>> { - let stack = Stack::default(); - - let mut state = SolveState { - forest: self, - context, - stack, - }; - - match state.ensure_root_answer(table, answer_index) { - Ok(()) => { - assert!(state.stack.is_empty()); - let answer = state.forest.answer(table, answer_index); - if !answer.subst.value.delayed_subgoals.is_empty() { - return Err(RootSearchFail::InvalidAnswer); - } - Ok(CompleteAnswer { - subst: Canonical { - binders: answer.subst.binders.clone(), - value: ConstrainedSubst { - subst: answer.subst.value.subst.clone(), - constraints: answer.subst.value.constraints.clone(), - }, - }, - ambiguous: answer.ambiguous, - }) - } - Err(err) => Err(err), - } - } - - pub(super) fn any_future_answer( - &self, - table: TableIndex, - mut answer_index: AnswerIndex, - mut test: impl FnMut(&Substitution<I>) -> bool, - ) -> bool { - // Check any cached answers, starting at `answer_index`. - while let Some(answer) = self.tables[table].answer(answer_index) { - info!("answer cached = {:?}", answer); - if test(&answer.subst.value.subst) { - return true; - } - answer_index.increment(); - } - - // Check any unsolved strands, which may give further answers. - self.tables[table] - .strands() - .any(|strand| test(&strand.value.ex_clause.subst)) - } - - pub(crate) fn answer(&self, table: TableIndex, answer: AnswerIndex) -> &Answer<I> { - self.tables[table].answer(answer).unwrap() - } - - fn canonicalize_strand_from( - context: &SlgContextOps<I>, - infer: &mut InferenceTable<I>, - strand: &Strand<I>, - ) -> CanonicalStrand<I> { - infer - .canonicalize(context.program().interner(), strand.clone()) - .quantified - } - - /// Given a subgoal, converts the literal into u-canonical form - /// and searches for an existing table. If one is found, it is - /// returned, but otherwise a new table is created (and populated - /// with its initial set of strands). - /// - /// Returns `None` if the literal cannot be converted into a table - /// -- for example, this can occur when we have selected a - /// negative literal with free existential variables, in which - /// case the execution is said to "flounder". - /// - /// In terms of the NFTD paper, creating a new table corresponds - /// to the *New Subgoal* step as well as the *Program Clause - /// Resolution* steps. - #[instrument(level = "debug", skip(self, context, infer))] - fn get_or_create_table_for_subgoal( - &mut self, - context: &SlgContextOps<I>, - infer: &mut InferenceTable<I>, - subgoal: &Literal<I>, - ) -> Option<(TableIndex, UniverseMap)> { - // Subgoal abstraction: - let (ucanonical_subgoal, universe_map) = match subgoal { - Literal::Positive(subgoal) => { - Forest::abstract_positive_literal(context, infer, subgoal.clone())? - } - Literal::Negative(subgoal) => { - Forest::abstract_negative_literal(context, infer, subgoal.clone())? - } - }; - - debug!(?ucanonical_subgoal, ?universe_map); - - let table = self.get_or_create_table_for_ucanonical_goal(context, ucanonical_subgoal); - - Some((table, universe_map)) - } - - /// Given a u-canonical goal, searches for an existing table. If - /// one is found, it is returned, but otherwise a new table is - /// created (and populated with its initial set of strands). - /// - /// In terms of the NFTD paper, creating a new table corresponds - /// to the *New Subgoal* step as well as the *Program Clause - /// Resolution* steps. - #[instrument(level = "debug", skip(self, context))] - pub(crate) fn get_or_create_table_for_ucanonical_goal( - &mut self, - context: &SlgContextOps<I>, - goal: UCanonical<InEnvironment<Goal<I>>>, - ) -> TableIndex { - if let Some(table) = self.tables.index_of(&goal) { - debug!(?table, "found existing table"); - return table; - } - - info!( - table = ?self.tables.next_index(), - "creating new table with goal = {:#?}", - goal, - ); - let table = Self::build_table(context, self.tables.next_index(), goal); - self.tables.insert(table) - } - - /// When a table is first created, this function is invoked to - /// create the initial set of strands. If the table represents a - /// domain goal, these strands are created from the program - /// clauses as well as the clauses found in the environment. If - /// the table represents a non-domain goal, such as `for<T> G` - /// etc, then `simplify_goal` is invoked to create a strand - /// that breaks the goal down. - /// - /// In terms of the NFTD paper, this corresponds to the *Program - /// Clause Resolution* step being applied eagerly, as many times - /// as possible. - fn build_table( - context: &SlgContextOps<I>, - table_idx: TableIndex, - goal: UCanonical<InEnvironment<Goal<I>>>, - ) -> Table<I> { - let coinductive = goal.is_coinductive(context.program()); - let mut table = Table::new(goal.clone(), coinductive); - - let goal_data = goal.canonical.value.goal.data(context.program().interner()); - match goal_data { - GoalData::DomainGoal(domain_goal) => { - let canon_domain_goal = UCanonical { - canonical: Canonical { - binders: goal.canonical.binders, - value: InEnvironment::new( - &goal.canonical.value.environment, - domain_goal.clone(), - ), - }, - universes: goal.universes, - }; - - let db = context.program(); - let canon_goal = canon_domain_goal.canonical.value.goal.clone(); - let could_match = |c: &ProgramClause<I>| { - c.could_match(db.interner(), db.unification_database(), &canon_goal) - }; - - match program_clauses_that_could_match(db, &canon_domain_goal) { - Ok(mut clauses) => { - clauses.retain(could_match); - clauses.extend(db.custom_clauses().into_iter().filter(could_match)); - - let (infer, subst, goal) = - chalk_solve::infer::InferenceTable::from_canonical( - context.program().interner(), - canon_domain_goal.universes, - canon_domain_goal.canonical, - ); - - clauses.extend( - db.program_clauses_for_env(&goal.environment) - .iter(db.interner()) - .cloned() - .filter(could_match), - ); - - let InEnvironment { environment, goal } = goal; - - for clause in clauses { - info!("program clause = {:#?}", clause); - let mut infer = infer.clone(); - if let Ok(resolvent) = infer.resolvent_clause( - context.unification_database(), - context.program().interner(), - &environment, - &goal, - &subst, - &clause, - ) { - info!("pushing initial strand with ex-clause: {:#?}", &resolvent,); - let strand = Strand { - ex_clause: resolvent, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), - }; - let canonical_strand = - Self::canonicalize_strand_from(context, &mut infer, &strand); - table.enqueue_strand(canonical_strand); - } - } - } - Err(Floundered) => { - debug!( - table = ?table_idx, - "Marking table {:?} as floundered! (failed to create program clauses)", - table_idx - ); - table.mark_floundered(); - } - } - } - - _ => { - let (mut infer, subst, InEnvironment { environment, goal }) = - chalk_solve::infer::InferenceTable::from_canonical( - context.program().interner(), - goal.universes, - goal.canonical, - ); - // The goal for this table is not a domain goal, so we instead - // simplify it into a series of *literals*, all of which must be - // true. Thus, in EWFS terms, we are effectively creating a - // single child of the `A :- A` goal that is like `A :- B, C, D` - // where B, C, and D are the simplified subgoals. You can think - // of this as applying built-in "meta program clauses" that - // reduce goals into Domain goals. - match Self::simplify_goal(context, &mut infer, subst, environment, goal) { - FallibleOrFloundered::Ok(ex_clause) => { - info!( - ex_clause = ?DeepNormalizer::normalize_deep( - &mut infer, - context.program().interner(), - ex_clause.clone(), - ), - "pushing initial strand" - ); - let strand = Strand { - ex_clause, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), - }; - let canonical_strand = - Self::canonicalize_strand_from(context, &mut infer, &strand); - table.enqueue_strand(canonical_strand); - } - FallibleOrFloundered::NoSolution => {} - FallibleOrFloundered::Floundered => table.mark_floundered(), - } - } - } - - table - } - - /// Given a selected positive subgoal, applies the subgoal - /// abstraction function to yield the canonical form that will be - /// used to pick a table. Typically, this abstraction has no - /// effect, and hence we are simply returning the canonical form - /// of `subgoal`; but if the subgoal is getting too big, we return - /// `None`, which causes the subgoal to flounder. - fn abstract_positive_literal( - context: &SlgContextOps<I>, - infer: &mut InferenceTable<I>, - subgoal: InEnvironment<Goal<I>>, - ) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> { - if truncate::needs_truncation( - context.program().interner(), - infer, - context.max_size(), - &subgoal, - ) { - None - } else { - let canonicalized_goal = infer - .canonicalize(context.program().interner(), subgoal) - .quantified; - let UCanonicalized { - quantified, - universes, - } = InferenceTable::u_canonicalize(context.program().interner(), &canonicalized_goal); - Some((quantified, universes)) - } - } - - /// Given a selected negative subgoal, the subgoal is "inverted" - /// (see `InferenceTable<I, C>::invert`) and then potentially truncated - /// (see `abstract_positive_literal`). The result subgoal is - /// canonicalized. In some cases, this may return `None` and hence - /// fail to yield a useful result, for example if free existential - /// variables appear in `subgoal` (in which case the execution is - /// said to "flounder"). - fn abstract_negative_literal( - context: &SlgContextOps<I>, - infer: &mut InferenceTable<I>, - subgoal: InEnvironment<Goal<I>>, - ) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)> { - // First, we have to check that the selected negative literal - // is ground, and invert any universally quantified variables. - // - // DIVERGENCE -- In the RR paper, to ensure completeness, they - // permit non-ground negative literals, but only consider - // them to succeed when the target table has no answers at - // all. This is equivalent inverting those free existentials - // into universals, as discussed in the comments of - // `invert`. This is clearly *sound*, but the completeness is - // a subtle point. In particular, it can cause **us** to reach - // false conclusions, because e.g. given a program like - // (selected left-to-right): - // - // not { ?T: Copy }, ?T = Vec<u32> - // - // we would select `not { ?T: Copy }` first. For this goal to - // succeed we would require that -- effectively -- `forall<T> - // { not { T: Copy } }`, which clearly doesn't hold. (In the - // terms of RR, we would require that the table for `?T: Copy` - // has failed before we can continue.) - // - // In the RR paper, this is acceptable because they assume all - // of their input programs are both **normal** (negative - // literals are selected after positive ones) and **safe** - // (all free variables in negative literals occur in positive - // literals). It is plausible for us to guarantee "normal" - // form, we can reorder clauses as we need. I suspect we can - // guarantee safety too, but I have to think about it. - // - // For now, we opt for the safer route of terming such - // executions as floundering, because I think our use of - // negative goals is sufficiently limited we can get away with - // it. The practical effect is that we will judge more - // executions as floundering than we ought to (i.e., where we - // could instead generate an (imprecise) result). As you can - // see a bit later, we also diverge in some other aspects that - // affect completeness when it comes to subgoal abstraction. - let inverted_subgoal = infer.invert(context.program().interner(), subgoal)?; - - if truncate::needs_truncation( - context.program().interner(), - infer, - context.max_size(), - &inverted_subgoal, - ) { - None - } else { - let canonicalized_goal = infer - .canonicalize(context.program().interner(), inverted_subgoal) - .quantified; - let UCanonicalized { - quantified, - universes, - } = InferenceTable::u_canonicalize(context.program().interner(), &canonicalized_goal); - Some((quantified, universes)) - } - } -} - -pub(crate) struct SolveState<'forest, I: Interner> { - forest: &'forest mut Forest<I>, - context: &'forest SlgContextOps<'forest, I>, - stack: Stack<I>, -} - -impl<'forest, I: Interner> Drop for SolveState<'forest, I> { - fn drop(&mut self) { - if !self.stack.is_empty() { - if let Some(active_strand) = self.stack.top().active_strand.take() { - let table = self.stack.top().table; - self.forest.tables[table].enqueue_strand(active_strand); - } - self.unwind_stack(); - } - } -} - -impl<'forest, I: Interner> SolveState<'forest, I> { - /// Ensures that answer with the given index is available from the - /// given table. Returns `Ok` if there is an answer. - /// - /// This function first attempts to fetch answer that is cached in - /// the table. If none is found, then it will recursively search - /// to find an answer. - #[instrument(level = "info", skip(self))] - fn ensure_root_answer( - &mut self, - initial_table: TableIndex, - initial_answer: AnswerIndex, - ) -> RootSearchResult<()> { - info!( - "table goal = {:#?}", - self.forest.tables[initial_table].table_goal - ); - // Check if this table has floundered. - if self.forest.tables[initial_table].is_floundered() { - return Err(RootSearchFail::Floundered); - } - // Check for a tabled answer. - if let Some(answer) = self.forest.tables[initial_table].answer(initial_answer) { - info!("answer cached = {:?}", answer); - return Ok(()); - } - - // If no tabled answer is present, we ought to be requesting - // the next available index. - assert_eq!( - self.forest.tables[initial_table].next_answer_index(), - initial_answer - ); - - self.stack - .push(initial_table, Minimums::MAX, self.forest.increment_clock()); - loop { - let clock = self.stack.top().clock; - // If we had an active strand, continue to pursue it - let table = self.stack.top().table; - let table_answer_mode = self.forest.tables[table].answer_mode; - - // We track when we last pursued each strand. If all the strands have been - // pursued at this depth, then that means they all encountered a cycle. - // We also know that if the first strand has been pursued at this depth, - // then all have. Otherwise, an answer to any strand would have provided an - // answer for the table. - let forest = &mut self.forest; - let next_strand = self.stack.top().active_strand.take().or_else(|| { - forest.tables[table].dequeue_next_strand_that(|strand| { - let time_eligble = strand.value.last_pursued_time < clock; - let mode_eligble = match (table_answer_mode, strand.value.ex_clause.ambiguous) { - (AnswerMode::Complete, false) => true, - (AnswerMode::Complete, true) => false, - (AnswerMode::Ambiguous, _) => true, - }; - time_eligble && mode_eligble - }) - }); - match next_strand { - Some(mut canonical_strand) => { - debug!("starting next strand = {:#?}", canonical_strand); - - canonical_strand.value.last_pursued_time = clock; - match self.select_subgoal(&mut canonical_strand) { - SubGoalSelection::Selected => { - // A subgoal has been selected. We now check this subgoal - // table for an existing answer or if it's in a cycle. - // If neither of those are the case, a strand is selected - // and the next loop iteration happens. - self.on_subgoal_selected(canonical_strand)?; - continue; - } - SubGoalSelection::NotSelected => { - match self.on_no_remaining_subgoals(canonical_strand) { - NoRemainingSubgoalsResult::RootAnswerAvailable => return Ok(()), - NoRemainingSubgoalsResult::RootSearchFail(e) => return Err(e), - NoRemainingSubgoalsResult::Success => continue, - }; - } - } - } - None => { - self.on_no_strands_left()?; - continue; - } - } - } - } - - /// This is called when an answer is available for the selected subgoal - /// of the strand. First, if the selected subgoal is a `Positive` subgoal, - /// it first clones the strand pursuing the next answer. Then, it merges the - /// answer into the provided `Strand`. - /// On success, `Ok` is returned and the `Strand` can be continued to process - /// On failure, `Err` is returned and the `Strand` should be discarded - fn merge_answer_into_strand( - &mut self, - infer: &mut InferenceTable<I>, - strand: &mut Strand<I>, - ) -> RootSearchResult<()> { - // At this point, we know we have an answer for - // the selected subgoal of the strand. - // Now, we have to unify that answer onto the strand. - - // If this answer is ambiguous and we don't want ambiguous answers - // yet, then we act like this is a floundered subgoal. - let ambiguous = { - let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); - let answer = self.forest.answer( - selected_subgoal.subgoal_table, - selected_subgoal.answer_index, - ); - answer.ambiguous - }; - if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { - if ambiguous { - // FIXME: we could try to be a little bit smarter here. This can - // really be split into cases: - // 1) Cases where no amount of solving will cause this ambiguity to change. - // (e.g. `CannnotProve`) - // 2) Cases where we may be able to get a better answer if we - // solve other subgoals first. - // (e.g. the `non_enumerable_traits_reorder` test) - // We really only need to delay merging an ambiguous answer for - // case 2. Do note, though, that even if we *do* merge the answer - // case 1, we should stop solving this strand when in - // `AnswerMode::Complete` since we wouldn't use this answer yet - // *anyways*. - - // The selected subgoal returned an ambiguous answer, but we don't want that. - // So, we treat this subgoal as floundered. - let selected_subgoal = strand.selected_subgoal.take().unwrap(); - self.flounder_subgoal(&mut strand.ex_clause, selected_subgoal.subgoal_index); - return Ok(()); - } - } - - // If this subgoal was a `Positive` one, whichever way this - // particular answer turns out, there may yet be *more* answers, - // if this isn't a trivial substitution. - // Enqueue that alternative for later. - // NOTE: this is separate from the match below because we `take` the selected_subgoal - // below, but here we keep it for the new `Strand`. - let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); - if let Literal::Positive(_) = strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { - let answer = self.forest.answer( - selected_subgoal.subgoal_table, - selected_subgoal.answer_index, - ); - if !self.forest.tables[selected_subgoal.subgoal_table] - .table_goal - .is_trivial_substitution(self.context.program().interner(), &answer.subst) - { - let mut next_subgoal = selected_subgoal.clone(); - next_subgoal.answer_index.increment(); - let next_strand = Strand { - ex_clause: strand.ex_clause.clone(), - selected_subgoal: Some(next_subgoal), - last_pursued_time: strand.last_pursued_time, - }; - let table = self.stack.top().table; - let canonical_next_strand = - Forest::canonicalize_strand_from(self.context, infer, &next_strand); - self.forest.tables[table].enqueue_strand(canonical_next_strand); - } - } - - // Deselect and remove the selected subgoal, now that we have an answer for it. - let selected_subgoal = strand.selected_subgoal.take().unwrap(); - let subgoal = strand - .ex_clause - .subgoals - .remove(selected_subgoal.subgoal_index); - match subgoal { - Literal::Positive(subgoal) => { - let SelectedSubgoal { - subgoal_index: _, - subgoal_table, - answer_index, - ref universe_map, - } = selected_subgoal; - use chalk_solve::infer::ucanonicalize::UniverseMapExt; - let table_goal = universe_map.map_from_canonical( - self.context.program().interner(), - &self.forest.tables[subgoal_table].table_goal.canonical, - ); - let answer_subst = universe_map.map_from_canonical( - self.context.program().interner(), - &self.forest.answer(subgoal_table, answer_index).subst, - ); - match infer.apply_answer_subst( - self.context.program().interner(), - self.context.unification_database(), - &mut strand.ex_clause, - &subgoal, - &table_goal, - answer_subst, - ) { - Ok(()) => { - let ex_clause = &mut strand.ex_clause; - - // If the answer had was ambiguous, we have to - // ensure that `ex_clause` is also ambiguous. This is - // the SLG FACTOR operation, though NFTD just makes it - // part of computing the SLG resolvent. - if self.forest.answer(subgoal_table, answer_index).ambiguous { - debug!("Marking Strand as ambiguous because answer to (positive) subgoal was ambiguous"); - ex_clause.ambiguous = true; - } - - // Increment the answer time for the `ex_clause`. Floundered - // subgoals may be eligble to be pursued again. - ex_clause.answer_time.increment(); - - // Ok, we've applied the answer to this Strand. - Ok(()) - } - - // This answer led nowhere. Give up for now, but of course - // there may still be other strands to pursue, so return - // `QuantumExceeded`. - Err(NoSolution) => { - info!("answer not unifiable -> NoSolution"); - // This strand as no solution. It is no longer active, - // so it dropped at the end of this scope. - - // Now we want to propogate back to the up with `QuantumExceeded` - self.unwind_stack(); - Err(RootSearchFail::QuantumExceeded) - } - } - } - Literal::Negative(_) => { - let SelectedSubgoal { - subgoal_index: _, - subgoal_table, - answer_index, - universe_map: _, - } = selected_subgoal; - // We got back an answer. This is bad, because we want - // to disprove the subgoal, but it may be - // "conditional" (maybe true, maybe not). - let answer = self.forest.answer(subgoal_table, answer_index); - - // By construction, we do not expect negative subgoals - // to have delayed subgoals. This is because we do not - // need to permit `not { L }` where `L` is a - // coinductive goal. We could improve this if needed, - // but it keeps things simple. - if !answer.subst.value.delayed_subgoals.is_empty() { - panic!("Negative subgoal had delayed_subgoals"); - } - - if !answer.ambiguous { - // We want to disproval the subgoal, but we - // have an unconditional answer for the subgoal, - // therefore we have failed to disprove it. - info!("found unconditional answer to neg literal -> NoSolution"); - - // This strand as no solution. By returning an Err, - // the caller should discard this `Strand`. - - // Now we want to propogate back to the up with `QuantumExceeded` - self.unwind_stack(); - return Err(RootSearchFail::QuantumExceeded); - } - - // Otherwise, the answer is ambiguous. We can keep going, - // but we have to mark our strand, too, as ambiguous. - // - // We want to disproval the subgoal, but we - // have an unconditional answer for the subgoal, - // therefore we have failed to disprove it. - debug!(?strand, "Marking Strand as ambiguous because answer to (negative) subgoal was ambiguous"); - strand.ex_clause.ambiguous = true; - - // Strand is ambigious. - Ok(()) - } - } - } - - /// This is called when the selected subgoal for a strand has floundered. - /// We have to decide what this means for the strand. - /// - If the strand was positively dependent on the subgoal, we flounder, - /// the subgoal, then return `false`. This strand may be able to be - /// retried later. - /// - If the strand was negatively dependent on the subgoal, then strand - /// has led nowhere of interest and we return `true`. This strand should - /// be discarded. - /// - /// In other words, we return whether this strand flounders. - fn propagate_floundered_subgoal(&mut self, strand: &mut CanonicalStrand<I>) -> bool { - // This subgoal selection for the strand is finished, so take it - let selected_subgoal = strand.value.selected_subgoal.take().unwrap(); - match strand.value.ex_clause.subgoals[selected_subgoal.subgoal_index] { - Literal::Positive(_) => { - // If this strand depends on this positively, then we can - // come back to it later. So, we mark that subgoal as - // floundered and yield `QuantumExceeded` up the stack - - // If this subgoal floundered, push it onto the - // floundered list, along with the time that it - // floundered. We'll try to solve some other subgoals - // and maybe come back to it. - self.flounder_subgoal(&mut strand.value.ex_clause, selected_subgoal.subgoal_index); - - false - } - Literal::Negative(_) => { - // Floundering on a negative literal isn't like a - // positive search: we only pursue negative literals - // when we already know precisely the type we are - // looking for. So there's no point waiting for other - // subgoals, we'll never recover more information. - // - // In fact, floundering on negative searches shouldn't - // normally happen, since there are no uninferred - // variables in the goal, but it can with forall - // goals: - // - // forall<T> { not { T: Debug } } - // - // Here, the table we will be searching for answers is - // `?T: Debug`, so it could well flounder. - - // This strand has no solution. It is no longer active, - // so it dropped at the end of this scope. - - true - } - } - } - - /// This is called if the selected subgoal for a `Strand` is - /// a coinductive cycle. - fn on_coinductive_subgoal( - &mut self, - mut canonical_strand: CanonicalStrand<I>, - ) -> Result<(), RootSearchFail> { - // This is a co-inductive cycle. That is, this table - // appears somewhere higher on the stack, and has now - // recursively requested an answer for itself. This - // means that we have to delay this subgoal until we - // reach a trivial self-cycle. - - // This subgoal selection for the strand is finished, so take it - let selected_subgoal = canonical_strand.value.selected_subgoal.take().unwrap(); - match canonical_strand - .value - .ex_clause - .subgoals - .remove(selected_subgoal.subgoal_index) - { - Literal::Positive(subgoal) => { - // We delay this subgoal - let table = self.stack.top().table; - assert!( - self.forest.tables[table].coinductive_goal - && self.forest.tables[selected_subgoal.subgoal_table].coinductive_goal - ); - - canonical_strand - .value - .ex_clause - .delayed_subgoals - .push(subgoal); - - self.stack.top().active_strand = Some(canonical_strand); - Ok(()) - } - Literal::Negative(_) => { - // We don't allow coinduction for negative literals - info!("found coinductive answer to negative literal"); - panic!("Coinductive cycle with negative literal"); - } - } - } - - /// This is called if the selected subgoal for `strand` is - /// a positive, non-coinductive cycle. - /// - /// # Parameters - /// - /// * `strand` the strand from the top of the stack we are pursuing - /// * `minimums` is the collected minimum clock times - fn on_positive_cycle( - &mut self, - canonical_strand: CanonicalStrand<I>, - minimums: Minimums, - ) -> Result<(), RootSearchFail> { - // We can't take this because we might need it later to clear the cycle - let selected_subgoal = canonical_strand.value.selected_subgoal.as_ref().unwrap(); - - match canonical_strand.value.ex_clause.subgoals[selected_subgoal.subgoal_index] { - Literal::Positive(_) => { - self.stack.top().cyclic_minimums.take_minimums(&minimums); - } - Literal::Negative(_) => { - // We depend on `not(subgoal)`. For us to continue, - // `subgoal` must be completely evaluated. Therefore, - // we depend (negatively) on the minimum link of - // `subgoal` as a whole -- it doesn't matter whether - // it's pos or neg. - let mins = Minimums { - positive: self.stack.top().clock, - negative: minimums.minimum_of_pos_and_neg(), - }; - self.stack.top().cyclic_minimums.take_minimums(&mins); - } - } - - // Ok, we've taken the minimums from this cycle above. Now, - // we just return the strand to the table. The table only - // pulls strands if they have not been checked at this - // depth. - // - // We also can't mark these and return early from this - // because the stack above us might change. - let table = self.stack.top().table; - self.forest.tables[table].enqueue_strand(canonical_strand); - - // The strand isn't active, but the table is, so just continue - Ok(()) - } - - /// Invoked after we've selected a (new) subgoal for the top-most - /// strand. Attempts to pursue this selected subgoal. - /// - /// Returns: - /// - /// * `Ok` if we should keep searching. - /// * `Err` if the subgoal failed in some way such that the strand can be abandoned. - fn on_subgoal_selected( - &mut self, - mut canonical_strand: CanonicalStrand<I>, - ) -> Result<(), RootSearchFail> { - // This may be a newly selected subgoal or an existing selected subgoal. - - let SelectedSubgoal { - subgoal_index: _, - subgoal_table, - answer_index, - universe_map: _, - } = *canonical_strand.value.selected_subgoal.as_ref().unwrap(); - - debug!( - ?subgoal_table, - goal = ?self.forest.tables[subgoal_table].table_goal, - "table selection {:?} with goal: {:?}", - subgoal_table, self.forest.tables[subgoal_table].table_goal - ); - - // This is checked inside select_subgoal - assert!(!self.forest.tables[subgoal_table].is_floundered()); - - // Check for a tabled answer. - if let Some(answer) = self.forest.tables[subgoal_table].answer(answer_index) { - info!("answer cached = {:?}", answer); - - // There was a previous answer available for this table - // We need to check if we can merge it into the current `Strand`. - let num_universes = self.forest.tables[self.stack.top().table] - .table_goal - .universes; - let (mut infer, _, mut strand) = chalk_solve::infer::InferenceTable::from_canonical( - self.context.program().interner(), - num_universes, - canonical_strand.clone(), - ); - match self.merge_answer_into_strand(&mut infer, &mut strand) { - Err(e) => { - debug!(?strand, "could not merge into current strand"); - drop(strand); - return Err(e); - } - Ok(_) => { - debug!(?strand, "merged answer into current strand"); - canonical_strand = - Forest::canonicalize_strand_from(self.context, &mut infer, &strand); - self.stack.top().active_strand = Some(canonical_strand); - return Ok(()); - } - } - } - - // If no tabled answer is present, we ought to be requesting - // the next available index. - assert_eq!( - self.forest.tables[subgoal_table].next_answer_index(), - answer_index - ); - - // Next, check if the table is already active. If so, then we - // have a recursive attempt. - if let Some(cyclic_depth) = self.stack.is_active(subgoal_table) { - info!("cycle detected at depth {:?}", cyclic_depth); - let minimums = Minimums { - positive: self.stack[cyclic_depth].clock, - negative: TimeStamp::MAX, - }; - - if self.top_of_stack_is_coinductive_from(cyclic_depth) { - debug!("table is coinductive"); - return self.on_coinductive_subgoal(canonical_strand); - } - - debug!("table encountered a positive cycle"); - return self.on_positive_cycle(canonical_strand, minimums); - } - - // We don't know anything about the selected subgoal table. - // Set this strand as active and push it onto the stack. - self.stack.top().active_strand = Some(canonical_strand); - - let cyclic_minimums = Minimums::MAX; - self.stack.push( - subgoal_table, - cyclic_minimums, - self.forest.increment_clock(), - ); - Ok(()) - } - - /// This is called when there are no remaining subgoals for a strand, so - /// it represents an answer. If the strand is ambiguous and we don't want - /// it yet, we just enqueue it again to pick it up later. Otherwise, we - /// add the answer from the strand onto the table. - fn on_no_remaining_subgoals( - &mut self, - canonical_strand: CanonicalStrand<I>, - ) -> NoRemainingSubgoalsResult { - let ambiguous = canonical_strand.value.ex_clause.ambiguous; - if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { - if ambiguous { - // The strand can only return an ambiguous answer, but we don't - // want that right now, so requeue and we'll deal with it later. - self.forest.tables[self.stack.top().table].enqueue_strand(canonical_strand); - return NoRemainingSubgoalsResult::RootSearchFail(RootSearchFail::QuantumExceeded); - } - } - let floundered = !canonical_strand - .value - .ex_clause - .floundered_subgoals - .is_empty(); - if floundered { - debug!("all remaining subgoals floundered for the table"); - } else { - debug!("no remaining subgoals for the table"); - }; - match self.pursue_answer(canonical_strand) { - Some(answer_index) => { - debug!("answer is available"); - - // We found an answer for this strand, and therefore an - // answer for this table. Now, this table was either a - // subgoal for another strand, or was the root table. - let table = self.stack.top().table; - match self.stack.pop_and_take_caller_strand() { - Some(caller_strand) => { - self.stack.top().active_strand = Some(caller_strand); - NoRemainingSubgoalsResult::Success - } - None => { - // That was the root table, so we are done -- - // *well*, unless there were delayed - // subgoals. In that case, we want to evaluate - // those delayed subgoals to completion, so we - // have to create a fresh strand that will - // take them as goals. Note that we *still - // need the original answer in place*, because - // we might have to build on it (see the - // Delayed Trivial Self Cycle, Variant 3 - // example). - - let answer = self.forest.answer(table, answer_index); - if let Some(strand) = self.create_refinement_strand(table, answer) { - self.forest.tables[table].enqueue_strand(strand); - } - - NoRemainingSubgoalsResult::RootAnswerAvailable - } - } - } - None => { - debug!("answer is not available (or not new)"); - - // This strand led nowhere of interest. There might be *other* - // answers on this table, but we don't care right now, we'll - // try again at another time. - - // Now we yield with `QuantumExceeded` - self.unwind_stack(); - NoRemainingSubgoalsResult::RootSearchFail(RootSearchFail::QuantumExceeded) - } - } - } - - /// A "refinement" strand is used in coinduction. When the root - /// table on the stack publishes an answer has delayed subgoals, - /// we create a new strand that will attempt to prove out those - /// delayed subgoals (the root answer here is not *special* except - /// in so far as that there is nothing above it, and hence we know - /// that the delayed subgoals (which resulted in some cycle) must - /// be referring to a table that now has completed). - /// - /// Note that it is important for this to be a *refinement* strand - /// -- meaning that the answer with delayed subgoals has been - /// published. This is necessary because sometimes the strand must - /// build on that very answer that it is refining. See Delayed - /// Trivial Self Cycle, Variant 3. - fn create_refinement_strand( - &self, - table: TableIndex, - answer: &Answer<I>, - ) -> Option<CanonicalStrand<I>> { - // If there are no delayed subgoals, then there is no need for - // a refinement strand. - if answer.subst.value.delayed_subgoals.is_empty() { - return None; - } - - let num_universes = self.forest.tables[table].table_goal.universes; - let ( - mut infer, - _, - AnswerSubst { - subst, - constraints, - delayed_subgoals, - }, - ) = chalk_solve::infer::InferenceTable::from_canonical( - self.context.program().interner(), - num_universes, - answer.subst.clone(), - ); - - let delayed_subgoals = delayed_subgoals - .into_iter() - .map(Literal::Positive) - .collect(); - - let strand = Strand { - ex_clause: ExClause { - subst, - ambiguous: answer.ambiguous, - constraints: constraints - .as_slice(self.context.program().interner()) - .to_vec(), - subgoals: delayed_subgoals, - delayed_subgoals: Vec::new(), - answer_time: TimeStamp::default(), - floundered_subgoals: Vec::new(), - }, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), - }; - - Some(Forest::canonicalize_strand_from( - self.context, - &mut infer, - &strand, - )) - } - - fn on_no_strands_left(&mut self) -> Result<(), RootSearchFail> { - let table = self.stack.top().table; - debug!("no more strands available (or all cycles) for {:?}", table); - - // No more strands left to try! This is either because all - // strands have failed, because all strands encountered a - // cycle, or all strands have would give ambiguous answers. - - if self.forest.tables[table].strands_mut().count() == 0 { - // All strands for the table T on the top of the stack - // have **failed**. Hence we can pop it off the stack and - // check what this means for the table T' that was just - // below T on the stack (if any). - debug!("no more strands available"); - let caller_strand = match self.stack.pop_and_borrow_caller_strand() { - Some(s) => s, - None => { - // T was the root table, so we are done. - debug!("no more solutions"); - return Err(RootSearchFail::NoMoreSolutions); - } - }; - - // This subgoal selection for the strand is finished, so take it - let caller_selected_subgoal = caller_strand.value.selected_subgoal.take().unwrap(); - return match caller_strand.value.ex_clause.subgoals - [caller_selected_subgoal.subgoal_index] - { - // T' wanted an answer from T, but none is - // forthcoming. Therefore, the active strand from T' - // has failed and can be discarded. - Literal::Positive(_) => { - debug!("discarding strand because positive literal"); - self.stack.top().active_strand.take(); - self.unwind_stack(); - Err(RootSearchFail::QuantumExceeded) - } - - // T' wanted there to be no answer from T, but none is forthcoming. - Literal::Negative(_) => { - debug!("subgoal was proven because negative literal"); - - // There is no solution for this strand. But, this - // is what we want, so can remove this subgoal and - // keep going. - caller_strand - .value - .ex_clause - .subgoals - .remove(caller_selected_subgoal.subgoal_index); - - // This strand is still active, so continue - Ok(()) - } - }; - } - - // We can't consider this table as part of a cycle unless we've handled - // all strands, not just non-ambiguous ones. See chalk#571. - if let AnswerMode::Complete = self.forest.tables[table].answer_mode { - debug!("Allowing ambiguous answers."); - self.forest.tables[table].answer_mode = AnswerMode::Ambiguous; - return Err(RootSearchFail::QuantumExceeded); - } - - let clock = self.stack.top().clock; - let cyclic_minimums = self.stack.top().cyclic_minimums; - if cyclic_minimums.positive >= clock && cyclic_minimums.negative >= clock { - debug!("cycle with no new answers"); - - if cyclic_minimums.negative < TimeStamp::MAX { - // This is a negative cycle. - self.unwind_stack(); - return Err(RootSearchFail::NegativeCycle); - } - - // If all the things that we recursively depend on have - // positive dependencies on things below us in the stack, - // then no more answers are forthcoming. We can clear all - // the strands for those things recursively. - let table = self.stack.top().table; - let cyclic_strands = self.forest.tables[table].take_strands(); - self.clear_strands_after_cycle(cyclic_strands); - - // Now we yield with `QuantumExceeded` - self.unwind_stack(); - Err(RootSearchFail::QuantumExceeded) - } else { - debug!("table part of a cycle"); - - // This table resulted in a positive cycle, so we have - // to check what this means for the subgoal containing - // this strand - let caller_strand = match self.stack.pop_and_borrow_caller_strand() { - Some(s) => s, - None => { - panic!("nothing on the stack but cyclic result"); - } - }; - - // We can't take this because we might need it later to clear the cycle - let caller_selected_subgoal = caller_strand.value.selected_subgoal.as_ref().unwrap(); - match caller_strand.value.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { - Literal::Positive(_) => { - self.stack - .top() - .cyclic_minimums - .take_minimums(&cyclic_minimums); - } - Literal::Negative(_) => { - // We depend on `not(subgoal)`. For us to continue, - // `subgoal` must be completely evaluated. Therefore, - // we depend (negatively) on the minimum link of - // `subgoal` as a whole -- it doesn't matter whether - // it's pos or neg. - let mins = Minimums { - positive: self.stack.top().clock, - negative: cyclic_minimums.minimum_of_pos_and_neg(), - }; - self.stack.top().cyclic_minimums.take_minimums(&mins); - } - } - - // We can't pursue this strand anymore, so push it back onto the table - let active_strand = self.stack.top().active_strand.take().unwrap(); - let table = self.stack.top().table; - self.forest.tables[table].enqueue_strand(active_strand); - - // The strand isn't active, but the table is, so just continue - Ok(()) - } - } - - /// Unwinds the entire stack, returning all active strands back to - /// their tables (this time at the end of the queue). - fn unwind_stack(&mut self) { - loop { - match self.stack.pop_and_take_caller_strand() { - Some(active_strand) => { - let table = self.stack.top().table; - self.forest.tables[table].enqueue_strand(active_strand); - } - - None => return, - } - } - } - - /// Invoked after we have determined that every strand in `table` - /// encounters a cycle; `strands` is the set of strands (which - /// have been moved out of the table). This method then - /// recursively clears the active strands from the tables - /// referenced in `strands`, since all of them must encounter - /// cycles too. - fn clear_strands_after_cycle(&mut self, strands: impl IntoIterator<Item = CanonicalStrand<I>>) { - for strand in strands { - let selected_subgoal = strand.value.selected_subgoal; - let ex_clause = strand.value.ex_clause; - let selected_subgoal = selected_subgoal.unwrap_or_else(|| { - panic!( - "clear_strands_after_cycle invoked on strand in table \ - without a selected subgoal: {:?}", - ex_clause, - ) - }); - - let strand_table = selected_subgoal.subgoal_table; - let strands = self.forest.tables[strand_table].take_strands(); - self.clear_strands_after_cycle(strands); - } - } - - fn select_subgoal( - &mut self, - mut canonical_strand: &mut CanonicalStrand<I>, - ) -> SubGoalSelection { - loop { - while canonical_strand.value.selected_subgoal.is_none() { - if canonical_strand.value.ex_clause.subgoals.is_empty() { - if canonical_strand - .value - .ex_clause - .floundered_subgoals - .is_empty() - { - return SubGoalSelection::NotSelected; - } - - self.reconsider_floundered_subgoals(&mut canonical_strand.value.ex_clause); - - if canonical_strand.value.ex_clause.subgoals.is_empty() { - // All the subgoals of this strand floundered. We may be able - // to get helpful information from this strand still, but it - // will *always* be ambiguous, so mark it as so. - assert!(!canonical_strand - .value - .ex_clause - .floundered_subgoals - .is_empty()); - canonical_strand.value.ex_clause.ambiguous = true; - return SubGoalSelection::NotSelected; - } - - continue; - } - - let subgoal_index = - SlgContext::next_subgoal_index(&canonical_strand.value.ex_clause); - - // Get or create table for this subgoal. - let num_universes = self.forest.tables[self.stack.top().table] - .table_goal - .universes; - let (mut infer, _, strand) = chalk_solve::infer::InferenceTable::from_canonical( - self.context.program().interner(), - num_universes, - canonical_strand.clone(), - ); - match self.forest.get_or_create_table_for_subgoal( - self.context, - &mut infer, - &strand.ex_clause.subgoals[subgoal_index], - ) { - Some((subgoal_table, universe_map)) => { - canonical_strand.value.selected_subgoal = Some(SelectedSubgoal { - subgoal_index, - subgoal_table, - universe_map, - answer_index: AnswerIndex::ZERO, - }); - } - - None => { - // If we failed to create a table for the subgoal, - // that is because we have a floundered negative - // literal. - self.flounder_subgoal(&mut canonical_strand.value.ex_clause, subgoal_index); - } - } - } - - let selected_subgoal_table = canonical_strand - .value - .selected_subgoal - .as_ref() - .unwrap() - .subgoal_table; - if self.forest.tables[selected_subgoal_table].is_floundered() { - if self.propagate_floundered_subgoal(canonical_strand) { - // This strand will never lead anywhere of interest. - return SubGoalSelection::NotSelected; - } else { - // This subgoal has floundered and has been marked. - // We previously would immediately mark the table as - // floundered too, and maybe come back to it. Now, we - // try to see if any other subgoals can be pursued first. - continue; - } - } else { - return SubGoalSelection::Selected; - } - } - } - - /// Invoked when a strand represents an **answer**. This means - /// that the strand has no subgoals left. There are two possibilities: - /// - /// - the strand may represent an answer we have already found; in - /// that case, we can return `None`, as this - /// strand led nowhere of interest. - /// - the strand may represent a new answer, in which case it is - /// added to the table and `Some(())` is returned. - fn pursue_answer(&mut self, canonical_strand: CanonicalStrand<I>) -> Option<AnswerIndex> { - let table = self.stack.top().table; - let Canonical { - binders, - value: strand, - } = canonical_strand; - let ExClause { - subst, - constraints, - ambiguous, - subgoals, - delayed_subgoals, - answer_time: _, - floundered_subgoals, - } = strand.ex_clause; - // If there are subgoals left, they should be followed - assert!(subgoals.is_empty()); - // We can still try to get an ambiguous answer if there are floundered subgoals - let floundered = !floundered_subgoals.is_empty(); - // So let's make sure that it *really* is an ambiguous answer (this should be set previously) - assert!(!floundered || ambiguous); - - // FIXME: If there are floundered subgoals, we *could* potentially - // actually check if the partial answers to any of these subgoals - // conflict. But this requires that we think about whether they are - // positive or negative subgoals. This duplicates some of the logic - // in `merge_answer_into_strand`, so a bit of refactoring is needed. - - // If the answer gets too large, mark the table as floundered. - // This is the *most conservative* course. There are a few alternatives: - // 1) Replace the answer with a truncated version of it. (This was done - // previously, but turned out to be more complicated than we wanted and - // and a source of multiple bugs.) - // 2) Mark this *strand* as floundered. We don't currently have a mechanism - // for this (only floundered subgoals), so implementing this is more - // difficult because we don't want to just *remove* this strand from the - // table, because that might make the table give `NoMoreSolutions`, which - // is *wrong*. - // 3) Do something fancy with delayed subgoals, effectively delayed the - // truncated bits to a different strand (and a more "refined" answer). - // (This one probably needs more thought, but is here for "completeness") - // - // Ultimately, the current decision to flounder the entire table mostly boils - // down to "it works as we expect for the current tests". And, we likely don't - // even *need* the added complexity just for potentially more answers. - if truncate::needs_truncation( - self.context.program().interner(), - &mut InferenceTable::new(), - self.context.max_size(), - &subst, - ) { - self.forest.tables[table].mark_floundered(); - return None; - } - - let table_goal = &self.forest.tables[table].table_goal; - - let filtered_delayed_subgoals = delayed_subgoals - .into_iter() - .filter(|delayed_subgoal| { - let canonicalized = InferenceTable::u_canonicalize( - self.context.program().interner(), - &chalk_ir::Canonical { - binders: binders.clone(), - value: delayed_subgoal.clone(), - }, - ) - .quantified; - *table_goal != canonicalized - }) - .collect(); - - let subst = Canonical { - binders, - value: AnswerSubst { - subst, - constraints: Constraints::from_iter(self.context.program().interner(), constraints), - delayed_subgoals: filtered_delayed_subgoals, - }, - }; - debug!(?table, ?subst, ?floundered, "found answer"); - - let answer = Answer { subst, ambiguous }; - - // A "trivial" answer is one that is 'just true for all cases' - // -- in other words, it gives no information back to the - // caller. For example, `Vec<u32>: Sized` is "just true". - // Such answers are important because they are the most - // general case, and after we provide a trivial answer, no - // further answers are useful -- therefore we can clear any - // further pending strands (this is a "green cut", in - // Prolog parlance). - // - // This optimization is *crucial* for performance: for - // example, `projection_from_env_slow` fails miserably without - // it. The reason is that we wind up (thanks to implied bounds) - // with a clause like this: - // - // ```ignore - // forall<T> { (<T as SliceExt>::Item: Clone) :- WF(T: SliceExt) } - // ``` - // - // we then apply that clause to `!1: Clone`, resulting in the - // table goal `!1: Clone :- <?0 as SliceExt>::Item = !1, - // WF(?0: SliceExt)`. This causes us to **enumerate all types - // `?0` that where `Slice<?0>` normalizes to `!1` -- this is - // an infinite set of types, effectively. Interestingly, - // though, we only need one and we are done, because (if you - // look) our goal (`!1: Clone`) doesn't have any output - // parameters. - // - // This is actually a kind of general case. Due to Rust's rule - // about constrained impl type parameters, generally speaking - // when we have some free inference variable (like `?0`) - // within our clause, it must appear in the head of the - // clause. This means that the values we create for it will - // propagate up to the caller, and they will quickly surmise - // that there is ambiguity and stop requesting more answers. - // Indeed, the only exception to this rule about constrained - // type parameters if with associated type projections, as in - // the case above! - // - // (Actually, because of the trivial answer cut off rule, we - // never even get to the point of asking the query above in - // `projection_from_env_slow`.) - // - // However, there is one fly in the ointment: answers include - // region constraints, and you might imagine that we could - // find future answers that are also trivial but with distinct - // sets of region constraints. **For this reason, we only - // apply this green cut rule if the set of generated - // constraints is empty.** - // - // The limitation on region constraints is quite a drag! We - // can probably do better, though: for example, coherence - // guarantees that, for any given set of types, only a single - // impl ought to be applicable, and that impl can only impose - // one set of region constraints. However, it's not quite that - // simple, thanks to specialization as well as the possibility - // of proving things from the environment (though the latter - // is a *bit* suspect; e.g., those things in the environment - // must be backed by an impl *eventually*). - let is_trivial_answer = { - self.forest.tables[table] - .table_goal - .is_trivial_substitution(self.context.program().interner(), &answer.subst) - && answer - .subst - .value - .constraints - .is_empty(self.context.program().interner()) - }; - - if let Some(answer_index) = self.forest.tables[table].push_answer(answer) { - // See above, if we have a *complete* and trivial answer, we don't - // want to follow any more strands - if !ambiguous && is_trivial_answer { - self.forest.tables[table].take_strands(); - } - - Some(answer_index) - } else { - info!("answer: not a new answer, returning None"); - None - } - } - - fn reconsider_floundered_subgoals(&mut self, ex_clause: &mut ExClause<I>) { - info!("reconsider_floundered_subgoals(ex_clause={:#?})", ex_clause,); - let ExClause { - answer_time, - subgoals, - floundered_subgoals, - .. - } = ex_clause; - for i in (0..floundered_subgoals.len()).rev() { - if floundered_subgoals[i].floundered_time < *answer_time { - let floundered_subgoal = floundered_subgoals.swap_remove(i); - subgoals.push(floundered_subgoal.floundered_literal); - } - } - } - - /// Removes the subgoal at `subgoal_index` from the strand's - /// subgoal list and adds it to the strand's floundered subgoal - /// list. - fn flounder_subgoal(&self, ex_clause: &mut ExClause<I>, subgoal_index: usize) { - let _s = debug_span!( - "flounder_subgoal", - answer_time = ?ex_clause.answer_time, - subgoal = ?ex_clause.subgoals[subgoal_index], - ); - let _s = _s.enter(); - - let floundered_time = ex_clause.answer_time; - let floundered_literal = ex_clause.subgoals.remove(subgoal_index); - ex_clause.floundered_subgoals.push(FlounderedSubgoal { - floundered_literal, - floundered_time, - }); - debug!(?ex_clause); - } - - /// True if all the tables on the stack starting from `depth` and - /// continuing until the top of the stack are coinductive. - /// - /// Example: Given a program like: - /// - /// ```notrust - /// struct Foo { a: Option<Box<Bar>> } - /// struct Bar { a: Option<Box<Foo>> } - /// trait XXX { } - /// impl<T: Send> XXX for T { } - /// ``` - /// - /// and then a goal of `Foo: XXX`, we would eventually wind up - /// with a stack like this: - /// - /// | StackIndex | Table Goal | - /// | ---------- | ----------- | - /// | 0 | `Foo: XXX` | - /// | 1 | `Foo: Send` | - /// | 2 | `Bar: Send` | - /// - /// Here, the top of the stack is `Bar: Send`. And now we are - /// asking `top_of_stack_is_coinductive_from(1)` -- the answer - /// would be true, since `Send` is an auto trait, which yields a - /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is - /// false, since `XXX` is not an auto trait. - pub(super) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool { - StackIndex::iterate_range(self.stack.top_of_stack_from(depth)).all(|d| { - let table = self.stack[d].table; - self.forest.tables[table].coinductive_goal - }) - } -} diff --git a/vendor/chalk-engine/src/normalize_deep.rs b/vendor/chalk-engine/src/normalize_deep.rs deleted file mode 100644 index 9f36f3ce5..000000000 --- a/vendor/chalk-engine/src/normalize_deep.rs +++ /dev/null @@ -1,172 +0,0 @@ -use chalk_derive::FallibleTypeFolder; -use chalk_ir::fold::shift::Shift; -use chalk_ir::fold::{TypeFoldable, TypeFolder}; -use chalk_ir::interner::Interner; -use chalk_ir::*; -use chalk_solve::infer::InferenceTable; - -#[derive(FallibleTypeFolder)] -pub(crate) struct DeepNormalizer<'table, I: Interner> { - table: &'table mut InferenceTable<I>, - interner: I, -} - -impl<I: Interner> DeepNormalizer<'_, I> { - /// Given a value `value` with variables in it, replaces those variables - /// with their instantiated values (if any). Uninstantiated variables are - /// left as-is. - /// - /// This is mainly intended for getting final values to dump to - /// the user and its use should otherwise be avoided, particularly - /// given the possibility of snapshots and rollbacks. - /// - /// See also `InferenceTable::canonicalize`, which -- during real - /// processing -- is often used to capture the "current state" of - /// variables. - pub fn normalize_deep<T: TypeFoldable<I>>( - table: &mut InferenceTable<I>, - interner: I, - value: T, - ) -> T { - value - .try_fold_with( - &mut DeepNormalizer { interner, table }, - DebruijnIndex::INNERMOST, - ) - .unwrap() - } -} - -impl<I: Interner> TypeFolder<I> for DeepNormalizer<'_, I> { - fn as_dyn(&mut self) -> &mut dyn TypeFolder<I> { - self - } - - fn fold_inference_ty( - &mut self, - var: InferenceVar, - kind: TyVariableKind, - _outer_binder: DebruijnIndex, - ) -> Ty<I> { - let interner = self.interner; - match self.table.probe_var(var) { - Some(ty) => ty - .assert_ty_ref(interner) - .clone() - .fold_with(self, DebruijnIndex::INNERMOST) - .shifted_in(interner), // FIXME shift - None => { - // Normalize all inference vars which have been unified into a - // single variable. Ena calls this the "root" variable. - self.table.inference_var_root(var).to_ty(interner, kind) - } - } - } - - fn fold_inference_lifetime( - &mut self, - var: InferenceVar, - _outer_binder: DebruijnIndex, - ) -> Lifetime<I> { - let interner = self.interner; - match self.table.probe_var(var) { - Some(l) => l - .assert_lifetime_ref(interner) - .clone() - .fold_with(self, DebruijnIndex::INNERMOST) - .shifted_in(interner), - None => var.to_lifetime(interner), // FIXME shift - } - } - - fn fold_inference_const( - &mut self, - ty: Ty<I>, - var: InferenceVar, - _outer_binder: DebruijnIndex, - ) -> Const<I> { - let interner = self.interner; - match self.table.probe_var(var) { - Some(c) => c - .assert_const_ref(interner) - .clone() - .fold_with(self, DebruijnIndex::INNERMOST) - .shifted_in(interner), - None => var.to_const(interner, ty), // FIXME shift - } - } - - fn forbid_free_vars(&self) -> bool { - true - } - - fn interner(&self) -> I { - self.interner - } -} - -#[cfg(test)] -mod test { - use super::*; - use chalk_integration::interner::ChalkIr; - use chalk_integration::{arg, ty}; - - const U0: UniverseIndex = UniverseIndex { counter: 0 }; - - // We just use a vec of 20 `Invariant`, since this is zipped and no substs are - // longer than this - #[derive(Debug)] - struct TestDatabase; - impl UnificationDatabase<ChalkIr> for TestDatabase { - fn fn_def_variance(&self, _fn_def_id: FnDefId<ChalkIr>) -> Variances<ChalkIr> { - Variances::from_iter(ChalkIr, [Variance::Invariant; 20].iter().copied()) - } - - fn adt_variance(&self, _adt_id: AdtId<ChalkIr>) -> Variances<ChalkIr> { - Variances::from_iter(ChalkIr, [Variance::Invariant; 20].iter().copied()) - } - } - - #[test] - fn infer() { - let interner = ChalkIr; - let mut table: InferenceTable<ChalkIr> = InferenceTable::new(); - let environment0 = Environment::new(interner); - let a = table.new_variable(U0).to_ty(interner); - let b = table.new_variable(U0).to_ty(interner); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &a, - &ty!(apply (item 0) (expr b)), - ) - .unwrap(); - // a is unified to Adt<#0>(c), where 'c' is a new inference var - // created by the generalizer to generalize 'b'. It then unifies 'b' - // and 'c', and when we normalize them, they'll both be output as - // the same "root" variable. However, there are no guarantees for - // _which_ of 'b' and 'c' becomes the root. We need to normalize - // "b" too, then, to ensure we get a consistent result. - assert_eq!( - DeepNormalizer::normalize_deep(&mut table, interner, a.clone()), - ty!(apply (item 0) (expr DeepNormalizer::normalize_deep(&mut table, interner, b.clone()))), - ); - table - .relate( - interner, - &TestDatabase, - &environment0, - Variance::Invariant, - &b, - &ty!(apply (item 1)), - ) - .unwrap(); - assert_eq!( - DeepNormalizer::normalize_deep(&mut table, interner, a), - ty!(apply (item 0) (apply (item 1))) - ); - } -} diff --git a/vendor/chalk-engine/src/simplify.rs b/vendor/chalk-engine/src/simplify.rs deleted file mode 100644 index 1c594af01..000000000 --- a/vendor/chalk-engine/src/simplify.rs +++ /dev/null @@ -1,141 +0,0 @@ -use crate::forest::Forest; -use crate::slg::SlgContextOps; -use crate::{ExClause, Literal, TimeStamp}; - -use chalk_ir::cast::{Cast, Caster}; -use chalk_ir::interner::Interner; -use chalk_ir::{ - Environment, FallibleOrFloundered, Goal, GoalData, InEnvironment, QuantifierKind, Substitution, - TyKind, TyVariableKind, Variance, -}; -use chalk_solve::infer::InferenceTable; -use tracing::debug; - -impl<I: Interner> Forest<I> { - /// Simplifies a goal into a series of positive domain goals - /// and negative goals. This operation may fail if the goal - /// includes unifications that cannot be completed. - pub(super) fn simplify_goal( - context: &SlgContextOps<I>, - infer: &mut InferenceTable<I>, - subst: Substitution<I>, - initial_environment: Environment<I>, - initial_goal: Goal<I>, - ) -> FallibleOrFloundered<ExClause<I>> { - let mut ex_clause = ExClause { - subst, - ambiguous: false, - constraints: vec![], - subgoals: vec![], - delayed_subgoals: vec![], - answer_time: TimeStamp::default(), - floundered_subgoals: vec![], - }; - - // A stack of higher-level goals to process. - let mut pending_goals = vec![(initial_environment, initial_goal)]; - - while let Some((environment, goal)) = pending_goals.pop() { - match goal.data(context.program().interner()) { - GoalData::Quantified(QuantifierKind::ForAll, subgoal) => { - let subgoal = infer.instantiate_binders_universally( - context.program().interner(), - subgoal.clone(), - ); - pending_goals.push((environment, subgoal.clone())); - } - GoalData::Quantified(QuantifierKind::Exists, subgoal) => { - let subgoal = infer.instantiate_binders_existentially( - context.program().interner(), - subgoal.clone(), - ); - pending_goals.push((environment, subgoal.clone())); - } - GoalData::Implies(wc, subgoal) => { - let new_environment = environment.add_clauses( - context.program().interner(), - wc.iter(context.program().interner()).cloned(), - ); - pending_goals.push((new_environment, subgoal.clone())); - } - GoalData::All(subgoals) => { - for subgoal in subgoals.iter(context.program().interner()) { - pending_goals.push((environment.clone(), subgoal.clone())); - } - } - GoalData::Not(subgoal) => { - ex_clause - .subgoals - .push(Literal::Negative(InEnvironment::new( - &environment, - subgoal.clone(), - ))); - } - GoalData::EqGoal(goal) => { - let interner = context.program().interner(); - let db = context.unification_database(); - let a = &goal.a; - let b = &goal.b; - - let result = - match infer.relate(interner, db, &environment, Variance::Invariant, a, b) { - Ok(r) => r, - Err(_) => return FallibleOrFloundered::NoSolution, - }; - ex_clause.subgoals.extend( - result - .goals - .into_iter() - .casted(interner) - .map(Literal::Positive), - ); - } - GoalData::SubtypeGoal(goal) => { - let interner = context.program().interner(); - let db = context.unification_database(); - let a_norm = infer.normalize_ty_shallow(interner, &goal.a); - let a = a_norm.as_ref().unwrap_or(&goal.a); - let b_norm = infer.normalize_ty_shallow(interner, &goal.b); - let b = b_norm.as_ref().unwrap_or(&goal.b); - - if matches!( - a.kind(interner), - TyKind::InferenceVar(_, TyVariableKind::General) - ) && matches!( - b.kind(interner), - TyKind::InferenceVar(_, TyVariableKind::General) - ) { - return FallibleOrFloundered::Floundered; - } - - let result = - match infer.relate(interner, db, &environment, Variance::Covariant, a, b) { - Ok(r) => r, - Err(_) => return FallibleOrFloundered::Floundered, - }; - ex_clause.subgoals.extend( - result - .goals - .into_iter() - .casted(interner) - .map(Literal::Positive), - ); - } - GoalData::DomainGoal(domain_goal) => { - ex_clause - .subgoals - .push(Literal::Positive(InEnvironment::new( - &environment, - domain_goal.clone().cast(context.program().interner()), - ))); - } - GoalData::CannotProve => { - debug!("Marking Strand as ambiguous because of a `CannotProve` subgoal"); - ex_clause.ambiguous = true; - } - } - } - - FallibleOrFloundered::Ok(ex_clause) - } -} diff --git a/vendor/chalk-engine/src/slg.rs b/vendor/chalk-engine/src/slg.rs deleted file mode 100644 index f3522e777..000000000 --- a/vendor/chalk-engine/src/slg.rs +++ /dev/null @@ -1,378 +0,0 @@ -use crate::ExClause; - -use chalk_derive::HasInterner; -use chalk_ir::interner::Interner; -use chalk_ir::*; -use chalk_solve::infer::InferenceTable; -use chalk_solve::RustIrDatabase; - -use std::fmt::Debug; -use std::marker::PhantomData; - -pub(crate) mod aggregate; -mod resolvent; - -#[derive(Clone, Debug, HasInterner)] -pub(crate) struct SlgContext<I: Interner> { - phantom: PhantomData<I>, -} - -impl<I: Interner> SlgContext<I> { - pub(crate) fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize { - // For now, we always pick the last subgoal in the - // list. - // - // FIXME(rust-lang-nursery/chalk#80) -- we should be more - // selective. For example, we don't want to pick a - // negative literal that will flounder, and we don't want - // to pick things like `?T: Sized` if we can help it. - ex_clause.subgoals.len() - 1 - } -} -#[derive(Clone, Debug)] -pub(crate) struct SlgContextOps<'me, I: Interner> { - program: &'me dyn RustIrDatabase<I>, - max_size: usize, - expected_answers: Option<usize>, -} - -impl<I: Interner> SlgContextOps<'_, I> { - pub(crate) fn new( - program: &dyn RustIrDatabase<I>, - max_size: usize, - expected_answers: Option<usize>, - ) -> SlgContextOps<'_, I> { - SlgContextOps { - program, - max_size, - expected_answers, - } - } - - fn identity_constrained_subst( - &self, - goal: &UCanonical<InEnvironment<Goal<I>>>, - ) -> Canonical<ConstrainedSubst<I>> { - let (mut infer, subst, _) = InferenceTable::from_canonical( - self.program.interner(), - goal.universes, - goal.canonical.clone(), - ); - infer - .canonicalize( - self.program.interner(), - ConstrainedSubst { - subst, - constraints: Constraints::empty(self.program.interner()), - }, - ) - .quantified - } - - pub(crate) fn program(&self) -> &dyn RustIrDatabase<I> { - self.program - } - - pub(crate) fn max_size(&self) -> usize { - self.max_size - } - - pub(crate) fn unification_database(&self) -> &dyn UnificationDatabase<I> { - self.program.unification_database() - } -} - -pub trait ResolventOps<I: Interner> { - /// Combines the `goal` (instantiated within `infer`) with the - /// given program clause to yield the start of a new strand (a - /// canonical ex-clause). - /// - /// The bindings in `infer` are unaffected by this operation. - fn resolvent_clause( - &mut self, - ops: &dyn UnificationDatabase<I>, - interner: I, - environment: &Environment<I>, - goal: &DomainGoal<I>, - subst: &Substitution<I>, - clause: &ProgramClause<I>, - ) -> Fallible<ExClause<I>>; - - fn apply_answer_subst( - &mut self, - interner: I, - unification_database: &dyn UnificationDatabase<I>, - ex_clause: &mut ExClause<I>, - selected_goal: &InEnvironment<Goal<I>>, - answer_table_goal: &Canonical<InEnvironment<Goal<I>>>, - canonical_answer_subst: Canonical<AnswerSubst<I>>, - ) -> Fallible<()>; -} - -trait SubstitutionExt<I: Interner> { - fn may_invalidate(&self, interner: I, subst: &Canonical<Substitution<I>>) -> bool; -} - -impl<I: Interner> SubstitutionExt<I> for Substitution<I> { - fn may_invalidate(&self, interner: I, subst: &Canonical<Substitution<I>>) -> bool { - self.iter(interner) - .zip(subst.value.iter(interner)) - .any(|(new, current)| MayInvalidate { interner }.aggregate_generic_args(new, current)) - } -} - -// This is a struct in case we need to add state at any point like in AntiUnifier -struct MayInvalidate<I> { - interner: I, -} - -impl<I: Interner> MayInvalidate<I> { - fn aggregate_generic_args(&mut self, new: &GenericArg<I>, current: &GenericArg<I>) -> bool { - let interner = self.interner; - match (new.data(interner), current.data(interner)) { - (GenericArgData::Ty(ty1), GenericArgData::Ty(ty2)) => self.aggregate_tys(ty1, ty2), - (GenericArgData::Lifetime(l1), GenericArgData::Lifetime(l2)) => { - self.aggregate_lifetimes(l1, l2) - } - (GenericArgData::Const(c1), GenericArgData::Const(c2)) => self.aggregate_consts(c1, c2), - (GenericArgData::Ty(_), _) - | (GenericArgData::Lifetime(_), _) - | (GenericArgData::Const(_), _) => panic!( - "mismatched parameter kinds: new={:?} current={:?}", - new, current - ), - } - } - - /// Returns true if the two types could be unequal. - fn aggregate_tys(&mut self, new: &Ty<I>, current: &Ty<I>) -> bool { - let interner = self.interner; - match (new.kind(interner), current.kind(interner)) { - (_, TyKind::BoundVar(_)) => { - // If the aggregate solution already has an inference - // variable here, then no matter what type we produce, - // the aggregate cannot get 'more generalized' than it - // already is. So return false, we cannot invalidate. - // - // (Note that "inference variables" show up as *bound - // variables* here, because we are looking at the - // canonical form.) - false - } - - (TyKind::BoundVar(_), _) => { - // If we see a type variable in the potential future - // solution, we have to be conservative. We don't know - // what type variable will wind up being! Remember - // that the future solution could be any instantiation - // of `ty0` -- or it could leave this variable - // unbound, if the result is true for all types. - // - // (Note that "inference variables" show up as *bound - // variables* here, because we are looking at the - // canonical form.) - true - } - - (TyKind::InferenceVar(_, _), _) | (_, TyKind::InferenceVar(_, _)) => { - panic!( - "unexpected free inference variable in may-invalidate: {:?} vs {:?}", - new, current, - ); - } - - (TyKind::Placeholder(p1), TyKind::Placeholder(p2)) => { - self.aggregate_placeholders(p1, p2) - } - - ( - TyKind::Alias(AliasTy::Projection(proj1)), - TyKind::Alias(AliasTy::Projection(proj2)), - ) => self.aggregate_projection_tys(proj1, proj2), - - ( - TyKind::Alias(AliasTy::Opaque(opaque_ty1)), - TyKind::Alias(AliasTy::Opaque(opaque_ty2)), - ) => self.aggregate_opaque_ty_tys(opaque_ty1, opaque_ty2), - - (TyKind::Adt(id_a, substitution_a), TyKind::Adt(id_b, substitution_b)) => { - self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - } - ( - TyKind::AssociatedType(id_a, substitution_a), - TyKind::AssociatedType(id_b, substitution_b), - ) => self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b), - (TyKind::Scalar(scalar_a), TyKind::Scalar(scalar_b)) => scalar_a != scalar_b, - (TyKind::Str, TyKind::Str) => false, - (TyKind::Tuple(arity_a, substitution_a), TyKind::Tuple(arity_b, substitution_b)) => { - self.aggregate_name_and_substs(arity_a, substitution_a, arity_b, substitution_b) - } - ( - TyKind::OpaqueType(id_a, substitution_a), - TyKind::OpaqueType(id_b, substitution_b), - ) => self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b), - (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => self.aggregate_tys(ty_a, ty_b), - (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => { - self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - } - (TyKind::Ref(id_a, lifetime_a, ty_a), TyKind::Ref(id_b, lifetime_b, ty_b)) => { - id_a != id_b - || self.aggregate_lifetimes(lifetime_a, lifetime_b) - || self.aggregate_tys(ty_a, ty_b) - } - (TyKind::Raw(id_a, ty_a), TyKind::Raw(id_b, ty_b)) => { - id_a != id_b || self.aggregate_tys(ty_a, ty_b) - } - (TyKind::Never, TyKind::Never) => false, - (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => { - self.aggregate_tys(ty_a, ty_b) || self.aggregate_consts(const_a, const_b) - } - (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => { - self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - } - (TyKind::Generator(id_a, substitution_a), TyKind::Generator(id_b, substitution_b)) => { - self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - } - ( - TyKind::GeneratorWitness(id_a, substitution_a), - TyKind::GeneratorWitness(id_b, substitution_b), - ) => self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b), - (TyKind::Foreign(id_a), TyKind::Foreign(id_b)) => id_a != id_b, - (TyKind::Error, TyKind::Error) => false, - - (_, _) => true, - } - } - - /// Returns true if the two consts could be unequal. - fn aggregate_lifetimes(&mut self, _: &Lifetime<I>, _: &Lifetime<I>) -> bool { - true - } - - /// Returns true if the two consts could be unequal. - fn aggregate_consts(&mut self, new: &Const<I>, current: &Const<I>) -> bool { - let interner = self.interner; - let ConstData { - ty: new_ty, - value: new_value, - } = new.data(interner); - let ConstData { - ty: current_ty, - value: current_value, - } = current.data(interner); - - if self.aggregate_tys(new_ty, current_ty) { - return true; - } - - match (new_value, current_value) { - (_, ConstValue::BoundVar(_)) => { - // see comment in aggregate_tys - false - } - - (ConstValue::BoundVar(_), _) => { - // see comment in aggregate_tys - true - } - - (ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => { - panic!( - "unexpected free inference variable in may-invalidate: {:?} vs {:?}", - new, current, - ); - } - - (ConstValue::Placeholder(p1), ConstValue::Placeholder(p2)) => { - self.aggregate_placeholders(p1, p2) - } - - (ConstValue::Concrete(c1), ConstValue::Concrete(c2)) => { - !c1.const_eq(new_ty, c2, interner) - } - - // Only variants left are placeholder = concrete, which always fails - (ConstValue::Placeholder(_), _) | (ConstValue::Concrete(_), _) => true, - } - } - - fn aggregate_placeholders( - &mut self, - new: &PlaceholderIndex, - current: &PlaceholderIndex, - ) -> bool { - new != current - } - - fn aggregate_projection_tys( - &mut self, - new: &ProjectionTy<I>, - current: &ProjectionTy<I>, - ) -> bool { - let ProjectionTy { - associated_ty_id: new_name, - substitution: new_substitution, - } = new; - let ProjectionTy { - associated_ty_id: current_name, - substitution: current_substitution, - } = current; - - self.aggregate_name_and_substs( - new_name, - new_substitution, - current_name, - current_substitution, - ) - } - - fn aggregate_opaque_ty_tys(&mut self, new: &OpaqueTy<I>, current: &OpaqueTy<I>) -> bool { - let OpaqueTy { - opaque_ty_id: new_name, - substitution: new_substitution, - } = new; - let OpaqueTy { - opaque_ty_id: current_name, - substitution: current_substitution, - } = current; - - self.aggregate_name_and_substs( - new_name, - new_substitution, - current_name, - current_substitution, - ) - } - - fn aggregate_name_and_substs<N>( - &mut self, - new_name: N, - new_substitution: &Substitution<I>, - current_name: N, - current_substitution: &Substitution<I>, - ) -> bool - where - N: Copy + Eq + Debug, - { - let interner = self.interner; - if new_name != current_name { - return true; - } - - let name = new_name; - - assert_eq!( - new_substitution.len(interner), - current_substitution.len(interner), - "does {:?} take {} substitution or {}? can't both be right", - name, - new_substitution.len(interner), - current_substitution.len(interner) - ); - - new_substitution - .iter(interner) - .zip(current_substitution.iter(interner)) - .any(|(new, current)| self.aggregate_generic_args(new, current)) - } -} diff --git a/vendor/chalk-engine/src/slg/aggregate.rs b/vendor/chalk-engine/src/slg/aggregate.rs deleted file mode 100644 index cce4e14dd..000000000 --- a/vendor/chalk-engine/src/slg/aggregate.rs +++ /dev/null @@ -1,642 +0,0 @@ -use crate::context::{self, AnswerResult}; -use crate::slg::SlgContextOps; -use crate::slg::SubstitutionExt; -use crate::CompleteAnswer; -use chalk_ir::cast::Cast; -use chalk_ir::interner::Interner; -use chalk_ir::*; -use chalk_solve::ext::*; -use chalk_solve::infer::InferenceTable; -use chalk_solve::solve::{Guidance, Solution}; - -use std::fmt::Debug; - -/// Methods for combining solutions to yield an aggregate solution. -pub trait AggregateOps<I: Interner> { - fn make_solution( - &self, - root_goal: &UCanonical<InEnvironment<Goal<I>>>, - answers: impl context::AnswerStream<I>, - should_continue: impl std::ops::Fn() -> bool, - ) -> Option<Solution<I>>; -} - -/// Draws as many answers as it needs from `answers` (but -/// no more!) in order to come up with a solution. -impl<I: Interner> AggregateOps<I> for SlgContextOps<'_, I> { - fn make_solution( - &self, - root_goal: &UCanonical<InEnvironment<Goal<I>>>, - mut answers: impl context::AnswerStream<I>, - should_continue: impl std::ops::Fn() -> bool, - ) -> Option<Solution<I>> { - let interner = self.program.interner(); - let CompleteAnswer { subst, ambiguous } = match answers.next_answer(&should_continue) { - AnswerResult::NoMoreSolutions => { - // No answers at all - return None; - } - AnswerResult::Answer(answer) => answer, - AnswerResult::Floundered => CompleteAnswer { - subst: self.identity_constrained_subst(root_goal), - ambiguous: true, - }, - AnswerResult::QuantumExceeded => { - return Some(Solution::Ambig(Guidance::Unknown)); - } - }; - - // Exactly 1 unconditional answer? - let next_answer = answers.peek_answer(&should_continue); - if next_answer.is_quantum_exceeded() { - if subst.value.subst.is_identity_subst(interner) { - return Some(Solution::Ambig(Guidance::Unknown)); - } else { - return Some(Solution::Ambig(Guidance::Suggested( - subst.map(interner, |cs| cs.subst), - ))); - } - } - if next_answer.is_no_more_solutions() && !ambiguous { - return Some(Solution::Unique(subst)); - } - - // Otherwise, we either have >1 answer, or else we have - // ambiguity. Either way, we are only going to be giving back - // **guidance**, and with guidance, the caller doesn't get - // back any region constraints. So drop them from our `subst` - // variable. - // - // FIXME-- there is actually a 3rd possibility. We could have - // >1 answer where all the answers have the same substitution, - // but different region constraints. We should collapse those - // cases into an `OR` region constraint at some point, but I - // leave that for future work. This is basically - // rust-lang/rust#21974. - let mut subst = subst.map(interner, |cs| cs.subst); - - // Extract answers and merge them into `subst`. Stop once we have - // a trivial subst (or run out of answers). - let mut num_answers = 1; - let guidance = loop { - if subst.value.is_empty(interner) || is_trivial(interner, &subst) { - break Guidance::Unknown; - } - - if !answers - .any_future_answer(|ref mut new_subst| new_subst.may_invalidate(interner, &subst)) - { - break Guidance::Definite(subst); - } - - if let Some(expected_answers) = self.expected_answers { - if num_answers >= expected_answers { - panic!("Too many answers for solution."); - } - } - - let new_subst = match answers.next_answer(&should_continue) { - AnswerResult::Answer(answer1) => answer1.subst, - AnswerResult::Floundered => { - // FIXME: this doesn't trigger for any current tests - self.identity_constrained_subst(root_goal) - } - AnswerResult::NoMoreSolutions => { - break Guidance::Definite(subst); - } - AnswerResult::QuantumExceeded => { - break Guidance::Suggested(subst); - } - }; - subst = merge_into_guidance(interner, &root_goal.canonical, subst, &new_subst); - num_answers += 1; - }; - - if let Some(expected_answers) = self.expected_answers { - assert_eq!( - expected_answers, num_answers, - "Not enough answers for solution." - ); - } - Some(Solution::Ambig(guidance)) - } -} - -/// Given a current substitution used as guidance for `root_goal`, and -/// a new possible answer to `root_goal`, returns a new set of -/// guidance that encompasses both of them. This is often more general -/// than the old guidance. For example, if we had a guidance of `?0 = -/// u32` and the new answer is `?0 = i32`, then the guidance would -/// become `?0 = ?X` (where `?X` is some fresh variable). -fn merge_into_guidance<I: Interner>( - interner: I, - root_goal: &Canonical<InEnvironment<Goal<I>>>, - guidance: Canonical<Substitution<I>>, - answer: &Canonical<ConstrainedSubst<I>>, -) -> Canonical<Substitution<I>> { - let mut infer = InferenceTable::new(); - let Canonical { - value: ConstrainedSubst { - subst: subst1, - constraints: _, - }, - binders: _, - } = answer; - - // Collect the types that the two substitutions have in - // common. - let aggr_generic_args: Vec<_> = guidance - .value - .iter(interner) - .zip(subst1.iter(interner)) - .enumerate() - .map(|(index, (p1, p2))| { - // We have two values for some variable X that - // appears in the root goal. Find out the universe - // of X. - let universe = *root_goal.binders.as_slice(interner)[index].skip_kind(); - - match p1.data(interner) { - GenericArgData::Ty(_) => (), - GenericArgData::Lifetime(_) => { - // Ignore the lifetimes from the substitution: we're just - // creating guidance here anyway. - return infer - .new_variable(universe) - .to_lifetime(interner) - .cast(interner); - } - GenericArgData::Const(_) => (), - }; - - // Combine the two types into a new type. - let mut aggr = AntiUnifier { - infer: &mut infer, - universe, - interner, - }; - aggr.aggregate_generic_args(p1, p2) - }) - .collect(); - - let aggr_subst = Substitution::from_iter(interner, aggr_generic_args); - - infer.canonicalize(interner, aggr_subst).quantified -} - -fn is_trivial<I: Interner>(interner: I, subst: &Canonical<Substitution<I>>) -> bool { - // A subst is trivial if.. - subst - .value - .iter(interner) - .enumerate() - .all(|(index, parameter)| { - let is_trivial = |b: Option<BoundVar>| match b { - None => false, - Some(bound_var) => { - if let Some(index1) = bound_var.index_if_innermost() { - index == index1 - } else { - false - } - } - }; - - match parameter.data(interner) { - // All types and consts are mapped to distinct variables. Since this - // has been canonicalized, those will also be the first N - // variables. - GenericArgData::Ty(t) => is_trivial(t.bound_var(interner)), - GenericArgData::Const(t) => is_trivial(t.bound_var(interner)), - - // And no lifetime mappings. (This is too strict, but we never - // product substs with lifetimes.) - GenericArgData::Lifetime(_) => false, - } - }) -} - -/// [Anti-unification] is the act of taking two things that do not -/// unify and finding a minimal generalization of them. So for -/// example `Vec<u32>` anti-unified with `Vec<i32>` might be -/// `Vec<?X>`. This is a **very simplistic** anti-unifier. -/// -/// NOTE: The values here are canonicalized, but output is not, this means -/// that any escaping bound variables that we see have to be replaced with -/// inference variables. -/// -/// [Anti-unification]: https://en.wikipedia.org/wiki/Anti-unification_(computer_science) -struct AntiUnifier<'infer, I: Interner> { - infer: &'infer mut InferenceTable<I>, - universe: UniverseIndex, - interner: I, -} - -impl<I: Interner> AntiUnifier<'_, I> { - fn aggregate_tys(&mut self, ty0: &Ty<I>, ty1: &Ty<I>) -> Ty<I> { - let interner = self.interner; - match (ty0.kind(interner), ty1.kind(interner)) { - // If we see bound things on either side, just drop in a - // fresh variable. This means we will sometimes - // overgeneralize. So for example if we have two - // solutions that are both `(X, X)`, we just produce `(Y, - // Z)` in all cases. - (TyKind::InferenceVar(_, _), TyKind::InferenceVar(_, _)) => self.new_ty_variable(), - - // Ugh. Aggregating two types like `for<'a> fn(&'a u32, - // &'a u32)` and `for<'a, 'b> fn(&'a u32, &'b u32)` seems - // kinda hard. Don't try to be smart for now, just plop a - // variable in there and be done with it. - // This also ensures that any bound variables we do see - // were bound by `Canonical`. - (TyKind::BoundVar(_), TyKind::BoundVar(_)) - | (TyKind::Function(_), TyKind::Function(_)) - | (TyKind::Dyn(_), TyKind::Dyn(_)) => self.new_ty_variable(), - - ( - TyKind::Alias(AliasTy::Projection(proj1)), - TyKind::Alias(AliasTy::Projection(proj2)), - ) => self.aggregate_projection_tys(proj1, proj2), - - ( - TyKind::Alias(AliasTy::Opaque(opaque_ty1)), - TyKind::Alias(AliasTy::Opaque(opaque_ty2)), - ) => self.aggregate_opaque_ty_tys(opaque_ty1, opaque_ty2), - - (TyKind::Placeholder(placeholder1), TyKind::Placeholder(placeholder2)) => { - self.aggregate_placeholder_tys(placeholder1, placeholder2) - } - - (TyKind::Adt(id_a, substitution_a), TyKind::Adt(id_b, substitution_b)) => self - .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - .map(|(&name, substitution)| TyKind::Adt(name, substitution).intern(interner)) - .unwrap_or_else(|| self.new_ty_variable()), - ( - TyKind::AssociatedType(id_a, substitution_a), - TyKind::AssociatedType(id_b, substitution_b), - ) => self - .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - .map(|(&name, substitution)| { - TyKind::AssociatedType(name, substitution).intern(interner) - }) - .unwrap_or_else(|| self.new_ty_variable()), - (TyKind::Scalar(scalar_a), TyKind::Scalar(scalar_b)) => { - if scalar_a == scalar_b { - TyKind::Scalar(*scalar_a).intern(interner) - } else { - self.new_ty_variable() - } - } - (TyKind::Str, TyKind::Str) => TyKind::Str.intern(interner), - (TyKind::Tuple(arity_a, substitution_a), TyKind::Tuple(arity_b, substitution_b)) => { - self.aggregate_name_and_substs(arity_a, substitution_a, arity_b, substitution_b) - .map(|(&name, substitution)| TyKind::Tuple(name, substitution).intern(interner)) - .unwrap_or_else(|| self.new_ty_variable()) - } - ( - TyKind::OpaqueType(id_a, substitution_a), - TyKind::OpaqueType(id_b, substitution_b), - ) => self - .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - .map(|(&name, substitution)| { - TyKind::OpaqueType(name, substitution).intern(interner) - }) - .unwrap_or_else(|| self.new_ty_variable()), - (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => { - TyKind::Slice(self.aggregate_tys(ty_a, ty_b)).intern(interner) - } - (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => self - .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - .map(|(&name, substitution)| TyKind::FnDef(name, substitution).intern(interner)) - .unwrap_or_else(|| self.new_ty_variable()), - (TyKind::Ref(id_a, lifetime_a, ty_a), TyKind::Ref(id_b, lifetime_b, ty_b)) => { - if id_a == id_b { - TyKind::Ref( - *id_a, - self.aggregate_lifetimes(lifetime_a, lifetime_b), - self.aggregate_tys(ty_a, ty_b), - ) - .intern(interner) - } else { - self.new_ty_variable() - } - } - (TyKind::Raw(id_a, ty_a), TyKind::Raw(id_b, ty_b)) => { - if id_a == id_b { - TyKind::Raw(*id_a, self.aggregate_tys(ty_a, ty_b)).intern(interner) - } else { - self.new_ty_variable() - } - } - (TyKind::Never, TyKind::Never) => TyKind::Never.intern(interner), - (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => TyKind::Array( - self.aggregate_tys(ty_a, ty_b), - self.aggregate_consts(const_a, const_b), - ) - .intern(interner), - (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => self - .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - .map(|(&name, substitution)| TyKind::Closure(name, substitution).intern(interner)) - .unwrap_or_else(|| self.new_ty_variable()), - (TyKind::Generator(id_a, substitution_a), TyKind::Generator(id_b, substitution_b)) => { - self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - .map(|(&name, substitution)| { - TyKind::Generator(name, substitution).intern(interner) - }) - .unwrap_or_else(|| self.new_ty_variable()) - } - ( - TyKind::GeneratorWitness(id_a, substitution_a), - TyKind::GeneratorWitness(id_b, substitution_b), - ) => self - .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b) - .map(|(&name, substitution)| { - TyKind::GeneratorWitness(name, substitution).intern(interner) - }) - .unwrap_or_else(|| self.new_ty_variable()), - (TyKind::Foreign(id_a), TyKind::Foreign(id_b)) => { - if id_a == id_b { - TyKind::Foreign(*id_a).intern(interner) - } else { - self.new_ty_variable() - } - } - (TyKind::Error, TyKind::Error) => TyKind::Error.intern(interner), - - (_, _) => self.new_ty_variable(), - } - } - - fn aggregate_placeholder_tys( - &mut self, - index1: &PlaceholderIndex, - index2: &PlaceholderIndex, - ) -> Ty<I> { - let interner = self.interner; - if index1 != index2 { - self.new_ty_variable() - } else { - TyKind::Placeholder(*index1).intern(interner) - } - } - - fn aggregate_projection_tys( - &mut self, - proj1: &ProjectionTy<I>, - proj2: &ProjectionTy<I>, - ) -> Ty<I> { - let interner = self.interner; - let ProjectionTy { - associated_ty_id: name1, - substitution: substitution1, - } = proj1; - let ProjectionTy { - associated_ty_id: name2, - substitution: substitution2, - } = proj2; - - self.aggregate_name_and_substs(name1, substitution1, name2, substitution2) - .map(|(&associated_ty_id, substitution)| { - TyKind::Alias(AliasTy::Projection(ProjectionTy { - associated_ty_id, - substitution, - })) - .intern(interner) - }) - .unwrap_or_else(|| self.new_ty_variable()) - } - - fn aggregate_opaque_ty_tys( - &mut self, - opaque_ty1: &OpaqueTy<I>, - opaque_ty2: &OpaqueTy<I>, - ) -> Ty<I> { - let OpaqueTy { - opaque_ty_id: name1, - substitution: substitution1, - } = opaque_ty1; - let OpaqueTy { - opaque_ty_id: name2, - substitution: substitution2, - } = opaque_ty2; - - self.aggregate_name_and_substs(name1, substitution1, name2, substitution2) - .map(|(&opaque_ty_id, substitution)| { - TyKind::Alias(AliasTy::Opaque(OpaqueTy { - opaque_ty_id, - substitution, - })) - .intern(self.interner) - }) - .unwrap_or_else(|| self.new_ty_variable()) - } - - fn aggregate_name_and_substs<N>( - &mut self, - name1: N, - substitution1: &Substitution<I>, - name2: N, - substitution2: &Substitution<I>, - ) -> Option<(N, Substitution<I>)> - where - N: Copy + Eq + Debug, - { - let interner = self.interner; - if name1 != name2 { - return None; - } - - let name = name1; - - assert_eq!( - substitution1.len(interner), - substitution2.len(interner), - "does {:?} take {} substitution or {}? can't both be right", - name, - substitution1.len(interner), - substitution2.len(interner) - ); - - let substitution = Substitution::from_iter( - interner, - substitution1 - .iter(interner) - .zip(substitution2.iter(interner)) - .map(|(p1, p2)| self.aggregate_generic_args(p1, p2)), - ); - - Some((name, substitution)) - } - - fn aggregate_generic_args(&mut self, p1: &GenericArg<I>, p2: &GenericArg<I>) -> GenericArg<I> { - let interner = self.interner; - match (p1.data(interner), p2.data(interner)) { - (GenericArgData::Ty(ty1), GenericArgData::Ty(ty2)) => { - self.aggregate_tys(ty1, ty2).cast(interner) - } - (GenericArgData::Lifetime(l1), GenericArgData::Lifetime(l2)) => { - self.aggregate_lifetimes(l1, l2).cast(interner) - } - (GenericArgData::Const(c1), GenericArgData::Const(c2)) => { - self.aggregate_consts(c1, c2).cast(interner) - } - (GenericArgData::Ty(_), _) - | (GenericArgData::Lifetime(_), _) - | (GenericArgData::Const(_), _) => { - panic!("mismatched parameter kinds: p1={:?} p2={:?}", p1, p2) - } - } - } - - fn aggregate_lifetimes(&mut self, l1: &Lifetime<I>, l2: &Lifetime<I>) -> Lifetime<I> { - let interner = self.interner; - match (l1.data(interner), l2.data(interner)) { - (LifetimeData::Phantom(void, ..), _) | (_, LifetimeData::Phantom(void, ..)) => { - match *void {} - } - (LifetimeData::BoundVar(..), _) | (_, LifetimeData::BoundVar(..)) => { - self.new_lifetime_variable() - } - _ => { - if l1 == l2 { - l1.clone() - } else { - self.new_lifetime_variable() - } - } - } - } - - fn aggregate_consts(&mut self, c1: &Const<I>, c2: &Const<I>) -> Const<I> { - let interner = self.interner; - - // It would be nice to check that c1 and c2 have the same type, even though - // on this stage of solving they should already have the same type. - - let ConstData { - ty: c1_ty, - value: c1_value, - } = c1.data(interner); - let ConstData { - ty: _c2_ty, - value: c2_value, - } = c2.data(interner); - - let ty = c1_ty.clone(); - - match (c1_value, c2_value) { - (ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => { - self.new_const_variable(ty) - } - - (ConstValue::BoundVar(_), _) | (_, ConstValue::BoundVar(_)) => { - self.new_const_variable(ty) - } - - (ConstValue::Placeholder(_), ConstValue::Placeholder(_)) => { - if c1 == c2 { - c1.clone() - } else { - self.new_const_variable(ty) - } - } - (ConstValue::Concrete(e1), ConstValue::Concrete(e2)) => { - if e1.const_eq(&ty, e2, interner) { - c1.clone() - } else { - self.new_const_variable(ty) - } - } - - (ConstValue::Placeholder(_), _) | (_, ConstValue::Placeholder(_)) => { - self.new_const_variable(ty) - } - } - } - - fn new_ty_variable(&mut self) -> Ty<I> { - let interner = self.interner; - self.infer.new_variable(self.universe).to_ty(interner) - } - - fn new_lifetime_variable(&mut self) -> Lifetime<I> { - let interner = self.interner; - self.infer.new_variable(self.universe).to_lifetime(interner) - } - - fn new_const_variable(&mut self, ty: Ty<I>) -> Const<I> { - let interner = self.interner; - self.infer - .new_variable(self.universe) - .to_const(interner, ty) - } -} - -#[cfg(test)] -mod test { - use crate::slg::aggregate::AntiUnifier; - use chalk_integration::{arg, ty}; - use chalk_ir::UniverseIndex; - use chalk_solve::infer::InferenceTable; - - /// Test the equivalent of `Vec<i32>` vs `Vec<u32>` - #[test] - fn vec_i32_vs_vec_u32() { - use chalk_integration::interner::ChalkIr; - let mut infer: InferenceTable<ChalkIr> = InferenceTable::new(); - let mut anti_unifier = AntiUnifier { - infer: &mut infer, - universe: UniverseIndex::root(), - interner: ChalkIr, - }; - - let ty = anti_unifier.aggregate_tys( - &ty!(apply (item 0) (apply (item 1))), - &ty!(apply (item 0) (apply (item 2))), - ); - assert_eq!(ty!(apply (item 0) (infer 0)), ty); - } - - /// Test the equivalent of `Vec<i32>` vs `Vec<i32>` - #[test] - fn vec_i32_vs_vec_i32() { - use chalk_integration::interner::ChalkIr; - let interner = ChalkIr; - let mut infer: InferenceTable<ChalkIr> = InferenceTable::new(); - let mut anti_unifier = AntiUnifier { - interner, - infer: &mut infer, - universe: UniverseIndex::root(), - }; - - let ty = anti_unifier.aggregate_tys( - &ty!(apply (item 0) (apply (item 1))), - &ty!(apply (item 0) (apply (item 1))), - ); - assert_eq!(ty!(apply (item 0) (apply (item 1))), ty); - } - - /// Test the equivalent of `Vec<X>` vs `Vec<Y>` - #[test] - fn vec_x_vs_vec_y() { - use chalk_integration::interner::ChalkIr; - let interner = ChalkIr; - let mut infer: InferenceTable<ChalkIr> = InferenceTable::new(); - let mut anti_unifier = AntiUnifier { - interner, - infer: &mut infer, - universe: UniverseIndex::root(), - }; - - // Note that the `var 0` and `var 1` in these types would be - // referring to canonicalized free variables, not variables in - // `infer`. - let ty = anti_unifier.aggregate_tys( - &ty!(apply (item 0) (infer 0)), - &ty!(apply (item 0) (infer 1)), - ); - - // But this `var 0` is from `infer. - assert_eq!(ty!(apply (item 0) (infer 0)), ty); - } -} diff --git a/vendor/chalk-engine/src/slg/resolvent.rs b/vendor/chalk-engine/src/slg/resolvent.rs deleted file mode 100644 index 3863fc429..000000000 --- a/vendor/chalk-engine/src/slg/resolvent.rs +++ /dev/null @@ -1,729 +0,0 @@ -use crate::normalize_deep::DeepNormalizer; -use crate::slg::ResolventOps; -use crate::{ExClause, Literal, TimeStamp}; -use chalk_ir::cast::Caster; -use chalk_ir::fold::shift::Shift; -use chalk_ir::fold::TypeFoldable; -use chalk_ir::interner::{HasInterner, Interner}; -use chalk_ir::zip::{Zip, Zipper}; -use chalk_ir::*; -use chalk_solve::infer::InferenceTable; -use tracing::{debug, instrument}; - -/////////////////////////////////////////////////////////////////////////// -// SLG RESOLVENTS -// -// The "SLG Resolvent" is used to combine a *goal* G with some -// clause or answer *C*. It unifies the goal's selected literal -// with the clause and then inserts the clause's conditions into -// the goal's list of things to prove, basically. Although this is -// one operation in EWFS, we have specialized variants for merging -// a program clause and an answer (though they share some code in -// common). -// -// Terminology note: The NFTD and RR papers use the term -// "resolvent" to mean both the factor and the resolvent, but EWFS -// distinguishes the two. We follow EWFS here since -- in the code -// -- we tend to know whether there are delayed literals or not, -// and hence to know which code path we actually want. -// -// From EWFS: -// -// Let G be an X-clause A :- D | L1,...Ln, where N > 0, and Li be selected atom. -// -// Let C be an X-clause with no delayed literals. Let -// -// C' = A' :- L'1...L'm -// -// be a variant of C such that G and C' have no variables in -// common. -// -// Let Li and A' be unified with MGU S. -// -// Then: -// -// S(A :- D | L1...Li-1, L1'...L'm, Li+1...Ln) -// -// is the SLG resolvent of G with C. - -impl<I: Interner> ResolventOps<I> for InferenceTable<I> { - /// Applies the SLG resolvent algorithm to incorporate a program - /// clause into the main X-clause, producing a new X-clause that - /// must be solved. - /// - /// # Parameters - /// - /// - `goal` is the goal G that we are trying to solve - /// - `clause` is the program clause that may be useful to that end - #[instrument(level = "debug", skip(self, interner, environment, subst))] - fn resolvent_clause( - &mut self, - db: &dyn UnificationDatabase<I>, - interner: I, - environment: &Environment<I>, - goal: &DomainGoal<I>, - subst: &Substitution<I>, - clause: &ProgramClause<I>, - ) -> Fallible<ExClause<I>> { - // Relating the above description to our situation: - // - // - `goal` G, except with binders for any existential variables. - // - Also, we always select the first literal in `ex_clause.literals`, so `i` is 0. - // - `clause` is C, except with binders for any existential variables. - - // C' in the description above is `consequence :- conditions`. - // - // Note that G and C' have no variables in common. - let ProgramClauseImplication { - consequence, - conditions, - constraints, - priority: _, - } = { - let ProgramClauseData(implication) = clause.data(interner); - - self.instantiate_binders_existentially(interner, implication.clone()) - }; - debug!(?consequence, ?conditions, ?constraints); - - // Unify the selected literal Li with C'. - let unification_result = self.relate( - interner, - db, - environment, - Variance::Invariant, - goal, - &consequence, - )?; - - // Final X-clause that we will return. - let mut ex_clause = ExClause { - subst: subst.clone(), - ambiguous: false, - constraints: vec![], - subgoals: vec![], - delayed_subgoals: vec![], - answer_time: TimeStamp::default(), - floundered_subgoals: vec![], - }; - - // Add the subgoals/region-constraints that unification gave us. - ex_clause.subgoals.extend( - unification_result - .goals - .into_iter() - .casted(interner) - .map(Literal::Positive), - ); - - ex_clause - .constraints - .extend(constraints.as_slice(interner).to_owned()); - - // Add the `conditions` from the program clause into the result too. - ex_clause - .subgoals - .extend(conditions.iter(interner).map(|c| match c.data(interner) { - GoalData::Not(c1) => { - Literal::Negative(InEnvironment::new(environment, Goal::clone(c1))) - } - _ => Literal::Positive(InEnvironment::new(environment, Goal::clone(c))), - })); - - Ok(ex_clause) - } - - /////////////////////////////////////////////////////////////////////////// - // apply_answer_subst - // - // Apply answer subst has the job of "plugging in" the answer to a - // query into the pending ex-clause. To see how it works, it's worth stepping - // up one level. Imagine that first we are trying to prove a goal A: - // - // A :- T: Foo<Vec<?U>>, ?U: Bar - // - // this spawns a subgoal `T: Foo<Vec<?0>>`, and it's this subgoal that - // has now produced an answer `?0 = u32`. When the goal A spawned the - // subgoal, it will also have registered a `PendingExClause` with its - // current state. At the point where *this* method has been invoked, - // that pending ex-clause has been instantiated with fresh variables and setup, - // so we have four bits of incoming information: - // - // - `ex_clause`, which is the remaining stuff to prove for the goal A. - // Here, the inference variable `?U` has been instantiated with a fresh variable - // `?X`. - // - `A :- ?X: Bar` - // - `selected_goal`, which is the thing we were trying to prove when we - // spawned the subgoal. It shares inference variables with `ex_clause`. - // - `T: Foo<Vec<?X>>` - // - `answer_table_goal`, which is the subgoal in canonical form: - // - `for<type> T: Foo<Vec<?0>>` - // - `canonical_answer_subst`, which is an answer to `answer_table_goal`. - // - `[?0 = u32]` - // - // In this case, this function will (a) unify `u32` and `?X` and then - // (b) return `ex_clause` (extended possibly with new region constraints - // and subgoals). - // - // One way to do this would be to (a) substitute - // `canonical_answer_subst` into `answer_table_goal` (yielding `T: - // Foo<Vec<u32>>`) and then (b) instantiate the result with fresh - // variables (no effect in this instance) and then (c) unify that with - // `selected_goal` (yielding, indirectly, that `?X = u32`). But that - // is not what we do: it's inefficient, to start, but it also causes - // problems because unification of projections can make new - // sub-goals. That is, even if the answers don't involve any - // projections, the table goals might, and this can create an infinite - // loop (see also #74). - // - // What we do instead is to (a) instantiate the substitution, which - // may have free variables in it (in this case, it would not, and the - // instantiation would have no effect) and then (b) zip - // `answer_table_goal` and `selected_goal` without having done any - // substitution. After all, these ought to be basically the same, - // since `answer_table_goal` was created by canonicalizing (and - // possibly truncating, but we'll get to that later) - // `selected_goal`. Then, whenever we reach a "free variable" in - // `answer_table_goal`, say `?0`, we go to the instantiated answer - // substitution and lookup the result (in this case, `u32`). We take - // that result and unify it with whatever we find in `selected_goal` - // (in this case, `?X`). - // - // Let's cover then some corner cases. First off, what is this - // business of instantiating the answer? Well, the answer may not be a - // simple type like `u32`, it could be a "family" of types, like - // `for<type> Vec<?0>` -- i.e., `Vec<X>: Bar` for *any* `X`. In that - // case, the instantiation would produce a substitution `[?0 := - // Vec<?Y>]` (note that the key is not affected, just the value). So - // when we do the unification, instead of unifying `?X = u32`, we - // would unify `?X = Vec<?Y>`. - // - // Next, truncation. One key thing is that the `answer_table_goal` may - // not be *exactly* the same as the `selected_goal` -- we will - // truncate it if it gets too deep. so, in our example, it may be that - // instead of `answer_table_goal` being `for<type> T: Foo<Vec<?0>>`, - // it could have been truncated to `for<type> T: Foo<?0>` (which is a - // more general goal). In that case, let's say that the answer is - // still `[?0 = u32]`, meaning that `T: Foo<u32>` is true (which isn't - // actually interesting to our original goal). When we do the zip - // then, we will encounter `?0` in the `answer_table_goal` and pair - // that with `Vec<?X>` from the pending goal. We will attempt to unify - // `Vec<?X>` with `u32` (from the substitution), which will fail. That - // failure will get propagated back up. - - #[instrument(level = "debug", skip(self, interner))] - fn apply_answer_subst( - &mut self, - interner: I, - unification_database: &dyn UnificationDatabase<I>, - ex_clause: &mut ExClause<I>, - selected_goal: &InEnvironment<Goal<I>>, - answer_table_goal: &Canonical<InEnvironment<Goal<I>>>, - canonical_answer_subst: Canonical<AnswerSubst<I>>, - ) -> Fallible<()> { - debug!(selected_goal = ?DeepNormalizer::normalize_deep(self, interner, selected_goal.clone())); - - // C' is now `answer`. No variables in common with G. - let AnswerSubst { - subst: answer_subst, - - // Assuming unification succeeds, we incorporate the - // region constraints from the answer into the result; - // we'll need them if this answer (which is not yet known - // to be true) winds up being true, and otherwise (if the - // answer is false or unknown) it doesn't matter. - constraints: answer_constraints, - - delayed_subgoals, - } = self.instantiate_canonical(interner, canonical_answer_subst); - - AnswerSubstitutor::substitute( - interner, - unification_database, - self, - &selected_goal.environment, - &answer_subst, - ex_clause, - &answer_table_goal.value, - selected_goal, - )?; - ex_clause - .constraints - .extend(answer_constraints.as_slice(interner).to_vec()); - // at that point we should only have goals that stemmed - // from non trivial self cycles - ex_clause.delayed_subgoals.extend(delayed_subgoals); - Ok(()) - } -} - -struct AnswerSubstitutor<'t, I: Interner> { - table: &'t mut InferenceTable<I>, - environment: &'t Environment<I>, - answer_subst: &'t Substitution<I>, - - /// Tracks the debrujn index of the first binder that is outside - /// the term we are traversing. This starts as `DebruijnIndex::INNERMOST`, - /// since we have not yet traversed *any* binders, but when we visit - /// the inside of a binder, it would be incremented. - /// - /// Example: If we are visiting `(for<type> A, B, C, for<type> for<type> D)`, - /// then this would be: - /// - /// * `1`, when visiting `A`, - /// * `0`, when visiting `B` and `C`, - /// * `2`, when visiting `D`. - outer_binder: DebruijnIndex, - - ex_clause: &'t mut ExClause<I>, - interner: I, - unification_database: &'t dyn UnificationDatabase<I>, -} - -impl<I: Interner> AnswerSubstitutor<'_, I> { - fn substitute<T: Zip<I>>( - interner: I, - unification_database: &dyn UnificationDatabase<I>, - table: &mut InferenceTable<I>, - environment: &Environment<I>, - answer_subst: &Substitution<I>, - ex_clause: &mut ExClause<I>, - answer: &T, - pending: &T, - ) -> Fallible<()> { - let mut this = AnswerSubstitutor { - interner, - unification_database, - table, - environment, - answer_subst, - ex_clause, - outer_binder: DebruijnIndex::INNERMOST, - }; - Zip::zip_with(&mut this, Variance::Invariant, answer, pending)?; - Ok(()) - } - - fn unify_free_answer_var( - &mut self, - interner: I, - db: &dyn UnificationDatabase<I>, - variance: Variance, - answer_var: BoundVar, - pending: GenericArgData<I>, - ) -> Fallible<bool> { - let answer_index = match answer_var.index_if_bound_at(self.outer_binder) { - Some(index) => index, - - // This variable is bound in the answer, not free, so it - // doesn't represent a reference into the answer substitution. - None => return Ok(false), - }; - - let answer_param = self.answer_subst.at(interner, answer_index); - - let pending_shifted = pending - .shifted_out_to(interner, self.outer_binder) - .expect("truncate extracted a pending value that references internal binder"); - - let result = self.table.relate( - interner, - db, - self.environment, - variance, - answer_param, - &GenericArg::new(interner, pending_shifted), - )?; - - self.ex_clause.subgoals.extend( - result - .goals - .into_iter() - .casted(interner) - .map(Literal::Positive), - ); - - Ok(true) - } - - /// When we encounter a variable in the answer goal, we first try - /// `unify_free_answer_var`. Assuming that this fails, the - /// variable must be a bound variable in the answer goal -- in - /// that case, there should be a corresponding bound variable in - /// the pending goal. This bit of code just checks that latter - /// case. - fn assert_matching_vars( - &mut self, - answer_var: BoundVar, - pending_var: BoundVar, - ) -> Fallible<()> { - let BoundVar { - debruijn: answer_depth, - index: answer_index, - } = answer_var; - let BoundVar { - debruijn: pending_depth, - index: pending_index, - } = pending_var; - - // Both bound variables are bound within the term we are matching - assert!(answer_depth.within(self.outer_binder)); - - // They are bound at the same (relative) depth - assert_eq!(answer_depth, pending_depth); - - // They are bound at the same index within the binder - assert_eq!(answer_index, pending_index,); - - Ok(()) - } -} - -impl<'i, I: Interner> Zipper<I> for AnswerSubstitutor<'i, I> { - fn zip_tys(&mut self, variance: Variance, answer: &Ty<I>, pending: &Ty<I>) -> Fallible<()> { - let interner = self.interner; - - if let Some(pending) = self.table.normalize_ty_shallow(interner, pending) { - return Zip::zip_with(self, variance, answer, &pending); - } - - // If the answer has a variable here, then this is one of the - // "inputs" to the subgoal table. We need to extract the - // resulting answer that the subgoal found and unify it with - // the value from our "pending subgoal". - if let TyKind::BoundVar(answer_depth) = answer.kind(interner) { - if self.unify_free_answer_var( - interner, - self.unification_database, - variance, - *answer_depth, - GenericArgData::Ty(pending.clone()), - )? { - return Ok(()); - } - } - - // Otherwise, the answer and the selected subgoal ought to be a perfect match for - // one another. - match (answer.kind(interner), pending.kind(interner)) { - (TyKind::BoundVar(answer_depth), TyKind::BoundVar(pending_depth)) => { - self.assert_matching_vars(*answer_depth, *pending_depth) - } - - (TyKind::Dyn(answer), TyKind::Dyn(pending)) => { - Zip::zip_with(self, variance, answer, pending) - } - - (TyKind::Alias(answer), TyKind::Alias(pending)) => { - Zip::zip_with(self, variance, answer, pending) - } - - (TyKind::Placeholder(answer), TyKind::Placeholder(pending)) => { - Zip::zip_with(self, variance, answer, pending) - } - - (TyKind::Function(answer), TyKind::Function(pending)) => Zip::zip_with( - self, - variance, - &answer.clone().into_binders(interner), - &pending.clone().into_binders(interner), - ), - - (TyKind::InferenceVar(_, _), _) | (_, TyKind::InferenceVar(_, _)) => panic!( - "unexpected inference var in answer `{:?}` or pending goal `{:?}`", - answer, pending, - ), - - (TyKind::Adt(id_a, substitution_a), TyKind::Adt(id_b, substitution_b)) => { - if id_a != id_b { - return Err(NoSolution); - } - self.zip_substs( - variance, - Some(self.unification_database().adt_variance(*id_a)), - substitution_a.as_slice(interner), - substitution_b.as_slice(interner), - ) - } - ( - TyKind::AssociatedType(id_a, substitution_a), - TyKind::AssociatedType(id_b, substitution_b), - ) => { - if id_a != id_b { - return Err(NoSolution); - } - self.zip_substs( - variance, - None, - substitution_a.as_slice(interner), - substitution_b.as_slice(interner), - ) - } - (TyKind::Scalar(scalar_a), TyKind::Scalar(scalar_b)) => { - Zip::zip_with(self, variance, scalar_a, scalar_b) - } - (TyKind::Str, TyKind::Str) => Ok(()), - (TyKind::Tuple(arity_a, substitution_a), TyKind::Tuple(arity_b, substitution_b)) => { - if arity_a != arity_b { - return Err(NoSolution); - } - self.zip_substs( - variance, - None, - substitution_a.as_slice(interner), - substitution_b.as_slice(interner), - ) - } - ( - TyKind::OpaqueType(id_a, substitution_a), - TyKind::OpaqueType(id_b, substitution_b), - ) => { - if id_a != id_b { - return Err(NoSolution); - } - self.zip_substs( - variance, - None, - substitution_a.as_slice(interner), - substitution_b.as_slice(interner), - ) - } - (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => Zip::zip_with(self, variance, ty_a, ty_b), - (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => { - if id_a != id_b { - return Err(NoSolution); - } - self.zip_substs( - variance, - Some(self.unification_database().fn_def_variance(*id_a)), - substitution_a.as_slice(interner), - substitution_b.as_slice(interner), - ) - } - ( - TyKind::Ref(mutability_a, lifetime_a, ty_a), - TyKind::Ref(mutability_b, lifetime_b, ty_b), - ) => { - if mutability_a != mutability_b { - return Err(NoSolution); - } - // The lifetime is `Contravariant` - Zip::zip_with( - self, - variance.xform(Variance::Contravariant), - lifetime_a, - lifetime_b, - )?; - // The type is `Covariant` when not mut, `Invariant` otherwise - let output_variance = match mutability_a { - Mutability::Not => Variance::Covariant, - Mutability::Mut => Variance::Invariant, - }; - Zip::zip_with(self, variance.xform(output_variance), ty_a, ty_b) - } - (TyKind::Raw(mutability_a, ty_a), TyKind::Raw(mutability_b, ty_b)) => { - if mutability_a != mutability_b { - return Err(NoSolution); - } - let ty_variance = match mutability_a { - Mutability::Not => Variance::Covariant, - Mutability::Mut => Variance::Invariant, - }; - Zip::zip_with(self, variance.xform(ty_variance), ty_a, ty_b) - } - (TyKind::Never, TyKind::Never) => Ok(()), - (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => { - Zip::zip_with(self, variance, ty_a, ty_b)?; - Zip::zip_with(self, variance, const_a, const_b) - } - (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => { - if id_a != id_b { - return Err(NoSolution); - } - self.zip_substs( - variance, - None, - substitution_a.as_slice(interner), - substitution_b.as_slice(interner), - ) - } - (TyKind::Generator(id_a, substitution_a), TyKind::Generator(id_b, substitution_b)) => { - if id_a != id_b { - return Err(NoSolution); - } - self.zip_substs( - variance, - None, - substitution_a.as_slice(interner), - substitution_b.as_slice(interner), - ) - } - ( - TyKind::GeneratorWitness(id_a, substitution_a), - TyKind::GeneratorWitness(id_b, substitution_b), - ) => { - if id_a != id_b { - return Err(NoSolution); - } - self.zip_substs( - variance, - None, - substitution_a.as_slice(interner), - substitution_b.as_slice(interner), - ) - } - (TyKind::Foreign(id_a), TyKind::Foreign(id_b)) => { - Zip::zip_with(self, variance, id_a, id_b) - } - (TyKind::Error, TyKind::Error) => Ok(()), - - (_, _) => panic!( - "structural mismatch between answer `{:?}` and pending goal `{:?}`", - answer, pending, - ), - } - } - - fn zip_lifetimes( - &mut self, - variance: Variance, - answer: &Lifetime<I>, - pending: &Lifetime<I>, - ) -> Fallible<()> { - let interner = self.interner; - if let Some(pending) = self.table.normalize_lifetime_shallow(interner, pending) { - return Zip::zip_with(self, variance, answer, &pending); - } - - if let LifetimeData::BoundVar(answer_depth) = answer.data(interner) { - if self.unify_free_answer_var( - interner, - self.unification_database, - variance, - *answer_depth, - GenericArgData::Lifetime(pending.clone()), - )? { - return Ok(()); - } - } - - match (answer.data(interner), pending.data(interner)) { - (LifetimeData::BoundVar(answer_depth), LifetimeData::BoundVar(pending_depth)) => { - self.assert_matching_vars(*answer_depth, *pending_depth) - } - - (LifetimeData::Static, LifetimeData::Static) - | (LifetimeData::Placeholder(_), LifetimeData::Placeholder(_)) - | (LifetimeData::Erased, LifetimeData::Erased) => { - assert_eq!(answer, pending); - Ok(()) - } - - (LifetimeData::InferenceVar(_), _) | (_, LifetimeData::InferenceVar(_)) => panic!( - "unexpected inference var in answer `{:?}` or pending goal `{:?}`", - answer, pending, - ), - - (LifetimeData::Static, _) - | (LifetimeData::BoundVar(_), _) - | (LifetimeData::Placeholder(_), _) - | (LifetimeData::Erased, _) => panic!( - "structural mismatch between answer `{:?}` and pending goal `{:?}`", - answer, pending, - ), - - (LifetimeData::Phantom(void, _), _) => match *void {}, - } - } - - fn zip_consts( - &mut self, - variance: Variance, - answer: &Const<I>, - pending: &Const<I>, - ) -> Fallible<()> { - let interner = self.interner; - if let Some(pending) = self.table.normalize_const_shallow(interner, pending) { - return Zip::zip_with(self, variance, answer, &pending); - } - - let ConstData { - ty: answer_ty, - value: answer_value, - } = answer.data(interner); - let ConstData { - ty: pending_ty, - value: pending_value, - } = pending.data(interner); - - self.zip_tys(variance, answer_ty, pending_ty)?; - - if let ConstValue::BoundVar(answer_depth) = answer_value { - if self.unify_free_answer_var( - interner, - self.unification_database, - variance, - *answer_depth, - GenericArgData::Const(pending.clone()), - )? { - return Ok(()); - } - } - - match (answer_value, pending_value) { - (ConstValue::BoundVar(answer_depth), ConstValue::BoundVar(pending_depth)) => { - self.assert_matching_vars(*answer_depth, *pending_depth) - } - - (ConstValue::Placeholder(_), ConstValue::Placeholder(_)) => { - assert_eq!(answer, pending); - Ok(()) - } - - (ConstValue::Concrete(c1), ConstValue::Concrete(c2)) => { - assert!(c1.const_eq(answer_ty, c2, interner)); - Ok(()) - } - - (ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => panic!( - "unexpected inference var in answer `{:?}` or pending goal `{:?}`", - answer, pending, - ), - - (ConstValue::BoundVar(_), _) - | (ConstValue::Placeholder(_), _) - | (ConstValue::Concrete(_), _) => panic!( - "structural mismatch between answer `{:?}` and pending goal `{:?}`", - answer, pending, - ), - } - } - - fn zip_binders<T>( - &mut self, - variance: Variance, - answer: &Binders<T>, - pending: &Binders<T>, - ) -> Fallible<()> - where - T: HasInterner<Interner = I> + Zip<I> + TypeFoldable<I>, - { - self.outer_binder.shift_in(); - Zip::zip_with( - self, - variance, - answer.skip_binders(), - pending.skip_binders(), - )?; - self.outer_binder.shift_out(); - Ok(()) - } - - fn interner(&self) -> I { - self.interner - } - - fn unification_database(&self) -> &dyn UnificationDatabase<I> { - self.unification_database - } -} diff --git a/vendor/chalk-engine/src/solve.rs b/vendor/chalk-engine/src/solve.rs deleted file mode 100644 index fc35adb66..000000000 --- a/vendor/chalk-engine/src/solve.rs +++ /dev/null @@ -1,89 +0,0 @@ -use crate::context::{AnswerResult, AnswerStream}; -use crate::forest::Forest; -use crate::slg::aggregate::AggregateOps; -use crate::slg::SlgContextOps; -use chalk_ir::interner::Interner; -use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical}; -use chalk_solve::{RustIrDatabase, Solution, Solver, SubstitutionResult}; - -use std::fmt; - -pub struct SLGSolver<I: Interner> { - pub(crate) forest: Forest<I>, - pub(crate) max_size: usize, - pub(crate) expected_answers: Option<usize>, -} - -impl<I: Interner> SLGSolver<I> { - pub fn new(max_size: usize, expected_answers: Option<usize>) -> Self { - Self { - forest: Forest::new(), - max_size, - expected_answers, - } - } -} - -impl<I: Interner> fmt::Debug for SLGSolver<I> { - fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result { - write!(fmt, "SLGSolver") - } -} - -impl<I: Interner> Solver<I> for SLGSolver<I> { - fn solve( - &mut self, - program: &dyn RustIrDatabase<I>, - goal: &UCanonical<InEnvironment<Goal<I>>>, - ) -> Option<Solution<I>> { - let ops = SlgContextOps::new(program, self.max_size, self.expected_answers); - ops.make_solution(goal, self.forest.iter_answers(&ops, goal), || true) - } - - fn solve_limited( - &mut self, - program: &dyn RustIrDatabase<I>, - goal: &UCanonical<InEnvironment<Goal<I>>>, - should_continue: &dyn std::ops::Fn() -> bool, - ) -> Option<Solution<I>> { - let ops = SlgContextOps::new(program, self.max_size, self.expected_answers); - ops.make_solution(goal, self.forest.iter_answers(&ops, goal), should_continue) - } - - fn solve_multiple( - &mut self, - program: &dyn RustIrDatabase<I>, - goal: &UCanonical<InEnvironment<Goal<I>>>, - f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool, - ) -> bool { - let ops = SlgContextOps::new(program, self.max_size, self.expected_answers); - let mut answers = self.forest.iter_answers(&ops, goal); - loop { - let subst = match answers.next_answer(|| true) { - AnswerResult::Answer(answer) => { - if !answer.ambiguous { - SubstitutionResult::Definite(answer.subst) - } else if answer - .subst - .value - .subst - .is_identity_subst(ops.program().interner()) - { - SubstitutionResult::Floundered - } else { - SubstitutionResult::Ambiguous(answer.subst) - } - } - AnswerResult::Floundered => SubstitutionResult::Floundered, - AnswerResult::NoMoreSolutions => { - return true; - } - AnswerResult::QuantumExceeded => continue, - }; - - if !f(subst, !answers.peek_answer(|| true).is_no_more_solutions()) { - return false; - } - } - } -} diff --git a/vendor/chalk-engine/src/stack.rs b/vendor/chalk-engine/src/stack.rs deleted file mode 100644 index 66b53fa58..000000000 --- a/vendor/chalk-engine/src/stack.rs +++ /dev/null @@ -1,175 +0,0 @@ -use crate::index_struct; -use crate::strand::CanonicalStrand; -use crate::tables::Tables; -use crate::{Minimums, TableIndex, TimeStamp}; -use std::fmt; -use std::ops::{Index, IndexMut, Range}; - -use chalk_ir::interner::Interner; - -/// See `Forest`. -#[derive(Debug)] -pub(crate) struct Stack<I: Interner> { - /// Stack: as described above, stores the in-progress goals. - stack: Vec<StackEntry<I>>, -} - -impl<I: Interner> Stack<I> { - // This isn't actually used, but it can be helpful when debugging stack issues - #[allow(dead_code)] - pub(crate) fn debug_with<'a>(&'a self, tables: &'a Tables<I>) -> StackDebug<'_, I> { - StackDebug { - stack: self, - tables, - } - } -} - -pub(crate) struct StackDebug<'a, I: Interner> { - stack: &'a Stack<I>, - tables: &'a Tables<I>, -} - -impl<I: Interner> fmt::Debug for StackDebug<'_, I> { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - writeln!(f, "---- Stack ----")?; - for entry in self.stack.stack.iter() { - writeln!(f, " --- StackEntry ---")?; - writeln!( - f, - " Table {:?} with goal {:?}", - entry.table, self.tables[entry.table].table_goal - )?; - writeln!(f, " Active strand: {:#?}", entry.active_strand)?; - writeln!( - f, - " Additional strands: {:#?}", - self.tables[entry.table].strands().collect::<Vec<_>>() - )?; - } - write!(f, "---- End Stack ----")?; - Ok(()) - } -} - -impl<I: Interner> Default for Stack<I> { - fn default() -> Self { - Stack { stack: vec![] } - } -} - -index_struct! { - /// The StackIndex identifies the position of a table's goal in the - /// stack of goals that are actively being processed. Note that once a - /// table is completely evaluated, it may be popped from the stack, - /// and hence no longer have a stack index. - pub(crate) struct StackIndex { - value: usize, - } -} - -#[derive(Debug)] -pub(crate) struct StackEntry<I: Interner> { - /// The goal G from the stack entry `A :- G` represented here. - pub(super) table: TableIndex, - - /// The clock TimeStamp of this stack entry. - pub(super) clock: TimeStamp, - - pub(super) cyclic_minimums: Minimums, - - // FIXME: should store this as an index. - // This would mean that if we unwind, - // we don't need to worry about losing a strand - pub(super) active_strand: Option<CanonicalStrand<I>>, -} - -impl<I: Interner> Stack<I> { - pub(super) fn is_empty(&self) -> bool { - self.stack.is_empty() - } - - /// Searches the stack to see if `table` is active. If so, returns - /// its stack index. - pub(super) fn is_active(&self, table: TableIndex) -> Option<StackIndex> { - self.stack - .iter() - .enumerate() - .filter_map(|(index, stack_entry)| { - if stack_entry.table == table { - Some(StackIndex::from(index)) - } else { - None - } - }) - .next() - } - - pub(super) fn top_of_stack_from(&self, depth: StackIndex) -> Range<StackIndex> { - depth..StackIndex::from(self.stack.len()) - } - - pub(super) fn push( - &mut self, - table: TableIndex, - cyclic_minimums: Minimums, - clock: TimeStamp, - ) -> StackIndex { - let old_len = self.stack.len(); - self.stack.push(StackEntry { - table, - clock, - cyclic_minimums, - active_strand: None, - }); - StackIndex::from(old_len) - } - - /// Pops the top-most entry from the stack: - /// * If the stack is now empty, returns false. - /// * Otherwise, returns true. - fn pop_and_adjust_depth(&mut self) -> bool { - self.stack.pop(); - !self.stack.is_empty() - } - - /// Pops the top-most entry from the stack, which should have the depth `*depth`: - /// * If the stack is now empty, returns None. - /// * Otherwise, `take`s the active strand from the new top and returns it. - pub(super) fn pop_and_take_caller_strand(&mut self) -> Option<CanonicalStrand<I>> { - if self.pop_and_adjust_depth() { - Some(self.top().active_strand.take().unwrap()) - } else { - None - } - } - - /// Pops the top-most entry from the stack, which should have the depth `*depth`: - /// * If the stack is now empty, returns None. - /// * Otherwise, borrows the active strand (mutably) from the new top and returns it. - pub(super) fn pop_and_borrow_caller_strand(&mut self) -> Option<&mut CanonicalStrand<I>> { - if self.pop_and_adjust_depth() { - Some(self.top().active_strand.as_mut().unwrap()) - } else { - None - } - } - - pub(super) fn top(&mut self) -> &mut StackEntry<I> { - self.stack.last_mut().unwrap() - } -} - -impl<I: Interner> Index<StackIndex> for Stack<I> { - type Output = StackEntry<I>; - - fn index(&self, index: StackIndex) -> &StackEntry<I> { - &self.stack[index.value] - } -} - -impl<I: Interner> IndexMut<StackIndex> for Stack<I> { - fn index_mut(&mut self, index: StackIndex) -> &mut StackEntry<I> { - &mut self.stack[index.value] - } -} diff --git a/vendor/chalk-engine/src/strand.rs b/vendor/chalk-engine/src/strand.rs deleted file mode 100644 index da25a778d..000000000 --- a/vendor/chalk-engine/src/strand.rs +++ /dev/null @@ -1,50 +0,0 @@ -use crate::table::AnswerIndex; -use crate::{ExClause, TableIndex, TimeStamp}; -use std::fmt::Debug; - -use chalk_derive::HasInterner; -use chalk_ir::fold::{FallibleTypeFolder, TypeFoldable}; -use chalk_ir::interner::Interner; -use chalk_ir::{Canonical, DebruijnIndex, UniverseMap}; - -#[derive(Clone, Debug, HasInterner)] -pub(crate) struct Strand<I: Interner> { - pub(super) ex_clause: ExClause<I>, - - /// Index into `ex_clause.subgoals`. - pub(crate) selected_subgoal: Option<SelectedSubgoal>, - - pub(crate) last_pursued_time: TimeStamp, -} - -pub(crate) type CanonicalStrand<I> = Canonical<Strand<I>>; - -#[derive(Clone, Debug)] -pub(crate) struct SelectedSubgoal { - /// The index of the subgoal in `ex_clause.subgoals` - pub(crate) subgoal_index: usize, - - /// The index of the table that we created or found for this subgoal - pub(super) subgoal_table: TableIndex, - - /// Index of the answer we should request next from the table - pub(crate) answer_index: AnswerIndex, - - /// Maps the universes of the subgoal to the canonical universes - /// used in the table - pub(crate) universe_map: UniverseMap, -} - -impl<I: Interner> TypeFoldable<I> for Strand<I> { - fn try_fold_with<E>( - self, - folder: &mut dyn FallibleTypeFolder<I, Error = E>, - outer_binder: DebruijnIndex, - ) -> Result<Self, E> { - Ok(Strand { - ex_clause: self.ex_clause.try_fold_with(folder, outer_binder)?, - last_pursued_time: self.last_pursued_time, - selected_subgoal: self.selected_subgoal, - }) - } -} diff --git a/vendor/chalk-engine/src/table.rs b/vendor/chalk-engine/src/table.rs deleted file mode 100644 index e883cad32..000000000 --- a/vendor/chalk-engine/src/table.rs +++ /dev/null @@ -1,173 +0,0 @@ -use crate::index_struct; -use crate::strand::CanonicalStrand; -use crate::{Answer, AnswerMode}; -use rustc_hash::FxHashMap; -use std::collections::hash_map::Entry; -use std::collections::VecDeque; -use std::mem; - -use chalk_ir::interner::Interner; -use chalk_ir::{AnswerSubst, Canonical, Goal, InEnvironment, UCanonical}; -use tracing::{debug, info, instrument}; - -#[derive(Debug)] -pub(crate) struct Table<I: Interner> { - /// The goal this table is trying to solve (also the key to look - /// it up). - pub(crate) table_goal: UCanonical<InEnvironment<Goal<I>>>, - - /// A goal is coinductive if it can assume itself to be true, more - /// or less. This is true for auto traits. - pub(crate) coinductive_goal: bool, - - /// True if this table is floundered, meaning that it doesn't have - /// enough types specified for us to solve. - floundered: bool, - - /// Stores the answers that we have found thus far. When we get a request - /// for an answer N, we will first check this vector. - answers: Vec<Answer<I>>, - - /// An alternative storage for the answers we have so far, used to - /// detect duplicates. Not every answer in `answers` will be - /// represented here -- we discard answers from `answers_hash` - /// (but not `answers`) when better answers arrive (in particular, - /// answers with no ambiguity). - /// - /// FIXME -- Ideally we would exclude the region constraints and - /// delayed subgoals from the hash, but that's a bit tricky to do - /// with the current canonicalization setup. It should be ok not - /// to do so though it can result in more answers than we need. - answers_hash: FxHashMap<Canonical<AnswerSubst<I>>, bool>, - - /// Stores the active strands that we can "pull on" to find more - /// answers. - strands: VecDeque<CanonicalStrand<I>>, - - pub(crate) answer_mode: AnswerMode, -} - -index_struct! { - pub(crate) struct AnswerIndex { - value: usize, - } -} - -impl<I: Interner> Table<I> { - pub(crate) fn new( - table_goal: UCanonical<InEnvironment<Goal<I>>>, - coinductive_goal: bool, - ) -> Table<I> { - Table { - table_goal, - coinductive_goal, - answers: Vec::new(), - floundered: false, - answers_hash: FxHashMap::default(), - strands: VecDeque::new(), - answer_mode: AnswerMode::Complete, - } - } - - /// Push a strand to the back of the queue of strands to be processed. - pub(crate) fn enqueue_strand(&mut self, strand: CanonicalStrand<I>) { - self.strands.push_back(strand); - } - - pub(crate) fn strands_mut(&mut self) -> impl Iterator<Item = &mut CanonicalStrand<I>> { - self.strands.iter_mut() - } - - pub(crate) fn strands(&self) -> impl Iterator<Item = &CanonicalStrand<I>> { - self.strands.iter() - } - - pub(crate) fn take_strands(&mut self) -> VecDeque<CanonicalStrand<I>> { - mem::take(&mut self.strands) - } - - /// Remove the next strand from the queue that meets the given criteria - pub(crate) fn dequeue_next_strand_that( - &mut self, - test: impl Fn(&CanonicalStrand<I>) -> bool, - ) -> Option<CanonicalStrand<I>> { - let first = self.strands.iter().position(test); - if let Some(first) = first { - self.strands.rotate_left(first); - self.strands.pop_front() - } else { - None - } - } - - /// Mark the table as floundered -- this also discards all pre-existing answers, - /// as they are no longer relevant. - pub(crate) fn mark_floundered(&mut self) { - self.floundered = true; - self.strands = Default::default(); - self.answers = Default::default(); - } - - /// Returns true if the table is floundered. - pub(crate) fn is_floundered(&self) -> bool { - self.floundered - } - - /// Adds `answer` to our list of answers, unless it is already present. - /// - /// Returns true if `answer` was added. - /// - /// # Panics - /// This will panic if a previous answer with the same substitution - /// was marked as ambgiuous, but the new answer is not. No current - /// tests trigger this case, and assumptions upstream assume that when - /// `true` is returned here, that a *new* answer was added (instead of an) - /// existing answer replaced. - #[instrument(level = "debug", skip(self))] - pub(super) fn push_answer(&mut self, answer: Answer<I>) -> Option<AnswerIndex> { - assert!(!self.floundered); - debug!( - "pre-existing entry: {:?}", - self.answers_hash.get(&answer.subst) - ); - - let added = match self.answers_hash.entry(answer.subst.clone()) { - Entry::Vacant(entry) => { - entry.insert(answer.ambiguous); - true - } - - Entry::Occupied(entry) => { - let was_ambiguous = entry.get(); - if *was_ambiguous && !answer.ambiguous { - panic!("New answer was not ambiguous whereas previous answer was."); - } - false - } - }; - - info!( - goal = ?self.table_goal, ?answer, - "new answer to table", - ); - if !added { - return None; - } - - let index = self.answers.len(); - self.answers.push(answer); - Some(AnswerIndex::from(index)) - } - - pub(super) fn answer(&self, index: AnswerIndex) -> Option<&Answer<I>> { - self.answers.get(index.value) - } - - pub(super) fn next_answer_index(&self) -> AnswerIndex { - AnswerIndex::from(self.answers.len()) - } -} - -impl AnswerIndex { - pub(crate) const ZERO: AnswerIndex = AnswerIndex { value: 0 }; -} diff --git a/vendor/chalk-engine/src/tables.rs b/vendor/chalk-engine/src/tables.rs deleted file mode 100644 index 76508eaa8..000000000 --- a/vendor/chalk-engine/src/tables.rs +++ /dev/null @@ -1,72 +0,0 @@ -use crate::table::Table; -use crate::TableIndex; -use rustc_hash::FxHashMap; -use std::ops::{Index, IndexMut}; - -use chalk_ir::interner::Interner; -use chalk_ir::{Goal, InEnvironment, UCanonical}; - -/// See `Forest`. -#[derive(Debug)] -pub(crate) struct Tables<I: Interner> { - /// Maps from a canonical goal to the index of its table. - table_indices: FxHashMap<UCanonical<InEnvironment<Goal<I>>>, TableIndex>, - - /// Table: as described above, stores the key information for each - /// tree in the forest. - tables: Vec<Table<I>>, -} - -impl<I: Interner> Tables<I> { - pub(crate) fn new() -> Tables<I> { - Tables { - table_indices: FxHashMap::default(), - tables: Vec::default(), - } - } - - /// The index that will be given to the next table to be inserted. - pub(super) fn next_index(&self) -> TableIndex { - TableIndex { - value: self.tables.len(), - } - } - - pub(super) fn insert(&mut self, table: Table<I>) -> TableIndex { - let goal = table.table_goal.clone(); - let index = self.next_index(); - self.tables.push(table); - self.table_indices.insert(goal, index); - index - } - - pub(super) fn index_of( - &self, - literal: &UCanonical<InEnvironment<Goal<I>>>, - ) -> Option<TableIndex> { - self.table_indices.get(literal).cloned() - } -} - -impl<I: Interner> Index<TableIndex> for Tables<I> { - type Output = Table<I>; - - fn index(&self, index: TableIndex) -> &Table<I> { - &self.tables[index.value] - } -} - -impl<I: Interner> IndexMut<TableIndex> for Tables<I> { - fn index_mut(&mut self, index: TableIndex) -> &mut Table<I> { - &mut self.tables[index.value] - } -} - -impl<'a, I: Interner> IntoIterator for &'a mut Tables<I> { - type IntoIter = <&'a mut Vec<Table<I>> as IntoIterator>::IntoIter; - type Item = <&'a mut Vec<Table<I>> as IntoIterator>::Item; - - fn into_iter(self) -> Self::IntoIter { - IntoIterator::into_iter(&mut self.tables) - } -} |