vendor/chalk-solve-0.55.0/src/solve/truncate.rs

   1 //!
   2
   3 use crate::infer::InferenceTable;
   4 use chalk_ir::interner::Interner;
   5 use chalk_ir::visit::{ControlFlow, SuperVisit, Visit, Visitor};
   6 use chalk_ir::*;
   7 use std::cmp::max;
   8
   9 /// "Truncation" (called "abstraction" in the papers referenced below)
  10 /// refers to the act of modifying a goal or answer that has become
  11 /// too large in order to guarantee termination.
  12 ///
  13 /// Currently we don't perform truncation (but it might me readded later).
  14 ///
  15 /// Citations:
  16 ///
  17 /// - Terminating Evaluation of Logic Programs with Finite Three-Valued Models
  18 ///   - Riguzzi and Swift; ACM Transactions on Computational Logic 2013
  19 /// - Radial Restraint
  20 ///   - Grosof and Swift; 2013
  21 pub fn needs_truncation<I: Interner>(
  22     interner: &I,
  23     infer: &mut InferenceTable<I>,
  24     max_size: usize,
  25     value: impl Visit<I>,
  26 ) -> bool {
  27     let mut visitor = TySizeVisitor::new(interner, infer);
  28     value.visit_with(&mut visitor, DebruijnIndex::INNERMOST);
  29
  30     visitor.max_size > max_size
  31 }
  32
  33 struct TySizeVisitor<'infer, 'i, I: Interner> {
  34     interner: &'i I,
  35     infer: &'infer mut InferenceTable<I>,
  36     size: usize,
  37     depth: usize,
  38     max_size: usize,
  39 }
  40
  41 impl<'infer, 'i, I: Interner> TySizeVisitor<'infer, 'i, I> {
  42     fn new(interner: &'i I, infer: &'infer mut InferenceTable<I>) -> Self {
  43         Self {
  44             interner,
  45             infer,
  46             size: 0,
  47             depth: 0,
  48             max_size: 0,
  49         }
  50     }
  51 }
  52
  53 impl<'infer, 'i, I: Interner> Visitor<'i, I> for TySizeVisitor<'infer, 'i, I> {
  54     type BreakTy = ();
  55
  56     fn as_dyn(&mut self) -> &mut dyn Visitor<'i, I, BreakTy = Self::BreakTy> {
  57         self
  58     }
  59
  60     fn visit_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> ControlFlow<()> {
  61         if let Some(normalized_ty) = self.infer.normalize_ty_shallow(self.interner, ty) {
  62             normalized_ty.visit_with(self, outer_binder);
  63             return ControlFlow::CONTINUE;
  64         }
  65
  66         self.size += 1;
  67         self.max_size = max(self.size, self.max_size);
  68
  69         self.depth += 1;
  70         ty.super_visit_with(self, outer_binder);
  71         self.depth -= 1;
  72
  73         // When we get back to the first invocation, clear the counters.
  74         // We process each outermost type independently.
  75         if self.depth == 0 {
  76             self.size = 0;
  77         }
  78         ControlFlow::CONTINUE
  79     }
  80
  81     fn interner(&self) -> &'i I {
  82         self.interner
  83     }
  84 }
  85
  86 #[cfg(test)]
  87 mod tests {
  88     use super::*;
  89     use chalk_integration::{arg, ty};
  90
  91     #[test]
  92     fn one_type() {
  93         use chalk_integration::interner::ChalkIr;
  94         let interner = &ChalkIr;
  95         let mut table = InferenceTable::<chalk_integration::interner::ChalkIr>::new();
  96         let _u1 = table.new_universe();
  97
  98         // Vec<Vec<Vec<Vec<T>>>>
  99         let ty0 = ty!(apply (item 0)
 100                       (apply (item 0)
 101                        (apply (item 0)
 102                         (apply (item 0)
 103                          (placeholder 1)))));
 104
 105         let mut visitor = TySizeVisitor::new(interner, &mut table);
 106         ty0.visit_with(&mut visitor, DebruijnIndex::INNERMOST);
 107         assert!(visitor.max_size == 5);
 108     }
 109
 110     #[test]
 111     fn multiple_types() {
 112         use chalk_integration::interner::ChalkIr;
 113         let interner = &ChalkIr;
 114         let mut table = InferenceTable::<chalk_integration::interner::ChalkIr>::new();
 115         let _u1 = table.new_universe();
 116
 117         // Vec<Vec<Vec<Vec<T>>>>
 118         let ty0 = ty!(apply (item 0)
 119                       (apply (item 0)
 120                        (apply (item 0)
 121                         (apply (item 0)
 122                          (placeholder 1)))));
 123
 124         let ty1 = ty!(apply (item 0)
 125                       (apply (item 0)
 126                        (apply (item 0)
 127                         (placeholder 1))));
 128
 129         let mut visitor = TySizeVisitor::new(interner, &mut table);
 130         vec![&ty0, &ty1].visit_with(&mut visitor, DebruijnIndex::INNERMOST);
 131         assert!(visitor.max_size == 5);
 132     }
 133 }