summaryrefslogtreecommitdiffstats
path: root/vendor/chalk-solve-0.87.0/src/solve/truncate.rs
diff options
context:
space:
mode:
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/solve/truncate.rs')
-rw-r--r--vendor/chalk-solve-0.87.0/src/solve/truncate.rs134
1 files changed, 0 insertions, 134 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/solve/truncate.rs b/vendor/chalk-solve-0.87.0/src/solve/truncate.rs
deleted file mode 100644
index 1ed47b94f..000000000
--- a/vendor/chalk-solve-0.87.0/src/solve/truncate.rs
+++ /dev/null
@@ -1,134 +0,0 @@
-//!
-
-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);
- }
-}