summaryrefslogtreecommitdiffstats
path: root/vendor/chalk-solve/src/solve
diff options
context:
space:
mode:
authorDaniel Baumann <daniel.baumann@progress-linux.org>2024-04-17 12:18:25 +0000
committerDaniel Baumann <daniel.baumann@progress-linux.org>2024-04-17 12:18:25 +0000
commit5363f350887b1e5b5dd21a86f88c8af9d7fea6da (patch)
tree35ca005eb6e0e9a1ba3bb5dbc033209ad445dc17 /vendor/chalk-solve/src/solve
parentAdding debian version 1.66.0+dfsg1-1. (diff)
downloadrustc-5363f350887b1e5b5dd21a86f88c8af9d7fea6da.tar.xz
rustc-5363f350887b1e5b5dd21a86f88c8af9d7fea6da.zip
Merging upstream version 1.67.1+dfsg1.
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'vendor/chalk-solve/src/solve')
-rw-r--r--vendor/chalk-solve/src/solve/test/bench.rs111
-rw-r--r--vendor/chalk-solve/src/solve/truncate.rs134
2 files changed, 245 insertions, 0 deletions
diff --git a/vendor/chalk-solve/src/solve/test/bench.rs b/vendor/chalk-solve/src/solve/test/bench.rs
new file mode 100644
index 000000000..6ef6eb1f9
--- /dev/null
+++ b/vendor/chalk-solve/src/solve/test/bench.rs
@@ -0,0 +1,111 @@
+//! Benchmarking tests.
+
+extern crate test;
+use self::test::Bencher;
+
+use crate::db::ChalkDatabase;
+use crate::query::{ProgramSolverChoice, ProgramText};
+use chalk_solve::SolverChoice;
+use ir;
+use std::sync::Arc;
+
+use super::{assert_result, parse_and_lower_goal, parse_and_lower_program};
+
+fn run_bench(
+ program_text: &str,
+ solver_choice: SolverChoice,
+ goal_text: &str,
+ bencher: &mut Bencher,
+ expected: &str,
+) {
+ ChalkDatabase::with_program(Arc::new(program_text.to_string()), solver_choice, |db| {
+ let program = db.lowered_program().unwrap();
+ let env = db.environment().unwrap();
+ ir::tls::set_current_program(&program, || {
+ let goal = parse_and_lower_goal(&program, goal_text).unwrap();
+ let peeled_goal = goal.into_peeled_goal();
+
+ // Execute once to get an expected result.
+ let result = solver_choice.solve_root_goal(&env, &peeled_goal);
+
+ // Check expectation.
+ assert_result(&result, expected);
+
+ // Then do it many times to measure time.
+ bencher.iter(|| solver_choice.solve_root_goal(&env, &peeled_goal));
+ });
+ });
+}
+
+const CYCLEY: &str = "
+trait AsRef<T> { }
+trait Clone { }
+trait Copy where Self: Clone { }
+trait Sized { }
+
+struct i32 { }
+impl Copy for i32 { }
+impl Clone for i32 { }
+impl Sized for i32 { }
+
+struct u32 { }
+impl Copy for u32 { }
+impl Clone for u32 { }
+impl Sized for u32 { }
+
+struct Rc<T> { }
+impl<T> Clone for Rc<T> { }
+impl<T> Sized for Rc<T> { }
+
+struct Box<T> { }
+impl<T> AsRef<T> for Box<T> where T: Sized { }
+impl<T> Clone for Box<T> where T: Clone { }
+impl<T> Sized for Box<T> { }
+
+// Meant to be [T]
+struct Slice<T> where T: Sized { }
+impl<T> Sized for Slice<T> { }
+impl<T> AsRef<Slice<T>> for Slice<T> where T: Sized { }
+
+struct Vec<T> where T: Sized { }
+impl<T> AsRef<Slice<T>> for Vec<T> where T: Sized { }
+impl<T> AsRef<Vec<T>> for Vec<T> where T: Sized { }
+impl<T> Clone for Vec<T> where T: Clone, T: Sized { }
+impl<T> Sized for Vec<T> where T: Sized { }
+
+trait SliceExt
+ where <Self as SliceExt>::Item: Clone
+{
+ type Item;
+}
+
+impl<T> SliceExt for Slice<T>
+ where T: Clone
+{
+ type Item = T;
+}
+";
+
+const CYCLEY_GOAL: &str = "
+forall<T> {
+ if (
+ <Slice<T> as SliceExt>::Item: Clone;
+ <Slice<T> as SliceExt>::Item: Sized;
+ T: Clone;
+ T: Sized
+ ) {
+ T: Sized
+ }
+}
+";
+
+#[bench]
+fn cycley_slg(b: &mut Bencher) {
+ run_bench(
+ CYCLEY,
+ SolverChoice::SLG { max_size: 20 },
+ CYCLEY_GOAL,
+ b,
+ "Unique",
+ );
+}
diff --git a/vendor/chalk-solve/src/solve/truncate.rs b/vendor/chalk-solve/src/solve/truncate.rs
new file mode 100644
index 000000000..1ed47b94f
--- /dev/null
+++ b/vendor/chalk-solve/src/solve/truncate.rs
@@ -0,0 +1,134 @@
+//!
+
+use crate::infer::InferenceTable;
+use chalk_ir::interner::Interner;
+use chalk_ir::visit::{TypeSuperVisitable, TypeVisitable, TypeVisitor};
+use chalk_ir::*;
+use std::cmp::max;
+use std::ops::ControlFlow;
+
+/// "Truncation" (called "abstraction" in the papers referenced below)
+/// refers to the act of modifying a goal or answer that has become
+/// too large in order to guarantee termination.
+///
+/// Currently we don't perform truncation (but it might me readded later).
+///
+/// Citations:
+///
+/// - Terminating Evaluation of Logic Programs with Finite Three-Valued Models
+/// - Riguzzi and Swift; ACM Transactions on Computational Logic 2013
+/// - Radial Restraint
+/// - Grosof and Swift; 2013
+pub fn needs_truncation<I: Interner>(
+ interner: I,
+ infer: &mut InferenceTable<I>,
+ max_size: usize,
+ value: impl TypeVisitable<I>,
+) -> bool {
+ let mut visitor = TySizeVisitor::new(interner, infer);
+ value.visit_with(&mut visitor, DebruijnIndex::INNERMOST);
+
+ visitor.max_size > max_size
+}
+
+struct TySizeVisitor<'infer, I: Interner> {
+ interner: I,
+ infer: &'infer mut InferenceTable<I>,
+ size: usize,
+ depth: usize,
+ max_size: usize,
+}
+
+impl<'infer, I: Interner> TySizeVisitor<'infer, I> {
+ fn new(interner: I, infer: &'infer mut InferenceTable<I>) -> Self {
+ Self {
+ interner,
+ infer,
+ size: 0,
+ depth: 0,
+ max_size: 0,
+ }
+ }
+}
+
+impl<'infer, I: Interner> TypeVisitor<I> for TySizeVisitor<'infer, I> {
+ type BreakTy = ();
+
+ fn as_dyn(&mut self) -> &mut dyn TypeVisitor<I, BreakTy = Self::BreakTy> {
+ self
+ }
+
+ fn visit_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> ControlFlow<()> {
+ if let Some(normalized_ty) = self.infer.normalize_ty_shallow(self.interner, ty) {
+ normalized_ty.visit_with(self, outer_binder);
+ return ControlFlow::Continue(());
+ }
+
+ self.size += 1;
+ self.max_size = max(self.size, self.max_size);
+
+ self.depth += 1;
+ ty.super_visit_with(self, outer_binder);
+ self.depth -= 1;
+
+ // When we get back to the first invocation, clear the counters.
+ // We process each outermost type independently.
+ if self.depth == 0 {
+ self.size = 0;
+ }
+ ControlFlow::Continue(())
+ }
+
+ fn interner(&self) -> I {
+ self.interner
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+ use chalk_integration::{arg, ty};
+
+ #[test]
+ fn one_type() {
+ use chalk_integration::interner::ChalkIr;
+ let interner = ChalkIr;
+ let mut table = InferenceTable::<chalk_integration::interner::ChalkIr>::new();
+ let _u1 = table.new_universe();
+
+ // Vec<Vec<Vec<Vec<T>>>>
+ let ty0 = ty!(apply (item 0)
+ (apply (item 0)
+ (apply (item 0)
+ (apply (item 0)
+ (placeholder 1)))));
+
+ let mut visitor = TySizeVisitor::new(interner, &mut table);
+ ty0.visit_with(&mut visitor, DebruijnIndex::INNERMOST);
+ assert!(visitor.max_size == 5);
+ }
+
+ #[test]
+ fn multiple_types() {
+ use chalk_integration::interner::ChalkIr;
+ let interner = ChalkIr;
+ let mut table = InferenceTable::<chalk_integration::interner::ChalkIr>::new();
+ let _u1 = table.new_universe();
+
+ // Vec<Vec<Vec<Vec<T>>>>
+ let ty0 = ty!(apply (item 0)
+ (apply (item 0)
+ (apply (item 0)
+ (apply (item 0)
+ (placeholder 1)))));
+
+ let ty1 = ty!(apply (item 0)
+ (apply (item 0)
+ (apply (item 0)
+ (placeholder 1))));
+
+ let mut visitor = TySizeVisitor::new(interner, &mut table);
+ vec![&ty0, &ty1].visit_with(&mut visitor, DebruijnIndex::INNERMOST);
+ assert!(visitor.max_size == 5);
+ }
+}