chalk_solve/solve/
truncate.rs

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

chalk_solve/solve/
truncate.rs
