From 5363f350887b1e5b5dd21a86f88c8af9d7fea6da Mon Sep 17 00:00:00 2001 From: Daniel Baumann Date: Wed, 17 Apr 2024 14:18:25 +0200 Subject: Merging upstream version 1.67.1+dfsg1. Signed-off-by: Daniel Baumann --- vendor/chalk-solve/src/solve/test/bench.rs | 111 ++++++++++++++++++++++++ vendor/chalk-solve/src/solve/truncate.rs | 134 +++++++++++++++++++++++++++++ 2 files changed, 245 insertions(+) create mode 100644 vendor/chalk-solve/src/solve/test/bench.rs create mode 100644 vendor/chalk-solve/src/solve/truncate.rs (limited to 'vendor/chalk-solve/src/solve') 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 { } +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 { } +impl Clone for Rc { } +impl Sized for Rc { } + +struct Box { } +impl AsRef for Box where T: Sized { } +impl Clone for Box where T: Clone { } +impl Sized for Box { } + +// Meant to be [T] +struct Slice where T: Sized { } +impl Sized for Slice { } +impl AsRef> for Slice where T: Sized { } + +struct Vec where T: Sized { } +impl AsRef> for Vec where T: Sized { } +impl AsRef> for Vec where T: Sized { } +impl Clone for Vec where T: Clone, T: Sized { } +impl Sized for Vec where T: Sized { } + +trait SliceExt + where ::Item: Clone +{ + type Item; +} + +impl SliceExt for Slice + where T: Clone +{ + type Item = T; +} +"; + +const CYCLEY_GOAL: &str = " +forall { + if ( + as SliceExt>::Item: Clone; + 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( + interner: I, + infer: &mut InferenceTable, + max_size: usize, + value: impl TypeVisitable, +) -> 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, + size: usize, + depth: usize, + max_size: usize, +} + +impl<'infer, I: Interner> TySizeVisitor<'infer, I> { + fn new(interner: I, infer: &'infer mut InferenceTable) -> Self { + Self { + interner, + infer, + size: 0, + depth: 0, + max_size: 0, + } + } +} + +impl<'infer, I: Interner> TypeVisitor for TySizeVisitor<'infer, I> { + type BreakTy = (); + + fn as_dyn(&mut self) -> &mut dyn TypeVisitor { + self + } + + fn visit_ty(&mut self, ty: &Ty, 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::::new(); + let _u1 = table.new_universe(); + + // Vec>>> + 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::::new(); + let _u1 = table.new_universe(); + + // Vec>>> + 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); + } +} -- cgit v1.2.3